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 |
(* val _ = PolyML.Compiler.maxInlineSize := 0; *)
|
|
9 |
|
|
10 |
signature CODEGEN_DATA =
|
|
11 |
sig
|
|
12 |
type lthms = thm list Susp.T;
|
|
13 |
val lazy: (unit -> thm list) -> lthms
|
|
14 |
val eval_always: bool ref
|
|
15 |
|
|
16 |
val add_func: thm -> theory -> theory
|
|
17 |
val del_func: thm -> theory -> theory
|
|
18 |
val add_funcl: CodegenConsts.const * lthms -> theory -> theory
|
|
19 |
val add_datatype: string * (((string * sort) list * (string * typ list) list) * lthms)
|
|
20 |
-> theory -> theory
|
|
21 |
val del_datatype: string -> theory -> theory
|
|
22 |
val add_inline: thm -> theory -> theory
|
|
23 |
val del_inline: thm -> theory -> theory
|
|
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
|
|
34 |
val preprocess_cterm: theory -> cterm -> thm
|
|
35 |
val preprocess: theory -> thm list -> thm list
|
|
36 |
|
|
37 |
val debug: bool ref
|
|
38 |
val strict_functyp: bool ref
|
|
39 |
end;
|
|
40 |
|
|
41 |
signature PRIVATE_CODEGEN_DATA =
|
|
42 |
sig
|
|
43 |
include CODEGEN_DATA
|
|
44 |
type data
|
|
45 |
structure CodeData: THEORY_DATA
|
|
46 |
val declare: string -> Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T)
|
|
47 |
-> (CodegenConsts.const list option -> Object.T -> Object.T) -> serial
|
|
48 |
val init: serial -> theory -> theory
|
|
49 |
val get: serial -> (Object.T -> 'a) -> data -> 'a
|
|
50 |
val put: serial -> ('a -> Object.T) -> 'a -> data -> data
|
|
51 |
end;
|
|
52 |
|
|
53 |
structure CodegenData : PRIVATE_CODEGEN_DATA =
|
|
54 |
struct
|
|
55 |
|
|
56 |
(** diagnostics **)
|
|
57 |
|
|
58 |
val debug = ref false;
|
|
59 |
fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x);
|
|
60 |
|
|
61 |
|
|
62 |
|
|
63 |
(** lazy theorems, certificate theorems **)
|
|
64 |
|
|
65 |
type lthms = thm list Susp.T;
|
|
66 |
val eval_always = ref false;
|
|
67 |
val _ = eval_always := true;
|
|
68 |
|
|
69 |
fun lazy f = if !eval_always
|
|
70 |
then Susp.value (f ())
|
|
71 |
else Susp.delay f;
|
|
72 |
|
|
73 |
fun string_of_lthms r = case Susp.peek r
|
|
74 |
of SOME thms => (map string_of_thm o rev) thms
|
|
75 |
| NONE => ["[...]"];
|
|
76 |
|
|
77 |
fun pretty_lthms ctxt r = case Susp.peek r
|
|
78 |
of SOME thms => (map (ProofContext.pretty_thm ctxt) o rev) thms
|
|
79 |
| NONE => [Pretty.str "[...]"];
|
|
80 |
|
|
81 |
fun certificate f r =
|
|
82 |
case Susp.peek r
|
|
83 |
of SOME thms => (Susp.value o f) thms
|
|
84 |
| NONE => lazy (fn () => (f o Susp.force) r);
|
|
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 |
|
|
110 |
(* making function theorems *)
|
|
111 |
|
|
112 |
fun bad_thm msg thm =
|
|
113 |
error (msg ^ ": " ^ string_of_thm thm);
|
|
114 |
|
|
115 |
fun typ_func thy = snd o dest_Const o fst o strip_comb o fst
|
|
116 |
o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of;
|
|
117 |
|
|
118 |
val mk_rew =
|
|
119 |
#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of;
|
|
120 |
|
|
121 |
val strict_functyp = ref true;
|
|
122 |
|
|
123 |
fun mk_func thy raw_thm =
|
|
124 |
let
|
|
125 |
fun dest_func thy = dest_Const o fst o strip_comb o Envir.beta_eta_contract
|
|
126 |
o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of;
|
|
127 |
fun mk_head thm = case try (dest_func thy) thm
|
|
128 |
of SOME (c_ty as (c, ty)) =>
|
|
129 |
let
|
|
130 |
val is_classop = (is_some o AxClass.class_of_param thy) c;
|
|
131 |
val const = CodegenConsts.norm_of_typ thy c_ty;
|
20704
|
132 |
val ty_decl = CodegenConsts.disc_typ_of_const thy
|
|
133 |
(snd o CodegenConsts.typ_of_inst thy) const;
|
20600
|
134 |
val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
|
|
135 |
in if Sign.typ_equiv thy (ty_decl, ty)
|
|
136 |
then (const, thm)
|
|
137 |
else ((if is_classop orelse !strict_functyp then error else warning)
|
|
138 |
("Type\n" ^ string_of_typ ty
|
|
139 |
^ "\nof function theorem\n"
|
|
140 |
^ string_of_thm thm
|
|
141 |
^ "\nis strictly less general than declared function type\n"
|
|
142 |
^ string_of_typ ty_decl); (const, thm))
|
|
143 |
end
|
|
144 |
| NONE => bad_thm "Not a function equation" thm;
|
|
145 |
in
|
|
146 |
mk_rew thy raw_thm
|
|
147 |
|> map mk_head
|
|
148 |
end;
|
|
149 |
|
|
150 |
fun get_prim_def_funcs thy c =
|
|
151 |
let
|
|
152 |
fun constrain thm0 thm = case AxClass.class_of_param thy (fst c)
|
|
153 |
of SOME _ =>
|
|
154 |
let
|
20704
|
155 |
val ty_decl = CodegenConsts.disc_typ_of_classop thy c;
|
20600
|
156 |
val max = maxidx_of_typ ty_decl + 1;
|
|
157 |
val thm = Thm.incr_indexes max thm;
|
|
158 |
val ty = typ_func thy thm;
|
|
159 |
val (env, _) = Sign.typ_unify thy (ty_decl, ty) (Vartab.empty, max);
|
|
160 |
val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
|
|
161 |
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
|
|
162 |
in Thm.instantiate (instT, []) thm end
|
|
163 |
| NONE => thm
|
|
164 |
in case CodegenConsts.find_def thy c
|
|
165 |
of SOME ((_, thm), _) =>
|
|
166 |
thm
|
|
167 |
|> Thm.transfer thy
|
|
168 |
|> try (map snd o mk_func thy)
|
|
169 |
|> these
|
|
170 |
|> map (constrain thm)
|
|
171 |
| NONE => []
|
|
172 |
end;
|
|
173 |
|
|
174 |
|
|
175 |
(* pairs of (selected, deleted) function theorems *)
|
|
176 |
|
|
177 |
type sdthms = lthms * thm list;
|
|
178 |
|
|
179 |
fun add_drop_redundant thm thms =
|
|
180 |
let
|
20608
|
181 |
(* val _ = writeln "add_drop 01"; *)
|
20600
|
182 |
val thy = Context.check_thy (Thm.theory_of_thm thm);
|
20608
|
183 |
(* val _ = writeln "add_drop 02"; *)
|
20600
|
184 |
val pattern = (fst o Logic.dest_equals o Drule.plain_prop_of) thm;
|
|
185 |
fun matches thm' = if (curry (Pattern.matches thy) pattern o
|
|
186 |
fst o Logic.dest_equals o Drule.plain_prop_of) thm'
|
|
187 |
then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); true)
|
|
188 |
else false
|
|
189 |
in thm :: filter_out matches thms end;
|
|
190 |
|
|
191 |
fun add_thm thm (sels, dels) =
|
|
192 |
(Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels);
|
|
193 |
|
|
194 |
fun add_lthms lthms (sels, []) =
|
|
195 |
(lazy (fn () => fold add_drop_redundant
|
|
196 |
(Susp.force lthms) (Susp.force sels)), [])
|
|
197 |
| add_lthms lthms (sels, dels) =
|
|
198 |
fold add_thm (Susp.force lthms) (sels, dels);
|
|
199 |
|
|
200 |
fun del_thm thm (sels, dels) =
|
|
201 |
(Susp.value (remove eq_thm thm (Susp.force sels)), thm :: dels);
|
|
202 |
|
|
203 |
fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
|
|
204 |
|
|
205 |
fun merge_sdthms c ((sels1, dels1), (sels2, dels2)) =
|
|
206 |
let
|
|
207 |
val (dels_t, dels) = merge_thms (dels1, dels2);
|
|
208 |
in if dels_t
|
|
209 |
then let
|
|
210 |
val (_, sels) = merge_thms (Susp.force sels1, subtract eq_thm dels1 (Susp.force sels2))
|
|
211 |
val (_, dels) = merge_thms (dels1, subtract eq_thm (Susp.force sels1) dels2)
|
|
212 |
in (true, ((lazy o K) sels, dels)) end
|
|
213 |
else let
|
|
214 |
val (sels_t, sels) = merge_lthms (sels1, sels2)
|
|
215 |
in (sels_t, (sels, dels)) end
|
|
216 |
end;
|
|
217 |
|
|
218 |
|
|
219 |
(** data structures **)
|
|
220 |
|
|
221 |
structure Consttab = CodegenConsts.Consttab;
|
|
222 |
|
|
223 |
datatype preproc = Preproc of {
|
|
224 |
inlines: thm list,
|
|
225 |
preprocs: (serial * (theory -> thm list -> thm list)) list
|
|
226 |
};
|
|
227 |
|
|
228 |
fun mk_preproc (inlines, preprocs) =
|
|
229 |
Preproc { inlines = inlines, preprocs = preprocs };
|
|
230 |
fun map_preproc f (Preproc { inlines, preprocs }) =
|
|
231 |
mk_preproc (f (inlines, preprocs));
|
|
232 |
fun merge_preproc (Preproc { inlines = inlines1, preprocs = preprocs1 },
|
|
233 |
Preproc { inlines = inlines2, preprocs = preprocs2 }) =
|
|
234 |
let
|
|
235 |
val (touched1, inlines) = merge_thms (inlines1, inlines2);
|
|
236 |
val (touched2, preprocs) = merge_alist (op =) (K true) (preprocs1, preprocs2);
|
|
237 |
in (touched1 orelse touched2, mk_preproc (inlines, preprocs)) end;
|
|
238 |
|
|
239 |
fun join_func_thms (tabs as (tab1, tab2)) =
|
|
240 |
let
|
|
241 |
val cs1 = Consttab.keys tab1;
|
|
242 |
val cs2 = Consttab.keys tab2;
|
|
243 |
val cs' = filter (member CodegenConsts.eq_const cs2) cs1;
|
|
244 |
val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2;
|
|
245 |
val cs''' = ref [] : CodegenConsts.const list ref;
|
|
246 |
fun merge c x = let val (touched, thms') = merge_sdthms c x in
|
|
247 |
(if touched then cs''' := cons c (!cs''') else (); thms') end;
|
|
248 |
in (cs'' @ !cs''', Consttab.join merge tabs) end;
|
|
249 |
fun merge_funcs (thms1, thms2) =
|
|
250 |
let
|
|
251 |
val (consts, thms) = join_func_thms (thms1, thms2);
|
|
252 |
in (SOME consts, thms) end;
|
|
253 |
|
|
254 |
val eq_string = op = : string * string -> bool;
|
|
255 |
fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) =
|
|
256 |
gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
|
|
257 |
andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2);
|
|
258 |
fun merge_dtyps (tabs as (tab1, tab2)) =
|
|
259 |
let
|
|
260 |
(*EXTEND: could be more clever with respect to constructors*)
|
|
261 |
val tycos1 = Symtab.keys tab1;
|
|
262 |
val tycos2 = Symtab.keys tab2;
|
|
263 |
val tycos' = filter (member eq_string tycos2) tycos1;
|
|
264 |
val touched = gen_eq_set (eq_pair (op =) (eq_dtyp))
|
|
265 |
(AList.make (the o Symtab.lookup tab1) tycos',
|
|
266 |
AList.make (the o Symtab.lookup tab2) tycos');
|
|
267 |
in (touched, Symtab.merge (K true) tabs) end;
|
|
268 |
|
|
269 |
datatype spec = Spec of {
|
|
270 |
funcs: sdthms Consttab.table,
|
|
271 |
dconstrs: string Consttab.table,
|
|
272 |
dtyps: (((string * sort) list * (string * typ list) list) * lthms) Symtab.table
|
|
273 |
};
|
|
274 |
|
|
275 |
fun mk_spec ((funcs, dconstrs), dtyps) =
|
|
276 |
Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps };
|
|
277 |
fun map_spec f (Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps }) =
|
|
278 |
mk_spec (f ((funcs, dconstrs), dtyps));
|
|
279 |
fun merge_spec (Spec { funcs = funcs1, dconstrs = dconstrs1, dtyps = dtyps1 },
|
|
280 |
Spec { funcs = funcs2, dconstrs = dconstrs2, dtyps = dtyps2 }) =
|
|
281 |
let
|
|
282 |
val (touched_cs, funcs) = merge_funcs (funcs1, funcs2);
|
|
283 |
val dconstrs = Consttab.merge (K true) (dconstrs1, dconstrs2);
|
|
284 |
val (touched', dtyps) = merge_dtyps (dtyps1, dtyps2);
|
|
285 |
val touched = if touched' then NONE else touched_cs;
|
|
286 |
in (touched, mk_spec ((funcs, dconstrs), dtyps)) end;
|
|
287 |
|
|
288 |
datatype exec = Exec of {
|
|
289 |
preproc: preproc,
|
|
290 |
spec: spec
|
|
291 |
};
|
|
292 |
|
|
293 |
fun mk_exec (preproc, spec) =
|
|
294 |
Exec { preproc = preproc, spec = spec };
|
|
295 |
fun map_exec f (Exec { preproc = preproc, spec = spec }) =
|
|
296 |
mk_exec (f (preproc, spec));
|
|
297 |
fun merge_exec (Exec { preproc = preproc1, spec = spec1 },
|
|
298 |
Exec { preproc = preproc2, spec = spec2 }) =
|
|
299 |
let
|
|
300 |
val (touched', preproc) = merge_preproc (preproc1, preproc2);
|
|
301 |
val (touched_cs, spec) = merge_spec (spec1, spec2);
|
|
302 |
val touched = if touched' then NONE else touched_cs;
|
|
303 |
in (touched, mk_exec (preproc, spec)) end;
|
|
304 |
val empty_exec = mk_exec (mk_preproc ([], []),
|
|
305 |
mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty));
|
|
306 |
|
|
307 |
fun the_preproc (Exec { preproc = Preproc x, ...}) = x;
|
|
308 |
fun the_spec (Exec { spec = Spec x, ...}) = x;
|
|
309 |
val the_funcs = #funcs o the_spec;
|
|
310 |
val the_dcontrs = #dconstrs o the_spec;
|
|
311 |
val the_dtyps = #dtyps o the_spec;
|
|
312 |
val map_preproc = map_exec o apfst o map_preproc;
|
|
313 |
val map_funcs = map_exec o apsnd o map_spec o apfst o apfst;
|
|
314 |
val map_dconstrs = map_exec o apsnd o map_spec o apfst o apsnd;
|
|
315 |
val map_dtyps = map_exec o apsnd o map_spec o apsnd;
|
|
316 |
|
|
317 |
|
|
318 |
(** code data structures **)
|
|
319 |
|
|
320 |
(*private copy avoids potential conflict of table exceptions*)
|
|
321 |
structure Datatab = TableFun(type key = int val ord = int_ord);
|
|
322 |
|
|
323 |
|
|
324 |
(* data slots *)
|
|
325 |
|
|
326 |
local
|
|
327 |
|
|
328 |
type kind = {
|
|
329 |
name: string,
|
|
330 |
empty: Object.T,
|
|
331 |
merge: Pretty.pp -> Object.T * Object.T -> Object.T,
|
|
332 |
purge: CodegenConsts.const list option -> Object.T -> Object.T
|
|
333 |
};
|
|
334 |
|
|
335 |
val kinds = ref (Datatab.empty: kind Datatab.table);
|
|
336 |
|
|
337 |
fun invoke meth_name meth_fn k =
|
|
338 |
(case Datatab.lookup (! kinds) k of
|
|
339 |
SOME kind => meth_fn kind |> transform_failure (fn exn =>
|
|
340 |
EXCEPTION (exn, "Code data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
|
|
341 |
| NONE => sys_error ("Invalid code data identifier " ^ string_of_int k));
|
|
342 |
|
|
343 |
|
|
344 |
in
|
|
345 |
|
|
346 |
fun invoke_name k = invoke "name" (K o #name) k ();
|
|
347 |
fun invoke_empty k = invoke "empty" (K o #empty) k ();
|
|
348 |
fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
|
|
349 |
fun invoke_purge cs = invoke "purge" (fn kind => #purge kind cs);
|
|
350 |
|
|
351 |
fun declare name empty merge purge =
|
|
352 |
let
|
|
353 |
val k = serial ();
|
|
354 |
val kind = {name = name, empty = empty, merge = merge, purge = purge};
|
|
355 |
val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () =>
|
|
356 |
warning ("Duplicate declaration of code data " ^ quote name));
|
|
357 |
val _ = change kinds (Datatab.update (k, kind));
|
|
358 |
in k end;
|
|
359 |
|
|
360 |
end; (*local*)
|
|
361 |
|
|
362 |
|
|
363 |
(* theory store *)
|
|
364 |
|
|
365 |
type data = Object.T Datatab.table;
|
|
366 |
|
|
367 |
structure CodeData = TheoryDataFun
|
|
368 |
(struct
|
|
369 |
val name = "Pure/codegen_data";
|
|
370 |
type T = exec * data ref;
|
|
371 |
val empty = (empty_exec, ref Datatab.empty : data ref);
|
|
372 |
fun copy (exec, data) = (exec, ref (! data));
|
|
373 |
val extend = copy;
|
|
374 |
fun merge pp ((exec1, data1), (exec2, data2)) =
|
|
375 |
let
|
|
376 |
val (touched, exec) = merge_exec (exec1, exec2);
|
|
377 |
val data1' = Datatab.map' (invoke_purge touched) (! data1);
|
|
378 |
val data2' = Datatab.map' (invoke_purge touched) (! data2);
|
|
379 |
val data = Datatab.join (invoke_merge pp) (data1', data2');
|
|
380 |
in (exec, ref data) end;
|
|
381 |
fun print thy (exec, _) =
|
|
382 |
let
|
|
383 |
val ctxt = ProofContext.init thy;
|
|
384 |
fun pretty_func (s, lthms) =
|
|
385 |
(Pretty.block o Pretty.fbreaks) (
|
|
386 |
Pretty.str s :: pretty_sdthms ctxt lthms
|
|
387 |
);
|
|
388 |
fun pretty_dtyp (s, cos) =
|
|
389 |
(Pretty.block o Pretty.breaks) (
|
|
390 |
Pretty.str s
|
|
391 |
:: Pretty.str "="
|
|
392 |
:: Pretty.separate "|" (map (fn (c, []) => Pretty.str c
|
|
393 |
| (c, tys) =>
|
|
394 |
Pretty.block
|
|
395 |
(Pretty.str c :: Pretty.brk 1 :: Pretty.str "of" :: Pretty.brk 1
|
|
396 |
:: Pretty.breaks (map (Pretty.quote o Sign.pretty_typ thy) tys))) cos)
|
|
397 |
)
|
|
398 |
val inlines = (#inlines o the_preproc) exec;
|
|
399 |
val funs = the_funcs exec
|
|
400 |
|> Consttab.dest
|
|
401 |
|> (map o apfst) (CodegenConsts.string_of_const thy)
|
|
402 |
|> sort (string_ord o pairself fst);
|
|
403 |
val dtyps = the_dtyps exec
|
|
404 |
|> Symtab.dest
|
|
405 |
|> map (fn (dtco, ((vs, cos), _)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
|
|
406 |
|> sort (string_ord o pairself fst)
|
|
407 |
in
|
|
408 |
(Pretty.writeln o Pretty.block o Pretty.fbreaks) ([
|
|
409 |
Pretty.str "code theorems:",
|
|
410 |
Pretty.str "function theorems:" ] @
|
|
411 |
map pretty_func funs @ [
|
|
412 |
Pretty.block (
|
|
413 |
Pretty.str "inlined theorems:"
|
|
414 |
:: Pretty.fbrk
|
|
415 |
:: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines
|
|
416 |
),
|
|
417 |
Pretty.block (
|
|
418 |
Pretty.str "datatypes:"
|
|
419 |
:: Pretty.fbrk
|
|
420 |
:: (Pretty.fbreaks o map pretty_dtyp) dtyps
|
|
421 |
)]
|
|
422 |
)
|
|
423 |
end;
|
|
424 |
end);
|
|
425 |
|
|
426 |
fun print_thms thy = CodeData.print thy;
|
|
427 |
|
|
428 |
fun init k = CodeData.map
|
|
429 |
(fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
|
|
430 |
|
|
431 |
fun get k dest data =
|
|
432 |
(case Datatab.lookup data k of
|
|
433 |
SOME x => (dest x handle Match =>
|
|
434 |
error ("Failed to access code data " ^ quote (invoke_name k)))
|
|
435 |
| NONE => error ("Uninitialized code data " ^ quote (invoke_name k)));
|
|
436 |
|
|
437 |
fun put k mk x = Datatab.update (k, mk x);
|
|
438 |
|
|
439 |
fun map_exec_purge touched f =
|
|
440 |
CodeData.map (fn (exec, data) =>
|
|
441 |
(f exec, ref (Datatab.map' (invoke_purge touched) (! data))));
|
|
442 |
|
|
443 |
val get_exec = fst o CodeData.get;
|
|
444 |
|
|
445 |
val _ = Context.add_setup CodeData.init;
|
|
446 |
|
|
447 |
|
|
448 |
|
|
449 |
(** theorem transformation and certification **)
|
|
450 |
|
|
451 |
fun rewrite_func rewrites thm =
|
|
452 |
let
|
|
453 |
val rewrite = Tactic.rewrite true rewrites;
|
|
454 |
val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o cprop_of) thm;
|
|
455 |
val Const ("==", _) = term_of ct_eq;
|
|
456 |
val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
|
|
457 |
val rhs' = rewrite ct_rhs;
|
|
458 |
val args' = map rewrite ct_args;
|
|
459 |
val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1)
|
|
460 |
args' (Thm.reflexive ct_f));
|
|
461 |
in
|
|
462 |
Thm.transitive (Thm.transitive lhs' thm) rhs'
|
|
463 |
end handle Bind => raise ERROR "rewrite_func"
|
|
464 |
|
|
465 |
fun common_typ_funcs thy [] = []
|
|
466 |
| common_typ_funcs thy [thm] = [thm]
|
|
467 |
| common_typ_funcs thy thms =
|
|
468 |
let
|
|
469 |
fun incr_thm thm max =
|
|
470 |
let
|
|
471 |
val thm' = incr_indexes max thm;
|
|
472 |
val max' = (maxidx_of_typ o fastype_of o Drule.plain_prop_of) thm' + 1;
|
|
473 |
in (thm', max') end;
|
|
474 |
val (thms', maxidx) = fold_map incr_thm thms 0;
|
|
475 |
val (ty1::tys) = map (typ_func thy) thms;
|
|
476 |
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
|
|
477 |
handle Type.TUNIFY =>
|
|
478 |
error ("Type unificaton failed, while unifying function equations\n"
|
|
479 |
^ (cat_lines o map Display.string_of_thm) thms
|
|
480 |
^ "\nwith types\n"
|
|
481 |
^ (cat_lines o map (Sign.string_of_typ thy)) (ty1 :: tys));
|
|
482 |
val (env, _) = fold unify tys (Vartab.empty, maxidx)
|
|
483 |
val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
|
|
484 |
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
|
|
485 |
in map (Thm.instantiate (instT, [])) thms end;
|
|
486 |
|
|
487 |
fun certify_const thy c thms =
|
|
488 |
let
|
|
489 |
fun cert (c', thm) = if CodegenConsts.eq_const (c, c')
|
|
490 |
then thm else bad_thm ("Wrong head of function equation,\nexpected constant "
|
|
491 |
^ CodegenConsts.string_of_const thy c) thm
|
|
492 |
in (map cert o maps (mk_func thy)) thms end;
|
|
493 |
|
|
494 |
fun mk_cos tyco vs cos =
|
|
495 |
let
|
|
496 |
val dty = Type (tyco, map TFree vs);
|
|
497 |
fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys);
|
|
498 |
in map mk_co cos end;
|
|
499 |
|
|
500 |
fun mk_co_args (co, tys) ctxt =
|
|
501 |
let
|
|
502 |
val names = Name.invents ctxt "a" (length tys);
|
|
503 |
val ctxt' = fold Name.declare names ctxt;
|
|
504 |
val vs = map2 (fn v => fn ty => Free (fst (v, 0), I ty)) names tys;
|
|
505 |
in (vs, ctxt') end;
|
|
506 |
|
|
507 |
fun check_freeness thy cos thms =
|
|
508 |
let
|
|
509 |
val props = AList.make Drule.plain_prop_of thms;
|
|
510 |
fun sym_product [] = []
|
|
511 |
| sym_product (x::xs) = map (pair x) xs @ sym_product xs;
|
|
512 |
val quodlibet =
|
|
513 |
let
|
|
514 |
val judg = ObjectLogic.fixed_judgment (the_context ()) "x";
|
|
515 |
val [free] = fold_aterms (fn v as Free _ => cons v | _ => I) judg [];
|
|
516 |
val judg' = Term.subst_free [(free, Bound 0)] judg;
|
|
517 |
val prop = Type ("prop", []);
|
|
518 |
val prop' = fastype_of judg';
|
|
519 |
in
|
|
520 |
Const ("all", (prop' --> prop) --> prop) $ Abs ("P", prop', judg')
|
|
521 |
end;
|
|
522 |
fun check_inj (co, []) =
|
|
523 |
NONE
|
|
524 |
| check_inj (co, tys) =
|
|
525 |
let
|
|
526 |
val ((xs, ys), _) = Name.context
|
|
527 |
|> mk_co_args (co, tys)
|
|
528 |
||>> mk_co_args (co, tys);
|
|
529 |
val prem = Logic.mk_equals
|
|
530 |
(list_comb (co, xs), list_comb (co, ys));
|
|
531 |
val concl = Logic.mk_conjunction_list
|
|
532 |
(map2 (curry Logic.mk_equals) xs ys);
|
|
533 |
val t = Logic.mk_implies (prem, concl);
|
|
534 |
in case find_first (curry Term.could_unify t o snd) props
|
|
535 |
of SOME (thm, _) => SOME thm
|
|
536 |
| NONE => error ("Could not prove injectiveness statement\n"
|
|
537 |
^ Sign.string_of_term thy t
|
|
538 |
^ "\nfor constructor "
|
|
539 |
^ CodegenConsts.string_of_const_typ thy (dest_Const co)
|
|
540 |
^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
|
|
541 |
end;
|
|
542 |
fun check_dist ((co1, tys1), (co2, tys2)) =
|
|
543 |
let
|
|
544 |
val ((xs1, xs2), _) = Name.context
|
|
545 |
|> mk_co_args (co1, tys1)
|
|
546 |
||>> mk_co_args (co2, tys2);
|
|
547 |
val prem = Logic.mk_equals
|
|
548 |
(list_comb (co1, xs1), list_comb (co2, xs2));
|
|
549 |
val t = Logic.mk_implies (prem, quodlibet);
|
|
550 |
in case find_first (curry Term.could_unify t o snd) props
|
|
551 |
of SOME (thm, _) => thm
|
|
552 |
| NONE => error ("Could not prove distinctness statement\n"
|
|
553 |
^ Sign.string_of_term thy t
|
|
554 |
^ "\nfor constructors "
|
|
555 |
^ CodegenConsts.string_of_const_typ thy (dest_Const co1)
|
|
556 |
^ " and "
|
|
557 |
^ CodegenConsts.string_of_const_typ thy (dest_Const co2)
|
|
558 |
^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
|
|
559 |
end;
|
|
560 |
in (map_filter check_inj cos, map check_dist (sym_product cos)) end;
|
|
561 |
|
|
562 |
fun certify_datatype thy dtco cs thms =
|
|
563 |
(op @) (check_freeness thy cs thms);
|
|
564 |
|
|
565 |
|
|
566 |
|
|
567 |
(** interfaces **)
|
|
568 |
|
|
569 |
fun add_func thm thy =
|
|
570 |
let
|
|
571 |
val thms = mk_func thy thm;
|
|
572 |
val cs = map fst thms;
|
|
573 |
in
|
|
574 |
map_exec_purge (SOME cs) (map_funcs
|
|
575 |
(fold (fn (c, thm) => Consttab.map_default
|
|
576 |
(c, (Susp.value [], [])) (add_thm thm)) thms)) thy
|
|
577 |
end;
|
|
578 |
|
|
579 |
fun del_func thm thy =
|
|
580 |
let
|
|
581 |
val thms = mk_func thy thm;
|
|
582 |
val cs = map fst thms;
|
|
583 |
in
|
|
584 |
map_exec_purge (SOME cs) (map_funcs
|
|
585 |
(fold (fn (c, thm) => Consttab.map_entry c
|
|
586 |
(del_thm thm)) thms)) thy
|
|
587 |
end;
|
|
588 |
|
|
589 |
fun add_funcl (c, lthms) thy =
|
|
590 |
let
|
|
591 |
val c' = CodegenConsts.norm thy c;
|
|
592 |
val lthms' = certificate (certify_const thy c') lthms;
|
|
593 |
in
|
|
594 |
map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], []))
|
|
595 |
(add_lthms lthms'))) thy
|
|
596 |
end;
|
|
597 |
|
|
598 |
fun add_datatype (tyco, (vs_cos as (vs, cos), lthms)) thy =
|
|
599 |
let
|
|
600 |
val cs = mk_cos tyco vs cos;
|
|
601 |
val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
|
|
602 |
val add =
|
|
603 |
map_dtyps (Symtab.update_new (tyco,
|
|
604 |
(vs_cos, certificate (certify_datatype thy tyco cs) lthms)))
|
|
605 |
#> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
|
|
606 |
in map_exec_purge (SOME consts) add thy end;
|
|
607 |
|
|
608 |
fun del_datatype tyco thy =
|
|
609 |
let
|
20639
|
610 |
val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco;
|
|
611 |
val cs = mk_cos tyco vs cos;
|
|
612 |
val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
|
20600
|
613 |
val del =
|
|
614 |
map_dtyps (Symtab.delete tyco)
|
20639
|
615 |
#> map_dconstrs (fold Consttab.delete consts)
|
|
616 |
in map_exec_purge (SOME consts) del thy end;
|
20600
|
617 |
|
|
618 |
fun add_inline thm thy =
|
|
619 |
map_exec_purge NONE (map_preproc (apfst (fold (insert eq_thm) (mk_rew thy thm)))) thy;
|
|
620 |
|
|
621 |
fun del_inline thm thy =
|
|
622 |
map_exec_purge NONE (map_preproc (apfst (fold (remove eq_thm) (mk_rew thy thm)))) thy ;
|
|
623 |
|
|
624 |
fun add_preproc f =
|
|
625 |
map_exec_purge NONE (map_preproc (apsnd (cons (serial (), f))));
|
|
626 |
|
|
627 |
fun getf_first [] _ = NONE
|
|
628 |
| getf_first (f::fs) x = case f x
|
|
629 |
of NONE => getf_first fs x
|
|
630 |
| y as SOME x => y;
|
|
631 |
|
|
632 |
fun getf_first_list [] x = []
|
|
633 |
| getf_first_list (f::fs) x = case f x
|
|
634 |
of [] => getf_first_list fs x
|
|
635 |
| xs => xs;
|
|
636 |
|
|
637 |
fun preprocess thy thms =
|
|
638 |
let
|
|
639 |
fun cmp_thms (thm1, thm2) =
|
|
640 |
not (Sign.typ_instance thy (typ_func thy thm1, typ_func thy thm2));
|
|
641 |
in
|
|
642 |
thms
|
|
643 |
|> map (rewrite_func ((#inlines o the_preproc o get_exec) thy))
|
|
644 |
|> fold (fn (_, f) => f thy) ((#preprocs o the_preproc o get_exec) thy)
|
|
645 |
|> map (rewrite_func ((#inlines o the_preproc o get_exec) thy))
|
|
646 |
|> sort (make_ord cmp_thms)
|
|
647 |
|> common_typ_funcs thy
|
|
648 |
end;
|
|
649 |
|
|
650 |
fun preprocess_cterm thy =
|
|
651 |
Tactic.rewrite false ((#inlines o the_preproc o get_exec) thy);
|
|
652 |
|
|
653 |
fun these_funcs thy c =
|
|
654 |
let
|
|
655 |
fun test_funcs c =
|
|
656 |
Consttab.lookup ((the_funcs o get_exec) thy) c
|
|
657 |
|> Option.map (Susp.force o fst)
|
|
658 |
|> these
|
|
659 |
|> map (Thm.transfer thy);
|
|
660 |
val test_defs = get_prim_def_funcs thy;
|
|
661 |
fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
|
|
662 |
o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
|
|
663 |
in
|
|
664 |
getf_first_list [test_funcs, test_defs] c
|
|
665 |
|> preprocess thy
|
|
666 |
|> drop_refl thy
|
|
667 |
end;
|
|
668 |
|
|
669 |
fun get_datatype thy tyco =
|
|
670 |
Symtab.lookup ((the_dtyps o get_exec) thy) tyco
|
|
671 |
|> Option.map (fn (spec, thms) => (Susp.force thms; spec));
|
|
672 |
|
|
673 |
fun get_datatype_of_constr thy c =
|
|
674 |
Consttab.lookup ((the_dcontrs o get_exec) thy) c
|
|
675 |
|> (Option.map o tap) (fn dtco => get_datatype thy dtco);
|
|
676 |
|
|
677 |
|
|
678 |
|
|
679 |
(** code attributes **)
|
|
680 |
|
|
681 |
local
|
|
682 |
fun add_simple_attribute (name, f) =
|
|
683 |
(Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
|
|
684 |
(Context.map_theory o f);
|
|
685 |
in
|
|
686 |
val _ = map (Context.add_setup o add_simple_attribute) [
|
|
687 |
("func", add_func),
|
|
688 |
("nofunc", del_func),
|
|
689 |
("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
|
|
690 |
("inline", add_inline),
|
|
691 |
("noinline", del_inline)
|
|
692 |
]
|
|
693 |
end; (*local*)
|
|
694 |
|
|
695 |
end; (*struct*)
|
|
696 |
|
|
697 |
|
|
698 |
|
|
699 |
(** type-safe interfaces for data depedent on executable content **)
|
|
700 |
|
|
701 |
signature CODE_DATA_ARGS =
|
|
702 |
sig
|
|
703 |
val name: string
|
|
704 |
type T
|
|
705 |
val empty: T
|
|
706 |
val merge: Pretty.pp -> T * T -> T
|
|
707 |
val purge: CodegenConsts.const list option -> T -> T
|
|
708 |
end;
|
|
709 |
|
|
710 |
signature CODE_DATA =
|
|
711 |
sig
|
|
712 |
type T
|
|
713 |
val init: theory -> theory
|
|
714 |
val get: theory -> T
|
|
715 |
val change: theory -> (T -> T) -> T
|
|
716 |
val change_yield: theory -> (T -> 'a * T) -> 'a * T
|
|
717 |
end;
|
|
718 |
|
|
719 |
functor CodeDataFun(Data: CODE_DATA_ARGS): CODE_DATA =
|
|
720 |
struct
|
|
721 |
|
|
722 |
type T = Data.T;
|
|
723 |
exception Data of T;
|
|
724 |
fun dest (Data x) = x
|
|
725 |
|
|
726 |
val kind = CodegenData.declare Data.name (Data Data.empty)
|
|
727 |
(fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)))
|
|
728 |
(fn cs => fn Data x => Data (Data.purge cs x));
|
|
729 |
|
|
730 |
val init = CodegenData.init kind;
|
|
731 |
fun get thy = CodegenData.get kind dest ((! o snd o CodegenData.CodeData.get) thy);
|
|
732 |
fun change thy f =
|
|
733 |
let
|
|
734 |
val data_ref = (snd o CodegenData.CodeData.get) thy;
|
|
735 |
val x = (f o CodegenData.get kind dest o !) data_ref;
|
|
736 |
val data = CodegenData.put kind Data x (! data_ref);
|
|
737 |
in (data_ref := data; x) end;
|
|
738 |
fun change_yield thy f =
|
|
739 |
let
|
|
740 |
val data_ref = (snd o CodegenData.CodeData.get) thy;
|
|
741 |
val (y, x) = (f o CodegenData.get kind dest o !) data_ref;
|
|
742 |
val data = CodegenData.put kind Data x (! data_ref);
|
|
743 |
in (data_ref := data; (y, x)) end;
|
|
744 |
|
|
745 |
end;
|
|
746 |
|
|
747 |
structure CodegenData : CODEGEN_DATA =
|
|
748 |
struct
|
|
749 |
|
|
750 |
open CodegenData;
|
|
751 |
|
|
752 |
end;
|