Skip to content

Commit 5b054e7

Browse files
simondfostersimondfoster
committed
In progress
1 parent 642da08 commit 5b054e7

File tree

2 files changed

+91
-25
lines changed

2 files changed

+91
-25
lines changed

‎Channel_Type.ML

Lines changed: 44 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -44,15 +44,15 @@ fun mk_def ty x v = Const ("Pure.eq", ty --> ty --> Term.propT) $ Free (x, ty) $
4444
val is_prefix = "is_";
4545
val un_prefix = "un_";
4646

47-
fun def qual (x, tm) ctx =
47+
fun def typ 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, @{attributes [lens_defs, chan_defs]}), mk_def dummyT x tm) ctx
49+
val ((_, (_, thm)), d) = definition (SOME (Binding.qualify false qual (Binding.name x), SOME typ, NoSyn)) [] [] ((Binding.empty, @{attributes [lens_defs, chan_defs]}), mk_def typ x tm) ctx
5050
in (thm, d)
5151
end
5252

53-
fun defs qual inds f ctx =
53+
fun defs typ qual inds f ctx =
5454
fold (fn i => fn (thms, ctx) =>
55-
let val (thm, ctx') = def qual (i, f i) ctx
55+
let val (thm, ctx') = def typ qual (i, f i) ctx
5656
in (thms @ [thm], ctx') end) inds ([], ctx)
5757

5858
fun mk_chantyperep chans ctx =
@@ -71,25 +71,29 @@ fun mk_chantyperep chans ctx =
7171
mk_list dummyT (map mk_chanrep chans)
7272
end
7373

74-
fun chantyperep_def name raw_chans ct ctx =
74+
fun chantyperep_def name raw_chans ct vmap ctx =
7575
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
76+
open Syntax; open HOLogic; open Global_Theory; open Proof_Context
77+
val ty = read_type_name {proper = true, strict = false} ctx name;
78+
fun repl_tvars ty = map_type_tfree (fn (n, s) => TFree (the (AList.lookup (op =) vmap n), s)) ty
79+
val chans = @{print} (map (fn (n, t) => (n, mk_typerep (repl_tvars (read_typ ctx t)))) raw_chans)
7980
val lhs = ct $ Free ("T", Term.itselfT ty);
8081
val rhs = mk_chantyperep chans ctx;
8182
val eq = check_term ctx (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
8283
in snd (Specification.definition NONE [] [] ((Binding.empty, @{attributes [chantyperep_defs]}), eq) ctx)
8384
end;
8485

85-
fun chantyperep_instance name raw_chans thy =
86+
fun chantyperep_instance raw_vars vars sorts name raw_chans thy =
8687
let
8788
open Syntax; open HOLogic; open Global_Theory;
88-
val ty = read_typ (Named_Target.theory_init thy) name;
89+
val vmap = ListPair.zip (raw_vars, vars)
90+
val tvars = ListPair.zip (vars, sorts)
91+
val ty = Proof_Context.read_type_name {proper = true, strict = false} (Named_Target.theory_init thy) name;
8992
val tyco = fst (dest_Type ty);
90-
val ctx0 = Class.instantiation ([tyco], [], \<^sort>\<open>chantyperep\<close>) thy;
93+
val ctx0 = Class.instantiation ([tyco], tvars, \<^sort>\<open>chantyperep\<close>) thy;
9194
val ctx1 = snd (Local_Theory.begin_nested ctx0)
92-
val ctx2 = chantyperep_def name raw_chans \<^Const>\<open>chantyperep ty\<close> ctx1
95+
val ty' = Type (tyco, map (read_typ ctx1) vars)
96+
val ctx2 = chantyperep_def name raw_chans \<^Const>\<open>chantyperep ty'\<close> vmap ctx1
9397
val ctx3 = Local_Theory.end_nested ctx2;
9498
val disc_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".discI")
9599
val exhaust_disc_thms = if length raw_chans = 1 then [] else get_thms thy (tyco ^ ".exhaust_disc")
@@ -101,7 +105,7 @@ fun chantyperep_instance name raw_chans thy =
101105
Class.prove_instantiation_exit (fn _ => NO_CONTEXT_TACTIC ctx5 (Method_Closure.apply_method ctx5 @{method chantyperep_inst} [] [] [] ctx5 [])) ctx5
102106
end;
103107

104-
fun make_chantype (name, chans) thy =
108+
fun make_chantype tvars vars sorts name chans thy =
105109
let
106110
open BNF_FP_Def_Sugar; open BNF_FP_Rec_Sugar_Util; open BNF_LFP; open Ctr_Sugar
107111
open Prism_Lib; open Lens_Lib; open Local_Theory; open Specification; open Syntax; open HOLogic; open Global_Theory
@@ -117,8 +121,11 @@ fun make_chantype (name, chans) thy =
117121
val dummy_disc = absdummy dummyT @{term True}
118122
val ctx1 = co_datatype_cmd Least_FP construct_lfp
119123
((K Plugin_Name.default_filter, true),
120-
[((((([],Binding.name name), Mixfix.NoSyn), ctrs), (Binding.empty, Binding.empty, Binding.empty)),[])]) ctx
121-
val typ = read_typ ctx1 name
124+
[(((((tvars, Binding.name name), Mixfix.NoSyn), ctrs), (Binding.empty, Binding.empty, Binding.empty)),[])]) ctx
125+
val typ = Proof_Context.read_type_name {proper = true, strict = false} ctx1 name
126+
val tyco = fst (dest_Type typ);
127+
val typ' = Type (tyco, map TFree (ListPair.zip (vars, sorts)))
128+
val ptyp = prismT dummyT typ'
122129
in
123130
(
124131
(* The datatype package does not produce a discriminator for the second constructor when
@@ -138,7 +145,7 @@ fun make_chantype (name, chans) thy =
138145
(is_prefix ^ nth pnames 0 ^ ctor_suffix)
139146
(Abs ("x", typ, @{term "True"}))) false
140147
else I)
141-
#> defs name pnames (fn x => (const @{const_name ctor_prism}
148+
#> defs ptyp name pnames (fn x => (const @{const_name ctor_prism}
142149
$ const (prefix ^ x ^ ctor_suffix)
143150
$ (if (length pnames = 1) then dummy_disc else const (prefix ^ is_prefix ^ x ^ ctor_suffix))
144151
$ const (prefix ^ un_prefix ^ x ^ ctor_suffix)))
@@ -152,14 +159,19 @@ fun make_chantype (name, chans) thy =
152159

153160
fun prism_has_chanrep n ctx =
154161
let open Syntax; open HOLogic
155-
val c = read_term ctx n in
156-
Trueprop $ (const @{const_name has_chanrep} $ c)
162+
val c = parse_term ctx n in
163+
Trueprop $ (const @{const_name has_chanrep} $ c)
157164
end
158165

166+
fun
167+
add_typerep_tfrees (Type (n, ts)) = Type (n, map add_typerep_tfrees ts) |
168+
add_typerep_tfrees (TFree (n, sorts)) = TFree (n, sorts @ @{sort typerep}) |
169+
add_typerep_tfrees (TVar (n, sorts)) = TVar (n, sorts @ @{sort typerep})
170+
159171
fun prism_has_chanrep_proof ctx (n, t) =
160172
let open Simplifier; open Prism_Lib; open Syntax; open HOLogic
161173
val d = read_term ctx ("is_" ^ n ^ "_C")
162-
val ct = Syntax.check_term ctx ((const @{const_name Chanrep} $ mk_literal n $ mk_typerep (read_typ ctx t)) $ d)
174+
val ct = Syntax.check_term ctx ((const @{const_name Chanrep} $ mk_literal n $ mk_typerep (add_typerep_tfrees (read_typ ctx t))) $ d)
163175
in
164176
Goal.prove ctx [] []
165177
(Syntax.check_term ctx (prism_has_chanrep n ctx))
@@ -169,7 +181,7 @@ fun prism_has_chanrep_proof ctx (n, t) =
169181
fun prism_chanrep n t ctx =
170182
let open Syntax; open HOLogic
171183
val c = read_term ctx n; val d = read_term ctx ("is_" ^ n ^ "_C")
172-
val ct = ((const @{const_name Chanrep} $ mk_literal n $ mk_typerep t) $ d) in
184+
val ct = ((const @{const_name Chanrep} $ mk_literal n $ mk_typerep (add_typerep_tfrees t)) $ d) in
173185
Trueprop $ (eq_const dummyT $ (const @{const_name chanrep_of} $ c) $ ct)
174186
end
175187

@@ -190,18 +202,25 @@ fun prism_chanrep_proofs (name, chans) thy =
190202

191203

192204

193-
fun compile_chantype (name, chans) =
194-
make_chantype (name, chans) #>
205+
fun compile_chantype ((tvars, name), chans) thy =
206+
let
207+
open Syntax
208+
val ctx = Named_Target.theory_init thy;
209+
val vars = map (fn n => "'" ^ Char.toString (Char.chr n)) (97 upto (96 + length tvars));
210+
val sorts = map (fn t => case snd (snd t) of SOME s => read_sort ctx s @ @{sort typerep} | NONE => @{sort typerep}) tvars
211+
in
212+
(make_chantype tvars vars sorts name chans #>
195213
(* Generate chantyperep instance *)
196-
chantyperep_instance name chans #>
214+
chantyperep_instance (map (fst o snd) tvars) vars sorts name chans #>
197215
(* Generate representations for each prism (channel) *)
198-
prism_chanrep_proofs (name, chans)
216+
prism_chanrep_proofs (name, chans)) thy
217+
end
199218

200219
end;
201220

202221
let open Parse; open Parse_Spec; open Scan in
203222
Outer_Syntax.command @{command_keyword chantype} "define a channel datatype"
204-
((name --
223+
((( BNF_Util.parse_type_args_named_constrained -- name) --
205224
(@{keyword "="} |-- repeat1 (name -- ($$$ "::" |-- !!! typ))))
206225
>> (fn x => Toplevel.theory (Channel_Type.compile_chantype x)))
207226
end;

‎Channel_Type.thy

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,4 +220,51 @@ subsection \<open> Channel Type Command \<close>
220220

221221
ML_file "Channel_Type.ML"
222222

223+
(*
224+
datatype 'a ty =
225+
x "'a"
226+
227+
ML \<open> Syntax.read_typ @{context} "'a ty"\<close>
228+
229+
ML \<open> Syntax.check_typ @{context} (Proof_Context.read_type_name {proper = true, strict = false} @{context} "ty") \<close>
230+
*)
231+
232+
declare [[show_sorts]]
233+
234+
ML \<open>
235+
open BNF_FP_Def_Sugar;
236+
open BNF_FP_Def_Sugar; open BNF_FP_Rec_Sugar_Util; open BNF_LFP; open Ctr_Sugar;
237+
238+
\<close>
239+
240+
ML \<open>
241+
val ctrs = [(((Binding.empty, Binding.name "MyCtr"), [(Binding.empty, @{typ int})]), NoSyn)];
242+
243+
(fn ctrs =>
244+
co_datatypes Least_FP construct_lfp
245+
((Plugin_Name.default_filter, true), [((((([], Binding.name "myt"), Mixfix.NoSyn), ctrs), (Binding.empty, Binding.empty, Binding.empty)),[])]))
246+
ctrs @{context}
247+
248+
; \<close>
249+
chantype 'a::typerep ty =
250+
x :: "'a list"
251+
y :: "nat"
252+
z :: bool
253+
254+
term x
255+
256+
257+
term x
258+
259+
term "CHANTYPEREP('v::typerep ty)"
260+
261+
lemma "has_chanrep x"
262+
apply (simp add: has_chanrep_def chantyperep_ty_def)
263+
apply (prism_has_chanrep "chanrep_of x")
264+
265+
declare [[show_sorts]]
266+
267+
term x
268+
269+
223270
end

0 commit comments

Comments
 (0)