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