Skip to content

Commit fdd89c0

Browse files
simondfostersimondfoster
committed
Added code that generates basic infrastructure for channel introspection using the "chantyperep" class
1 parent ed437b4 commit fdd89c0

File tree

3 files changed

+60
-16
lines changed

3 files changed

+60
-16
lines changed

‎Channel_Type.ML

Lines changed: 41 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -57,18 +57,50 @@ fun defs qual inds f ctx =
5757
in (thms @ [thm], ctx') end) inds ([], ctx)
5858

5959
fun mk_chantyperep chans ctx =
60-
let open HOLogic; open Syntax
61-
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))
60+
let open HOLogic; open Syntax; open Proof_Context
61+
fun mk_chanrep (n, t) =
62+
let val c =
63+
case read_const {proper = false, strict = false} ctx (is_prefix ^ n ^ ctor_suffix)
64+
of Free (c', _) => free c' | Const (c', _) => const c' | _ => raise Match;
65+
in
66+
(* check_term ctx *)
67+
(const @{const_name Chanrep}
68+
$ mk_literal n $ t
69+
$ c)
70+
end
6271
in
63-
@{print} (mk_list dummyT (map mk_chanrep chans))
72+
mk_list dummyT (map mk_chanrep chans)
6473
end
6574

66-
fun compile_chantype (name, chans) ctx =
75+
fun chantyperep_instance name raw_chans thy =
76+
let
77+
open Syntax; open HOLogic; open Global_Theory;
78+
val ty = Syntax.read_typ (Named_Target.theory_init thy) name;
79+
val tyco = fst (dest_Type ty);
80+
val disc_intro_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".disc");
81+
val disc_elim_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".exhaust_disc");
82+
val ctx0 = Class.instantiation ([tyco], [], \<^sort>\<open>chantyperep\<close>) thy;
83+
val chans = map (fn (n, t) => (n, mk_typerep (read_typ ctx0 t))) raw_chans
84+
val lhs = \<^Const>\<open>chantyperep ty\<close> $ Free ("T", Term.itselfT ty);
85+
val rhs = mk_chantyperep chans ctx0;
86+
val ctx1 = snd (Local_Theory.begin_nested ctx0)
87+
val eq = check_term ctx1 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
88+
val (_, ctx2) = Specification.definition NONE [] [] ((Binding.empty, @{attributes [chantyperep_defs]}), eq) ctx1;
89+
val ctx3 = Local_Theory.end_nested ctx2;
90+
val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_intros") disc_intro_thms ctx3;
91+
val ctx5 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_elims") disc_elim_thms ctx4;
92+
in
93+
Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx5 (Method_Closure.apply_method ctx5 @{method chantyperep_inst} [] [] [] ctx5 [])) ctx5
94+
end;
95+
96+
fun compile_chantype (name, chans) thy =
6797
let
6898
open BNF_FP_Def_Sugar; open BNF_FP_Rec_Sugar_Util; open BNF_LFP; open Ctr_Sugar
69-
open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax
99+
open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax; open HOLogic
100+
val ctx = Named_Target.theory_init thy;
70101
val ctrs = map (fn (n, t) => (((Binding.empty, Binding.name (n ^ ctor_suffix)), [(Binding.empty, t)]), Mixfix.NoSyn)) chans
71102
val pnames = map fst chans
103+
val tyreps = map (mk_typerep o read_typ ctx o snd) chans
72104
val thypfx =
73105
case (Named_Target.locale_of ctx) of
74106
SOME loc => loc ^ "." |
@@ -107,7 +139,9 @@ fun compile_chantype (name, chans) ctx =
107139
(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
108140
#> (snd o note ((Binding.qualify false name (Binding.name codepsN), attrs), map (codep_proof thms ctx) (pairings pnames)))
109141
) ctx)
110-
(* #> (fn ctx => snd ((def name ("ctrep", mk_chantyperep chans ctx1)) ctx)) *))
142+
#> Local_Theory.exit_global
143+
(* Generate chantyperep instance *)
144+
#> chantyperep_instance name chans)
111145
ctx1
112146
end;
113147

@@ -117,5 +151,5 @@ let open Parse; open Parse_Spec; open Scan in
117151
Outer_Syntax.command @{command_keyword chantype} "define a channel datatype"
118152
((name --
119153
(@{keyword "="} |-- repeat1 (name -- ($$$ "::" |-- !!! typ))))
120-
>> (fn x => Toplevel.local_theory NONE NONE (Channel_Type.compile_chantype x)))
154+
>> (fn x => Toplevel.theory (Channel_Type.compile_chantype x)))
121155
end;

