Added code that generates basic infrastructure for channel introspect…

…ion using the "chantyperep" class

Channel_Type.ML

@@ -57,18 +57,50 @@ fun defs qual inds f ctx =
         in (thms @ [thm], ctx') end) inds ([], ctx)
 
 fun mk_chantyperep chans ctx = 
-  let open HOLogic; open Syntax  
-  fun mk_chanrep (n, t) = check_term ctx (const @{const_name Chanrep} $ mk_literal n $ mk_literal t $ parse_term ctx (is_prefix ^ n ^ ctor_suffix))
+  let open HOLogic; open Syntax; open Proof_Context  
+  fun mk_chanrep (n, t) =
+      let val c = 
+          case read_const {proper = false, strict = false} ctx (is_prefix ^ n ^ ctor_suffix)
+          of Free (c', _) => free c' | Const (c', _) => const c' | _ => raise Match;
+      in  
+      (* check_term ctx *) 
+        (const @{const_name Chanrep} 
+         $ mk_literal n $ t 
+         $ c)
+      end
   in
-  @{print} (mk_list dummyT (map mk_chanrep chans))
+  mk_list dummyT (map mk_chanrep chans)
   end
 
-fun compile_chantype (name, chans) ctx =
+fun chantyperep_instance name raw_chans thy =
+  let  
+  open Syntax; open HOLogic; open Global_Theory;
+  val ty = Syntax.read_typ (Named_Target.theory_init thy) name;
+  val tyco = fst (dest_Type ty);
+  val disc_intro_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".disc");
+  val disc_elim_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".exhaust_disc");
+  val ctx0 = Class.instantiation ([tyco], [], \<^sort>\<open>chantyperep\<close>) thy;
+  val chans = map (fn (n, t) => (n, mk_typerep (read_typ ctx0 t))) raw_chans
+  val lhs = \<^Const>\<open>chantyperep ty\<close> $ Free ("T", Term.itselfT ty);
+  val rhs = mk_chantyperep chans ctx0;
+  val ctx1 = snd (Local_Theory.begin_nested ctx0)
+  val eq = check_term ctx1 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
+  val (_, ctx2) = Specification.definition NONE [] [] ((Binding.empty, @{attributes [chantyperep_defs]}), eq) ctx1;
+  val ctx3 = Local_Theory.end_nested ctx2;
+  val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_intros") disc_intro_thms ctx3;
+  val ctx5 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_elims") disc_elim_thms ctx4;
+  in
+  Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx5 (Method_Closure.apply_method ctx5 @{method chantyperep_inst} [] [] [] ctx5 [])) ctx5
+  end;
+
+fun compile_chantype (name, chans) thy =
   let 
     open BNF_FP_Def_Sugar; open BNF_FP_Rec_Sugar_Util; open BNF_LFP; open Ctr_Sugar
-    open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax
+    open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax; open HOLogic
+    val ctx = Named_Target.theory_init thy;
     val ctrs = map (fn (n, t) => (((Binding.empty, Binding.name (n ^ ctor_suffix)), [(Binding.empty, t)]), Mixfix.NoSyn)) chans 
     val pnames = map fst chans
+    val tyreps = map (mk_typerep o read_typ ctx o snd) chans
     val thypfx = 
       case (Named_Target.locale_of ctx) of
         SOME loc => loc ^ "." |
@@ -107,7 +139,9 @@ fun compile_chantype (name, chans) ctx =
        (fold (fn x => fn thy => snd (note ((Binding.qualify false name (Binding.name (x ^ wb_prism_suffix)), attrs), [wb_prism_proof x thms thy]) thy)) pnames
        #> (snd o note ((Binding.qualify false name (Binding.name codepsN), attrs), map (codep_proof thms ctx) (pairings pnames)))
        ) ctx)
-  (* #> (fn ctx => snd ((def name ("ctrep", mk_chantyperep chans ctx1)) ctx)) *))
+  #> Local_Theory.exit_global
+  (* Generate chantyperep instance *) 
+  #> chantyperep_instance name chans)
   ctx1
   end;
 
@@ -117,5 +151,5 @@ let open Parse; open Parse_Spec; open Scan in
   Outer_Syntax.command @{command_keyword chantype} "define a channel datatype"
     ((name --
       (@{keyword "="} |-- repeat1 (name -- ($$$ "::" |-- !!! typ))))
-    >> (fn x => Toplevel.local_theory NONE NONE (Channel_Type.compile_chantype x)))
+    >> (fn x => Toplevel.theory (Channel_Type.compile_chantype x)))
   end;

