1 (* Title: Tools/code/code_funcgr.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Retrieving, normalizing and structuring code equations in graph |
|
5 with explicit dependencies. |
|
6 |
|
7 Legacy. To be replaced by Tools/code/code_wellsorted.ML |
|
8 *) |
|
9 |
|
10 signature CODE_WELLSORTED = |
|
11 sig |
|
12 type T |
|
13 val eqns: T -> string -> (thm * bool) list |
|
14 val typ: T -> string -> (string * sort) list * typ |
|
15 val all: T -> string list |
|
16 val pretty: theory -> T -> Pretty.T |
|
17 val make: theory -> string list |
|
18 -> ((sort -> sort) * Sorts.algebra) * T |
|
19 val eval_conv: theory |
|
20 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm |
|
21 val eval_term: theory |
|
22 -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a |
|
23 val timing: bool ref |
|
24 end |
|
25 |
|
26 structure Code_Wellsorted : CODE_WELLSORTED = |
|
27 struct |
|
28 |
|
29 (** the graph type **) |
|
30 |
|
31 type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T; |
|
32 |
|
33 fun eqns funcgr = |
|
34 these o Option.map snd o try (Graph.get_node funcgr); |
|
35 |
|
36 fun typ funcgr = |
|
37 fst o Graph.get_node funcgr; |
|
38 |
|
39 fun all funcgr = Graph.keys funcgr; |
|
40 |
|
41 fun pretty thy funcgr = |
|
42 AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr) |
|
43 |> (map o apfst) (Code_Unit.string_of_const thy) |
|
44 |> sort (string_ord o pairself fst) |
|
45 |> map (fn (s, thms) => |
|
46 (Pretty.block o Pretty.fbreaks) ( |
|
47 Pretty.str s |
|
48 :: map (Display.pretty_thm o fst) thms |
|
49 )) |
|
50 |> Pretty.chunks; |
|
51 |
|
52 |
|
53 (** generic combinators **) |
|
54 |
|
55 fun fold_consts f thms = |
|
56 thms |
|
57 |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) |
|
58 |> (fold o fold_aterms) (fn Const c => f c | _ => I); |
|
59 |
|
60 fun consts_of (const, []) = [] |
|
61 | consts_of (const, thms as _ :: _) = |
|
62 let |
|
63 fun the_const (c, _) = if c = const then I else insert (op =) c |
|
64 in fold_consts the_const (map fst thms) [] end; |
|
65 |
|
66 fun insts_of thy algebra tys sorts = |
|
67 let |
|
68 fun class_relation (x, _) _ = x; |
|
69 fun type_constructor tyco xs class = |
|
70 (tyco, class) :: (maps o maps) fst xs; |
|
71 fun type_variable (TVar (_, sort)) = map (pair []) sort |
|
72 | type_variable (TFree (_, sort)) = map (pair []) sort; |
|
73 fun of_sort_deriv ty sort = |
|
74 Sorts.of_sort_derivation (Syntax.pp_global thy) algebra |
|
75 { class_relation = class_relation, type_constructor = type_constructor, |
|
76 type_variable = type_variable } |
|
77 (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*) |
|
78 in (flat o flat) (map2 of_sort_deriv tys sorts) end; |
|
79 |
|
80 fun meets_of thy algebra = |
|
81 let |
|
82 fun meet_of ty sort tab = |
|
83 Sorts.meet_sort algebra (ty, sort) tab |
|
84 handle Sorts.CLASS_ERROR _ => tab (*permissive!*); |
|
85 in fold2 meet_of end; |
|
86 |
|
87 |
|
88 (** graph algorithm **) |
|
89 |
|
90 val timing = ref false; |
|
91 |
|
92 local |
|
93 |
|
94 fun resort_thms thy algebra typ_of thms = |
|
95 let |
|
96 val cs = fold_consts (insert (op =)) thms []; |
|
97 fun meets (c, ty) = case typ_of c |
|
98 of SOME (vs, _) => |
|
99 meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs) |
|
100 | NONE => I; |
|
101 val tab = fold meets cs Vartab.empty; |
|
102 in map (Code_Unit.inst_thm thy tab) thms end; |
|
103 |
|
104 fun resort_eqnss thy algebra funcgr = |
|
105 let |
|
106 val typ_funcgr = try (fst o Graph.get_node funcgr); |
|
107 val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr); |
|
108 fun resort_rec typ_of (c, []) = (true, (c, [])) |
|
109 | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c) |
|
110 then (true, (c, thms)) |
|
111 else let |
|
112 val (_, (vs, ty)) = Code_Unit.head_eqn thy thm; |
|
113 val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms |
|
114 val (_, (vs', ty')) = Code_Unit.head_eqn thy thm'; (*FIXME simplify check*) |
|
115 in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end; |
|
116 fun resort_recs eqnss = |
|
117 let |
|
118 fun typ_of c = case these (AList.lookup (op =) eqnss c) |
|
119 of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn thy) thm |
|
120 | [] => NONE; |
|
121 val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss); |
|
122 val unchanged = fold (fn x => fn y => x andalso y) unchangeds true; |
|
123 in (unchanged, eqnss') end; |
|
124 fun resort_rec_until eqnss = |
|
125 let |
|
126 val (unchanged, eqnss') = resort_recs eqnss; |
|
127 in if unchanged then eqnss' else resort_rec_until eqnss' end; |
|
128 in map resort_dep #> resort_rec_until end; |
|
129 |
|
130 fun instances_of thy algebra insts = |
|
131 let |
|
132 val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy; |
|
133 fun all_classparams tyco class = |
|
134 these (try (#params o AxClass.get_info thy) class) |
|
135 |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco)) |
|
136 in |
|
137 Symtab.empty |
|
138 |> fold (fn (tyco, class) => |
|
139 Symtab.map_default (tyco, []) (insert (op =) class)) insts |
|
140 |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco) |
|
141 (Graph.all_succs thy_classes classes))) tab []) |
|
142 end; |
|
143 |
|
144 fun instances_of_consts thy algebra funcgr consts = |
|
145 let |
|
146 fun inst (cexpr as (c, ty)) = insts_of thy algebra |
|
147 (Sign.const_typargs thy (c, ty)) ((map snd o fst) (typ funcgr c)); |
|
148 in |
|
149 [] |
|
150 |> fold (fold (insert (op =)) o inst) consts |
|
151 |> instances_of thy algebra |
|
152 end; |
|
153 |
|
154 fun ensure_const' thy algebra funcgr const auxgr = |
|
155 if can (Graph.get_node funcgr) const |
|
156 then (NONE, auxgr) |
|
157 else if can (Graph.get_node auxgr) const |
|
158 then (SOME const, auxgr) |
|
159 else if is_some (Code.get_datatype_of_constr thy const) then |
|
160 auxgr |
|
161 |> Graph.new_node (const, []) |
|
162 |> pair (SOME const) |
|
163 else let |
|
164 val thms = Code.these_eqns thy const |
|
165 |> burrow_fst (Code_Unit.norm_args thy) |
|
166 |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var); |
|
167 val rhs = consts_of (const, thms); |
|
168 in |
|
169 auxgr |
|
170 |> Graph.new_node (const, thms) |
|
171 |> fold_map (ensure_const thy algebra funcgr) rhs |
|
172 |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const') |
|
173 | NONE => I) rhs') |
|
174 |> pair (SOME const) |
|
175 end |
|
176 and ensure_const thy algebra funcgr const = |
|
177 let |
|
178 val timeap = if !timing |
|
179 then Output.timeap_msg ("time for " ^ Code_Unit.string_of_const thy const) |
|
180 else I; |
|
181 in timeap (ensure_const' thy algebra funcgr const) end; |
|
182 |
|
183 fun merge_eqnss thy algebra raw_eqnss funcgr = |
|
184 let |
|
185 val eqnss = raw_eqnss |
|
186 |> resort_eqnss thy algebra funcgr |
|
187 |> filter_out (can (Graph.get_node funcgr) o fst); |
|
188 fun typ_eqn c [] = Code.default_typscheme thy c |
|
189 | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn thy) thm; |
|
190 fun add_eqns (const, thms) = |
|
191 Graph.new_node (const, (typ_eqn const thms, thms)); |
|
192 fun add_deps (eqns as (const, thms)) funcgr = |
|
193 let |
|
194 val deps = consts_of eqns; |
|
195 val insts = instances_of_consts thy algebra funcgr |
|
196 (fold_consts (insert (op =)) (map fst thms) []); |
|
197 in |
|
198 funcgr |
|
199 |> ensure_consts thy algebra insts |
|
200 |> fold (curry Graph.add_edge const) deps |
|
201 |> fold (curry Graph.add_edge const) insts |
|
202 end; |
|
203 in |
|
204 funcgr |
|
205 |> fold add_eqns eqnss |
|
206 |> fold add_deps eqnss |
|
207 end |
|
208 and ensure_consts thy algebra cs funcgr = |
|
209 let |
|
210 val auxgr = Graph.empty |
|
211 |> fold (snd oo ensure_const thy algebra funcgr) cs; |
|
212 in |
|
213 funcgr |
|
214 |> fold (merge_eqnss thy algebra) |
|
215 (map (AList.make (Graph.get_node auxgr)) |
|
216 (rev (Graph.strong_conn auxgr))) |
|
217 end; |
|
218 |
|
219 in |
|
220 |
|
221 (** retrieval interfaces **) |
|
222 |
|
223 val ensure_consts = ensure_consts; |
|
224 |
|
225 fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr = |
|
226 let |
|
227 val ct = cterm_of proto_ct; |
|
228 val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct); |
|
229 val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) (); |
|
230 fun consts_of t = |
|
231 fold_aterms (fn Const c_ty => cons c_ty | _ => I) t []; |
|
232 val algebra = Code.coregular_algebra thy; |
|
233 val thm = Code.preprocess_conv thy ct; |
|
234 val ct' = Thm.rhs_of thm; |
|
235 val t' = Thm.term_of ct'; |
|
236 val consts = map fst (consts_of t'); |
|
237 val funcgr' = ensure_consts thy algebra consts funcgr; |
|
238 val (t'', evaluator_funcgr) = evaluator t'; |
|
239 val consts' = consts_of t''; |
|
240 val dicts = instances_of_consts thy algebra funcgr' consts'; |
|
241 val funcgr'' = ensure_consts thy algebra dicts funcgr'; |
|
242 in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end; |
|
243 |
|
244 fun proto_eval_conv thy = |
|
245 let |
|
246 fun evaluator_lift evaluator thm1 funcgr = |
|
247 let |
|
248 val thm2 = evaluator funcgr; |
|
249 val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2); |
|
250 in |
|
251 Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ => |
|
252 error ("could not construct evaluation proof:\n" |
|
253 ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3]) |
|
254 end; |
|
255 in proto_eval thy I evaluator_lift end; |
|
256 |
|
257 fun proto_eval_term thy = |
|
258 let |
|
259 fun evaluator_lift evaluator _ funcgr = evaluator funcgr; |
|
260 in proto_eval thy (Thm.cterm_of thy) evaluator_lift end; |
|
261 |
|
262 end; (*local*) |
|
263 |
|
264 structure Funcgr = CodeDataFun |
|
265 ( |
|
266 type T = T; |
|
267 val empty = Graph.empty; |
|
268 fun purge _ cs funcgr = |
|
269 Graph.del_nodes ((Graph.all_preds funcgr |
|
270 o filter (can (Graph.get_node funcgr))) cs) funcgr; |
|
271 ); |
|
272 |
|
273 fun make thy = |
|
274 pair (Code.operational_algebra thy) |
|
275 o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy); |
|
276 |
|
277 fun eval_conv thy f = |
|
278 fst o Funcgr.change_yield thy o proto_eval_conv thy f; |
|
279 |
|
280 fun eval_term thy f = |
|
281 fst o Funcgr.change_yield thy o proto_eval_term thy f; |
|
282 |
|
283 |
|
284 (** diagnostic commands **) |
|
285 |
|
286 fun code_depgr thy consts = |
|
287 let |
|
288 val (_, gr) = make thy consts; |
|
289 val select = Graph.all_succs gr consts; |
|
290 in |
|
291 gr |
|
292 |> not (null consts) ? Graph.subgraph (member (op =) select) |
|
293 |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy)) |
|
294 end; |
|
295 |
|
296 fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy; |
|
297 |
|
298 fun code_deps thy consts = |
|
299 let |
|
300 val gr = code_depgr thy consts; |
|
301 fun mk_entry (const, (_, (_, parents))) = |
|
302 let |
|
303 val name = Code_Unit.string_of_const thy const; |
|
304 val nameparents = map (Code_Unit.string_of_const thy) parents; |
|
305 in { name = name, ID = name, dir = "", unfold = true, |
|
306 path = "", parents = nameparents } |
|
307 end; |
|
308 val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr []; |
|
309 in Present.display_graph prgr end; |
|
310 |
|
311 local |
|
312 |
|
313 structure P = OuterParse |
|
314 and K = OuterKeyword |
|
315 |
|
316 fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy; |
|
317 fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy; |
|
318 |
|
319 in |
|
320 |
|
321 val _ = |
|
322 OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag |
|
323 (Scan.repeat P.term_group |
|
324 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
325 o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
|
326 |
|
327 val _ = |
|
328 OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag |
|
329 (Scan.repeat P.term_group |
|
330 >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
|
331 o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
|
332 |
|
333 end; |
|
334 |
|
335 end; (*struct*) |
|