Skip to content

Commit 7803286

Browse files
simondfostersimondfoster
committed
Optimised generation of chantyperep proofs, and added generation of prism chanrep theorems. Also added test with 50 channels.
1 parent 5eeb184 commit 7803286

File tree

4 files changed

+112
-22
lines changed

4 files changed

+112
-22
lines changed

‎Channel_Type.ML

Lines changed: 56 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -46,11 +46,10 @@ val un_prefix = "un_";
4646

4747
fun def qual (x, tm) ctx =
4848
let open Specification; open Syntax
49-
val ((_, (_, thm)), d) = definition (SOME (Binding.qualify false qual (Binding.name x), NONE, NoSyn)) [] [] ((Binding.empty, [Attrib.check_src @{context} (Token.make_src ("lens_defs", Position.none) [])]), mk_def dummyT x tm) ctx
49+
val ((_, (_, thm)), d) = definition (SOME (Binding.qualify false qual (Binding.name x), NONE, NoSyn)) [] [] ((Binding.empty, @{attributes [lens_defs, chan_defs]}), mk_def dummyT x tm) ctx
5050
in (thm, d)
5151
end
5252

53-
5453
fun defs qual inds f ctx =
5554
fold (fn i => fn (thms, ctx) =>
5655
let val (thm, ctx') = def qual (i, f i) ctx
@@ -72,30 +71,40 @@ fun mk_chantyperep chans ctx =
7271
mk_list dummyT (map mk_chanrep chans)
7372
end
7473

74+
fun chantyperep_def name raw_chans ct ctx =
75+
let
76+
open Syntax; open HOLogic; open Global_Theory;
77+
val ty = read_typ ctx name;
78+
val chans = map (fn (n, t) => (n, mk_typerep (read_typ ctx t))) raw_chans
79+
val lhs = ct $ Free ("T", Term.itselfT ty);
80+
val rhs = mk_chantyperep chans ctx;
81+
val eq = check_term ctx (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
82+
in snd (Specification.definition NONE [] [] ((Binding.empty, @{attributes [chantyperep_defs]}), eq) ctx)
83+
end;
84+
7585
fun chantyperep_instance name raw_chans thy =
7686
let
7787
open Syntax; open HOLogic; open Global_Theory;
78-
val ty = Syntax.read_typ (Named_Target.theory_init thy) name;
88+
val ty = read_typ (Named_Target.theory_init thy) name;
7989
val tyco = fst (dest_Type ty);
80-
val disc_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".disc") @ get_thms thy (tyco ^ ".exhaust_disc")
81-
@ (if length raw_chans = 2 then [] else get_thms thy (tyco ^ ".distinct_disc"));
8290
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;
8691
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;
92+
val ctx2 = chantyperep_def name raw_chans \<^Const>\<open>chantyperep ty\<close> ctx1
8993
val ctx3 = Local_Theory.end_nested ctx2;
90-
val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_thms") disc_thms ctx3;
91-
in
92-
Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx4 (Method_Closure.apply_method ctx4 @{method chantyperep_inst} [] [] [] ctx4 [])) ctx4
94+
val disc_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".discI")
95+
val exhaust_disc_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".exhaust_disc")
96+
val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.disc_thms") disc_thms ctx3;
97+
val ctx5 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.exhaust_disc_thms") exhaust_disc_thms ctx4;
98+
99+
(* val ctx4 = fold (Context.proof_map o Named_Theorems.add_thm "Channel_Type.datatype_disc_thms") disc_thms ctx3; *)
100+
in
101+
Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx5 (Method_Closure.apply_method ctx5 @{method chantyperep_inst} [] [] [] ctx5 [])) ctx5
93102
end;
94103

95-
fun compile_chantype (name, chans) thy =
104+
fun make_chantype (name, chans) thy =
96105
let
97106
open BNF_FP_Def_Sugar; open BNF_FP_Rec_Sugar_Util; open BNF_LFP; open Ctr_Sugar
98-
open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax; open HOLogic
107+
open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax; open HOLogic; open Global_Theory
99108
val ctx = Named_Target.theory_init thy;
100109
val ctrs = map (fn (n, t) => (((Binding.empty, Binding.name (n ^ ctor_suffix)), [(Binding.empty, t)]), Mixfix.NoSyn)) chans
101110
val pnames = map fst chans
@@ -137,12 +146,41 @@ fun compile_chantype (name, chans) thy =
137146
(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
138147
#> (snd o note ((Binding.qualify false name (Binding.name codepsN), attrs), map (codep_proof thms ctx) (pairings pnames)))
139148
) ctx)
140-
#> Local_Theory.exit_global
141-
(* Generate chantyperep instance *)
142-
#> chantyperep_instance name chans)
149+
#> Local_Theory.exit_global)
143150
ctx1
144151
end;
145152

