1 (* Title: Tools/code/code_funcgr.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Retrieving, well-sorting and structuring code equations in graph |
|
5 with explicit dependencies -- the waisenhaus algorithm. |
|
6 *) |
|
7 |
|
8 signature CODE_FUNCGR = |
|
9 sig |
|
10 type T |
|
11 val eqns: T -> string -> (thm * bool) list |
|
12 val typ: T -> string -> (string * sort) list * typ |
|
13 val all: T -> string list |
|
14 val pretty: theory -> T -> Pretty.T |
|
15 val make: theory -> string list |
|
16 -> ((sort -> sort) * Sorts.algebra) * T |
|
17 val eval_conv: theory |
|
18 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm |
|
19 val eval_term: theory |
|
20 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a |
|
21 end |
|
22 |
|
23 structure Code_Funcgr : CODE_FUNCGR = |
|
24 struct |
|
25 |
|
26 (** the graph type **) |
|
27 |
|
28 type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T; |
|
29 |
|
30 fun eqns funcgr = these o Option.map snd o try (Graph.get_node funcgr); |
|
31 fun typ funcgr = fst o Graph.get_node funcgr; |
|
32 fun all funcgr = Graph.keys funcgr; |
|
33 |
|
34 fun pretty thy funcgr = |
|
35 AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr) |
|
36 |> (map o apfst) (Code_Unit.string_of_const thy) |
|
37 |> sort (string_ord o pairself fst) |
|
38 |> map (fn (s, thms) => |
|
39 (Pretty.block o Pretty.fbreaks) ( |
|
40 Pretty.str s |
|
41 :: map (Display.pretty_thm o fst) thms |
|
42 )) |
|
43 |> Pretty.chunks; |
|
44 |
|
45 |
|
46 (** graph algorithm **) |
|
47 |
|
48 (* generic *) |
|
49 |
|
50 fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); |
|
51 |
|
52 fun complete_proper_sort thy = |
|
53 Sign.complete_sort thy #> filter (can (AxClass.get_info thy)); |
|
54 |
|
55 fun inst_params thy tyco class = |
|
56 map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) |
|
57 ((#params o AxClass.get_info thy) class); |
|
58 |
|
59 fun consts_of thy eqns = [] |> (fold o fold o fold_aterms) |
|
60 (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) |
|
61 (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); |
|
62 |
|
63 fun lhs_rhss_of thy c = |
|
64 let |
|
65 val eqns = Code.these_eqns thy c |
|
66 |> burrow_fst (Code_Unit.norm_args thy) |
|
67 |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var); |
|
68 val (lhs, _) = case eqns of [] => Code.default_typscheme thy c |
|
69 | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm; |
|
70 val rhss = consts_of thy eqns; |
|
71 in (lhs, rhss) end; |
|
72 |
|
73 |
|
74 (* data structures *) |
|
75 |
|
76 datatype const = Fun of string | Inst of class * string; |
|
77 |
|
78 fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2) |
|
79 | const_ord (Inst class_tyco1, Inst class_tyco2) = |
|
80 prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2) |
|
81 | const_ord (Fun _, Inst _) = LESS |
|
82 | const_ord (Inst _, Fun _) = GREATER; |
|
83 |
|
84 type var = const * int; |
|
85 |
|
86 structure Vargraph = |
|
87 GraphFun(type key = var val ord = prod_ord const_ord int_ord); |
|
88 |
|
89 datatype styp = Tyco of string * styp list | Var of var; |
|
90 |
|
91 type vardeps = const list * ((string * styp list) list * class list) Vargraph.T; |
|
92 |
|
93 |
|
94 (* computing instantiations -- FIXME does not consider existing things *) |
|
95 |
|
96 fun add_classes thy c_k new_classes vardeps = |
|
97 let |
|
98 val _ = tracing "add_classes"; |
|
99 val (styps, old_classes) = Vargraph.get_node (snd vardeps) c_k; |
|
100 val diff_classes = new_classes |> subtract (op =) old_classes; |
|
101 in if null diff_classes then vardeps |
|
102 else let |
|
103 val c_ks = Vargraph.imm_succs (snd vardeps) c_k |> insert (op =) c_k; |
|
104 in |
|
105 vardeps |
|
106 |> (apsnd o Vargraph.map_node c_k o apsnd) (append diff_classes) |
|
107 |> fold (fn styp => fold (add_typmatch_inst thy styp) new_classes) styps |
|
108 |> fold (fn c_k => add_classes thy c_k diff_classes) c_ks |
|
109 end end |
|
110 and add_styp thy c_k tyco_styps vardeps = |
|
111 let |
|
112 val _ = tracing "add_styp"; |
|
113 val (old_styps, classes) = Vargraph.get_node (snd vardeps) c_k; |
|
114 in if member (op =) old_styps tyco_styps then vardeps |
|
115 else |
|
116 vardeps |
|
117 |> (apsnd o Vargraph.map_node c_k o apfst) (cons tyco_styps) |
|
118 |> fold (add_typmatch_inst thy tyco_styps) classes |
|
119 end |
|
120 and add_dep thy c_k c_k' vardeps = |
|
121 let |
|
122 val _ = tracing ("add_dep " ^ makestring c_k ^ " -> " ^ makestring c_k'); |
|
123 val (_, classes) = Vargraph.get_node (snd vardeps) c_k; |
|
124 in |
|
125 vardeps |
|
126 |> add_classes thy c_k' classes |
|
127 |> apsnd (Vargraph.add_edge (c_k, c_k')) |
|
128 end |
|
129 and add_typmatch_inst thy (tyco, styps) class vardeps = if can (Sign.arity_sorts thy tyco) [class] |
|
130 then vardeps |
|
131 |> tap (fn _ => tracing "add_typmatch_inst") |
|
132 |> assert thy (Inst (class, tyco)) |
|
133 |> fold_index (fn (k, styp) => |
|
134 add_typmatch thy styp (Inst (class, tyco), k)) styps |
|
135 else vardeps (*permissive!*) |
|
136 and add_typmatch thy (Var c_k') c_k vardeps = |
|
137 vardeps |
|
138 |> tap (fn _ => tracing "add_typmatch (Inst)") |
|
139 |> add_dep thy c_k c_k' |
|
140 | add_typmatch thy (Tyco tyco_styps) c_k vardeps = |
|
141 vardeps |
|
142 |> tap (fn _ => tracing "add_typmatch (Tyco)") |
|
143 |> add_styp thy c_k tyco_styps |
|
144 and add_inst thy (class, tyco) vardeps = |
|
145 let |
|
146 val _ = tracing ("add_inst " ^ tyco ^ "::" ^ class); |
|
147 val superclasses = complete_proper_sort thy |
|
148 (Sign.super_classes thy class); |
|
149 val classess = map (complete_proper_sort thy) |
|
150 (Sign.arity_sorts thy tyco [class]); |
|
151 val inst_params = inst_params thy tyco class; |
|
152 (*FIXME also consider existing things here*) |
|
153 in |
|
154 vardeps |
|
155 |> fold (fn superclass => assert thy (Inst (superclass, tyco))) superclasses |
|
156 |> fold (assert thy o Fun) inst_params |
|
157 |> fold_index (fn (k, classes) => |
|
158 apsnd (Vargraph.default_node ((Inst (class, tyco), k), ([] ,[]))) |
|
159 #> add_classes thy (Inst (class, tyco), k) classes |
|
160 #> fold (fn superclass => |
|
161 add_dep thy (Inst (superclass, tyco), k) |
|
162 (Inst (class, tyco), k)) superclasses |
|
163 #> fold (fn inst_param => |
|
164 add_dep thy (Fun inst_param, k) |
|
165 (Inst (class, tyco), k) |
|
166 ) inst_params |
|
167 ) classess |
|
168 end |
|
169 and add_const thy c vardeps = |
|
170 let |
|
171 val _ = tracing "add_const"; |
|
172 val (lhs, rhss) = lhs_rhss_of thy c; |
|
173 (*FIXME build lhs_rhss_of such that it points to existing graph if possible*) |
|
174 fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys) |
|
175 | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs); |
|
176 val rhss' = (map o apsnd o map) styp_of rhss; |
|
177 in |
|
178 vardeps |
|
179 |> fold_index (fn (k, (_, sort)) => |
|
180 apsnd (Vargraph.default_node ((Fun c, k), ([] ,[]))) |
|
181 #> add_classes thy (Fun c, k) (complete_proper_sort thy sort)) lhs |
|
182 |> fold (assert thy o Fun o fst) rhss' |
|
183 |> fold (fn (c', styps) => fold_index (fn (k', styp) => |
|
184 add_typmatch thy styp (Fun c', k')) styps) rhss' |
|
185 end |
|
186 and assert thy c (vardeps as (asserted, _)) = |
|
187 if member (op =) asserted c then vardeps |
|
188 else case c |
|
189 of Fun const => vardeps |> apfst (cons c) |> add_const thy const |
|
190 | Inst inst => vardeps |> apfst (cons c) |> add_inst thy inst; |
|
191 |
|
192 |
|
193 (* applying instantiations *) |
|
194 |
|
195 fun dicts_of thy (proj_sort, algebra) (T, sort) = |
|
196 let |
|
197 fun class_relation (x, _) _ = x; |
|
198 fun type_constructor tyco xs class = |
|
199 inst_params thy tyco class @ (maps o maps) fst xs; |
|
200 fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort); |
|
201 in |
|
202 flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra |
|
203 { class_relation = class_relation, type_constructor = type_constructor, |
|
204 type_variable = type_variable } (T, proj_sort sort) |
|
205 handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) |
|
206 end; |
|
207 |
|
208 fun algebra_of thy vardeps = |
|
209 let |
|
210 val pp = Syntax.pp_global thy; |
|
211 val thy_algebra = Sign.classes_of thy; |
|
212 val is_proper = can (AxClass.get_info thy); |
|
213 val classrels = Sorts.classrels_of thy_algebra |
|
214 |> filter (is_proper o fst) |
|
215 |> (map o apsnd) (filter is_proper); |
|
216 val instances = Sorts.instances_of thy_algebra |
|
217 |> filter (is_proper o snd); |
|
218 fun add_class (class, superclasses) algebra = |
|
219 Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra; |
|
220 val arity_constraints = Vargraph.fold (fn ((Fun _, _), _) => I |
|
221 | ((Inst (class, tyco), k), ((_, classes), _)) => |
|
222 AList.map_default (op =) |
|
223 ((tyco, class), replicate (Sign.arity_number thy tyco) []) |
|
224 (nth_map k (K classes))) vardeps []; |
|
225 fun add_arity (tyco, class) algebra = |
|
226 case AList.lookup (op =) arity_constraints (tyco, class) |
|
227 of SOME sorts => (tracing (Pretty.output (Syntax.pretty_arity (ProofContext.init thy) |
|
228 (tyco, sorts, [class]))); |
|
229 Sorts.add_arities pp |
|
230 (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra) |
|
231 | NONE => if Sign.arity_number thy tyco = 0 |
|
232 then Sorts.add_arities pp (tyco, [(class, [])]) algebra |
|
233 else algebra; |
|
234 in |
|
235 Sorts.empty_algebra |
|
236 |> fold add_class classrels |
|
237 |> fold add_arity instances |
|
238 end; |
|
239 |
|
240 fun add_eqs thy (proj_sort, algebra) vardeps c gr = |
|
241 let |
|
242 val eqns = Code.these_eqns thy c |
|
243 |> burrow_fst (Code_Unit.norm_args thy) |
|
244 |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var); |
|
245 val (vs, _) = case eqns of [] => Code.default_typscheme thy c |
|
246 | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm; |
|
247 val inst = Vartab.empty |> fold_index (fn (k, (v, _)) => |
|
248 Vartab.update ((v, 0), snd (Vargraph.get_node vardeps (Fun c, k)))) vs; |
|
249 val eqns' = eqns |
|
250 |> (map o apfst) (Code_Unit.inst_thm thy inst); |
|
251 val tyscm = case eqns' of [] => Code.default_typscheme thy c |
|
252 | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm; |
|
253 val _ = tracing ("tyscm " ^ makestring (map snd (fst tyscm))); |
|
254 val rhss = consts_of thy eqns'; |
|
255 in |
|
256 gr |
|
257 |> Graph.new_node (c, (tyscm, eqns')) |
|
258 |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' |
|
259 #-> (fn (vs, _) => |
|
260 fold2 (ensure_match thy (proj_sort, algebra) vardeps c) Ts (map snd vs))) rhss |
|
261 |> pair tyscm |
|
262 end |
|
263 and ensure_match thy (proj_sort, algebra) vardeps c T sort gr = |
|
264 gr |
|
265 |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' #> snd) |
|
266 (dicts_of thy (proj_sort, algebra) (T, proj_sort sort)) |
|
267 and ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' gr = |
|
268 gr |
|
269 |> ensure_eqs thy (proj_sort, algebra) vardeps c' |
|
270 ||> Graph.add_edge (c, c') |
|
271 and ensure_eqs thy (proj_sort, algebra) vardeps c gr = |
|
272 case try (Graph.get_node gr) c |
|
273 of SOME (tyscm, _) => (tyscm, gr) |
|
274 | NONE => add_eqs thy (proj_sort, algebra) vardeps c gr; |
|
275 |
|
276 fun extend_graph thy cs gr = |
|
277 let |
|
278 val _ = tracing ("extending with " ^ commas cs); |
|
279 val _ = tracing "obtaining instantiations"; |
|
280 val (_, vardeps) = fold (assert thy o Fun) cs ([], Vargraph.empty) |
|
281 val _ = tracing "obtaining algebra"; |
|
282 val algebra = algebra_of thy vardeps; |
|
283 val _ = tracing "obtaining equations"; |
|
284 val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra; |
|
285 val (_, gr') = fold_map (ensure_eqs thy (proj_sort, algebra) vardeps) cs gr; |
|
286 val _ = tracing "sort projection"; |
|
287 in ((proj_sort, algebra), gr') end; |
|
288 |
|
289 |
|
290 (** retrieval interfaces **) |
|
291 |
|
292 fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr = |
|
293 let |
|
294 val ct = cterm_of proto_ct; |
|
295 val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct); |
|
296 val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); |
|
297 fun consts_of t = |
|
298 fold_aterms (fn Const c_ty => cons c_ty | _ => I) t []; |
|
299 val thm = Code.preprocess_conv thy ct; |
|
300 val ct' = Thm.rhs_of thm; |
|
301 val t' = Thm.term_of ct'; |
|
302 val consts = map fst (consts_of t'); |
|
303 val (algebra', funcgr') = extend_graph thy consts funcgr; |
|
304 val (t'', evaluator_funcgr) = evaluator t'; |
|
305 val consts' = consts_of t''; |
|
306 val const_matches = fold (fn (c, ty) => |
|
307 insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' []; |
|
308 val typ_matches = maps (fn (tys, c) => tys ~~ map snd (fst (fst (Graph.get_node funcgr' c)))) |
|
309 const_matches; |
|
310 val dicts = maps (dicts_of thy algebra') typ_matches; |
|
311 val (algebra'', funcgr'') = extend_graph thy dicts funcgr'; |
|
312 in (evaluator_lift (evaluator_funcgr algebra'') thm funcgr'', funcgr'') end; |
|
313 |
|
314 fun proto_eval_conv thy = |
|
315 let |
|
316 fun evaluator_lift evaluator thm1 funcgr = |
|
317 let |
|
318 val thm2 = evaluator funcgr; |
|
319 val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2); |
|
320 in |
|
321 Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => |
|
322 error ("could not construct evaluation proof:\n" |
|
323 ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) |
|
324 end; |
|
325 in proto_eval thy I evaluator_lift end; |
|
326 |
|
327 fun proto_eval_term thy = |
|
328 let |
|
329 fun evaluator_lift evaluator _ funcgr = evaluator funcgr; |
|
330 in proto_eval thy (Thm.cterm_of thy) evaluator_lift end; |
|
331 |
|
332 structure Funcgr = CodeDataFun |
|
333 ( |
|
334 type T = T; |
|
335 val empty = Graph.empty; |
|
336 fun purge _ cs funcgr = |
|
337 Graph.del_nodes ((Graph.all_preds funcgr |
|
338 o filter (can (Graph.get_node funcgr))) cs) funcgr; |
|
339 ); |
|
340 |
|
341 fun make thy = Funcgr.change_yield thy o extend_graph thy; |
|
342 |
|
343 fun eval_conv thy f = |
|
344 fst o Funcgr.change_yield thy o proto_eval_conv thy f; |
|
345 |
|
346 fun eval_term thy f = |
|
347 fst o Funcgr.change_yield thy o proto_eval_term thy f; |
|
348 |
|
349 |
|
350 (** diagnostic commands **) |
|
351 |
|
352 fun code_depgr thy consts = |
|
353 let |
|
354 val (_, gr) = make thy consts; |
|
355 val select = Graph.all_succs gr consts; |
|
356 in |
|
357 gr |
|
358 |> not (null consts) ? Graph.subgraph (member (op =) select) |
|
359 |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy)) |
|
360 end; |
|
361 |
|
362 fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy; |
|
363 |
|
364 fun code_deps thy consts = |
|
365 let |
|
366 val gr = code_depgr thy consts; |
|
367 fun mk_entry (const, (_, (_, parents))) = |
|
368 let |
|
369 val name = Code_Unit.string_of_const thy const; |
|
370 val nameparents = map (Code_Unit.string_of_const thy) parents; |
|
371 in { name = name, ID = name, dir = "", unfold = true, |
|
372 path = "", parents = nameparents } |
|
373 end; |
|
374 val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr []; |
|
375 in Present.display_graph prgr end; |
|
376 |
|
377 local |
|
378 |
|
379 structure P = OuterParse |
|
380 and K = OuterKeyword |
|
381 |
|
382 fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy; |
|
383 fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy; |
|
384 |
|
385 in |
|
386 |
|
387 val _ = |
|
388 OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag |
|
389 (Scan.repeat P.term_group |
|
390 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
391 o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
|
392 |
|
393 val _ = |
|
394 OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag |
|
395 (Scan.repeat P.term_group |
|
396 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
397 o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
|
398 |
|
399 end; |
|
400 |
|
401 end; (*struct*) |
|