Skip to content

Commit bb78a46

Browse files
simondfostersimondfoster
committed
Added types for reflecting the structure of a channel type. The ML code to generate these still needs some work.
1 parent d152729 commit bb78a46

File tree

2 files changed

+138
-6
lines changed

2 files changed

+138
-6
lines changed

‎Channel_Type.ML

Lines changed: 24 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,13 @@ fun defs qual inds f ctx =
5656
let val (thm, ctx') = def qual (i, f i) ctx
5757
in (thms @ [thm], ctx') end) inds ([], ctx)
5858

59+
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))
62+
in
63+
@{print} (mk_list dummyT (map mk_chanrep chans))
64+
end
65+
5966
fun compile_chantype (name, chans) ctx =
6067
let
6168
open BNF_FP_Def_Sugar; open BNF_FP_Rec_Sugar_Util; open BNF_LFP; open Ctr_Sugar
@@ -69,28 +76,39 @@ fun compile_chantype (name, chans) ctx =
6976
val prefix = thypfx ^ name ^ "."
7077
val attrs = @{attributes [simp, code_unfold]}
7178
val dummy_disc = absdummy dummyT @{term True}
79+
val ctx1 = co_datatype_cmd Least_FP construct_lfp
80+
((K Plugin_Name.default_filter, true),
81+
[((((([],Binding.name name), Mixfix.NoSyn), ctrs), (Binding.empty, Binding.empty, Binding.empty)),[])]) ctx
82+
val typ = read_typ ctx1 name
7283
in
73-
(co_datatype_cmd Least_FP construct_lfp
74-
((K Plugin_Name.default_filter, true),
75-
[((((([],Binding.name name), Mixfix.NoSyn), ctrs), (Binding.empty, Binding.empty, Binding.empty)),[])])
84+
(
7685
(* The datatype package does not produce a discriminator for the second constructor when
7786
there are two constructors. We here generate one for uniformity. *)
78-
#> (if (length pnames = 2)
87+
(if (length pnames = 2)
7988
then abbreviation
8089
Syntax.mode_default (SOME (Binding.qualify false name (Binding.name (is_prefix ^ nth pnames 1 ^ ctor_suffix)), NONE, NoSyn)) []
8190
(mk_def dummyT
8291
(is_prefix ^ nth pnames 1 ^ ctor_suffix)
8392
(const @{const_name comp} $ @{term Not} $ const (prefix ^ is_prefix ^ nth pnames 0 ^ ctor_suffix))) false
8493
else I)
94+
(* The datatype also does not produce a discrimator when the length is 1 *)
95+
#> (if (length pnames = 1)
96+
then abbreviation
97+
Syntax.mode_default (SOME (Binding.qualify false name (Binding.name (is_prefix ^ nth pnames 0 ^ ctor_suffix)), NONE, NoSyn)) []
98+
(mk_def dummyT
99+
(is_prefix ^ nth pnames 0 ^ ctor_suffix)
100+
(Abs ("x", typ, @{term "True"}))) false
101+
else I)
85102
#> defs name pnames (fn x => (const @{const_name ctor_prism}
86103
$ const (prefix ^ x ^ ctor_suffix)
87104
$ (if (length pnames = 1) then dummy_disc else const (prefix ^ is_prefix ^ x ^ ctor_suffix))
88105
$ const (prefix ^ un_prefix ^ x ^ ctor_suffix)))
89106
#> (fn (thms, ctx) =>
90107
(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
91108
#> (snd o note ((Binding.qualify false name (Binding.name codepsN), attrs), map (codep_proof thms ctx) (pairings pnames)))
92-
) ctx))
93-
ctx
109+
) ctx)
110+
(* #> (fn ctx => snd ((def name ("ctrep", mk_chantyperep chans ctx1)) ctx)) *))
111+
ctx1
94112
end;
95113

96114
end;

‎Channel_Type.thy

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ begin
88
text \<open> A channel type is a simplified algebraic datatype where each constructor has exactly
99
one parameter, and it is wrapped up as a prism. It a dual of an alphabet type. \<close>
1010

11+
subsection \<open> Datatype Constructor Prisms \<close>
12+
1113
definition ctor_prism :: "('a \<Rightarrow> 'd) \<Rightarrow> ('d \<Rightarrow> bool) \<Rightarrow> ('d \<Rightarrow> 'a) \<Rightarrow> ('a \<Longrightarrow>\<^sub>\<triangle> 'd)" where
1214
[lens_defs]:
1315
"ctor_prism ctor disc sel = \<lparr> prism_match = (\<lambda> d. if (disc d) then Some (sel d) else None)
@@ -27,6 +29,118 @@ lemma ctor_codep_intro:
2729
shows "ctor_prism ctor1 disc1 sel1 \<nabla> ctor_prism ctor2 disc2 sel2"
2830
by (rule prism_diff_intro, simp add: lens_defs assms)
2931

32+
subsection \<open> Channel Type Representation \<close>
33+
34+
text \<open> A channel is represented by a name, a type, and a predicate that determines whether the event is on this channel. \<close>
35+
36+
datatype 'a chanrep = Chanrep (chan_name: String.literal) (chan_type: String.literal) (is_chan: "'a \<Rightarrow> bool")
37+
38+
definition evs_of :: "'a chanrep \<Rightarrow> 'a set" where
39+
"evs_of c = {e. is_chan c e}"
40+
41+
lemma evs_of_Chanrep [simp]: "evs_of (Chanrep n t P) = Collect P"
42+
by (simp add: evs_of_def)
43+
44+
text \<open> A channel type is represented by a list of channels \<close>
45+
46+
type_synonym 'a chantyperep = "'a chanrep list"
47+
48+
text \<open> Well-formed channel type representations \<close>
49+
50+
definition wf_chantyperep :: "'a chanrep list \<Rightarrow> bool" where
51+
"wf_chantyperep ct =
52+
(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>
55+
\<and> (\<forall> c\<in>set ct. \<exists> e. is_chan c e))" \<comment> \<open> Every channel has at least one event \<close>
56+
57+
method wf_chantyperep uses disc def = (force intro: disc simp add: wf_chantyperep_def def)
58+
59+
lemma foldr_disj_one_True: "foldr (\<or>) Ps False \<Longrightarrow> (\<exists> P\<in>set Ps. P)"
60+
by (induct Ps, auto)
61+
62+
text \<open> Every event has a channel \<close>
63+
64+
lemma chantyperep_ev_has_chan: "wf_chantyperep ct \<Longrightarrow> \<exists> c\<in>set ct. is_chan c e"
65+
using foldr_disj_one_True by (fastforce simp add: wf_chantyperep_def)
66+
67+
definition find_chanrep :: "'a chantyperep \<Rightarrow> 'a \<Rightarrow> 'a chanrep option" where
68+
"find_chanrep ct e = find (\<lambda> c. is_chan c e) ct"
69+
70+
lemma find_chanrep_Some: "wf_chantyperep ct \<Longrightarrow> \<exists> c\<in>set ct. find_chanrep ct e = Some c"
71+
by (metis chantyperep_ev_has_chan find_None_iff2 find_Some_iff find_chanrep_def not_Some_eq nth_mem)
72+
73+
text \<open> Every channel has at least one event \<close>
74+
75+
lemma chantyperep_chan_has_ev:"\<lbrakk> wf_chantyperep ct; c \<in> set ct \<rbrakk> \<Longrightarrow> \<exists>e. is_chan c e"
76+
using wf_chantyperep_def by fastforce
77+
78+
lemma evs_of_inj: "\<lbrakk> wf_chantyperep ct; c \<in> set ct; d \<in> set ct; evs_of c = evs_of d \<rbrakk> \<Longrightarrow> c = d"
79+
by (metis evs_of_def mem_Collect_eq wf_chantyperep_def)
80+
81+
class chantyperep =
82+
fixes chantyperep :: "'a itself \<Rightarrow> 'a chantyperep"
83+
assumes wf_chantyperep: "wf_chantyperep (chantyperep TYPE('a))"
84+
85+
syntax "_chantyperep" :: "type \<Rightarrow> logic" ("CHANTYPEREP'(_')")
86+
translations "CHANTYPEREP('a)" == "CONST chantyperep TYPE('a)"
87+
88+
context chantyperep
89+
begin
90+
91+
definition chan_names :: "'a itself \<Rightarrow> String.literal list" where
92+
"chan_names t = map chan_name (chantyperep t)"
93+
94+
lemma distinct_chan_names [simp]: "distinct (chan_names TYPE('a))"
95+
using chan_names_def local.wf_chantyperep wf_chantyperep_def by auto
96+
97+
definition chanrep_of :: "'a \<Rightarrow> 'a chanrep" where
98+
"chanrep_of e = the (find_chanrep CHANTYPEREP('a) e)"
99+
100+
lemma range_chanrep_of: "range chanrep_of = set CHANTYPEREP('a)"
101+
apply (auto simp add: chanrep_of_def image_def)
102+
apply (metis find_chanrep_Some local.wf_chantyperep option.sel)
103+
apply (metis find_Some_iff find_chanrep_Some find_chanrep_def local.wf_chantyperep option.sel wf_chantyperep_def)
104+
done
105+
106+
lemma finite_chanreps: "finite (range chanrep_of)"
107+
using range_chanrep_of by auto
108+
109+
text \<open> An independent family of events, each corresponding to one set of channels. \<close>
110+
111+
definition ChanBasis :: "'a set set" where
112+
"ChanBasis = evs_of ` range chanrep_of"
113+
114+
lemma family_chan_basis: "\<Union> ChanBasis = UNIV"
115+
apply (auto simp add: ChanBasis_def evs_of_def)
116+
apply (metis chantyperep_ev_has_chan image_iff local.wf_chantyperep range_chanrep_of)
117+
done
118+
119+
lemma indep_chan_basis: "\<lbrakk> A \<in> ChanBasis; B \<in> ChanBasis; A \<noteq> B \<rbrakk> \<Longrightarrow> A \<inter> B = {}"
120+
apply (auto simp add: ChanBasis_def evs_of_def)
121+
apply (metis local.wf_chantyperep rangeI range_chanrep_of wf_chantyperep_def)+
122+
done
123+
124+
end
125+
126+
subsection \<open> Prisms with a Channel Representation \<close>
127+
128+
definition prism_chanrep :: "('a \<Longrightarrow>\<^sub>\<triangle> 'e::chantyperep) \<Rightarrow> 'e chanrep" where
129+
"prism_chanrep c = (SOME d. d \<in> set CHANTYPEREP('e) \<and> evs_of d = dom (match\<^bsub>c\<^esub>))"
130+
131+
lemma prism_chanrep_eqI:
132+
fixes c :: "'a \<Longrightarrow>\<^sub>\<triangle> 'e::chantyperep" and d :: "'e chanrep"
133+
assumes "wb_prism c" "d \<in> set CHANTYPEREP('e)" "dom match\<^bsub>c\<^esub> = evs_of d"
134+
shows "prism_chanrep c = d"
135+
using assms
136+
apply (simp add: prism_chanrep_def)
137+
apply (rule some_equality)
138+
apply simp
139+
using evs_of_inj wf_chantyperep apply blast
140+
done
141+
142+
subsection \<open> Channel Type Command \<close>
143+
30144
ML_file "Channel_Type.ML"
31145

32146
end

0 commit comments

Comments
 (0)