Channel_Type.thy

@@ -6,7 +6,7 @@ theory Channel_Type
 begin
 
 text \<open> A channel type is a simplified algebraic datatype where each constructor has exactly 
-  one parameter, and it is wrapped up as a prism. It a dual of an alphabet type. \<close>
+  one parameter, and it is wrapped up as a prism. It is a dual of an alphabet type. \<close>
 
 subsection \<open> Datatype Constructor Prisms \<close>
 
@@ -33,7 +33,7 @@ subsection \<open> Channel Type Representation \<close>
 
 text \<open> A channel is represented by a name, a type, and a predicate that determines whether the event is on this channel. \<close>
 
-datatype 'a chanrep = Chanrep (chan_name: String.literal) (chan_type: String.literal) (is_chan: "'a \<Rightarrow> bool") 
+datatype 'a chanrep = Chanrep (chan_name: String.literal) (chan_type: typerep) (is_chan: "'a \<Rightarrow> bool") 
 
 definition evs_of :: "'a chanrep \<Rightarrow> 'a set" where
 "evs_of c = {e. is_chan c e}"
@@ -55,7 +55,7 @@ definition wf_chantyperep :: "'a raw_chantyperep \<Rightarrow> bool" where
   \<and> (\<forall> c\<in>set ct. \<exists> e. is_chan c e))" \<comment> \<open> Every channel has at least one event \<close>
 
 typedef 'a chantyperep = "{ctr::'a raw_chantyperep. wf_chantyperep ctr}"
-  apply (rule_tac x="[Chanrep STR ''x'' STR ''t'' (\<lambda> x. True)]" in exI)
+  apply (rule_tac x="[Chanrep STR ''x'' TYPEREP(bool) (\<lambda> x. True)]" in exI)
   apply (auto simp add: wf_chantyperep_def)
   done
 
@@ -70,7 +70,11 @@ definition set_chan :: "'a chantyperep \<Rightarrow> String.literal \<Rightarrow
 definition set_chans :: "'a chantyperep \<Rightarrow> String.literal set \<Rightarrow> 'a set" where
 "set_chans ct ns = \<Union> (set_chan ct ` ns)" 
 
-method wf_chantyperep uses disc def = (force intro: disc simp add: wf_chantyperep_def def)
+named_theorems datatype_disc_elims
+named_theorems datatype_disc_intros 
+named_theorems chantyperep_defs
+
+method wf_chantyperep = (force intro: datatype_disc_intros simp add: comp_def wf_chantyperep_def chantyperep_defs)
 
 lemma foldr_disj_one_True: "foldr (\<or>) Ps False \<Longrightarrow> (\<exists> P\<in>set Ps. P)"
   by (induct Ps, auto)
@@ -98,6 +102,10 @@ class chantyperep =
   fixes chantyperep :: "'a itself \<Rightarrow> 'a raw_chantyperep"
   assumes wf_chantyperep: "wf_chantyperep (chantyperep TYPE('a))"
 
+(* The following method works, but relies too much on auto. It should be optimised *)
+
+method chantyperep_inst = (rule chantyperep_class.intro, (intro_classes)[1], rule_tac class.chantyperep.intro, insert datatype_disc_elims, auto intro!:datatype_disc_intros simp add: comp_def wf_chantyperep_def chantyperep_defs)
+
 syntax "_chantyperep" :: "type \<Rightarrow> logic" ("CHANTYPEREP'(_')")
 translations "CHANTYPEREP('a)" == "CONST chantyperep TYPE('a)"
 

Channel_Type_Example.thy

@@ -2,6 +2,13 @@ theory Channel_Type_Example
   imports Channel_Type
 begin
 
+chantype ch_single =
+  chnat :: nat
+
+chantype ch_two =
+  chbool :: bool
+  chint :: int
+
 chantype ch_buffer =
   inp :: unit
   outp :: nat
@@ -11,14 +18,9 @@ thm ch_buffer.inp_wb_prism
 
 thm ch_buffer.codeps
 
-locale C1
-begin
-
 chantype ch_buffer2 =
   inp2 :: unit
   outp2 :: nat
   mod2 :: bool
 
-end
-
 end