20600
|
1 |
(* Title: Pure/Tools/codegen_funcgr.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
20855
|
5 |
Retrieving, normalizing and structuring code function theorems
|
|
6 |
in graph with explicit dependencies.
|
20600
|
7 |
*)
|
|
8 |
|
|
9 |
signature CODEGEN_FUNCGR =
|
|
10 |
sig
|
|
11 |
type T;
|
21120
|
12 |
val make: theory -> CodegenConsts.const list -> T
|
21129
|
13 |
val make_term: theory -> ((thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
|
21120
|
14 |
val funcs: T -> CodegenConsts.const -> thm list
|
|
15 |
val typ: T -> CodegenConsts.const -> typ
|
|
16 |
val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
|
|
17 |
val all: T -> CodegenConsts.const list
|
|
18 |
val norm_vars: theory -> thm list -> thm list
|
20600
|
19 |
val print_codethms: theory -> CodegenConsts.const list -> unit
|
20938
|
20 |
structure Constgraph : GRAPH
|
20600
|
21 |
end;
|
|
22 |
|
|
23 |
structure CodegenFuncgr: CODEGEN_FUNCGR =
|
|
24 |
struct
|
|
25 |
|
|
26 |
(** code data **)
|
|
27 |
|
|
28 |
structure Consttab = CodegenConsts.Consttab;
|
|
29 |
structure Constgraph = GraphFun (
|
|
30 |
type key = CodegenConsts.const;
|
|
31 |
val ord = CodegenConsts.const_ord;
|
|
32 |
);
|
|
33 |
|
|
34 |
type T = (typ * thm list) Constgraph.T;
|
|
35 |
|
|
36 |
structure Funcgr = CodeDataFun
|
|
37 |
(struct
|
|
38 |
val name = "Pure/codegen_funcgr";
|
|
39 |
type T = T;
|
|
40 |
val empty = Constgraph.empty;
|
|
41 |
fun merge _ _ = Constgraph.empty;
|
20938
|
42 |
fun purge _ NONE _ = Constgraph.empty
|
|
43 |
| purge _ (SOME cs) funcgr =
|
|
44 |
Constgraph.del_nodes ((Constgraph.all_succs funcgr
|
|
45 |
o filter (can (Constgraph.get_node funcgr))) cs) funcgr;
|
20600
|
46 |
end);
|
|
47 |
|
|
48 |
val _ = Context.add_setup Funcgr.init;
|
|
49 |
|
|
50 |
|
|
51 |
(** theorem purification **)
|
|
52 |
|
|
53 |
fun abs_norm thy thm =
|
|
54 |
let
|
20705
|
55 |
fun eta_expand thm =
|
20600
|
56 |
let
|
20705
|
57 |
val lhs = (fst o Logic.dest_equals o Drule.plain_prop_of) thm;
|
20600
|
58 |
val tys = (fst o strip_type o fastype_of) lhs;
|
20896
|
59 |
val ctxt = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
|
20705
|
60 |
val vs_ct = map (fn (v, ty) => cterm_of thy (Var ((v, 0), ty)))
|
20896
|
61 |
(Name.names ctxt "a" tys);
|
20600
|
62 |
in
|
20705
|
63 |
fold (fn ct => fn thm => Thm.combination thm (Thm.reflexive ct)) vs_ct thm
|
20600
|
64 |
end;
|
|
65 |
in
|
|
66 |
thm
|
20705
|
67 |
|> eta_expand
|
21120
|
68 |
|> Drule.fconv_rule Drule.beta_eta_conversion
|
20600
|
69 |
end;
|
|
70 |
|
21120
|
71 |
|
20600
|
72 |
fun canonical_tvars thy thm =
|
|
73 |
let
|
21159
|
74 |
fun tvars_subst_for thm = (fold_types o fold_atyps)
|
|
75 |
(fn TVar (v_i as (v, _), sort) => let
|
|
76 |
val v' = CodegenNames.purify_var v
|
|
77 |
in if v = v' then I
|
|
78 |
else insert (op =) (v_i, (v', sort)) end
|
20600
|
79 |
| _ => I) (prop_of thm) [];
|
21159
|
80 |
fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
|
|
81 |
let
|
|
82 |
val ty = TVar (v_i, sort)
|
|
83 |
in
|
|
84 |
(maxidx + 1, (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
|
|
85 |
end;
|
20600
|
86 |
val maxidx = Thm.maxidx_of thm + 1;
|
21159
|
87 |
val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
|
20600
|
88 |
in Thm.instantiate (inst, []) thm end;
|
|
89 |
|
|
90 |
fun canonical_vars thy thm =
|
|
91 |
let
|
21159
|
92 |
fun vars_subst_for thm = fold_aterms
|
|
93 |
(fn Var (v_i as (v, _), ty) => let
|
|
94 |
val v' = CodegenNames.purify_var v
|
|
95 |
in if v = v' then I
|
|
96 |
else insert (op =) (v_i, (v', ty)) end
|
20600
|
97 |
| _ => I) (prop_of thm) [];
|
21159
|
98 |
fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
|
|
99 |
let
|
|
100 |
val t = Var (v_i, ty)
|
|
101 |
in
|
|
102 |
(maxidx + 1, (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
|
|
103 |
end;
|
20600
|
104 |
val maxidx = Thm.maxidx_of thm + 1;
|
21159
|
105 |
val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
|
20600
|
106 |
in Thm.instantiate ([], inst) thm end;
|
|
107 |
|
21120
|
108 |
fun norm_vars thy thms =
|
20600
|
109 |
let
|
|
110 |
fun burrow_thms f [] = []
|
|
111 |
| burrow_thms f thms =
|
|
112 |
thms
|
|
113 |
|> Conjunction.intr_list
|
|
114 |
|> f
|
|
115 |
|> Conjunction.elim_list;
|
|
116 |
in
|
|
117 |
thms
|
|
118 |
|> map (abs_norm thy)
|
21159
|
119 |
|> burrow_thms (canonical_tvars thy)
|
|
120 |
|> map (canonical_vars thy)
|
|
121 |
|> map Drule.zero_var_indexes
|
20600
|
122 |
end;
|
|
123 |
|
|
124 |
|
|
125 |
|
|
126 |
(** retrieval **)
|
|
127 |
|
21120
|
128 |
fun funcs funcgr =
|
|
129 |
these o Option.map snd o try (Constgraph.get_node funcgr);
|
20600
|
130 |
|
21120
|
131 |
fun typ funcgr =
|
|
132 |
fst o Constgraph.get_node funcgr;
|
20600
|
133 |
|
21120
|
134 |
fun deps funcgr cs =
|
20835
|
135 |
let
|
|
136 |
val conn = Constgraph.strong_conn funcgr;
|
|
137 |
val order = rev conn;
|
|
138 |
in
|
|
139 |
(map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
|
|
140 |
|> filter_out null
|
|
141 |
end;
|
|
142 |
|
21120
|
143 |
fun all funcgr = Constgraph.keys funcgr;
|
|
144 |
|
20600
|
145 |
local
|
|
146 |
|
|
147 |
fun add_things_of thy f (c, thms) =
|
|
148 |
(fold o fold_aterms)
|
|
149 |
(fn Const c_ty => let
|
|
150 |
val c' = CodegenConsts.norm_of_typ thy c_ty
|
21120
|
151 |
in if is_some c andalso CodegenConsts.eq_const (the c, c') then I
|
20600
|
152 |
else f (c', c_ty) end
|
|
153 |
| _ => I) (maps (op :: o swap o apfst (snd o strip_comb)
|
|
154 |
o Logic.dest_equals o Drule.plain_prop_of) thms)
|
|
155 |
|
|
156 |
fun rhs_of thy (c, thms) =
|
|
157 |
Consttab.empty
|
21120
|
158 |
|> add_things_of thy (Consttab.update o rpair () o fst) (SOME c, thms)
|
20600
|
159 |
|> Consttab.keys;
|
|
160 |
|
|
161 |
fun insts_of thy funcgr (c, ty) =
|
|
162 |
let
|
|
163 |
val tys = Sign.const_typargs thy (c, ty);
|
|
164 |
val c' = CodegenConsts.norm thy (c, tys);
|
20705
|
165 |
val ty_decl = CodegenConsts.disc_typ_of_const thy
|
|
166 |
(fst o Constgraph.get_node funcgr o CodegenConsts.norm thy) (c, tys);
|
20600
|
167 |
val tys_decl = Sign.const_typargs thy (c, ty_decl);
|
|
168 |
fun constructor tyco xs class =
|
|
169 |
(tyco, class) :: maps (maps fst) xs;
|
|
170 |
fun variable (TVar (_, sort)) = map (pair []) sort
|
|
171 |
| variable (TFree (_, sort)) = map (pair []) sort;
|
|
172 |
fun mk_inst ty (TVar (_, sort)) = cons (ty, sort)
|
|
173 |
| mk_inst ty (TFree (_, sort)) = cons (ty, sort)
|
|
174 |
| mk_inst (Type (tyco1, tys1)) (Type (tyco2, tys2)) =
|
|
175 |
if tyco1 <> tyco2 then error "bad instance"
|
|
176 |
else fold2 mk_inst tys1 tys2;
|
21120
|
177 |
val pp = Sign.pp thy;
|
|
178 |
val algebra = Sign.classes_of thy;
|
|
179 |
fun classrel (x, _) _ = x;
|
|
180 |
fun of_sort_deriv (ty, sort) =
|
|
181 |
Sorts.of_sort_derivation pp algebra
|
|
182 |
{ classrel = classrel, constructor = constructor, variable = variable }
|
|
183 |
(ty, sort)
|
20600
|
184 |
in
|
21120
|
185 |
flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
|
20600
|
186 |
end;
|
|
187 |
|
|
188 |
fun all_classops thy tyco class =
|
21120
|
189 |
AxClass.params_of thy class
|
|
190 |
(* |> tap (fn _ => writeln ("INST " ^ tyco ^ " - " ^ class)) *)
|
20705
|
191 |
|> AList.make (fn c => CodegenConsts.disc_typ_of_classop thy (c, [Type (tyco, [])]))
|
20600
|
192 |
(*typ_of_classop is very liberal in its type arguments*)
|
|
193 |
|> map (CodegenConsts.norm_of_typ thy);
|
|
194 |
|
|
195 |
fun instdefs_of thy insts =
|
|
196 |
let
|
|
197 |
val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
|
|
198 |
in
|
|
199 |
Symtab.empty
|
|
200 |
|> fold (fn (tyco, class) =>
|
|
201 |
Symtab.map_default (tyco, []) (insert (op =) class)) insts
|
|
202 |
|> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops thy tyco)
|
|
203 |
(Graph.all_succs thy_classes classes))) tab [])
|
|
204 |
end;
|
|
205 |
|
21120
|
206 |
fun insts_of_thms thy funcgr (c, thms) =
|
20600
|
207 |
let
|
|
208 |
val insts = add_things_of thy (fn (_, c_ty) => fold (insert (op =))
|
21120
|
209 |
(insts_of thy funcgr c_ty)) (SOME c, thms) [];
|
20600
|
210 |
in instdefs_of thy insts end;
|
|
211 |
|
|
212 |
fun ensure_const thy funcgr c auxgr =
|
|
213 |
if can (Constgraph.get_node funcgr) c
|
|
214 |
then (NONE, auxgr)
|
|
215 |
else if can (Constgraph.get_node auxgr) c
|
|
216 |
then (SOME c, auxgr)
|
|
217 |
else if is_some (CodegenData.get_datatype_of_constr thy c) then
|
|
218 |
auxgr
|
|
219 |
|> Constgraph.new_node (c, [])
|
|
220 |
|> pair (SOME c)
|
|
221 |
else let
|
21120
|
222 |
val thms = norm_vars thy (CodegenData.these_funcs thy c);
|
20600
|
223 |
val rhs = rhs_of thy (c, thms);
|
|
224 |
in
|
|
225 |
auxgr
|
|
226 |
|> Constgraph.new_node (c, thms)
|
|
227 |
|> fold_map (ensure_const thy funcgr) rhs
|
|
228 |
|-> (fn rhs' => fold (fn SOME c' => Constgraph.add_edge (c, c')
|
|
229 |
| NONE => I) rhs')
|
|
230 |
|> pair (SOME c)
|
|
231 |
end;
|
|
232 |
|
|
233 |
fun specialize_typs thy funcgr eqss =
|
|
234 |
let
|
|
235 |
fun max k [] = k
|
|
236 |
| max k (l::ls) = max (if k < l then l else k) ls;
|
|
237 |
fun typscheme_of (c, ty) =
|
|
238 |
try (Constgraph.get_node funcgr) (CodegenConsts.norm_of_typ thy (c, ty))
|
|
239 |
|> Option.map fst;
|
21120
|
240 |
fun incr_indices (c:'a, thms) maxidx =
|
20600
|
241 |
let
|
|
242 |
val thms' = map (Thm.incr_indexes maxidx) thms;
|
|
243 |
val maxidx' = Int.max
|
|
244 |
(maxidx, max ~1 (map Thm.maxidx_of thms') + 1);
|
|
245 |
in ((c, thms'), maxidx') end;
|
|
246 |
val tsig = Sign.tsig_of thy;
|
|
247 |
fun unify_const thms (c, ty) (env, maxidx) =
|
|
248 |
case typscheme_of (c, ty)
|
|
249 |
of SOME ty_decl => let
|
|
250 |
val ty_decl' = Logic.incr_tvar maxidx ty_decl;
|
|
251 |
val maxidx' = Int.max (Term.maxidx_of_typ ty_decl' + 1, maxidx);
|
|
252 |
in Type.unify tsig (ty_decl', ty) (env, maxidx')
|
|
253 |
handle TUNIFY => error ("Failed to instantiate\n"
|
|
254 |
^ (Sign.string_of_typ thy o Envir.norm_type env) ty_decl' ^ "\nto\n"
|
|
255 |
^ (Sign.string_of_typ thy o Envir.norm_type env) ty ^ ",\n"
|
|
256 |
^ "in function theorems\n"
|
|
257 |
^ cat_lines (map string_of_thm thms))
|
|
258 |
end
|
|
259 |
| NONE => (env, maxidx);
|
|
260 |
fun apply_unifier unif (c, []) = (c, [])
|
|
261 |
| apply_unifier unif (c, thms as thm :: _) =
|
|
262 |
let
|
21120
|
263 |
val tvars = Term.add_tvars (Thm.prop_of thm) [];
|
|
264 |
fun mk_inst (v_i_sort as (v, _)) =
|
|
265 |
let
|
|
266 |
val ty = TVar v_i_sort;
|
|
267 |
in
|
|
268 |
pairself (Thm.ctyp_of thy) (ty,
|
|
269 |
TVar (v, (snd o dest_TVar o Envir.norm_type unif) ty))
|
|
270 |
end;
|
|
271 |
val instmap = map mk_inst tvars;
|
|
272 |
val (thms' as thm' :: _) = map (Drule.zero_var_indexes o Thm.instantiate (instmap, [])) thms
|
|
273 |
val _ = if fst c <> "" andalso not (Sign.typ_equiv thy (Type.strip_sorts (CodegenData.typ_func thy thm), Type.strip_sorts (CodegenData.typ_func thy thm')))
|
|
274 |
then error ("illegal function type instantiation:\n" ^ Sign.string_of_typ thy (CodegenData.typ_func thy thm)
|
|
275 |
^ "\nto" ^ Sign.string_of_typ thy (CodegenData.typ_func thy thm'))
|
|
276 |
else ();
|
|
277 |
in (c, thms') end;
|
|
278 |
fun rhs_of' thy (("", []), thms as [_]) =
|
|
279 |
add_things_of thy (cons o snd) (NONE, thms) []
|
|
280 |
| rhs_of' thy (c, thms) =
|
|
281 |
add_things_of thy (cons o snd) (SOME c, thms) [];
|
20600
|
282 |
val (eqss', maxidx) =
|
|
283 |
fold_map incr_indices eqss 0;
|
|
284 |
val (unif, _) =
|
|
285 |
fold (fn (c, thms) => fold (unify_const thms) (rhs_of' thy (c, thms)))
|
|
286 |
eqss' (Vartab.empty, maxidx);
|
|
287 |
val eqss'' =
|
|
288 |
map (apply_unifier unif) eqss';
|
|
289 |
in eqss'' end;
|
|
290 |
|
|
291 |
fun merge_eqsyss thy raw_eqss funcgr =
|
|
292 |
let
|
|
293 |
val eqss = specialize_typs thy funcgr raw_eqss;
|
20938
|
294 |
val tys = map (CodegenData.typ_funcs thy) eqss;
|
20600
|
295 |
val rhss = map (rhs_of thy) eqss;
|
|
296 |
in
|
|
297 |
funcgr
|
|
298 |
|> fold2 (fn (c, thms) => fn ty => Constgraph.new_node (c, (ty, thms))) eqss tys
|
|
299 |
|> `(fn funcgr => map (insts_of_thms thy funcgr) eqss)
|
|
300 |
|-> (fn rhs_insts => fold2 (fn (c, _) => fn rhs_inst =>
|
|
301 |
ensure_consts thy rhs_inst #> fold (curry Constgraph.add_edge c) rhs_inst) eqss rhs_insts)
|
|
302 |
|> fold2 (fn (c, _) => fn rhs => fold (curry Constgraph.add_edge c) rhs) eqss rhss
|
|
303 |
end
|
20705
|
304 |
and merge_new_eqsyss thy raw_eqss funcgr =
|
|
305 |
if exists (member CodegenConsts.eq_const (Constgraph.keys funcgr)) (map fst raw_eqss)
|
|
306 |
then funcgr
|
|
307 |
else merge_eqsyss thy raw_eqss funcgr
|
20600
|
308 |
and ensure_consts thy cs funcgr =
|
|
309 |
fold (snd oo ensure_const thy funcgr) cs Constgraph.empty
|
20705
|
310 |
|> (fn auxgr => fold (merge_new_eqsyss thy)
|
20600
|
311 |
(map (AList.make (Constgraph.get_node auxgr))
|
|
312 |
(rev (Constgraph.strong_conn auxgr))) funcgr);
|
|
313 |
|
21120
|
314 |
fun drop_classes thy tfrees thm =
|
|
315 |
let
|
|
316 |
(* val _ = writeln ("DROP1 " ^ setmp show_types true string_of_thm thm); *)
|
|
317 |
val (_, thm') = Thm.varifyT' [] thm;
|
|
318 |
val tvars = Term.add_tvars (Thm.prop_of thm') [];
|
|
319 |
(* val _ = writeln ("DROP2 " ^ setmp show_types true string_of_thm thm'); *)
|
|
320 |
val unconstr = map (Thm.ctyp_of thy o TVar) tvars;
|
|
321 |
val instmap = map2 (fn (v_i, _) => fn (v, sort) => pairself (Thm.ctyp_of thy)
|
|
322 |
(TVar (v_i, []), TFree (v, sort))) tvars tfrees;
|
|
323 |
in
|
|
324 |
thm'
|
|
325 |
|> fold Thm.unconstrainT unconstr
|
|
326 |
|> Thm.instantiate (instmap, [])
|
|
327 |
|> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy))
|
|
328 |
(* |> tap (fn thm => writeln ("DROP3 " ^ setmp show_types true string_of_thm thm)) *)
|
|
329 |
end;
|
|
330 |
|
20600
|
331 |
in
|
|
332 |
|
|
333 |
val ensure_consts = ensure_consts;
|
|
334 |
|
21120
|
335 |
fun make thy consts =
|
|
336 |
Funcgr.change thy (ensure_consts thy consts);
|
|
337 |
|
21129
|
338 |
fun make_term thy f ct =
|
21120
|
339 |
let
|
|
340 |
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
|
|
341 |
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
|
|
342 |
val thm1 = CodegenData.preprocess_cterm thy ct;
|
|
343 |
(* val _ = writeln ("THM1 " ^ setmp show_types true string_of_thm thm1); *)
|
|
344 |
val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1);
|
|
345 |
val consts = CodegenConsts.consts_of thy (Thm.term_of ct');
|
|
346 |
val funcgr = make thy consts;
|
|
347 |
val (_, thm2) = Thm.varifyT' [] thm1;
|
|
348 |
(* val _ = writeln ("THM2 " ^ setmp show_types true string_of_thm thm2); *)
|
|
349 |
val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2));
|
|
350 |
(* val _ = writeln ("THM3 " ^ setmp show_types true string_of_thm thm3); *)
|
|
351 |
val [(_, [thm4])] = specialize_typs thy funcgr [(("", []), [thm3])];
|
|
352 |
(* val _ = writeln ("THM4 " ^ setmp show_types true string_of_thm thm4); *)
|
|
353 |
val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
|
|
354 |
(* val _ = writeln "TFREES"; *)
|
|
355 |
(* val _ = (writeln o cat_lines o map (fn (v, sort) => v ^ "::" ^ Sign.string_of_sort thy sort)) tfrees; *)
|
|
356 |
fun inst thm =
|
|
357 |
let
|
|
358 |
val tvars = Term.add_tvars (Thm.prop_of thm) [];
|
|
359 |
(* val _ = writeln "TVARS"; *)
|
|
360 |
(* val _ = (writeln o cat_lines o map (fn ((v, i), sort) => v ^ "_" ^ string_of_int i ^ "::" ^ Sign.string_of_sort thy sort)) tvars; *)
|
|
361 |
val instmap = map2 (fn (v_i, sort) => fn (v, _) => pairself (Thm.ctyp_of thy)
|
|
362 |
(TVar (v_i, sort), TFree (v, sort))) tvars tfrees;
|
|
363 |
in Thm.instantiate (instmap, []) thm end;
|
|
364 |
val thm5 = inst thm2;
|
|
365 |
val thm6 = inst thm4;
|
|
366 |
(* val _ = writeln ("THM5 " ^ setmp show_types true string_of_thm thm5); *)
|
|
367 |
(* val _ = writeln ("THM6 " ^ setmp show_types true string_of_thm thm6); *)
|
|
368 |
val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6);
|
|
369 |
val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
|
|
370 |
val drop = drop_classes thy tfrees;
|
|
371 |
(* val _ = writeln "ADD INST"; *)
|
|
372 |
val funcgr' = ensure_consts thy
|
|
373 |
(instdefs_of thy (fold (fold (insert (op =)) o insts_of thy funcgr) cs [])) funcgr
|
21129
|
374 |
in (f drop ct'' thm5, Funcgr.change thy (K funcgr')) end;
|
20600
|
375 |
|
|
376 |
end; (*local*)
|
|
377 |
|
|
378 |
fun print_funcgr thy funcgr =
|
|
379 |
AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr)
|
|
380 |
|> (map o apfst) (CodegenConsts.string_of_const thy)
|
|
381 |
|> sort (string_ord o pairself fst)
|
|
382 |
|> map (fn (s, thms) =>
|
|
383 |
(Pretty.block o Pretty.fbreaks) (
|
|
384 |
Pretty.str s
|
|
385 |
:: map Display.pretty_thm thms
|
|
386 |
))
|
|
387 |
|> Pretty.chunks
|
|
388 |
|> Pretty.writeln;
|
|
389 |
|
|
390 |
fun print_codethms thy consts =
|
21120
|
391 |
make thy consts |> print_funcgr thy;
|
20600
|
392 |
|
|
393 |
fun print_codethms_e thy cs =
|
|
394 |
print_codethms thy (map (CodegenConsts.read_const thy) cs);
|
|
395 |
|
|
396 |
|
|
397 |
(** Isar **)
|
|
398 |
|
|
399 |
structure P = OuterParse;
|
|
400 |
|
|
401 |
val print_codethmsK = "print_codethms";
|
|
402 |
|
|
403 |
val print_codethmsP =
|
|
404 |
OuterSyntax.improper_command print_codethmsK "print code theorems of this theory" OuterKeyword.diag
|
|
405 |
(Scan.option (P.$$$ "(" |-- Scan.repeat P.term --| P.$$$ ")")
|
|
406 |
>> (fn NONE => CodegenData.print_thms
|
|
407 |
| SOME cs => fn thy => print_codethms_e thy cs)
|
|
408 |
>> (fn f => Toplevel.no_timing o Toplevel.unknown_theory
|
|
409 |
o Toplevel.keep (f o Toplevel.theory_of)));
|
|
410 |
|
|
411 |
val _ = OuterSyntax.add_parsers [print_codethmsP];
|
|
412 |
|
|
413 |
end; (*struct*)
|