author | haftmann |
Fri, 30 Mar 2007 16:19:03 +0200 | |
changeset 22554 | d1499fff65d8 |
parent 22507 | 3572bc633d9a |
child 22570 | f166a5416b3f |
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 |
|
27 |
val init: theory -> theory |
|
20600 | 28 |
end; |
29 |
||
22212 | 30 |
structure CodegenFuncgr = (*signature is added later*) |
20600 | 31 |
struct |
32 |
||
22212 | 33 |
(** the graph type **) |
20600 | 34 |
|
35 |
structure Constgraph = GraphFun ( |
|
36 |
type key = CodegenConsts.const; |
|
37 |
val ord = CodegenConsts.const_ord; |
|
38 |
); |
|
39 |
||
40 |
type T = (typ * thm list) Constgraph.T; |
|
41 |
||
22185 | 42 |
fun funcs funcgr = |
43 |
these o Option.map snd o try (Constgraph.get_node funcgr); |
|
44 |
||
45 |
fun typ funcgr = |
|
46 |
fst o Constgraph.get_node funcgr; |
|
47 |
||
48 |
fun deps funcgr cs = |
|
49 |
let |
|
50 |
val conn = Constgraph.strong_conn funcgr; |
|
51 |
val order = rev conn; |
|
52 |
in |
|
53 |
(map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order |
|
54 |
|> filter_out null |
|
55 |
end; |
|
56 |
||
57 |
fun all funcgr = Constgraph.keys funcgr; |
|
58 |
||
22212 | 59 |
fun pretty thy funcgr = |
60 |
AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr) |
|
61 |
|> (map o apfst) (CodegenConsts.string_of_const thy) |
|
62 |
|> sort (string_ord o pairself fst) |
|
63 |
|> map (fn (s, thms) => |
|
64 |
(Pretty.block o Pretty.fbreaks) ( |
|
65 |
Pretty.str s |
|
66 |
:: map Display.pretty_thm thms |
|
67 |
)) |
|
68 |
|> Pretty.chunks; |
|
20600 | 69 |
|
70 |
||
22185 | 71 |
(** generic combinators **) |
20600 | 72 |
|
22185 | 73 |
fun fold_consts f thms = |
74 |
thms |
|
75 |
|> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Drule.plain_prop_of) |
|
76 |
|> (fold o fold_aterms) (fn Const c => f c | _ => I); |
|
20600 | 77 |
|
22185 | 78 |
fun consts_of (const, []) = [] |
79 |
| consts_of (const, thms as thm :: _) = |
|
80 |
let |
|
81 |
val thy = Thm.theory_of_thm thm; |
|
82 |
val is_refl = curry CodegenConsts.eq_const const; |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
83 |
fun the_const c = case try (CodegenConsts.const_of_cexpr thy) c |
22185 | 84 |
of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const |
85 |
| NONE => I |
|
86 |
in fold_consts the_const thms [] end; |
|
20600 | 87 |
|
22185 | 88 |
fun insts_of thy algebra c ty_decl ty = |
20600 | 89 |
let |
22185 | 90 |
val tys_decl = Sign.const_typargs thy (c, ty_decl); |
20600 | 91 |
val tys = Sign.const_typargs thy (c, ty); |
22185 | 92 |
fun classrel (x, _) _ = x; |
20600 | 93 |
fun constructor tyco xs class = |
94 |
(tyco, class) :: maps (maps fst) xs; |
|
95 |
fun variable (TVar (_, sort)) = map (pair []) sort |
|
96 |
| variable (TFree (_, sort)) = map (pair []) sort; |
|
97 |
fun mk_inst ty (TVar (_, sort)) = cons (ty, sort) |
|
98 |
| mk_inst ty (TFree (_, sort)) = cons (ty, sort) |
|
22198 | 99 |
| mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2; |
21120 | 100 |
fun of_sort_deriv (ty, sort) = |
22185 | 101 |
Sorts.of_sort_derivation (Sign.pp thy) algebra |
21120 | 102 |
{ classrel = classrel, constructor = constructor, variable = variable } |
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 |
|
159 |
val ty = CodegenFunc.typ_func thm; |
|
160 |
val thms' as thm' :: _ = resort_thms algebra tap_typ thms |
|
161 |
val ty' = CodegenFunc.typ_func thm'; |
|
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 |
|
169 |
|> Option.map CodegenFunc.typ_func |
|
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 |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
243 |
| typ_func (_, NONE) (thm :: _) = CodegenFunc.typ_func thm |
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 |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22507
diff
changeset
|
246 |
val ty = CodegenFunc.typ_func thm; |
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 |
|
316 |
val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm; |
|
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); |
|
21120 | 322 |
val ct' = Drule.dest_equals_rhs (Thm.cprop_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; |
327 |
val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_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; |
|
339 |
val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6); |
|
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 |
|
22212 | 350 |
functor CodegenFuncgrRetrieval (val name: string; val rewrites: theory -> thm list) : CODEGEN_FUNCGR_RETRIEVAL = |
351 |
struct |
|
20600 | 352 |
|
22212 | 353 |
(** code data **) |
354 |
||
355 |
type T = CodegenFuncgr.T; |
|
20600 | 356 |
|
22212 | 357 |
structure Funcgr = CodeDataFun |
358 |
(struct |
|
359 |
val name = name; |
|
360 |
type T = T; |
|
361 |
val empty = CodegenFuncgr.Constgraph.empty; |
|
362 |
fun merge _ _ = CodegenFuncgr.Constgraph.empty; |
|
363 |
fun purge _ NONE _ = CodegenFuncgr.Constgraph.empty |
|
364 |
| purge _ (SOME cs) funcgr = |
|
365 |
CodegenFuncgr.Constgraph.del_nodes ((CodegenFuncgr.Constgraph.all_preds funcgr |
|
366 |
o filter (can (CodegenFuncgr.Constgraph.get_node funcgr))) cs) funcgr; |
|
367 |
end); |
|
20600 | 368 |
|
22212 | 369 |
fun make thy = |
370 |
Funcgr.change thy o CodegenFuncgr.ensure_consts rewrites thy; |
|
20600 | 371 |
|
22212 | 372 |
fun make_consts thy = |
373 |
Funcgr.change_yield thy o CodegenFuncgr.check_consts rewrites thy; |
|
374 |
||
375 |
fun make_term thy f = |
|
376 |
Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_term rewrites thy f; |
|
20600 | 377 |
|
22212 | 378 |
val init = Funcgr.init; |
379 |
||
380 |
end; (*functor*) |
|
381 |
||
382 |
structure CodegenFuncgr : CODEGEN_FUNCGR = |
|
383 |
struct |
|
384 |
||
385 |
open CodegenFuncgr; |
|
20600 | 386 |
|
387 |
end; (*struct*) |