153+
fun prism_chanrep n t ctx =
154+
let open Syntax; open HOLogic
155+
val c = read_term ctx n; val d = read_term ctx ("is_" ^ n ^ "_C") in
156+
Trueprop $ (eq_const dummyT $ (const @{const_name prism_chanrep} $ c)
157+
$ ((const @{const_name Chanrep} $ mk_literal n $ mk_typerep t) $ d))
158+
end
159+
160+
fun prism_chanrep_proof ctx (n, t) =
161+
let open Simplifier; open Prism_Lib; open Syntax
162+
in
163+
Goal.prove ctx [] []
164+
(Syntax.check_term ctx (prism_chanrep n (read_typ ctx t) ctx))
165+
(fn {context = context, prems = _}
166+
=> NO_CONTEXT_TACTIC ctx (Method_Closure.apply_method ctx @{method prism_chanrep} [] [] [] ctx []))
167+
end
168+
169+
fun prism_chanrep_proofs (name, chans) thy =
170+
let val ctx = Named_Target.theory_init thy
171+
in
172+
Local_Theory.exit_global (snd (Local_Theory.note ((Binding.qualify false name (Binding.name "prism_chanreps"), @{attributes [simp, code_unfold]}), map (prism_chanrep_proof ctx) chans) ctx))
173+
end
174+
175+
176+
177+
fun compile_chantype (name, chans) =
178+
make_chantype (name, chans) #>
179+
(* Generate chantyperep instance *)
180+
chantyperep_instance name chans #>
181+
(* Generate representations for each prism (channel) *)
182+
prism_chanrep_proofs (name, chans)
183+
146184
end;
147185

148186
let open Parse; open Parse_Spec; open Scan in

‎Channel_Type.thy

Lines changed: 28 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,12 @@ lemma ctor_codep_intro:
2929
shows "ctor_prism ctor1 disc1 sel1 \<nabla> ctor_prism ctor2 disc2 sel2"
3030
by (rule prism_diff_intro, simp add: lens_defs assms)
3131

32+
lemma dom_match_ctor_prism [simp]:
33+
"dom match\<^bsub>ctor_prism ctor disc sel\<^esub> = Collect disc"
34+
by (simp add: ctor_prism_def dom_def)
35+
36+
named_theorems chan_defs
37+
3238
subsection \<open> Channel Type Representation \<close>
3339

3440
text \<open> A channel is represented by a name, a type, and a predicate that determines whether the event is on this channel. \<close>
@@ -50,10 +56,17 @@ text \<open> Well-formed channel type representations \<close>
5056
definition wf_chantyperep :: "'a raw_chantyperep \<Rightarrow> bool" where
5157
"wf_chantyperep ct =
5258
(distinct (map chan_name ct) \<comment> \<open> Each channel name is unique \<close>
53-
\<and> (\<forall> x. foldr (\<or>) (map (\<lambda> c. is_chan c x) ct) False) \<comment> \<open> Every event has a channel \<close>
54-
\<and> (\<forall> c1\<in>set ct. \<forall> c2\<in>set ct. \<forall> e. is_chan c1 e \<and> is_chan c2 e \<longrightarrow> c1 = c2) \<comment> \<open> Every event has exactly one channel \<close>
59+
\<and> (\<forall> x. foldr (\<or>) (map (\<lambda> c. is_chan c x) ct) False) \<comment> \<open> Every event has at least one channel \<close>
60+
\<and> (\<forall> c1\<in>set ct. \<forall> c2\<in>set ct. \<forall> e. is_chan c1 e \<and> is_chan c2 e \<longrightarrow> c1 = c2) \<comment> \<open> Every event has no more than one channel \<close>
5561
\<and> (\<forall> c\<in>set ct. \<exists> e. is_chan c e))" \<comment> \<open> Every channel has at least one event \<close>
5662

