author | haftmann |
Tue, 30 Jan 2007 08:21:22 +0100 | |
changeset 22212 | 079de24eee65 |
parent 22198 | 226d29db8e0a |
child 22223 | 69d4b98f4c47 |
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 |
18 |
end |
|
19 |
||
20 |
signature CODEGEN_FUNCGR_RETRIEVAL = |
|
21 |
sig |
|
22 |
type T (* = CODEGEN_FUNCGR.T *) |
|
23 |
val make: theory -> CodegenConsts.const list -> T |
|
24 |
val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T |
|
25 |
val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T |
|
26 |
val init: theory -> theory |
|
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 |
|
74 |
|> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Drule.plain_prop_of) |
|
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; |
|
82 |
fun the_const c = case try (CodegenConsts.norm_of_typ thy) c |
|
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); |
22185 | 91 |
fun classrel (x, _) _ = x; |
20600 | 92 |
fun constructor tyco xs class = |
93 |
(tyco, class) :: maps (maps fst) xs; |
|
94 |
fun variable (TVar (_, sort)) = map (pair []) sort |
|
95 |
| variable (TFree (_, sort)) = map (pair []) sort; |
|
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 |
21120 | 101 |
{ classrel = classrel, constructor = constructor, variable = variable } |
102 |
(ty, sort) |
|
20600 | 103 |
in |
21120 | 104 |
flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl [])) |
20600 | 105 |
end; |
106 |
||
22212 | 107 |
fun drop_classes thy tfrees thm = |
108 |
let |
|
109 |
val (_, thm') = Thm.varifyT' [] thm; |
|
110 |
val tvars = Term.add_tvars (Thm.prop_of thm') []; |
|
111 |
val unconstr = map (Thm.ctyp_of thy o TVar) tvars; |
|
112 |
val instmap = map2 (fn (v_i, _) => fn (v, sort) => pairself (Thm.ctyp_of thy) |
|
113 |
(TVar (v_i, []), TFree (v, sort))) tvars tfrees; |
|
114 |
in |
|
115 |
thm' |
|
116 |
|> fold Thm.unconstrainT unconstr |
|
117 |
|> Thm.instantiate (instmap, []) |
|
118 |
|> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy)) |
|
119 |
end; |
|
120 |
||
22039 | 121 |
|
22185 | 122 |
(** graph algorithm **) |
20600 | 123 |
|
22185 | 124 |
val timing = ref false; |
20600 | 125 |
|
22185 | 126 |
local |
20600 | 127 |
|
22185 | 128 |
exception INVALID of CodegenConsts.const list * string; |
20600 | 129 |
|
22198 | 130 |
fun resort_thms algebra tap_typ [] = [] |
131 |
| resort_thms algebra tap_typ (thms as thm :: _) = |
|
20600 | 132 |
let |
22198 | 133 |
val thy = Thm.theory_of_thm thm; |
134 |
val cs = fold_consts (insert (op =)) thms []; |
|
135 |
fun match_const c (ty, ty_decl) = |
|
20600 | 136 |
let |
22198 | 137 |
val tys = CodegenConsts.typargs thy (c, ty); |
138 |
val sorts = map (snd o dest_TVar) (CodegenConsts.typargs thy (c, ty_decl)); |
|
139 |
in fold2 (curry (CodegenConsts.typ_sort_inst algebra)) tys sorts end; |
|
140 |
fun match (c_ty as (c, ty)) = |
|
141 |
case tap_typ c_ty |
|
142 |
of SOME ty_decl => match_const c (ty, ty_decl) |
|
143 |
| NONE => I; |
|
144 |
val tvars = fold match cs Vartab.empty; |
|
145 |
in map (CodegenFunc.inst_thm tvars) thms end; |
|
20600 | 146 |
|
22198 | 147 |
fun resort_funcss thy algebra funcgr = |
148 |
let |
|
149 |
val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodegenConsts.norm_of_typ thy); |
|
150 |
fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms) |
|
151 |
handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e |
|
152 |
^ ",\nfor constant " ^ CodegenConsts.string_of_const thy const |
|
153 |
^ "\nin defining equations\n" |
|
154 |
^ (cat_lines o map string_of_thm) thms) |
|
155 |
fun resort_rec tap_typ (const, []) = (true, (const, [])) |
|
156 |
| resort_rec tap_typ (const, thms as thm :: _) = |
|
157 |
let |
|
158 |
val ty = CodegenFunc.typ_func thm; |
|
159 |
val thms' as thm' :: _ = resort_thms algebra tap_typ thms |
|
160 |
val ty' = CodegenFunc.typ_func thm'; |
|
161 |
in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end; |
|
162 |
fun resort_recs funcss = |
|
163 |
let |
|
164 |
fun tap_typ c_ty = case try (CodegenConsts.norm_of_typ thy) c_ty |
|
165 |
of SOME const => AList.lookup (CodegenConsts.eq_const) funcss const |
|
166 |
|> these |
|
167 |
|> try hd |
|
168 |
|> Option.map CodegenFunc.typ_func |
|
169 |
| NONE => NONE; |
|
170 |
val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss); |
|
171 |
val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; |
|
172 |
in (unchanged, funcss') end; |
|
173 |
fun resort_rec_until funcss = |
|
174 |
let |
|
175 |
val (unchanged, funcss') = resort_recs funcss; |
|
176 |
in if unchanged then funcss' else resort_rec_until funcss' end; |
|
177 |
in map resort_dep #> resort_rec_until end; |
|
22039 | 178 |
|
22185 | 179 |
fun classop_const thy algebra class classop tyco = |
180 |
let |
|
181 |
val sorts = Sorts.mg_domain algebra tyco [class] |
|
182 |
val (var, _) = try (AxClass.params_of_class thy) class |> the_default ("'a", []); |
|
183 |
val vs = Name.names (Name.declare var Name.context) "'a" sorts; |
|
184 |
val arity_typ = Type (tyco, map TFree vs); |
|
185 |
in (classop, [arity_typ]) end; |
|
186 |
||
187 |
fun instances_of thy algebra insts = |
|
188 |
let |
|
189 |
val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy; |
|
190 |
fun all_classops tyco class = |
|
191 |
try (AxClass.params_of_class thy) class |
|
192 |
|> Option.map snd |
|
193 |
|> these |
|
194 |
|> map (fn (c, _) => classop_const thy algebra class c tyco) |
|
195 |
|> map (CodegenConsts.norm thy) |
|
196 |
in |
|
197 |
Symtab.empty |
|
198 |
|> fold (fn (tyco, class) => |
|
199 |
Symtab.map_default (tyco, []) (insert (op =) class)) insts |
|
200 |
|> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco) |
|
201 |
(Graph.all_succs thy_classes classes))) tab []) |
|
202 |
end; |
|
203 |
||
204 |
fun instances_of_consts thy algebra funcgr consts = |
|
20600 | 205 |
let |
22185 | 206 |
fun inst (const as (c, ty)) = case try (CodegenConsts.norm_of_typ thy) const |
207 |
of SOME const => insts_of thy algebra c (fst (Constgraph.get_node funcgr const)) ty |
|
208 |
| NONE => []; |
|
209 |
in |
|
210 |
[] |
|
211 |
|> fold (fold (insert (op =)) o inst) consts |
|
212 |
|> instances_of thy algebra |
|
213 |
end; |
|
214 |
||
22212 | 215 |
fun ensure_const' rewrites thy algebra funcgr const auxgr = |
22185 | 216 |
if can (Constgraph.get_node funcgr) const |
217 |
then (NONE, auxgr) |
|
218 |
else if can (Constgraph.get_node auxgr) const |
|
219 |
then (SOME const, auxgr) |
|
220 |
else if is_some (CodegenData.get_datatype_of_constr thy const) then |
|
221 |
auxgr |
|
222 |
|> Constgraph.new_node (const, []) |
|
223 |
|> pair (SOME const) |
|
224 |
else let |
|
22212 | 225 |
val thms = CodegenData.these_funcs thy const |
226 |
|> map (CodegenFunc.rewrite_func (rewrites thy)) |
|
227 |
|> CodegenFunc.norm_args |
|
228 |
|> CodegenFunc.norm_varnames CodegenNames.purify_tvar CodegenNames.purify_var; |
|
22185 | 229 |
val rhs = consts_of (const, thms); |
230 |
in |
|
231 |
auxgr |
|
232 |
|> Constgraph.new_node (const, thms) |
|
22212 | 233 |
|> fold_map (ensure_const rewrites thy algebra funcgr) rhs |
22185 | 234 |
|-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const') |
235 |
| NONE => I) rhs') |
|
236 |
|> pair (SOME const) |
|
237 |
end |
|
22212 | 238 |
and ensure_const rewrites thy algebra funcgr const = |
22185 | 239 |
let |
240 |
val timeap = if !timing |
|
241 |
then Output.timeap_msg ("time for " ^ CodegenConsts.string_of_const thy const) |
|
242 |
else I; |
|
22212 | 243 |
in timeap (ensure_const' rewrites thy algebra funcgr const) end; |
22185 | 244 |
|
22212 | 245 |
fun merge_funcss rewrites thy algebra raw_funcss funcgr = |
22185 | 246 |
let |
22198 | 247 |
val funcss = resort_funcss thy algebra funcgr raw_funcss; |
248 |
fun classop_typ (c, [typarg]) class = |
|
249 |
let |
|
250 |
val ty = Sign.the_const_type thy c; |
|
251 |
val inst = case typarg |
|
252 |
of Type (tyco, _) => classop_const thy algebra class c tyco |
|
253 |
|> snd |
|
254 |
|> the_single |
|
255 |
|> Logic.varifyT |
|
256 |
| _ => TVar (("'a", 0), [class]); |
|
257 |
in Term.map_type_tvar (K inst) ty end; |
|
22185 | 258 |
fun default_typ (const as (c, tys)) = case CodegenData.tap_typ thy const |
259 |
of SOME ty => ty |
|
22198 | 260 |
| NONE => (case AxClass.class_of_param thy c |
261 |
of SOME class => classop_typ const class |
|
262 |
| NONE => Sign.the_const_type thy c) |
|
263 |
fun typ_func (const as (c, tys)) thm = |
|
264 |
let |
|
265 |
val ty = CodegenFunc.typ_func thm; |
|
266 |
in case AxClass.class_of_param thy c |
|
267 |
of SOME class => (case tys |
|
268 |
of [Type _] => let val ty_decl = classop_typ const class |
|
269 |
in if Sign.typ_equiv thy (ty, ty_decl) then ty |
|
270 |
else raise raise INVALID ([const], "Illegal instantation for class operation " |
|
271 |
^ CodegenConsts.string_of_const thy const |
|
272 |
^ ":\n" ^ CodegenConsts.string_of_typ thy ty_decl |
|
273 |
^ "\nto " ^ CodegenConsts.string_of_typ thy ty) |
|
274 |
end |
|
275 |
| _ => ty) |
|
276 |
| NONE => ty |
|
277 |
end; |
|
22185 | 278 |
fun add_funcs (const, thms as thm :: _) = |
22198 | 279 |
Constgraph.new_node (const, (typ_func const thm, thms)) |
22185 | 280 |
| add_funcs (const, []) = |
281 |
Constgraph.new_node (const, (default_typ const, [])); |
|
282 |
fun add_deps (funcs as (const, thms)) funcgr = |
|
283 |
let |
|
284 |
val deps = consts_of funcs; |
|
285 |
val insts = instances_of_consts thy algebra funcgr |
|
286 |
(fold_consts (insert (op =)) thms []); |
|
287 |
in |
|
288 |
funcgr |
|
22212 | 289 |
|> ensure_consts' rewrites thy algebra insts |
22185 | 290 |
|> fold (curry Constgraph.add_edge const) deps |
291 |
|> fold (curry Constgraph.add_edge const) insts |
|
292 |
end; |
|
20600 | 293 |
in |
294 |
funcgr |
|
22185 | 295 |
|> fold add_funcs funcss |
296 |
|> fold add_deps funcss |
|
20600 | 297 |
end |
22212 | 298 |
and ensure_consts' rewrites thy algebra cs funcgr = |
299 |
fold (snd oo ensure_const rewrites thy algebra funcgr) cs Constgraph.empty |
|
300 |
|> (fn auxgr => fold (merge_funcss rewrites thy algebra) |
|
20600 | 301 |
(map (AList.make (Constgraph.get_node auxgr)) |
21387
5d3d340cb783
clarified code for building function equation system; explicit check of type discipline
haftmann
parents:
21196
diff
changeset
|
302 |
(rev (Constgraph.strong_conn auxgr))) funcgr) |
22185 | 303 |
handle INVALID (cs', msg) => raise INVALID (fold (insert CodegenConsts.eq_const) cs' cs, msg); |
20600 | 304 |
|
22212 | 305 |
fun ensure_consts rewrites thy consts funcgr = |
22185 | 306 |
let |
307 |
val algebra = CodegenData.coregular_algebra thy |
|
22212 | 308 |
in ensure_consts' rewrites thy algebra consts funcgr |
22185 | 309 |
handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " |
310 |
^ commas (map (CodegenConsts.string_of_const thy) cs')) |
|
311 |
end; |
|
312 |
||
20600 | 313 |
in |
314 |
||
22212 | 315 |
(** retrieval interfaces **) |
20600 | 316 |
|
22212 | 317 |
val ensure_consts = ensure_consts; |
21120 | 318 |
|
22212 | 319 |
fun check_consts rewrites thy consts funcgr = |
22185 | 320 |
let |
321 |
val algebra = CodegenData.coregular_algebra thy; |
|
322 |
fun try_const const funcgr = |
|
22212 | 323 |
(SOME const, ensure_consts' rewrites thy algebra [const] funcgr) |
22185 | 324 |
handle INVALID (cs', msg) => (NONE, funcgr); |
22212 | 325 |
val (consts', funcgr') = fold_map try_const consts funcgr; |
326 |
in (map_filter I consts', funcgr') end; |
|
22185 | 327 |
|
22212 | 328 |
fun ensure_consts_term rewrites thy f ct funcgr = |
21120 | 329 |
let |
22212 | 330 |
fun rhs_conv conv thm = |
331 |
let |
|
332 |
val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm; |
|
333 |
in Thm.transitive thm thm' end |
|
21120 | 334 |
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct); |
335 |
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); |
|
22212 | 336 |
val thm1 = CodegenData.preprocess_cterm ct |
337 |
|> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy); |
|
21120 | 338 |
val ct' = Drule.dest_equals_rhs (Thm.cprop_of thm1); |
339 |
val consts = CodegenConsts.consts_of thy (Thm.term_of ct'); |
|
22212 | 340 |
val funcgr' = ensure_consts rewrites thy consts funcgr; |
22198 | 341 |
val algebra = CodegenData.coregular_algebra thy; |
21120 | 342 |
val (_, thm2) = Thm.varifyT' [] thm1; |
343 |
val thm3 = Thm.reflexive (Drule.dest_equals_rhs (Thm.cprop_of thm2)); |
|
22212 | 344 |
val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodegenConsts.norm_of_typ thy); |
22198 | 345 |
val [thm4] = resort_thms algebra typ_funcgr [thm3]; |
21120 | 346 |
val tfrees = Term.add_tfrees (Thm.prop_of thm1) []; |
347 |
fun inst thm = |
|
348 |
let |
|
349 |
val tvars = Term.add_tvars (Thm.prop_of thm) []; |
|
350 |
val instmap = map2 (fn (v_i, sort) => fn (v, _) => pairself (Thm.ctyp_of thy) |
|
351 |
(TVar (v_i, sort), TFree (v, sort))) tvars tfrees; |
|
352 |
in Thm.instantiate (instmap, []) thm end; |
|
353 |
val thm5 = inst thm2; |
|
354 |
val thm6 = inst thm4; |
|
355 |
val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6); |
|
356 |
val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') []; |
|
357 |
val drop = drop_classes thy tfrees; |
|
22212 | 358 |
val instdefs = instances_of_consts thy algebra funcgr' cs; |
359 |
val funcgr'' = ensure_consts rewrites thy instdefs funcgr'; |
|
360 |
in (f funcgr'' drop ct'' thm5, funcgr'') end; |
|
20600 | 361 |
|
362 |
end; (*local*) |
|
363 |
||
22212 | 364 |
end; (*struct*) |
22185 | 365 |
|
22212 | 366 |
functor CodegenFuncgrRetrieval (val name: string; val rewrites: theory -> thm list) : CODEGEN_FUNCGR_RETRIEVAL = |
367 |
struct |
|
20600 | 368 |
|
22212 | 369 |
(** code data **) |
370 |
||
371 |
type T = CodegenFuncgr.T; |
|
20600 | 372 |
|
22212 | 373 |
structure Funcgr = CodeDataFun |
374 |
(struct |
|
375 |
val name = name; |
|
376 |
type T = T; |
|
377 |
val empty = CodegenFuncgr.Constgraph.empty; |
|
378 |
fun merge _ _ = CodegenFuncgr.Constgraph.empty; |
|
379 |
fun purge _ NONE _ = CodegenFuncgr.Constgraph.empty |
|
380 |
| purge _ (SOME cs) funcgr = |
|
381 |
CodegenFuncgr.Constgraph.del_nodes ((CodegenFuncgr.Constgraph.all_preds funcgr |
|
382 |
o filter (can (CodegenFuncgr.Constgraph.get_node funcgr))) cs) funcgr; |
|
383 |
end); |
|
20600 | 384 |
|
22212 | 385 |
fun make thy = |
386 |
Funcgr.change thy o CodegenFuncgr.ensure_consts rewrites thy; |
|
20600 | 387 |
|
22212 | 388 |
fun make_consts thy = |
389 |
Funcgr.change_yield thy o CodegenFuncgr.check_consts rewrites thy; |
|
390 |
||
391 |
fun make_term thy f = |
|
392 |
Funcgr.change_yield thy o CodegenFuncgr.ensure_consts_term rewrites thy f; |
|
20600 | 393 |
|
22212 | 394 |
val init = Funcgr.init; |
395 |
||
396 |
end; (*functor*) |
|
397 |
||
398 |
structure CodegenFuncgr : CODEGEN_FUNCGR = |
|
399 |
struct |
|
400 |
||
401 |
open CodegenFuncgr; |
|
20600 | 402 |
|
403 |
end; (*struct*) |