20600
|
1 |
(* Title: Pure/Tools/codegen_data.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Basic code generator data structures; abstract executable content of theory.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature CODEGEN_DATA =
|
|
9 |
sig
|
|
10 |
type lthms = thm list Susp.T;
|
|
11 |
val lazy: (unit -> thm list) -> lthms
|
|
12 |
val eval_always: bool ref
|
|
13 |
|
|
14 |
val add_func: thm -> theory -> theory
|
|
15 |
val del_func: thm -> theory -> theory
|
|
16 |
val add_funcl: CodegenConsts.const * lthms -> theory -> theory
|
|
17 |
val add_datatype: string * (((string * sort) list * (string * typ list) list) * lthms)
|
|
18 |
-> theory -> theory
|
|
19 |
val del_datatype: string -> theory -> theory
|
|
20 |
val add_inline: thm -> theory -> theory
|
|
21 |
val del_inline: thm -> theory -> theory
|
20844
|
22 |
val add_inline_proc: (theory -> cterm list -> thm list) -> theory -> theory
|
|
23 |
val add_constrains: (theory -> term list -> (indexname * sort) list) -> theory -> theory
|
20600
|
24 |
val add_preproc: (theory -> thm list -> thm list) -> theory -> theory
|
|
25 |
val these_funcs: theory -> CodegenConsts.const -> thm list
|
|
26 |
val get_datatype: theory -> string
|
|
27 |
-> ((string * sort) list * (string * typ list) list) option
|
|
28 |
val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
|
|
29 |
|
|
30 |
val print_thms: theory -> unit
|
|
31 |
|
|
32 |
val typ_func: theory -> thm -> typ
|
|
33 |
val rewrite_func: thm list -> thm -> thm
|
20844
|
34 |
val preprocess_cterm: theory -> (string * typ -> typ) -> cterm -> thm * cterm
|
20600
|
35 |
|
20844
|
36 |
val trace: bool ref
|
20600
|
37 |
val strict_functyp: bool ref
|
|
38 |
end;
|
|
39 |
|
|
40 |
signature PRIVATE_CODEGEN_DATA =
|
|
41 |
sig
|
|
42 |
include CODEGEN_DATA
|
|
43 |
type data
|
|
44 |
structure CodeData: THEORY_DATA
|
|
45 |
val declare: string -> Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
|
|
46 |
-> (CodegenConsts.const list option -> Object.T -> Object.T) -> serial
|
|
47 |
val init: serial -> theory -> theory
|
|
48 |
val get: serial -> (Object.T -> 'a) -> data -> 'a
|
|
49 |
val put: serial -> ('a -> Object.T) -> 'a -> data -> data
|
|
50 |
end;
|
|
51 |
|
|
52 |
structure CodegenData : PRIVATE_CODEGEN_DATA =
|
|
53 |
struct
|
|
54 |
|
|
55 |
(** diagnostics **)
|
|
56 |
|
20844
|
57 |
val trace = ref false;
|
|
58 |
fun tracing f x = (if !trace then Output.tracing (f x) else (); x);
|
20600
|
59 |
|
|
60 |
|
|
61 |
|
|
62 |
(** lazy theorems, certificate theorems **)
|
|
63 |
|
|
64 |
type lthms = thm list Susp.T;
|
|
65 |
val eval_always = ref false;
|
|
66 |
|
|
67 |
fun lazy f = if !eval_always
|
|
68 |
then Susp.value (f ())
|
|
69 |
else Susp.delay f;
|
|
70 |
|
|
71 |
fun string_of_lthms r = case Susp.peek r
|
|
72 |
of SOME thms => (map string_of_thm o rev) thms
|
|
73 |
| NONE => ["[...]"];
|
|
74 |
|
|
75 |
fun pretty_lthms ctxt r = case Susp.peek r
|
|
76 |
of SOME thms => (map (ProofContext.pretty_thm ctxt) o rev) thms
|
|
77 |
| NONE => [Pretty.str "[...]"];
|
|
78 |
|
20844
|
79 |
fun certificate thy f r =
|
20600
|
80 |
case Susp.peek r
|
20844
|
81 |
of SOME thms => (Susp.value o f thy) thms
|
|
82 |
| NONE => let
|
|
83 |
val thy_ref = Theory.self_ref thy;
|
|
84 |
in lazy (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
|
20600
|
85 |
|
|
86 |
fun merge' _ ([], []) = (false, [])
|
|
87 |
| merge' _ ([], ys) = (true, ys)
|
|
88 |
| merge' eq (xs, ys) = fold_rev
|
|
89 |
(fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs);
|
|
90 |
|
|
91 |
fun merge_alist eq_key eq (xys as (xs, ys)) =
|
|
92 |
if eq_list (eq_pair eq_key eq) (xs, ys)
|
|
93 |
then (false, xs)
|
|
94 |
else (true, AList.merge eq_key eq xys);
|
|
95 |
|
|
96 |
val merge_thms = merge' eq_thm;
|
|
97 |
|
|
98 |
fun merge_lthms (r1, r2) =
|
|
99 |
if Susp.same (r1, r2) then (false, r1)
|
|
100 |
else case Susp.peek r1
|
|
101 |
of SOME [] => (true, r2)
|
|
102 |
| _ => case Susp.peek r2
|
|
103 |
of SOME [] => (true, r1)
|
|
104 |
| _ => (apsnd (lazy o K)) (merge_thms (Susp.force r1, Susp.force r2));
|
|
105 |
|
|
106 |
|
|
107 |
|
|
108 |
(** code theorems **)
|
|
109 |
|
20844
|
110 |
(* making rewrite theorems *)
|
20600
|
111 |
|
|
112 |
fun bad_thm msg thm =
|
|
113 |
error (msg ^ ": " ^ string_of_thm thm);
|
|
114 |
|
20844
|
115 |
fun check_rew thy thm =
|
|
116 |
let
|
|
117 |
val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm;
|
|
118 |
fun vars_of t = fold_aterms
|
|
119 |
(fn Var (v, _) => insert (op =) v
|
|
120 |
| Free _ => bad_thm "Illegal free variable in rewrite theorem" thm
|
|
121 |
| _ => I) t [];
|
|
122 |
fun tvars_of t = fold_term_types
|
|
123 |
(fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
|
|
124 |
| TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t [];
|
|
125 |
val lhs_vs = vars_of lhs;
|
|
126 |
val rhs_vs = vars_of rhs;
|
|
127 |
val lhs_tvs = tvars_of lhs;
|
|
128 |
val rhs_tvs = tvars_of lhs;
|
|
129 |
val _ = if null (subtract (op =) lhs_vs rhs_vs)
|
|
130 |
then ()
|
|
131 |
else bad_thm "Free variables on right hand side of rewrite theorems" thm
|
|
132 |
val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
|
|
133 |
then ()
|
|
134 |
else bad_thm "Free type variables on right hand side of rewrite theorems" thm
|
|
135 |
in thm end;
|
|
136 |
|
|
137 |
fun mk_rew thy thm =
|
|
138 |
let
|
|
139 |
val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm;
|
|
140 |
in
|
|
141 |
map (check_rew thy) thms
|
|
142 |
end;
|
|
143 |
|
|
144 |
|
|
145 |
(* making function theorems *)
|
|
146 |
|
20600
|
147 |
fun typ_func thy = snd o dest_Const o fst o strip_comb o fst
|
|
148 |
o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of;
|
|
149 |
|
20844
|
150 |
val strict_functyp = ref true;
|
|
151 |
|
|
152 |
fun dest_func thy = apfst dest_Const o strip_comb o Envir.beta_eta_contract
|
|
153 |
o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of;
|
|
154 |
|
|
155 |
fun mk_head thy thm =
|
|
156 |
((CodegenConsts.norm_of_typ thy o fst o dest_func thy) thm, thm);
|
20600
|
157 |
|
20844
|
158 |
fun check_func verbose thy thm = case try (dest_func thy) thm
|
|
159 |
of SOME (c_ty as (c, ty), args) =>
|
|
160 |
let
|
|
161 |
val _ =
|
|
162 |
if has_duplicates (op =)
|
|
163 |
((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args [])
|
|
164 |
then bad_thm "Repeated variables on left hand side of function equation" thm
|
|
165 |
else ()
|
|
166 |
val is_classop = (is_some o AxClass.class_of_param thy) c;
|
|
167 |
val const = CodegenConsts.norm_of_typ thy c_ty;
|
|
168 |
val ty_decl = CodegenConsts.disc_typ_of_const thy
|
|
169 |
(snd o CodegenConsts.typ_of_inst thy) const;
|
|
170 |
val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
|
|
171 |
in if Sign.typ_equiv thy (ty_decl, ty)
|
|
172 |
then (const, thm)
|
|
173 |
else (if is_classop orelse (!strict_functyp andalso not
|
|
174 |
(Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)))
|
|
175 |
then error else (if verbose then warning else K ()) #> K (const, thm))
|
|
176 |
("Type\n" ^ string_of_typ ty
|
|
177 |
^ "\nof function theorem\n"
|
|
178 |
^ string_of_thm thm
|
|
179 |
^ "\nis strictly less general than declared function type\n"
|
|
180 |
^ string_of_typ ty_decl)
|
|
181 |
end
|
|
182 |
| NONE => bad_thm "Not a function equation" thm;
|
|
183 |
|
|
184 |
fun check_typ_classop thy thm =
|
|
185 |
let
|
|
186 |
val (c_ty as (c, ty), _) = dest_func thy thm;
|
|
187 |
in case AxClass.class_of_param thy c
|
|
188 |
of SOME class => let
|
|
189 |
val const = CodegenConsts.norm_of_typ thy c_ty;
|
|
190 |
val ty_decl = CodegenConsts.disc_typ_of_const thy
|
|
191 |
(snd o CodegenConsts.typ_of_inst thy) const;
|
|
192 |
val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
|
|
193 |
in if Sign.typ_equiv thy (ty_decl, ty)
|
|
194 |
then thm
|
|
195 |
else error
|
|
196 |
("Type\n" ^ string_of_typ ty
|
|
197 |
^ "\nof function theorem\n"
|
|
198 |
^ string_of_thm thm
|
|
199 |
^ "\nis strictly less general than declared function type\n"
|
|
200 |
^ string_of_typ ty_decl)
|
|
201 |
end
|
|
202 |
| NONE => thm
|
|
203 |
end;
|
20600
|
204 |
|
|
205 |
fun mk_func thy raw_thm =
|
20844
|
206 |
mk_rew thy raw_thm
|
|
207 |
|> map (check_func true thy);
|
20600
|
208 |
|
|
209 |
fun get_prim_def_funcs thy c =
|
|
210 |
let
|
|
211 |
fun constrain thm0 thm = case AxClass.class_of_param thy (fst c)
|
|
212 |
of SOME _ =>
|
|
213 |
let
|
20704
|
214 |
val ty_decl = CodegenConsts.disc_typ_of_classop thy c;
|
20600
|
215 |
val max = maxidx_of_typ ty_decl + 1;
|
|
216 |
val thm = Thm.incr_indexes max thm;
|
|
217 |
val ty = typ_func thy thm;
|
|
218 |
val (env, _) = Sign.typ_unify thy (ty_decl, ty) (Vartab.empty, max);
|
|
219 |
val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
|
|
220 |
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
|
|
221 |
in Thm.instantiate (instT, []) thm end
|
|
222 |
| NONE => thm
|
|
223 |
in case CodegenConsts.find_def thy c
|
|
224 |
of SOME ((_, thm), _) =>
|
|
225 |
thm
|
|
226 |
|> Thm.transfer thy
|
|
227 |
|> try (map snd o mk_func thy)
|
|
228 |
|> these
|
|
229 |
|> map (constrain thm)
|
|
230 |
| NONE => []
|
|
231 |
end;
|
|
232 |
|
|
233 |
|
|
234 |
(* pairs of (selected, deleted) function theorems *)
|
|
235 |
|
|
236 |
type sdthms = lthms * thm list;
|
|
237 |
|
|
238 |
fun add_drop_redundant thm thms =
|
|
239 |
let
|
|
240 |
val thy = Context.check_thy (Thm.theory_of_thm thm);
|
|
241 |
val pattern = (fst o Logic.dest_equals o Drule.plain_prop_of) thm;
|
|
242 |
fun matches thm' = if (curry (Pattern.matches thy) pattern o
|
|
243 |
fst o Logic.dest_equals o Drule.plain_prop_of) thm'
|
|
244 |
then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); true)
|
|
245 |
else false
|
|
246 |
in thm :: filter_out matches thms end;
|
|
247 |
|
|
248 |
fun add_thm thm (sels, dels) =
|
|
249 |
(Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels);
|
|
250 |
|
|
251 |
fun add_lthms lthms (sels, []) =
|
|
252 |
(lazy (fn () => fold add_drop_redundant
|
|
253 |
(Susp.force lthms) (Susp.force sels)), [])
|
|
254 |
| add_lthms lthms (sels, dels) =
|
|
255 |
fold add_thm (Susp.force lthms) (sels, dels);
|
|
256 |
|
|
257 |
fun del_thm thm (sels, dels) =
|
|
258 |
(Susp.value (remove eq_thm thm (Susp.force sels)), thm :: dels);
|
|
259 |
|
|
260 |
fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
|
|
261 |
|
|
262 |
fun merge_sdthms c ((sels1, dels1), (sels2, dels2)) =
|
|
263 |
let
|
|
264 |
val (dels_t, dels) = merge_thms (dels1, dels2);
|
|
265 |
in if dels_t
|
|
266 |
then let
|
|
267 |
val (_, sels) = merge_thms (Susp.force sels1, subtract eq_thm dels1 (Susp.force sels2))
|
|
268 |
val (_, dels) = merge_thms (dels1, subtract eq_thm (Susp.force sels1) dels2)
|
|
269 |
in (true, ((lazy o K) sels, dels)) end
|
|
270 |
else let
|
|
271 |
val (sels_t, sels) = merge_lthms (sels1, sels2)
|
|
272 |
in (sels_t, (sels, dels)) end
|
|
273 |
end;
|
|
274 |
|
|
275 |
|
|
276 |
(** data structures **)
|
|
277 |
|
|
278 |
structure Consttab = CodegenConsts.Consttab;
|
|
279 |
|
|
280 |
datatype preproc = Preproc of {
|
|
281 |
inlines: thm list,
|
20844
|
282 |
inline_procs: (serial * (theory -> cterm list -> thm list)) list,
|
|
283 |
constrains: (serial * (theory -> term list -> (indexname * sort) list)) list,
|
20600
|
284 |
preprocs: (serial * (theory -> thm list -> thm list)) list
|
|
285 |
};
|
|
286 |
|
20844
|
287 |
fun mk_preproc ((inlines, inline_procs), (constrains, preprocs)) =
|
|
288 |
Preproc { inlines = inlines, inline_procs = inline_procs, constrains = constrains, preprocs = preprocs };
|
|
289 |
fun map_preproc f (Preproc { inlines, inline_procs, constrains, preprocs }) =
|
|
290 |
mk_preproc (f ((inlines, inline_procs), (constrains, preprocs)));
|
|
291 |
fun merge_preproc (Preproc { inlines = inlines1, inline_procs = inline_procs1, constrains = constrains1 , preprocs = preprocs1 },
|
|
292 |
Preproc { inlines = inlines2, inline_procs = inline_procs2, constrains = constrains2 , preprocs = preprocs2 }) =
|
20600
|
293 |
let
|
|
294 |
val (touched1, inlines) = merge_thms (inlines1, inlines2);
|
20844
|
295 |
val (touched2, inline_procs) = merge_alist (op =) (K true) (inline_procs1, inline_procs2);
|
|
296 |
val (touched3, constrains) = merge_alist (op =) (K true) (constrains1, constrains2);
|
|
297 |
val (touched4, preprocs) = merge_alist (op =) (K true) (preprocs1, preprocs2);
|
|
298 |
in (touched1 orelse touched2 orelse touched3 orelse touched4,
|
|
299 |
mk_preproc ((inlines, inline_procs), (constrains, preprocs))) end;
|
20600
|
300 |
|
|
301 |
fun join_func_thms (tabs as (tab1, tab2)) =
|
|
302 |
let
|
|
303 |
val cs1 = Consttab.keys tab1;
|
|
304 |
val cs2 = Consttab.keys tab2;
|
|
305 |
val cs' = filter (member CodegenConsts.eq_const cs2) cs1;
|
|
306 |
val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
|
|
307 |
val cs''' = ref [] : CodegenConsts.const list ref;
|
|
308 |
fun merge c x = let val (touched, thms') = merge_sdthms c x in
|
|
309 |
(if touched then cs''' := cons c (!cs''') else (); thms') end;
|
|
310 |
in (cs'' @ !cs''', Consttab.join merge tabs) end;
|
|
311 |
fun merge_funcs (thms1, thms2) =
|
|
312 |
let
|
|
313 |
val (consts, thms) = join_func_thms (thms1, thms2);
|
|
314 |
in (SOME consts, thms) end;
|
|
315 |
|
|
316 |
val eq_string = op = : string * string -> bool;
|
|
317 |
fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) =
|
|
318 |
gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
|
|
319 |
andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2);
|
|
320 |
fun merge_dtyps (tabs as (tab1, tab2)) =
|
|
321 |
let
|
|
322 |
val tycos1 = Symtab.keys tab1;
|
|
323 |
val tycos2 = Symtab.keys tab2;
|
|
324 |
val tycos' = filter (member eq_string tycos2) tycos1;
|
20844
|
325 |
val touched = not (gen_eq_set (op =) (tycos1, tycos2) andalso
|
|
326 |
gen_eq_set (eq_pair (op =) (eq_dtyp))
|
20600
|
327 |
(AList.make (the o Symtab.lookup tab1) tycos',
|
20844
|
328 |
AList.make (the o Symtab.lookup tab2) tycos'));
|
20600
|
329 |
in (touched, Symtab.merge (K true) tabs) end;
|
|
330 |
|
|
331 |
datatype spec = Spec of {
|
|
332 |
funcs: sdthms Consttab.table,
|
|
333 |
dconstrs: string Consttab.table,
|
|
334 |
dtyps: (((string * sort) list * (string * typ list) list) * lthms) Symtab.table
|
|
335 |
};
|
|
336 |
|
|
337 |
fun mk_spec ((funcs, dconstrs), dtyps) =
|
|
338 |
Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps };
|
|
339 |
fun map_spec f (Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps }) =
|
|
340 |
mk_spec (f ((funcs, dconstrs), dtyps));
|
|
341 |
fun merge_spec (Spec { funcs = funcs1, dconstrs = dconstrs1, dtyps = dtyps1 },
|
|
342 |
Spec { funcs = funcs2, dconstrs = dconstrs2, dtyps = dtyps2 }) =
|
|
343 |
let
|
|
344 |
val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
|
|
345 |
val dconstrs = Consttab.merge (K true) (dconstrs1, dconstrs2);
|
|
346 |
val (touched', dtyps) = merge_dtyps (dtyps1, dtyps2);
|
|
347 |
val touched = if touched' then NONE else touched_cs;
|
|
348 |
in (touched, mk_spec ((funcs, dconstrs), dtyps)) end;
|
|
349 |
|
|
350 |
datatype exec = Exec of {
|
|
351 |
preproc: preproc,
|
|
352 |
spec: spec
|
|
353 |
};
|
|
354 |
|
|
355 |
fun mk_exec (preproc, spec) =
|
|
356 |
Exec { preproc = preproc, spec = spec };
|
|
357 |
fun map_exec f (Exec { preproc = preproc, spec = spec }) =
|
|
358 |
mk_exec (f (preproc, spec));
|
|
359 |
fun merge_exec (Exec { preproc = preproc1, spec = spec1 },
|
|
360 |
Exec { preproc = preproc2, spec = spec2 }) =
|
|
361 |
let
|
|
362 |
val (touched', preproc) = merge_preproc (preproc1, preproc2);
|
|
363 |
val (touched_cs, spec) = merge_spec (spec1, spec2);
|
|
364 |
val touched = if touched' then NONE else touched_cs;
|
|
365 |
in (touched, mk_exec (preproc, spec)) end;
|
20844
|
366 |
val empty_exec = mk_exec (mk_preproc (([], []), ([], [])),
|
20600
|
367 |
mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty));
|
|
368 |
|
|
369 |
fun the_preproc (Exec { preproc = Preproc x, ...}) = x;
|
|
370 |
fun the_spec (Exec { spec = Spec x, ...}) = x;
|
|
371 |
val the_funcs = #funcs o the_spec;
|
|
372 |
val the_dcontrs = #dconstrs o the_spec;
|
|
373 |
val the_dtyps = #dtyps o the_spec;
|
|
374 |
val map_preproc = map_exec o apfst o map_preproc;
|
|
375 |
val map_funcs = map_exec o apsnd o map_spec o apfst o apfst;
|
|
376 |
val map_dconstrs = map_exec o apsnd o map_spec o apfst o apsnd;
|
|
377 |
val map_dtyps = map_exec o apsnd o map_spec o apsnd;
|
|
378 |
|
|
379 |
|
|
380 |
(** code data structures **)
|
|
381 |
|
|
382 |
(*private copy avoids potential conflict of table exceptions*)
|
|
383 |
structure Datatab = TableFun(type key = int val ord = int_ord);
|
|
384 |
|
|
385 |
|
|
386 |
(* data slots *)
|
|
387 |
|
|
388 |
local
|
|
389 |
|
|
390 |
type kind = {
|
|
391 |
name: string,
|
|
392 |
empty: Object.T,
|
|
393 |
merge: Pretty.pp -> Object.T * Object.T -> Object.T,
|
|
394 |
purge: CodegenConsts.const list option -> Object.T -> Object.T
|
|
395 |
};
|
|
396 |
|
|
397 |
val kinds = ref (Datatab.empty: kind Datatab.table);
|
|
398 |
|
|
399 |
fun invoke meth_name meth_fn k =
|
|
400 |
(case Datatab.lookup (! kinds) k of
|
|
401 |
SOME kind => meth_fn kind |> transform_failure (fn exn =>
|
|
402 |
EXCEPTION (exn, "Code data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
|
|
403 |
| NONE => sys_error ("Invalid code data identifier " ^ string_of_int k));
|
|
404 |
|
|
405 |
|
|
406 |
in
|
|
407 |
|
|
408 |
fun invoke_name k = invoke "name" (K o #name) k ();
|
|
409 |
fun invoke_empty k = invoke "empty" (K o #empty) k ();
|
|
410 |
fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
|
|
411 |
fun invoke_purge cs = invoke "purge" (fn kind => #purge kind cs);
|
|
412 |
|
|
413 |
fun declare name empty merge purge =
|
|
414 |
let
|
|
415 |
val k = serial ();
|
|
416 |
val kind = {name = name, empty = empty, merge = merge, purge = purge};
|
|
417 |
val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
|
|
418 |
warning ("Duplicate declaration of code data " ^ quote name));
|
|
419 |
val _ = change kinds (Datatab.update (k, kind));
|
|
420 |
in k end;
|
|
421 |
|
|
422 |
end; (*local*)
|
|
423 |
|
|
424 |
|
|
425 |
(* theory store *)
|
|
426 |
|
|
427 |
type data = Object.T Datatab.table;
|
|
428 |
|
|
429 |
structure CodeData = TheoryDataFun
|
|
430 |
(struct
|
|
431 |
val name = "Pure/codegen_data";
|
|
432 |
type T = exec * data ref;
|
|
433 |
val empty = (empty_exec, ref Datatab.empty : data ref);
|
|
434 |
fun copy (exec, data) = (exec, ref (! data));
|
|
435 |
val extend = copy;
|
|
436 |
fun merge pp ((exec1, data1), (exec2, data2)) =
|
|
437 |
let
|
|
438 |
val (touched, exec) = merge_exec (exec1, exec2);
|
|
439 |
val data1' = Datatab.map' (invoke_purge touched) (! data1);
|
|
440 |
val data2' = Datatab.map' (invoke_purge touched) (! data2);
|
|
441 |
val data = Datatab.join (invoke_merge pp) (data1', data2');
|
|
442 |
in (exec, ref data) end;
|
|
443 |
fun print thy (exec, _) =
|
|
444 |
let
|
|
445 |
val ctxt = ProofContext.init thy;
|
|
446 |
fun pretty_func (s, lthms) =
|
|
447 |
(Pretty.block o Pretty.fbreaks) (
|
|
448 |
Pretty.str s :: pretty_sdthms ctxt lthms
|
|
449 |
);
|
|
450 |
fun pretty_dtyp (s, cos) =
|
|
451 |
(Pretty.block o Pretty.breaks) (
|
|
452 |
Pretty.str s
|
|
453 |
:: Pretty.str "="
|
|
454 |
:: Pretty.separate "|" (map (fn (c, []) => Pretty.str c
|
|
455 |
| (c, tys) =>
|
|
456 |
Pretty.block
|
|
457 |
(Pretty.str c :: Pretty.brk 1 :: Pretty.str "of" :: Pretty.brk 1
|
|
458 |
:: Pretty.breaks (map (Pretty.quote o Sign.pretty_typ thy) tys))) cos)
|
|
459 |
)
|
|
460 |
val inlines = (#inlines o the_preproc) exec;
|
|
461 |
val funs = the_funcs exec
|
|
462 |
|> Consttab.dest
|
|
463 |
|> (map o apfst) (CodegenConsts.string_of_const thy)
|
|
464 |
|> sort (string_ord o pairself fst);
|
|
465 |
val dtyps = the_dtyps exec
|
|
466 |
|> Symtab.dest
|
|
467 |
|> map (fn (dtco, ((vs, cos), _)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
|
|
468 |
|> sort (string_ord o pairself fst)
|
|
469 |
in
|
|
470 |
(Pretty.writeln o Pretty.block o Pretty.fbreaks) ([
|
|
471 |
Pretty.str "code theorems:",
|
|
472 |
Pretty.str "function theorems:" ] @
|
|
473 |
map pretty_func funs @ [
|
|
474 |
Pretty.block (
|
|
475 |
Pretty.str "inlined theorems:"
|
|
476 |
:: Pretty.fbrk
|
|
477 |
:: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
|
|
478 |
),
|
|
479 |
Pretty.block (
|
|
480 |
Pretty.str "datatypes:"
|
|
481 |
:: Pretty.fbrk
|
|
482 |
:: (Pretty.fbreaks o map pretty_dtyp) dtyps
|
|
483 |
)]
|
|
484 |
)
|
|
485 |
end;
|
|
486 |
end);
|
|
487 |
|
|
488 |
fun print_thms thy = CodeData.print thy;
|
|
489 |
|
|
490 |
fun init k = CodeData.map
|
|
491 |
(fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
|
|
492 |
|
|
493 |
fun get k dest data =
|
|
494 |
(case Datatab.lookup data k of
|
|
495 |
SOME x => (dest x handle Match =>
|
|
496 |
error ("Failed to access code data " ^ quote (invoke_name k)))
|
|
497 |
| NONE => error ("Uninitialized code data " ^ quote (invoke_name k)));
|
|
498 |
|
|
499 |
fun put k mk x = Datatab.update (k, mk x);
|
|
500 |
|
|
501 |
fun map_exec_purge touched f =
|
|
502 |
CodeData.map (fn (exec, data) =>
|
|
503 |
(f exec, ref (Datatab.map' (invoke_purge touched) (! data))));
|
|
504 |
|
|
505 |
val get_exec = fst o CodeData.get;
|
|
506 |
|
|
507 |
val _ = Context.add_setup CodeData.init;
|
|
508 |
|
|
509 |
|
|
510 |
|
|
511 |
(** theorem transformation and certification **)
|
|
512 |
|
|
513 |
fun rewrite_func rewrites thm =
|
|
514 |
let
|
20844
|
515 |
val rewrite = Tactic.rewrite false rewrites;
|
|
516 |
val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
|
|
517 |
val Const ("==", _) = Thm.term_of ct_eq;
|
20600
|
518 |
val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
|
|
519 |
val rhs' = rewrite ct_rhs;
|
|
520 |
val args' = map rewrite ct_args;
|
|
521 |
val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1)
|
|
522 |
args' (Thm.reflexive ct_f));
|
|
523 |
in
|
|
524 |
Thm.transitive (Thm.transitive lhs' thm) rhs'
|
|
525 |
end handle Bind => raise ERROR "rewrite_func"
|
|
526 |
|
|
527 |
fun common_typ_funcs thy [] = []
|
|
528 |
| common_typ_funcs thy [thm] = [thm]
|
|
529 |
| common_typ_funcs thy thms =
|
|
530 |
let
|
|
531 |
fun incr_thm thm max =
|
|
532 |
let
|
|
533 |
val thm' = incr_indexes max thm;
|
|
534 |
val max' = (maxidx_of_typ o fastype_of o Drule.plain_prop_of) thm' + 1;
|
|
535 |
in (thm', max') end;
|
|
536 |
val (thms', maxidx) = fold_map incr_thm thms 0;
|
|
537 |
val (ty1::tys) = map (typ_func thy) thms;
|
|
538 |
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
|
|
539 |
handle Type.TUNIFY =>
|
|
540 |
error ("Type unificaton failed, while unifying function equations\n"
|
|
541 |
^ (cat_lines o map Display.string_of_thm) thms
|
|
542 |
^ "\nwith types\n"
|
|
543 |
^ (cat_lines o map (Sign.string_of_typ thy)) (ty1 :: tys));
|
|
544 |
val (env, _) = fold unify tys (Vartab.empty, maxidx)
|
|
545 |
val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
|
|
546 |
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
|
|
547 |
in map (Thm.instantiate (instT, [])) thms end;
|
|
548 |
|
20844
|
549 |
fun certify_const thy c c_thms =
|
20600
|
550 |
let
|
|
551 |
fun cert (c', thm) = if CodegenConsts.eq_const (c, c')
|
|
552 |
then thm else bad_thm ("Wrong head of function equation,\nexpected constant "
|
|
553 |
^ CodegenConsts.string_of_const thy c) thm
|
20844
|
554 |
in map cert c_thms end;
|
20600
|
555 |
|
|
556 |
fun mk_cos tyco vs cos =
|
|
557 |
let
|
|
558 |
val dty = Type (tyco, map TFree vs);
|
|
559 |
fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys);
|
|
560 |
in map mk_co cos end;
|
|
561 |
|
|
562 |
fun mk_co_args (co, tys) ctxt =
|
|
563 |
let
|
|
564 |
val names = Name.invents ctxt "a" (length tys);
|
|
565 |
val ctxt' = fold Name.declare names ctxt;
|
|
566 |
val vs = map2 (fn v => fn ty => Free (fst (v, 0), I ty)) names tys;
|
|
567 |
in (vs, ctxt') end;
|
|
568 |
|
|
569 |
fun check_freeness thy cos thms =
|
|
570 |
let
|
|
571 |
val props = AList.make Drule.plain_prop_of thms;
|
|
572 |
fun sym_product [] = []
|
|
573 |
| sym_product (x::xs) = map (pair x) xs @ sym_product xs;
|
|
574 |
val quodlibet =
|
|
575 |
let
|
|
576 |
val judg = ObjectLogic.fixed_judgment (the_context ()) "x";
|
|
577 |
val [free] = fold_aterms (fn v as Free _ => cons v | _ => I) judg [];
|
|
578 |
val judg' = Term.subst_free [(free, Bound 0)] judg;
|
|
579 |
val prop = Type ("prop", []);
|
|
580 |
val prop' = fastype_of judg';
|
|
581 |
in
|
|
582 |
Const ("all", (prop' --> prop) --> prop) $ Abs ("P", prop', judg')
|
|
583 |
end;
|
|
584 |
fun check_inj (co, []) =
|
|
585 |
NONE
|
|
586 |
| check_inj (co, tys) =
|
|
587 |
let
|
|
588 |
val ((xs, ys), _) = Name.context
|
|
589 |
|> mk_co_args (co, tys)
|
|
590 |
||>> mk_co_args (co, tys);
|
|
591 |
val prem = Logic.mk_equals
|
|
592 |
(list_comb (co, xs), list_comb (co, ys));
|
|
593 |
val concl = Logic.mk_conjunction_list
|
|
594 |
(map2 (curry Logic.mk_equals) xs ys);
|
|
595 |
val t = Logic.mk_implies (prem, concl);
|
|
596 |
in case find_first (curry Term.could_unify t o snd) props
|
|
597 |
of SOME (thm, _) => SOME thm
|
|
598 |
| NONE => error ("Could not prove injectiveness statement\n"
|
|
599 |
^ Sign.string_of_term thy t
|
|
600 |
^ "\nfor constructor "
|
|
601 |
^ CodegenConsts.string_of_const_typ thy (dest_Const co)
|
|
602 |
^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
|
|
603 |
end;
|
|
604 |
fun check_dist ((co1, tys1), (co2, tys2)) =
|
|
605 |
let
|
|
606 |
val ((xs1, xs2), _) = Name.context
|
|
607 |
|> mk_co_args (co1, tys1)
|
|
608 |
||>> mk_co_args (co2, tys2);
|
|
609 |
val prem = Logic.mk_equals
|
|
610 |
(list_comb (co1, xs1), list_comb (co2, xs2));
|
|
611 |
val t = Logic.mk_implies (prem, quodlibet);
|
|
612 |
in case find_first (curry Term.could_unify t o snd) props
|
|
613 |
of SOME (thm, _) => thm
|
|
614 |
| NONE => error ("Could not prove distinctness statement\n"
|
|
615 |
^ Sign.string_of_term thy t
|
|
616 |
^ "\nfor constructors "
|
|
617 |
^ CodegenConsts.string_of_const_typ thy (dest_Const co1)
|
|
618 |
^ " and "
|
|
619 |
^ CodegenConsts.string_of_const_typ thy (dest_Const co2)
|
|
620 |
^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
|
|
621 |
end;
|
|
622 |
in (map_filter check_inj cos, map check_dist (sym_product cos)) end;
|
|
623 |
|
|
624 |
fun certify_datatype thy dtco cs thms =
|
|
625 |
(op @) (check_freeness thy cs thms);
|
|
626 |
|
|
627 |
|
|
628 |
|
|
629 |
(** interfaces **)
|
|
630 |
|
|
631 |
fun add_func thm thy =
|
|
632 |
let
|
|
633 |
val thms = mk_func thy thm;
|
|
634 |
val cs = map fst thms;
|
|
635 |
in
|
|
636 |
map_exec_purge (SOME cs) (map_funcs
|
|
637 |
(fold (fn (c, thm) => Consttab.map_default
|
|
638 |
(c, (Susp.value [], [])) (add_thm thm)) thms)) thy
|
|
639 |
end;
|
|
640 |
|
|
641 |
fun del_func thm thy =
|
|
642 |
let
|
|
643 |
val thms = mk_func thy thm;
|
|
644 |
val cs = map fst thms;
|
|
645 |
in
|
|
646 |
map_exec_purge (SOME cs) (map_funcs
|
|
647 |
(fold (fn (c, thm) => Consttab.map_entry c
|
|
648 |
(del_thm thm)) thms)) thy
|
|
649 |
end;
|
|
650 |
|
|
651 |
fun add_funcl (c, lthms) thy =
|
|
652 |
let
|
|
653 |
val c' = CodegenConsts.norm thy c;
|
20844
|
654 |
val lthms' = certificate thy (fn thy => certify_const thy c' o maps (mk_func thy)) lthms;
|
20600
|
655 |
in
|
|
656 |
map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
|
|
657 |
(add_lthms lthms'))) thy
|
|
658 |
end;
|
|
659 |
|
|
660 |
fun add_datatype (tyco, (vs_cos as (vs, cos), lthms)) thy =
|
|
661 |
let
|
|
662 |
val cs = mk_cos tyco vs cos;
|
|
663 |
val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
|
|
664 |
val add =
|
|
665 |
map_dtyps (Symtab.update_new (tyco,
|
20844
|
666 |
(vs_cos, certificate thy (fn thy => certify_datatype thy tyco cs) lthms)))
|
20600
|
667 |
#> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
|
|
668 |
in map_exec_purge (SOME consts) add thy end;
|
|
669 |
|
|
670 |
fun del_datatype tyco thy =
|
|
671 |
let
|
20639
|
672 |
val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco;
|
|
673 |
val cs = mk_cos tyco vs cos;
|
|
674 |
val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
|
20600
|
675 |
val del =
|
|
676 |
map_dtyps (Symtab.delete tyco)
|
20639
|
677 |
#> map_dconstrs (fold Consttab.delete consts)
|
|
678 |
in map_exec_purge (SOME consts) del thy end;
|
20600
|
679 |
|
|
680 |
fun add_inline thm thy =
|
20844
|
681 |
(map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert eq_thm) (mk_rew thy thm)) thy;
|
20600
|
682 |
|
|
683 |
fun del_inline thm thy =
|
20844
|
684 |
(map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove eq_thm) (mk_rew thy thm)) thy ;
|
|
685 |
|
|
686 |
fun add_inline_proc f =
|
|
687 |
(map_exec_purge NONE o map_preproc o apfst o apsnd) (cons (serial (), f));
|
|
688 |
|
|
689 |
fun add_constrains f =
|
|
690 |
(map_exec_purge NONE o map_preproc o apsnd o apfst) (cons (serial (), f));
|
20600
|
691 |
|
|
692 |
fun add_preproc f =
|
20844
|
693 |
(map_exec_purge NONE o map_preproc o apsnd o apsnd) (cons (serial (), f));
|
|
694 |
|
|
695 |
local
|
|
696 |
|
|
697 |
fun gen_apply_constrain prep post const_typ thy fs x =
|
|
698 |
let
|
|
699 |
val ts = prep x;
|
|
700 |
val tvars = (fold o fold_aterms) Term.add_tvars ts [];
|
|
701 |
val consts = (fold o fold_aterms) (fn Const c => cons c | _ => I) ts [];
|
|
702 |
fun insts_of const_typ (c, ty) =
|
|
703 |
let
|
|
704 |
val ty_decl = const_typ (c, ty);
|
|
705 |
val env = Vartab.dest (Type.raw_match (ty_decl, ty) Vartab.empty);
|
|
706 |
val insts = map_filter
|
|
707 |
(fn (v, (sort, TVar (_, sort'))) =>
|
|
708 |
if Sorts.sort_le (Sign.classes_of thy) (sort, sort')
|
|
709 |
then NONE else SOME (v, sort)
|
|
710 |
| _ => NONE) env
|
|
711 |
in
|
|
712 |
insts
|
|
713 |
end
|
|
714 |
val const_insts = case const_typ
|
|
715 |
of NONE => []
|
|
716 |
| SOME const_typ => maps (insts_of const_typ) consts;
|
|
717 |
fun add_inst (v, sort') =
|
|
718 |
let
|
|
719 |
val sort = (the o AList.lookup (op =) tvars) v
|
|
720 |
in
|
|
721 |
AList.map_default (op =) (v, (sort, sort))
|
|
722 |
(apsnd (fn sort => Sorts.inter_sort (Sign.classes_of thy) (sort, sort')))
|
|
723 |
end;
|
|
724 |
val inst =
|
|
725 |
[]
|
|
726 |
|> fold (fn f => fold add_inst (f thy ts)) fs
|
|
727 |
|> fold add_inst const_insts;
|
|
728 |
in
|
|
729 |
post thy inst x
|
|
730 |
end;
|
20600
|
731 |
|
20844
|
732 |
val apply_constrain = gen_apply_constrain (maps
|
|
733 |
((fn (args, rhs) => rhs :: (snd o strip_comb) args) o Logic.dest_equals o Thm.prop_of))
|
|
734 |
(fn thy => fn inst => map (check_typ_classop thy o Thm.instantiate (map (fn (v, (sort, sort')) =>
|
|
735 |
(Thm.ctyp_of thy (TVar (v, sort)), Thm.ctyp_of thy (TVar (v, sort')))
|
|
736 |
) inst, []))) NONE;
|
|
737 |
fun apply_constrain_cterm thy const_typ = gen_apply_constrain (single o Thm.term_of)
|
|
738 |
(fn thy => fn inst => pair inst o Thm.cterm_of thy o map_types
|
|
739 |
(TermSubst.instantiateT (map (fn (v, (sort, sort')) => ((v, sort), TVar (v, sort'))) inst)) o Thm.term_of) (SOME const_typ) thy;
|
|
740 |
|
|
741 |
fun gen_apply_inline_proc prep post thy f x =
|
|
742 |
let
|
|
743 |
val cts = prep x;
|
|
744 |
val rews = map (check_rew thy) (f thy cts);
|
|
745 |
in post rews x end;
|
|
746 |
|
|
747 |
val apply_inline_proc = gen_apply_inline_proc (maps
|
|
748 |
((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of))
|
|
749 |
(fn rews => map (rewrite_func rews));
|
|
750 |
val apply_inline_proc_cterm = gen_apply_inline_proc single
|
|
751 |
(Tactic.rewrite false);
|
20600
|
752 |
|
20844
|
753 |
fun apply_preproc thy f [] = []
|
|
754 |
| apply_preproc thy f (thms as (thm :: _)) =
|
|
755 |
let
|
|
756 |
val thms' = f thy thms;
|
|
757 |
val c = (CodegenConsts.norm_of_typ thy o fst o dest_func thy) thm;
|
|
758 |
in (certify_const thy c o map (mk_head thy)) thms' end;
|
|
759 |
|
|
760 |
fun cmp_thms thy =
|
|
761 |
make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (typ_func thy thm1, typ_func thy thm2)));
|
|
762 |
|
|
763 |
fun rhs_conv conv thm =
|
|
764 |
let
|
|
765 |
val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm;
|
|
766 |
in Thm.transitive thm thm' end
|
|
767 |
|
|
768 |
fun drop_classes thy inst thm =
|
|
769 |
let
|
|
770 |
val unconstr = map (fn (v, (_, sort')) =>
|
|
771 |
(Thm.ctyp_of thy o TVar) (v, sort')) inst;
|
|
772 |
val instmap = map (fn (v, (sort, _)) =>
|
|
773 |
pairself (Thm.ctyp_of thy o TVar) ((v, []), (v, sort))) inst;
|
|
774 |
in
|
|
775 |
thm
|
|
776 |
|> fold Thm.unconstrainT unconstr
|
|
777 |
|> Thm.instantiate (instmap, [])
|
|
778 |
|> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy))
|
|
779 |
end;
|
|
780 |
|
|
781 |
in
|
20600
|
782 |
|
|
783 |
fun preprocess thy thms =
|
20844
|
784 |
thms
|
|
785 |
|> fold (fn (_, f) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy)
|
|
786 |
|> map (rewrite_func ((#inlines o the_preproc o get_exec) thy))
|
|
787 |
|> apply_constrain thy ((map snd o #constrains o the_preproc o get_exec) thy)
|
|
788 |
|> map (rewrite_func ((#inlines o the_preproc o get_exec) thy))
|
|
789 |
|> fold (fn (_, f) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
|
|
790 |
|> map (snd o check_func false thy)
|
|
791 |
|> sort (cmp_thms thy)
|
|
792 |
|> common_typ_funcs thy;
|
20600
|
793 |
|
20844
|
794 |
fun preprocess_cterm thy const_typ ct =
|
|
795 |
ct
|
|
796 |
|> apply_constrain_cterm thy const_typ ((map snd o #constrains o the_preproc o get_exec) thy)
|
|
797 |
|-> (fn inst =>
|
|
798 |
Thm.reflexive
|
|
799 |
#> fold (rhs_conv o Tactic.rewrite false o single) ((#inlines o the_preproc o get_exec) thy)
|
|
800 |
#> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f)) ((#inline_procs o the_preproc o get_exec) thy)
|
|
801 |
#> (fn thm => (drop_classes thy inst thm, ((fn xs => nth xs 1) o snd o Drule.strip_comb o Thm.cprop_of) thm))
|
|
802 |
);
|
|
803 |
|
|
804 |
end; (*local*)
|
20600
|
805 |
|
|
806 |
fun these_funcs thy c =
|
|
807 |
let
|
20844
|
808 |
val funcs_1 =
|
20600
|
809 |
Consttab.lookup ((the_funcs o get_exec) thy) c
|
|
810 |
|> Option.map (Susp.force o fst)
|
|
811 |
|> these
|
|
812 |
|> map (Thm.transfer thy);
|
20844
|
813 |
val funcs_2 = case funcs_1
|
|
814 |
of [] => get_prim_def_funcs thy c
|
|
815 |
| xs => xs;
|
20600
|
816 |
fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
|
|
817 |
o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
|
|
818 |
in
|
20844
|
819 |
funcs_2
|
20600
|
820 |
|> preprocess thy
|
|
821 |
|> drop_refl thy
|
|
822 |
end;
|
|
823 |
|
|
824 |
fun get_datatype thy tyco =
|
|
825 |
Symtab.lookup ((the_dtyps o get_exec) thy) tyco
|
|
826 |
|> Option.map (fn (spec, thms) => (Susp.force thms; spec));
|
|
827 |
|
|
828 |
fun get_datatype_of_constr thy c =
|
|
829 |
Consttab.lookup ((the_dcontrs o get_exec) thy) c
|
|
830 |
|> (Option.map o tap) (fn dtco => get_datatype thy dtco);
|
|
831 |
|
|
832 |
|
|
833 |
|
|
834 |
(** code attributes **)
|
|
835 |
|
|
836 |
local
|
|
837 |
fun add_simple_attribute (name, f) =
|
|
838 |
(Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
|
|
839 |
(Context.map_theory o f);
|
|
840 |
in
|
|
841 |
val _ = map (Context.add_setup o add_simple_attribute) [
|
|
842 |
("func", add_func),
|
|
843 |
("nofunc", del_func),
|
|
844 |
("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
|
|
845 |
("inline", add_inline),
|
|
846 |
("noinline", del_inline)
|
|
847 |
]
|
|
848 |
end; (*local*)
|
|
849 |
|
|
850 |
end; (*struct*)
|
|
851 |
|
|
852 |
|
|
853 |
|
|
854 |
(** type-safe interfaces for data depedent on executable content **)
|
|
855 |
|
|
856 |
signature CODE_DATA_ARGS =
|
|
857 |
sig
|
|
858 |
val name: string
|
|
859 |
type T
|
|
860 |
val empty: T
|
|
861 |
val merge: Pretty.pp -> T * T -> T
|
|
862 |
val purge: CodegenConsts.const list option -> T -> T
|
|
863 |
end;
|
|
864 |
|
|
865 |
signature CODE_DATA =
|
|
866 |
sig
|
|
867 |
type T
|
|
868 |
val init: theory -> theory
|
|
869 |
val get: theory -> T
|
|
870 |
val change: theory -> (T -> T) -> T
|
|
871 |
val change_yield: theory -> (T -> 'a * T) -> 'a * T
|
|
872 |
end;
|
|
873 |
|
|
874 |
functor CodeDataFun(Data: CODE_DATA_ARGS): CODE_DATA =
|
|
875 |
struct
|
|
876 |
|
|
877 |
type T = Data.T;
|
|
878 |
exception Data of T;
|
|
879 |
fun dest (Data x) = x
|
|
880 |
|
|
881 |
val kind = CodegenData.declare Data.name (Data Data.empty)
|
|
882 |
(fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
|
|
883 |
(fn cs => fn Data x => Data (Data.purge cs x));
|
|
884 |
|
|
885 |
val init = CodegenData.init kind;
|
|
886 |
fun get thy = CodegenData.get kind dest ((! o snd o CodegenData.CodeData.get) thy);
|
|
887 |
fun change thy f =
|
|
888 |
let
|
|
889 |
val data_ref = (snd o CodegenData.CodeData.get) thy;
|
|
890 |
val x = (f o CodegenData.get kind dest o !) data_ref;
|
|
891 |
val data = CodegenData.put kind Data x (! data_ref);
|
|
892 |
in (data_ref := data; x) end;
|
|
893 |
fun change_yield thy f =
|
|
894 |
let
|
|
895 |
val data_ref = (snd o CodegenData.CodeData.get) thy;
|
|
896 |
val (y, x) = (f o CodegenData.get kind dest o !) data_ref;
|
|
897 |
val data = CodegenData.put kind Data x (! data_ref);
|
|
898 |
in (data_ref := data; (y, x)) end;
|
|
899 |
|
|
900 |
end;
|
|
901 |
|
|
902 |
structure CodegenData : CODEGEN_DATA =
|
|
903 |
struct
|
|
904 |
|
|
905 |
open CodegenData;
|
|
906 |
|
|
907 |
end;
|