63+
lemma wf_chantyperepI:
64+
assumes "distinct (map chan_name ct)" "\<forall> x. foldr (\<or>) (map (\<lambda> c. is_chan c x) ct) False"
65+
"\<forall> c1\<in>set ct. \<forall> c2\<in>set ct. \<forall> e. is_chan c1 e \<and> is_chan c2 e \<longrightarrow> c1 = c2"
66+
"\<forall> c\<in>set ct. \<exists> e. is_chan c e"
67+
shows "wf_chantyperep ct"
68+
by (simp add: assms wf_chantyperep_def)
69+
5770
typedef 'a chantyperep = "{ctr::'a raw_chantyperep. wf_chantyperep ctr}"
5871
apply (rule_tac x="[Chanrep STR ''x'' TYPEREP(bool) (\<lambda> x. True)]" in exI)
5972
apply (auto simp add: wf_chantyperep_def)
@@ -71,10 +84,20 @@ definition set_chans :: "'a chantyperep \<Rightarrow> String.literal set \<Right
7184
"set_chans ct ns = \<Union> (set_chan ct ` ns)"
7285

7386
named_theorems datatype_disc_thms
87+
named_theorems disc_thms
88+
named_theorems exhaust_disc_thms
89+
7490
named_theorems chantyperep_defs
7591

7692
method wf_chantyperep = (simp add: comp_def wf_chantyperep_def chantyperep_defs, (meson datatype_disc_thms)?)
7793

94+
method wf_chantyperep' =
95+
(rule wf_chantyperepI
96+
, simp add: comp_def chantyperep_defs
97+
, (simp add: comp_def chantyperep_defs; (insert exhaust_disc_thms, blast))
98+
, (simp add: comp_def chantyperep_defs; blast) (* This step could do with optimising -- the simplification is very slow *)
99+
, (simp add: comp_def chantyperep_defs; (insert disc_thms, blast intro: disc_thms)))
100+
78101
lemma foldr_disj_one_True: "foldr (\<or>) Ps False \<Longrightarrow> (\<exists> P\<in>set Ps. P)"
79102
by (induct Ps, auto)
80103

@@ -101,7 +124,7 @@ class chantyperep =
101124
fixes chantyperep :: "'a itself \<Rightarrow> 'a raw_chantyperep"
102125
assumes wf_chantyperep: "wf_chantyperep (chantyperep TYPE('a))"
103126

104-
method chantyperep_inst = (rule chantyperep_class.intro, (intro_classes)[1], rule_tac class.chantyperep.intro, wf_chantyperep)
127+
method chantyperep_inst = (rule chantyperep_class.intro, (intro_classes)[1], rule_tac class.chantyperep.intro, wf_chantyperep')
105128

106129
syntax "_chantyperep" :: "type \<Rightarrow> logic" ("CHANTYPEREP'(_')")
107130
translations "CHANTYPEREP('a)" == "CONST chantyperep TYPE('a)"
@@ -160,6 +183,8 @@ lemma prism_chanrep_eqI:
160183
using evs_of_inj wf_chantyperep apply blast
161184
done
162185

186+
method prism_chanrep = (rule prism_chanrep_eqI, simp, simp add: chantyperep_defs, simp add: chan_defs)
187+
163188
subsection \<open> Channel Type Command \<close>
164189

165190
ML_file "Channel_Type.ML"

‎Channel_Type_Example.thy

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,28 @@ chantype ch_single =
88
chantype ch_two =
99
chbool :: bool
1010
chint :: int
11+
12+
chantype ct =
13+
a1 :: int
14+
a2 :: int
15+
a3 :: int
16+
a4 :: int
17+
a5 :: int
18+
a6 :: int
19+
a7 :: int
20+
a8 :: int
1121

1222
chantype ch_buffer =
1323
inp :: unit
1424
outp :: nat
15-
mod :: bool
25+
modif :: bool
1626

1727
thm ch_buffer.inp_wb_prism
1828

1929
thm ch_buffer.codeps
2030

31+
thm ch_buffer.prism_chanreps
32+
2133
chantype ch_buffer2 =
2234
inp2 :: unit
2335
outp2 :: nat

‎Channel_Type_Tests.thy

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
theory Channel_Type_Tests
2+
imports Channel_Type
3+
begin
4+
5+
(* Create a very large channel type (50 channels) to test proof and instantiation *)
6+
7+
ML \<open> val chans = map (fn n => ("a" ^ Int.toString n, "int")) (0 upto 49); \<close>
8+
9+
setup \<open> Channel_Type.compile_chantype ("ch_big", chans) \<close>
10+
11+
print_theorems
12+
13+
thm ch_big.prism_chanreps
14+
15+
end

0 commit comments

Comments
 (0)