‎Channel_Type.thy

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ theory Channel_Type
66
begin
77

88
text \<open> A channel type is a simplified algebraic datatype where each constructor has exactly
9-
one parameter, and it is wrapped up as a prism. It a dual of an alphabet type. \<close>
9+
one parameter, and it is wrapped up as a prism. It is a dual of an alphabet type. \<close>
1010

1111
subsection \<open> Datatype Constructor Prisms \<close>
1212

@@ -33,7 +33,7 @@ subsection \<open> Channel Type Representation \<close>
3333

3434
text \<open> A channel is represented by a name, a type, and a predicate that determines whether the event is on this channel. \<close>
3535

36-
datatype 'a chanrep = Chanrep (chan_name: String.literal) (chan_type: String.literal) (is_chan: "'a \<Rightarrow> bool")
36+
datatype 'a chanrep = Chanrep (chan_name: String.literal) (chan_type: typerep) (is_chan: "'a \<Rightarrow> bool")
3737

3838
definition evs_of :: "'a chanrep \<Rightarrow> 'a set" where
3939
"evs_of c = {e. is_chan c e}"
@@ -55,7 +55,7 @@ definition wf_chantyperep :: "'a raw_chantyperep \<Rightarrow> bool" where
5555
\<and> (\<forall> c\<in>set ct. \<exists> e. is_chan c e))" \<comment> \<open> Every channel has at least one event \<close>
5656

5757
typedef 'a chantyperep = "{ctr::'a raw_chantyperep. wf_chantyperep ctr}"
58-
apply (rule_tac x="[Chanrep STR ''x'' STR ''t'' (\<lambda> x. True)]" in exI)
58+
apply (rule_tac x="[Chanrep STR ''x'' TYPEREP(bool) (\<lambda> x. True)]" in exI)
5959
apply (auto simp add: wf_chantyperep_def)
6060
done
6161

@@ -70,7 +70,11 @@ definition set_chan :: "'a chantyperep \<Rightarrow> String.literal \<Rightarrow
7070
definition set_chans :: "'a chantyperep \<Rightarrow> String.literal set \<Rightarrow> 'a set" where
7171
"set_chans ct ns = \<Union> (set_chan ct ` ns)"
7272

73-
method wf_chantyperep uses disc def = (force intro: disc simp add: wf_chantyperep_def def)
73+
named_theorems datatype_disc_elims
74+
named_theorems datatype_disc_intros
75+
named_theorems chantyperep_defs
76+
77+
method wf_chantyperep = (force intro: datatype_disc_intros simp add: comp_def wf_chantyperep_def chantyperep_defs)
7478

7579
lemma foldr_disj_one_True: "foldr (\<or>) Ps False \<Longrightarrow> (\<exists> P\<in>set Ps. P)"
7680
by (induct Ps, auto)
@@ -98,6 +102,10 @@ class chantyperep =
98102
fixes chantyperep :: "'a itself \<Rightarrow> 'a raw_chantyperep"
99103
assumes wf_chantyperep: "wf_chantyperep (chantyperep TYPE('a))"
100104

105+
(* The following method works, but relies too much on auto. It should be optimised *)
106+
107+
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)
108+
101109
syntax "_chantyperep" :: "type \<Rightarrow> logic" ("CHANTYPEREP'(_')")
102110
translations "CHANTYPEREP('a)" == "CONST chantyperep TYPE('a)"
103111

‎Channel_Type_Example.thy

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,13 @@ theory Channel_Type_Example
22
imports Channel_Type
33
begin
44

5+
chantype ch_single =
6+
chnat :: nat
7+
8+
chantype ch_two =
9+
chbool :: bool
10+
chint :: int
11+
512
chantype ch_buffer =
613
inp :: unit
714
outp :: nat
@@ -11,14 +18,9 @@ thm ch_buffer.inp_wb_prism
1118

1219
thm ch_buffer.codeps
1320

14-
locale C1
15-
begin
16-
1721
chantype ch_buffer2 =
1822
inp2 :: unit
1923
outp2 :: nat
2024
mod2 :: bool
2125

22-
end
23-
2426
end

0 commit comments

Comments
 (0)