author | berghofe |
Tue, 17 Jul 2007 16:05:34 +0200 | |
changeset 23831 | 64e6e5c738a1 |
parent 23136 | 5a0378eada70 |
child 24166 | 7b28dc69bdbb |
permissions | -rw-r--r-- |
20600 | 1 |
(* Title: Pure/Tools/codegen_funcgr.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
22185 | 5 |
Retrieving, normalizing and structuring defining equations |
20855 | 6 |
in graph with explicit dependencies. |
20600 | 7 |
*) |
8 |
||
9 |
signature CODEGEN_FUNCGR = |
|
10 |
sig |
|
22212 | 11 |
type T |
12 |
val timing: bool ref |
|
21120 | 13 |
val funcs: T -> CodegenConsts.const -> thm list |
14 |
val typ: T -> CodegenConsts.const -> typ |
|
15 |
val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list |
|
16 |
val all: T -> CodegenConsts.const list |
|
22212 | 17 |
val pretty: theory -> T -> Pretty.T |
22507 | 18 |
structure Constgraph : GRAPH |
22212 | 19 |
end |
20 |
||
21 |
signature CODEGEN_FUNCGR_RETRIEVAL = |
|
22 |
sig |
|
23 |
type T (* = CODEGEN_FUNCGR.T *) |
|
24 |
val make: theory -> CodegenConsts.const list -> T |
|
25 |
val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T |
|
26 |
val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T |
|
20600 | 27 |
end; |
28 |
||
22212 | 29 |
structure CodegenFuncgr = (*signature is added later*) |
20600 | 30 |
struct |
31 |
||
22212 | 32 |
(** the graph type **) |
20600 | 33 |
|
34 |
structure Constgraph = GraphFun ( |
|
35 |
type key = CodegenConsts.const; |
|
36 |
val ord = CodegenConsts.const_ord; |
|
37 |
); |
|
38 |
||
39 |
type T = (typ * thm list) Constgraph.T; |
|
40 |
||
22185 | 41 |
fun funcs funcgr = |
42 |
these o Option.map snd o try (Constgraph.get_node funcgr); |
|
43 |
||
44 |
fun typ funcgr = |
|
45 |
fst o Constgraph.get_node funcgr; |
|
46 |
||
47 |
fun deps funcgr cs = |
|
48 |
let |
|
49 |
val conn = Constgraph.strong_conn funcgr; |
|
50 |
val order = rev conn; |
|
51 |
in |
|
52 |
(map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order |
|
53 |
|> filter_out null |
|
54 |
end; |
|
55 |
||
56 |
fun all funcgr = Constgraph.keys funcgr; |
|
57 |
||
22212 | 58 |
fun pretty thy funcgr = |
59 |
AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr) |
|
60 |
|> (map o apfst) (CodegenConsts.string_of_const thy) |
|
61 |
|> sort (string_ord o pairself fst) |
|
62 |
|> map (fn (s, thms) => |
|
63 |
(Pretty.block o Pretty.fbreaks) ( |
|
64 |
Pretty.str s |
|
65 |
:: map Display.pretty_thm thms |
|
66 |
)) |
|
67 |
|> Pretty.chunks; |
|
20600 | 68 |
|
69 |
||
22185 | 70 |
(** generic combinators **) |
20600 | 71 |
|
22185 | 72 |
fun fold_consts f thms = |
73 |
thms |
|
22705 | 74 |
|> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) |
22185 | 75 |
|> (fold o fold_aterms) (fn Const c => f c | _ => I); |
20600 | 76 |
|
22185 | 77 |
fun consts_of (const, []) = [] |
78 |
| consts_of (const, thms as thm :: _) = |
|
79 |
let |
|
80 |
val thy = Thm.theory_of_thm thm; |
|
81 |
val is_refl = curry CodegenConsts.eq_const const; |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
82 |
fun the_const c = case try (CodegenConsts.const_of_cexpr thy) c |
22185 | 83 |
of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const |
84 |
| NONE => I |
|
85 |
in fold_consts the_const thms [] end; |
|
20600 | 86 |
|
22185 | 87 |
fun insts_of thy algebra c ty_decl ty = |
20600 | 88 |
let |
22185 | 89 |
val tys_decl = Sign.const_typargs thy (c, ty_decl); |
20600 | 90 |
val tys = Sign.const_typargs thy (c, ty); |
22570
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22554
diff
changeset
|
91 |
fun class_relation (x, _) _ = x; |
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22554
diff
changeset
|
92 |
fun type_constructor tyco xs class = |
20600 | 93 |
(tyco, class) :: maps (maps fst) xs; |
22570
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22554
diff
changeset
|
94 |
fun type_variable (TVar (_, sort)) = map (pair []) sort |
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22554
diff
changeset
|
95 |
| type_variable (TFree (_, sort)) = map (pair []) sort; |
20600 | 96 |
fun mk_inst ty (TVar (_, sort)) = cons (ty, sort) |
97 |
| mk_inst ty (TFree (_, sort)) = cons (ty, sort) |
|
22198 | 98 |
| mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2; |
21120 | 99 |
fun of_sort_deriv (ty, sort) = |
22185 | 100 |
Sorts.of_sort_derivation (Sign.pp thy) algebra |
22570
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22554
diff
changeset
|
101 |
{ class_relation = class_relation, type_constructor = type_constructor, |
f166a5416b3f
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
wenzelm
parents:
22554
diff
changeset
|
102 |
type_variable = type_variable } |
21120 | 103 |
(ty, sort) |
20600 | 104 |
in |
21120 | 105 |
flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl [])) |
20600 | 106 |
end; |
107 |
||
22212 | 108 |
fun drop_classes thy tfrees thm = |
109 |
let |
|
110 |
val (_, thm') = Thm.varifyT' [] thm; |
|
111 |
val tvars = Term.add_tvars (Thm.prop_of thm') []; |
|
112 |
val unconstr = map (Thm.ctyp_of thy o TVar) tvars; |
|
113 |
val instmap = map2 (fn (v_i, _) => fn (v, sort) => pairself (Thm.ctyp_of thy) |
|
114 |
(TVar (v_i, []), TFree (v, sort))) tvars tfrees; |
|
115 |
in |
|
116 |
thm' |
|
117 |
|> fold Thm.unconstrainT unconstr |
|
118 |
|> Thm.instantiate (instmap, []) |
|
119 |
|> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy)) |
|
120 |
end; |
|
121 |
||
22039 | 122 |
|
22185 | 123 |
(** graph algorithm **) |
20600 | 124 |
|
22185 | 125 |
val timing = ref false; |
20600 | 126 |
|
22185 | 127 |
local |
20600 | 128 |
|
22185 | 129 |
exception INVALID of CodegenConsts.const list * string; |
20600 | 130 |
|
22198 | 131 |
fun resort_thms algebra tap_typ [] = [] |
132 |
| resort_thms algebra tap_typ (thms as thm :: _) = |
|
20600 | 133 |
let |
22198 | 134 |
val thy = Thm.theory_of_thm thm; |
135 |
val cs = fold_consts (insert (op =)) thms []; |
|
136 |
fun match_const c (ty, ty_decl) = |
|
20600 | 137 |
let |
22198 | 138 |
val tys = CodegenConsts.typargs thy (c, ty); |
139 |
val sorts = map (snd o dest_TVar) (CodegenConsts.typargs thy (c, ty_decl)); |
|
140 |
in fold2 (curry (CodegenConsts.typ_sort_inst algebra)) tys sorts end; |
|
141 |
fun match (c_ty as (c, ty)) = |
|
142 |
case tap_typ c_ty |
|
143 |
of SOME ty_decl => match_const c (ty, ty_decl) |
|
144 |
| NONE => I; |
|
145 |
val tvars = fold match cs Vartab.empty; |
|
146 |
in map (CodegenFunc.inst_thm tvars) thms end; |
|
20600 | 147 |
|
22198 | 148 |
fun resort_funcss thy algebra funcgr = |
149 |
let |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
150 |
val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy); |
22198 | 151 |
fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms) |
152 |
handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e |
|
153 |
^ ",\nfor constant " ^ CodegenConsts.string_of_const thy const |
|
154 |
^ "\nin defining equations\n" |
|
155 |
^ (cat_lines o map string_of_thm) thms) |
|
156 |
fun resort_rec tap_typ (const, []) = (true, (const, [])) |
|
157 |
| resort_rec tap_typ (const, thms as thm :: _) = |
|
158 |
let |
|
22737 | 159 |
val (_, ty) = CodegenFunc.head_func thm; |
22198 | 160 |
val thms' as thm' :: _ = resort_thms algebra tap_typ thms |
22737 | 161 |
val (_, ty') = CodegenFunc.head_func thm'; |
22198 | 162 |
in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end; |
163 |
fun resort_recs funcss = |
|
164 |
let |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
165 |
fun tap_typ c_ty = case try (CodegenConsts.const_of_cexpr thy) c_ty |
22198 | 166 |
of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const |
167 |
|> these |
|
168 |
|> try hd |
|
22737 | 169 |
|> Option.map (snd o CodegenFunc.head_func) |
22198 | 170 |
| NONE => NONE; |
171 |
val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss); |
|
172 |
val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; |
|
173 |
in (unchanged, funcss') end; |
|
174 |
fun resort_rec_until funcss = |
|
175 |
let |
|
176 |
val (unchanged, funcss') = resort_recs funcss; |
|
177 |
in if unchanged then funcss' else resort_rec_until funcss' end; |
|
178 |
in map resort_dep #> resort_rec_until end; |
|
22039 | 179 |
|
22185 | 180 |
fun instances_of thy algebra insts = |
181 |
let |
|
182 |
val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy; |
|
183 |
fun all_classops tyco class = |
|
184 |
try (AxClass.params_of_class thy) class |
|
185 |
|> Option.map snd |
|
186 |
|> these |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
187 |
|> map (fn (c, _) => (c, SOME tyco)) |
22185 | 188 |
in |
189 |
Symtab.empty |
|
190 |
|> fold (fn (tyco, class) => |
|
191 |
Symtab.map_default (tyco, []) (insert (op =) class)) insts |
|
192 |
|> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco) |
|
193 |
(Graph.all_succs thy_classes classes))) tab []) |
|
194 |
end; |
|
195 |
||
196 |
fun instances_of_consts thy algebra funcgr consts = |
|
20600 | 197 |
let |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
198 |
fun inst (cexpr as (c, ty)) = insts_of thy algebra c |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
199 |
((fst o Constgraph.get_node funcgr o CodegenConsts.const_of_cexpr thy) cexpr) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
200 |
ty handle CLASS_ERROR => []; |
22185 | 201 |
in |
202 |
[] |
|
203 |
|> fold (fold (insert (op =)) o inst) consts |
|
204 |
|> instances_of thy algebra |
|
205 |
end; |
|
206 |
||
22212 | 207 |
fun ensure_const' rewrites thy algebra funcgr const auxgr = |
22185 | 208 |
if can (Constgraph.get_node funcgr) const |
209 |
then (NONE, auxgr) |
|
210 |
else if can (Constgraph.get_node auxgr) const |
|
211 |
then (SOME const, auxgr) |
|
212 |
else if is_some (CodegenData.get_datatype_of_constr thy const) then |
|
213 |
auxgr |
|
214 |
|> Constgraph.new_node (const, []) |
|
215 |
|> pair (SOME const) |
|
216 |
else let |
|
22212 | 217 |
val thms = CodegenData.these_funcs thy const |
218 |
|> map (CodegenFunc.rewrite_func (rewrites thy)) |
|
219 |
|> CodegenFunc.norm_args |
|
220 |
|> CodegenFunc.norm_varnames CodegenNames.purify_tvar CodegenNames.purify_var; |
|
22185 | 221 |
val rhs = consts_of (const, thms); |
222 |
in |
|
223 |
auxgr |
|
224 |
|> Constgraph.new_node (const, thms) |
|
22212 | 225 |
|> fold_map (ensure_const rewrites thy algebra funcgr) rhs |
22185 | 226 |
|-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const') |
227 |
| NONE => I) rhs') |
|
228 |
|> pair (SOME const) |
|
229 |
end |
|
22212 | 230 |
and ensure_const rewrites thy algebra funcgr const = |
22185 | 231 |
let |
232 |
val timeap = if !timing |
|
233 |
then Output.timeap_msg ("time for " ^ CodegenConsts.string_of_const thy const) |
|
234 |
else I; |
|
22212 | 235 |
in timeap (ensure_const' rewrites thy algebra funcgr const) end; |
22185 | 236 |
|
22212 | 237 |
fun merge_funcss rewrites thy algebra raw_funcss funcgr = |
22185 | 238 |
let |
22401 | 239 |
val funcss = raw_funcss |
240 |
|> resort_funcss thy algebra funcgr |
|
241 |
|> filter_out (can (Constgraph.get_node funcgr) o fst); |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
242 |
fun typ_func const [] = CodegenData.default_typ thy const |
22737 | 243 |
| typ_func (_, NONE) (thm :: _) = (snd o CodegenFunc.head_func) thm |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
244 |
| typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
245 |
let |
22737 | 246 |
val (_, ty) = CodegenFunc.head_func thm; |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
247 |
val SOME class = AxClass.class_of_param thy c; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
248 |
val sorts_decl = Sorts.mg_domain algebra tyco [class]; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
249 |
val tys = CodegenConsts.typargs thy (c, ty); |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
250 |
val sorts = map (snd o dest_TVar) tys; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
251 |
in if sorts = sorts_decl then ty |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
252 |
else raise INVALID ([const], "Illegal instantation for class operation " |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
253 |
^ CodegenConsts.string_of_const thy const |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
254 |
^ "\nin defining equations\n" |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
255 |
^ (cat_lines o map string_of_thm) thms) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
256 |
end; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
257 |
fun add_funcs (const, thms) = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
258 |
Constgraph.new_node (const, (typ_func const thms, thms)); |
22185 | 259 |
fun add_deps (funcs as (const, thms)) funcgr = |
260 |
let |
|
261 |
val deps = consts_of funcs; |
|
262 |
val insts = instances_of_consts thy algebra funcgr |
|
263 |
(fold_consts (insert (op =)) thms []); |
|
264 |
in |
|
265 |
funcgr |
|
22212 | 266 |
|> ensure_consts' rewrites thy algebra insts |
22185 | 267 |
|> fold (curry Constgraph.add_edge const) deps |
268 |
|> fold (curry Constgraph.add_edge const) insts |
|
269 |
end; |
|
20600 | 270 |
in |
271 |
funcgr |
|
22185 | 272 |
|> fold add_funcs funcss |
273 |
|> fold add_deps funcss |
|
20600 | 274 |
end |
22212 | 275 |
and ensure_consts' rewrites thy algebra cs funcgr = |
22401 | 276 |
let |
277 |
val auxgr = Constgraph.empty |
|
278 |
|> fold (snd oo ensure_const rewrites thy algebra funcgr) cs; |
|
279 |
in |
|
280 |
funcgr |
|
281 |
|> fold (merge_funcss rewrites thy algebra) |
|
282 |
(map (AList.make (Constgraph.get_node auxgr)) |
|
283 |
(rev (Constgraph.strong_conn auxgr))) |
|
284 |
end handle INVALID (cs', msg) |
|
285 |
=> raise INVALID (fold (insert CodegenConsts.eq_const) cs' cs, msg); |
|
20600 | 286 |
|
22212 | 287 |
fun ensure_consts rewrites thy consts funcgr = |
22185 | 288 |
let |
289 |
val algebra = CodegenData.coregular_algebra thy |
|
22212 | 290 |
in ensure_consts' rewrites thy algebra consts funcgr |
22185 | 291 |
handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " |
292 |
^ commas (map (CodegenConsts.string_of_const thy) cs')) |
|
293 |
end; |
|
294 |
||
20600 | 295 |
in |
296 |
||
22212 | 297 |
(** retrieval interfaces **) |
20600 | 298 |
|
22212 | 299 |
val ensure_consts = ensure_consts; |
21120 | 300 |
|
22212 | 301 |
fun check_consts rewrites thy consts funcgr = |
22185 | 302 |
let |
303 |
val algebra = CodegenData.coregular_algebra thy; |
|
304 |
fun try_const const funcgr = |
|
22212 | 305 |
(SOME const, ensure_consts' rewrites thy algebra [const] funcgr) |
22185 | 306 |
handle INVALID (cs', msg) => (NONE, funcgr); |
22212 | 307 |
val (consts', funcgr') = fold_map try_const consts funcgr; |
308 |
in (map_filter I consts', funcgr') end; |
|
22185 | 309 |
|
22212 | 310 |
fun ensure_consts_term rewrites thy f ct funcgr = |
21120 | 311 |
let |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
312 |
fun consts_of thy t = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
313 |
fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t [] |
22212 | 314 |
fun rhs_conv conv thm = |
315 |
let |
|
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22737
diff
changeset
|
316 |
val thm' = (conv o Thm.rhs_of) thm; |
22212 | 317 |
in Thm.transitive thm thm' end |
21120 | 318 |
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct); |
319 |
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); |
|
22212 | 320 |
val thm1 = CodegenData.preprocess_cterm ct |
321 |
|> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy); |
|
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22737
diff
changeset
|
322 |
val ct' = Thm.rhs_of thm1; |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
323 |
val consts = consts_of thy (Thm.term_of ct'); |
22212 | 324 |
val funcgr' = ensure_consts rewrites thy consts funcgr; |
22198 | 325 |
val algebra = CodegenData.coregular_algebra thy; |
21120 | 326 |
val (_, thm2) = Thm.varifyT' [] thm1; |
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22737
diff
changeset
|
327 |
val thm3 = Thm.reflexive (Thm.rhs_of thm2); |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
328 |
val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.const_of_cexpr thy); |
22198 | 329 |
val [thm4] = resort_thms algebra typ_funcgr [thm3]; |
21120 | 330 |
val tfrees = Term.add_tfrees (Thm.prop_of thm1) []; |
331 |
fun inst thm = |
|
332 |
let |
|
333 |
val tvars = Term.add_tvars (Thm.prop_of thm) []; |
|
334 |
val instmap = map2 (fn (v_i, sort) => fn (v, _) => pairself (Thm.ctyp_of thy) |
|
335 |
(TVar (v_i, sort), TFree (v, sort))) tvars tfrees; |
|
336 |
in Thm.instantiate (instmap, []) thm end; |
|
337 |
val thm5 = inst thm2; |
|
338 |
val thm6 = inst thm4; |
|
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22737
diff
changeset
|
339 |
val ct'' = Thm.rhs_of thm6; |
21120 | 340 |
val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') []; |
341 |
val drop = drop_classes thy tfrees; |
|
22212 | 342 |
val instdefs = instances_of_consts thy algebra funcgr' cs; |
343 |
val funcgr'' = ensure_consts rewrites thy instdefs funcgr'; |
|
344 |
in (f funcgr'' drop ct'' thm5, funcgr'') end; |
|
20600 | 345 |
|
346 |
end; (*local*) |
|
347 |
||
22212 | 348 |
end; (*struct*) |
22185 | 349 |
|
23136 | 350 |
functor CodegenFuncgrRetrieval (val rewrites: theory -> thm list) : CODEGEN_FUNCGR_RETRIEVAL = |
22212 | 351 |
struct |
20600 | 352 |
|
22212 | 353 |
(** code data **) |
354 |
||
355 |
type T = CodegenFuncgr.T; |
|
20600 | 356 |
|
22212 | 357 |
structure Funcgr = CodeDataFun |
358 |
(struct |
|
359 |
type T = T; |
|
360 |
val empty = CodegenFuncgr.Constgraph.empty; |
|
361 |
fun merge _ _ = CodegenFuncgr.Constgraph.empty; |
|
362 |
fun purge _ NONE _ = CodegenFuncgr.Constgraph.empty |
|
363 |
| purge _ (SOME cs) funcgr = |
|
364 |
CodegenFuncgr.Constgraph.del_nodes ((CodegenFuncgr.Constgraph.all_preds funcgr |
|
365 |
o filter (can (CodegenFuncgr.Constgraph.get_node funcgr))) cs) funcgr; |
|
366 |
end); |
|
20600 | 367 |
|
22212 | 368 |
fun make thy = |
369 |
Funcgr.change thy o CodegenFuncgr.ensure_consts rewrites thy; |
|
20600 | 370 |
|
22212 | 371 |
fun make_consts thy = |
372 |
Funcgr.change_yield thy o CodegenFuncgr.check_consts rewrites thy; |
|
373 |
||
374 |
fun make_term thy f = |
|
375 |
Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_term rewrites thy f; |
|
20600 | 376 |
|
22212 | 377 |
end; (*functor*) |
378 |
||
379 |
structure CodegenFuncgr : CODEGEN_FUNCGR = |
|
380 |
struct |
|
381 |
||
382 |
open CodegenFuncgr; |
|
20600 | 383 |
|
384 |
end; (*struct*) |