haftmann@37743
|
1 |
(* Title: Tools/Code/code_preproc.ML
|
haftmann@29947
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@29947
|
3 |
|
haftmann@31125
|
4 |
Preprocessing code equations into a well-sorted system
|
haftmann@31125
|
5 |
in a graph with explicit dependencies.
|
haftmann@29947
|
6 |
*)
|
haftmann@29947
|
7 |
|
haftmann@31125
|
8 |
signature CODE_PREPROC =
|
haftmann@29947
|
9 |
sig
|
haftmann@31125
|
10 |
val map_pre: (simpset -> simpset) -> theory -> theory
|
haftmann@31125
|
11 |
val map_post: (simpset -> simpset) -> theory -> theory
|
haftmann@32064
|
12 |
val add_unfold: thm -> theory -> theory
|
haftmann@31125
|
13 |
val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
|
haftmann@31125
|
14 |
val del_functrans: string -> theory -> theory
|
haftmann@31125
|
15 |
val simple_functrans: (theory -> thm list -> thm list option)
|
haftmann@31125
|
16 |
-> theory -> (thm * bool) list -> (thm * bool) list option
|
haftmann@34893
|
17 |
val preprocess_functrans: theory -> (thm * bool) list -> (thm * bool) list
|
haftmann@31125
|
18 |
val print_codeproc: theory -> unit
|
haftmann@31125
|
19 |
|
haftmann@30947
|
20 |
type code_algebra
|
haftmann@30947
|
21 |
type code_graph
|
haftmann@34891
|
22 |
val cert: code_graph -> string -> Code.cert
|
haftmann@32873
|
23 |
val sortargs: code_graph -> string -> sort list
|
haftmann@30947
|
24 |
val all: code_graph -> string list
|
haftmann@30947
|
25 |
val pretty: theory -> code_graph -> Pretty.T
|
haftmann@30947
|
26 |
val obtain: theory -> string list -> term list -> code_algebra * code_graph
|
haftmann@32101
|
27 |
val eval_conv: theory
|
haftmann@30947
|
28 |
-> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
|
haftmann@32101
|
29 |
val eval: theory -> ((term -> term) -> 'a -> 'a)
|
haftmann@30947
|
30 |
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
|
haftmann@37417
|
31 |
val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
|
haftmann@31125
|
32 |
|
haftmann@31125
|
33 |
val setup: theory -> theory
|
haftmann@29947
|
34 |
end
|
haftmann@29947
|
35 |
|
haftmann@31125
|
36 |
structure Code_Preproc : CODE_PREPROC =
|
haftmann@29947
|
37 |
struct
|
haftmann@29947
|
38 |
|
haftmann@31125
|
39 |
(** preprocessor administration **)
|
haftmann@31125
|
40 |
|
haftmann@31125
|
41 |
(* theory data *)
|
haftmann@31125
|
42 |
|
haftmann@31125
|
43 |
datatype thmproc = Thmproc of {
|
haftmann@31125
|
44 |
pre: simpset,
|
haftmann@31125
|
45 |
post: simpset,
|
haftmann@31125
|
46 |
functrans: (string * (serial * (theory -> (thm * bool) list -> (thm * bool) list option))) list
|
haftmann@31125
|
47 |
};
|
haftmann@31125
|
48 |
|
haftmann@31599
|
49 |
fun make_thmproc ((pre, post), functrans) =
|
haftmann@31125
|
50 |
Thmproc { pre = pre, post = post, functrans = functrans };
|
haftmann@31125
|
51 |
fun map_thmproc f (Thmproc { pre, post, functrans }) =
|
haftmann@31599
|
52 |
make_thmproc (f ((pre, post), functrans));
|
haftmann@31125
|
53 |
fun merge_thmproc (Thmproc { pre = pre1, post = post1, functrans = functrans1 },
|
haftmann@31125
|
54 |
Thmproc { pre = pre2, post = post2, functrans = functrans2 }) =
|
haftmann@31125
|
55 |
let
|
haftmann@31125
|
56 |
val pre = Simplifier.merge_ss (pre1, pre2);
|
haftmann@31125
|
57 |
val post = Simplifier.merge_ss (post1, post2);
|
haftmann@34891
|
58 |
val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2)
|
haftmann@34891
|
59 |
handle AList.DUP => error ("Duplicate function transformer");
|
haftmann@31599
|
60 |
in make_thmproc ((pre, post), functrans) end;
|
haftmann@31125
|
61 |
|
wenzelm@33522
|
62 |
structure Code_Preproc_Data = Theory_Data
|
haftmann@31125
|
63 |
(
|
haftmann@31125
|
64 |
type T = thmproc;
|
haftmann@31599
|
65 |
val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
|
wenzelm@33522
|
66 |
val extend = I;
|
wenzelm@33522
|
67 |
val merge = merge_thmproc;
|
haftmann@31125
|
68 |
);
|
haftmann@31125
|
69 |
|
haftmann@31125
|
70 |
fun the_thmproc thy = case Code_Preproc_Data.get thy
|
haftmann@31125
|
71 |
of Thmproc x => x;
|
haftmann@31125
|
72 |
|
haftmann@31125
|
73 |
fun delete_force msg key xs =
|
haftmann@31125
|
74 |
if AList.defined (op =) xs key then AList.delete (op =) key xs
|
haftmann@31125
|
75 |
else error ("No such " ^ msg ^ ": " ^ quote key);
|
haftmann@31125
|
76 |
|
haftmann@32544
|
77 |
fun map_data f = Code.purge_data
|
haftmann@32544
|
78 |
#> (Code_Preproc_Data.map o map_thmproc) f;
|
haftmann@31125
|
79 |
|
haftmann@32064
|
80 |
val map_pre_post = map_data o apfst;
|
haftmann@32064
|
81 |
val map_pre = map_pre_post o apfst;
|
haftmann@32064
|
82 |
val map_post = map_pre_post o apsnd;
|
haftmann@31125
|
83 |
|
haftmann@32064
|
84 |
val add_unfold = map_pre o MetaSimplifier.add_simp;
|
haftmann@32064
|
85 |
val del_unfold = map_pre o MetaSimplifier.del_simp;
|
haftmann@31125
|
86 |
val add_post = map_post o MetaSimplifier.add_simp;
|
haftmann@31125
|
87 |
val del_post = map_post o MetaSimplifier.del_simp;
|
haftmann@32064
|
88 |
|
haftmann@32064
|
89 |
fun add_unfold_post raw_thm thy =
|
haftmann@32064
|
90 |
let
|
wenzelm@36633
|
91 |
val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm;
|
haftmann@32064
|
92 |
val thm_sym = Thm.symmetric thm;
|
haftmann@32064
|
93 |
in
|
haftmann@32064
|
94 |
thy |> map_pre_post (fn (pre, post) =>
|
haftmann@32064
|
95 |
(pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym))
|
haftmann@32064
|
96 |
end;
|
haftmann@32064
|
97 |
|
haftmann@31125
|
98 |
fun add_functrans (name, f) = (map_data o apsnd)
|
haftmann@31125
|
99 |
(AList.update (op =) (name, (serial (), f)));
|
haftmann@31125
|
100 |
|
haftmann@31125
|
101 |
fun del_functrans name = (map_data o apsnd)
|
haftmann@31125
|
102 |
(delete_force "function transformer" name);
|
haftmann@31125
|
103 |
|
haftmann@31125
|
104 |
|
haftmann@31125
|
105 |
(* post- and preprocessing *)
|
haftmann@31125
|
106 |
|
haftmann@33908
|
107 |
fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
|
haftmann@31125
|
108 |
|
haftmann@34891
|
109 |
fun eqn_conv conv ct =
|
haftmann@31957
|
110 |
let
|
haftmann@31957
|
111 |
fun lhs_conv ct = if can Thm.dest_comb ct
|
haftmann@31957
|
112 |
then Conv.combination_conv lhs_conv conv ct
|
haftmann@31957
|
113 |
else Conv.all_conv ct;
|
haftmann@34891
|
114 |
in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
|
haftmann@31957
|
115 |
|
haftmann@31957
|
116 |
val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
|
haftmann@31957
|
117 |
|
haftmann@31125
|
118 |
fun term_of_conv thy f =
|
haftmann@31125
|
119 |
Thm.cterm_of thy
|
haftmann@31125
|
120 |
#> f
|
haftmann@31125
|
121 |
#> Thm.prop_of
|
haftmann@31125
|
122 |
#> Logic.dest_equals
|
haftmann@31125
|
123 |
#> snd;
|
haftmann@31125
|
124 |
|
haftmann@34893
|
125 |
fun preprocess_functrans thy =
|
haftmann@34893
|
126 |
let
|
haftmann@34893
|
127 |
val functrans = (map (fn (_, (_, f)) => f thy) o #functrans
|
haftmann@34893
|
128 |
o the_thmproc) thy;
|
haftmann@34893
|
129 |
in perhaps (perhaps_loop (perhaps_apply functrans)) end;
|
haftmann@34893
|
130 |
|
haftmann@34893
|
131 |
fun preprocess thy =
|
haftmann@31125
|
132 |
let
|
wenzelm@35232
|
133 |
val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
|
haftmann@31125
|
134 |
in
|
haftmann@34893
|
135 |
preprocess_functrans thy
|
haftmann@34893
|
136 |
#> (map o apfst) (rewrite_eqn pre)
|
haftmann@31125
|
137 |
end;
|
haftmann@31125
|
138 |
|
haftmann@31125
|
139 |
fun preprocess_conv thy ct =
|
haftmann@31125
|
140 |
let
|
wenzelm@35232
|
141 |
val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
|
haftmann@31125
|
142 |
in
|
haftmann@31125
|
143 |
ct
|
haftmann@31125
|
144 |
|> Simplifier.rewrite pre
|
haftmann@33908
|
145 |
|> trans_conv_rule (AxClass.unoverload_conv thy)
|
haftmann@31125
|
146 |
end;
|
haftmann@31125
|
147 |
|
haftmann@31125
|
148 |
fun postprocess_conv thy ct =
|
haftmann@31125
|
149 |
let
|
wenzelm@35232
|
150 |
val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
|
haftmann@31125
|
151 |
in
|
haftmann@31125
|
152 |
ct
|
haftmann@31125
|
153 |
|> AxClass.overload_conv thy
|
haftmann@33908
|
154 |
|> trans_conv_rule (Simplifier.rewrite post)
|
haftmann@31125
|
155 |
end;
|
haftmann@31125
|
156 |
|
haftmann@32544
|
157 |
fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
|
haftmann@31125
|
158 |
|
haftmann@31125
|
159 |
fun print_codeproc thy =
|
haftmann@31125
|
160 |
let
|
wenzelm@36633
|
161 |
val ctxt = ProofContext.init_global thy;
|
haftmann@31125
|
162 |
val pre = (#pre o the_thmproc) thy;
|
haftmann@31125
|
163 |
val post = (#post o the_thmproc) thy;
|
haftmann@31125
|
164 |
val functrans = (map fst o #functrans o the_thmproc) thy;
|
haftmann@31125
|
165 |
in
|
haftmann@31125
|
166 |
(Pretty.writeln o Pretty.chunks) [
|
haftmann@31125
|
167 |
Pretty.block [
|
haftmann@31125
|
168 |
Pretty.str "preprocessing simpset:",
|
haftmann@31125
|
169 |
Pretty.fbrk,
|
haftmann@31125
|
170 |
Simplifier.pretty_ss ctxt pre
|
haftmann@31125
|
171 |
],
|
haftmann@31125
|
172 |
Pretty.block [
|
haftmann@31125
|
173 |
Pretty.str "postprocessing simpset:",
|
haftmann@31125
|
174 |
Pretty.fbrk,
|
haftmann@31125
|
175 |
Simplifier.pretty_ss ctxt post
|
haftmann@31125
|
176 |
],
|
haftmann@31125
|
177 |
Pretty.block (
|
haftmann@31125
|
178 |
Pretty.str "function transformers:"
|
haftmann@31125
|
179 |
:: Pretty.fbrk
|
haftmann@31125
|
180 |
:: (Pretty.fbreaks o map Pretty.str) functrans
|
haftmann@31125
|
181 |
)
|
haftmann@31125
|
182 |
]
|
haftmann@31125
|
183 |
end;
|
haftmann@31125
|
184 |
|
haftmann@31125
|
185 |
fun simple_functrans f thy eqns = case f thy (map fst eqns)
|
haftmann@31125
|
186 |
of SOME thms' => SOME (map (rpair (forall snd eqns)) thms')
|
haftmann@31125
|
187 |
| NONE => NONE;
|
haftmann@31125
|
188 |
|
haftmann@31125
|
189 |
|
haftmann@31125
|
190 |
(** sort algebra and code equation graph types **)
|
haftmann@29947
|
191 |
|
haftmann@30947
|
192 |
type code_algebra = (sort -> sort) * Sorts.algebra;
|
haftmann@34891
|
193 |
type code_graph = ((string * sort) list * Code.cert) Graph.T;
|
haftmann@29947
|
194 |
|
haftmann@34891
|
195 |
fun cert eqngr = snd o Graph.get_node eqngr;
|
haftmann@34891
|
196 |
fun sortargs eqngr = map snd o fst o Graph.get_node eqngr;
|
haftmann@29947
|
197 |
fun all eqngr = Graph.keys eqngr;
|
haftmann@29947
|
198 |
|
haftmann@29947
|
199 |
fun pretty thy eqngr =
|
haftmann@29947
|
200 |
AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
|
haftmann@31156
|
201 |
|> (map o apfst) (Code.string_of_const thy)
|
haftmann@29947
|
202 |
|> sort (string_ord o pairself fst)
|
haftmann@34895
|
203 |
|> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
|
haftmann@29947
|
204 |
|> Pretty.chunks;
|
haftmann@29947
|
205 |
|
haftmann@29947
|
206 |
|
haftmann@29947
|
207 |
(** the Waisenhaus algorithm **)
|
haftmann@29947
|
208 |
|
haftmann@29947
|
209 |
(* auxiliary *)
|
haftmann@29947
|
210 |
|
haftmann@30942
|
211 |
fun is_proper_class thy = can (AxClass.get_info thy);
|
haftmann@30942
|
212 |
|
haftmann@29947
|
213 |
fun complete_proper_sort thy =
|
haftmann@30942
|
214 |
Sign.complete_sort thy #> filter (is_proper_class thy);
|
haftmann@29947
|
215 |
|
haftmann@29966
|
216 |
fun inst_params thy tyco =
|
haftmann@29947
|
217 |
map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
|
haftmann@29966
|
218 |
o maps (#params o AxClass.get_info thy);
|
haftmann@29947
|
219 |
|
haftmann@29947
|
220 |
|
haftmann@29947
|
221 |
(* data structures *)
|
haftmann@29947
|
222 |
|
haftmann@29947
|
223 |
datatype const = Fun of string | Inst of class * string;
|
haftmann@29947
|
224 |
|
haftmann@29947
|
225 |
fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
|
haftmann@29947
|
226 |
| const_ord (Inst class_tyco1, Inst class_tyco2) =
|
haftmann@29947
|
227 |
prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
|
haftmann@29947
|
228 |
| const_ord (Fun _, Inst _) = LESS
|
haftmann@29947
|
229 |
| const_ord (Inst _, Fun _) = GREATER;
|
haftmann@29947
|
230 |
|
haftmann@29947
|
231 |
type var = const * int;
|
haftmann@29947
|
232 |
|
haftmann@29947
|
233 |
structure Vargraph =
|
wenzelm@31972
|
234 |
Graph(type key = var val ord = prod_ord const_ord int_ord);
|
haftmann@29947
|
235 |
|
haftmann@29991
|
236 |
datatype styp = Tyco of string * styp list | Var of var | Free;
|
haftmann@29947
|
237 |
|
haftmann@29991
|
238 |
fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
|
haftmann@29991
|
239 |
| styp_of c_lhs (TFree (v, _)) = case c_lhs
|
haftmann@29991
|
240 |
of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
|
haftmann@29991
|
241 |
| NONE => Free;
|
haftmann@29947
|
242 |
|
haftmann@29991
|
243 |
type vardeps_data = ((string * styp list) list * class list) Vargraph.T
|
haftmann@34891
|
244 |
* (((string * sort) list * Code.cert) Symtab.table
|
haftmann@29991
|
245 |
* (class * string) list);
|
haftmann@29991
|
246 |
|
haftmann@29991
|
247 |
val empty_vardeps_data : vardeps_data =
|
haftmann@29991
|
248 |
(Vargraph.empty, (Symtab.empty, []));
|
haftmann@29991
|
249 |
|
haftmann@30876
|
250 |
|
haftmann@29991
|
251 |
(* retrieving equations and instances from the background context *)
|
haftmann@29947
|
252 |
|
haftmann@29947
|
253 |
fun obtain_eqns thy eqngr c =
|
haftmann@29947
|
254 |
case try (Graph.get_node eqngr) c
|
haftmann@34891
|
255 |
of SOME (lhs, cert) => ((lhs, []), cert)
|
haftmann@29947
|
256 |
| NONE => let
|
haftmann@34891
|
257 |
val cert = Code.get_cert thy (preprocess thy) c;
|
haftmann@35224
|
258 |
val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
|
haftmann@34891
|
259 |
in ((lhs, rhss), cert) end;
|
haftmann@29947
|
260 |
|
haftmann@29947
|
261 |
fun obtain_instance thy arities (inst as (class, tyco)) =
|
haftmann@29947
|
262 |
case AList.lookup (op =) arities inst
|
haftmann@29947
|
263 |
of SOME classess => (classess, ([], []))
|
haftmann@29947
|
264 |
| NONE => let
|
haftmann@29966
|
265 |
val all_classes = complete_proper_sort thy [class];
|
haftmann@37359
|
266 |
val super_classes = remove (op =) class all_classes;
|
haftmann@29947
|
267 |
val classess = map (complete_proper_sort thy)
|
haftmann@29947
|
268 |
(Sign.arity_sorts thy tyco [class]);
|
haftmann@29966
|
269 |
val inst_params = inst_params thy tyco all_classes;
|
haftmann@37359
|
270 |
in (classess, (super_classes, inst_params)) end;
|
haftmann@29947
|
271 |
|
haftmann@29991
|
272 |
|
haftmann@29991
|
273 |
(* computing instantiations *)
|
haftmann@29991
|
274 |
|
haftmann@29947
|
275 |
fun add_classes thy arities eqngr c_k new_classes vardeps_data =
|
haftmann@29947
|
276 |
let
|
haftmann@29947
|
277 |
val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
|
haftmann@29947
|
278 |
val diff_classes = new_classes |> subtract (op =) old_classes;
|
haftmann@29947
|
279 |
in if null diff_classes then vardeps_data
|
haftmann@29947
|
280 |
else let
|
haftmann@29947
|
281 |
val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
|
haftmann@29947
|
282 |
in
|
haftmann@29947
|
283 |
vardeps_data
|
haftmann@29947
|
284 |
|> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
|
haftmann@31125
|
285 |
|> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
|
haftmann@29947
|
286 |
|> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
|
haftmann@29947
|
287 |
end end
|
haftmann@37359
|
288 |
and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
|
haftmann@29947
|
289 |
let
|
haftmann@37359
|
290 |
val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
|
haftmann@37359
|
291 |
in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
|
haftmann@29947
|
292 |
else
|
haftmann@29947
|
293 |
vardeps_data
|
haftmann@37359
|
294 |
|> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
|
haftmann@37359
|
295 |
|> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
|
haftmann@29947
|
296 |
end
|
haftmann@29947
|
297 |
and add_dep thy arities eqngr c_k c_k' vardeps_data =
|
haftmann@29947
|
298 |
let
|
haftmann@29947
|
299 |
val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
|
haftmann@29947
|
300 |
in
|
haftmann@29947
|
301 |
vardeps_data
|
haftmann@29947
|
302 |
|> add_classes thy arities eqngr c_k' classes
|
haftmann@29947
|
303 |
|> apfst (Vargraph.add_edge (c_k, c_k'))
|
haftmann@29947
|
304 |
end
|
haftmann@31125
|
305 |
and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
|
haftmann@29947
|
306 |
if can (Sign.arity_sorts thy tyco) [class]
|
haftmann@29947
|
307 |
then vardeps_data
|
haftmann@31125
|
308 |
|> ensure_inst thy arities eqngr (class, tyco)
|
haftmann@29947
|
309 |
|> fold_index (fn (k, styp) =>
|
haftmann@31125
|
310 |
ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
|
haftmann@29947
|
311 |
else vardeps_data (*permissive!*)
|
haftmann@31125
|
312 |
and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
|
haftmann@29991
|
313 |
if member (op =) insts inst then vardeps_data
|
haftmann@29991
|
314 |
else let
|
haftmann@37359
|
315 |
val (classess, (super_classes, inst_params)) =
|
haftmann@29947
|
316 |
obtain_instance thy arities inst;
|
haftmann@29947
|
317 |
in
|
haftmann@29947
|
318 |
vardeps_data
|
haftmann@29991
|
319 |
|> (apsnd o apsnd) (insert (op =) inst)
|
haftmann@30020
|
320 |
|> fold_index (fn (k, _) =>
|
haftmann@30020
|
321 |
apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
|
haftmann@37359
|
322 |
|> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
|
haftmann@31125
|
323 |
|> fold (ensure_fun thy arities eqngr) inst_params
|
haftmann@29947
|
324 |
|> fold_index (fn (k, classes) =>
|
haftmann@30012
|
325 |
add_classes thy arities eqngr (Inst (class, tyco), k) classes
|
haftmann@37359
|
326 |
#> fold (fn super_class =>
|
haftmann@37359
|
327 |
add_dep thy arities eqngr (Inst (super_class, tyco), k)
|
haftmann@37359
|
328 |
(Inst (class, tyco), k)) super_classes
|
haftmann@29947
|
329 |
#> fold (fn inst_param =>
|
haftmann@29947
|
330 |
add_dep thy arities eqngr (Fun inst_param, k)
|
haftmann@29947
|
331 |
(Inst (class, tyco), k)
|
haftmann@29947
|
332 |
) inst_params
|
haftmann@29947
|
333 |
) classess
|
haftmann@29947
|
334 |
end
|
haftmann@31125
|
335 |
and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
|
haftmann@29991
|
336 |
vardeps_data
|
haftmann@29991
|
337 |
|> add_styp thy arities eqngr c_k tyco_styps
|
haftmann@31125
|
338 |
| ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
|
haftmann@29991
|
339 |
vardeps_data
|
haftmann@29991
|
340 |
|> add_dep thy arities eqngr c_k c_k'
|
haftmann@31125
|
341 |
| ensure_typmatch thy arities eqngr Free c_k vardeps_data =
|
haftmann@29991
|
342 |
vardeps_data
|
haftmann@31125
|
343 |
and ensure_rhs thy arities eqngr (c', styps) vardeps_data =
|
haftmann@29991
|
344 |
vardeps_data
|
haftmann@31125
|
345 |
|> ensure_fun thy arities eqngr c'
|
haftmann@29991
|
346 |
|> fold_index (fn (k, styp) =>
|
haftmann@31125
|
347 |
ensure_typmatch thy arities eqngr styp (Fun c', k)) styps
|
haftmann@31125
|
348 |
and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
|
haftmann@29991
|
349 |
if Symtab.defined eqntab c then vardeps_data
|
haftmann@29991
|
350 |
else let
|
haftmann@29947
|
351 |
val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
|
haftmann@29991
|
352 |
val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
|
haftmann@29947
|
353 |
in
|
haftmann@29947
|
354 |
vardeps_data
|
haftmann@29991
|
355 |
|> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
|
haftmann@30020
|
356 |
|> fold_index (fn (k, _) =>
|
haftmann@30020
|
357 |
apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
|
haftmann@29947
|
358 |
|> fold_index (fn (k, (_, sort)) =>
|
haftmann@30020
|
359 |
add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
|
haftmann@31125
|
360 |
|> fold (ensure_rhs thy arities eqngr) rhss'
|
haftmann@29991
|
361 |
end;
|
haftmann@29947
|
362 |
|
haftmann@29947
|
363 |
|
haftmann@29947
|
364 |
(* applying instantiations *)
|
haftmann@29947
|
365 |
|
haftmann@29947
|
366 |
fun dicts_of thy (proj_sort, algebra) (T, sort) =
|
haftmann@29947
|
367 |
let
|
haftmann@29947
|
368 |
fun class_relation (x, _) _ = x;
|
wenzelm@36102
|
369 |
fun type_constructor (tyco, _) xs class =
|
haftmann@29991
|
370 |
inst_params thy tyco (Sorts.complete_sort algebra [class])
|
haftmann@29991
|
371 |
@ (maps o maps) fst xs;
|
haftmann@29947
|
372 |
fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
|
haftmann@29947
|
373 |
in
|
wenzelm@32802
|
374 |
flat (Sorts.of_sort_derivation algebra
|
wenzelm@36102
|
375 |
{ class_relation = K class_relation, type_constructor = type_constructor,
|
haftmann@29947
|
376 |
type_variable = type_variable } (T, proj_sort sort)
|
haftmann@29947
|
377 |
handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
|
haftmann@29947
|
378 |
end;
|
haftmann@29947
|
379 |
|
haftmann@29991
|
380 |
fun add_arity thy vardeps (class, tyco) =
|
haftmann@33061
|
381 |
AList.default (op =) ((class, tyco),
|
haftmann@34891
|
382 |
map_range (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
|
haftmann@34891
|
383 |
(Sign.arity_number thy tyco));
|
haftmann@29947
|
384 |
|
haftmann@34891
|
385 |
fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) =
|
haftmann@29995
|
386 |
if can (Graph.get_node eqngr) c then (rhss, eqngr)
|
haftmann@29995
|
387 |
else let
|
haftmann@29947
|
388 |
val lhs = map_index (fn (k, (v, _)) =>
|
haftmann@29947
|
389 |
(v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
|
haftmann@34895
|
390 |
val cert = Code.constrain_cert thy (map snd lhs) proto_cert;
|
haftmann@35224
|
391 |
val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
|
haftmann@34891
|
392 |
val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
|
haftmann@29991
|
393 |
in (map (pair c) rhss' @ rhss, eqngr') end;
|
haftmann@29947
|
394 |
|
haftmann@32873
|
395 |
fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
|
haftmann@29947
|
396 |
let
|
haftmann@30942
|
397 |
val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
|
haftmann@30942
|
398 |
insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
|
haftmann@29991
|
399 |
val (vardeps, (eqntab, insts)) = empty_vardeps_data
|
haftmann@31125
|
400 |
|> fold (ensure_fun thy arities eqngr) cs
|
haftmann@31125
|
401 |
|> fold (ensure_rhs thy arities eqngr) cs_rhss;
|
haftmann@29991
|
402 |
val arities' = fold (add_arity thy vardeps) insts arities;
|
haftmann@30001
|
403 |
val pp = Syntax.pp_global thy;
|
haftmann@30942
|
404 |
val algebra = Sorts.subalgebra pp (is_proper_class thy)
|
haftmann@30001
|
405 |
(AList.lookup (op =) arities') (Sign.classes_of thy);
|
haftmann@34891
|
406 |
val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
|
haftmann@30942
|
407 |
fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
|
haftmann@32873
|
408 |
(rhs ~~ sortargs eqngr' c);
|
haftmann@29991
|
409 |
val eqngr'' = fold (fn (c, rhs) => fold
|
haftmann@29991
|
410 |
(curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
|
haftmann@30942
|
411 |
in (algebra, (arities', eqngr'')) end;
|
haftmann@29947
|
412 |
|
haftmann@29947
|
413 |
|
haftmann@31125
|
414 |
(** store for preprocessed arities and code equations **)
|
haftmann@29947
|
415 |
|
haftmann@34160
|
416 |
structure Wellsorted = Code_Data
|
haftmann@29947
|
417 |
(
|
haftmann@30947
|
418 |
type T = ((string * class) * sort list) list * code_graph;
|
haftmann@29947
|
419 |
val empty = ([], Graph.empty);
|
haftmann@29947
|
420 |
);
|
haftmann@29947
|
421 |
|
haftmann@29947
|
422 |
|
haftmann@31125
|
423 |
(** retrieval and evaluation interfaces **)
|
haftmann@29947
|
424 |
|
haftmann@34246
|
425 |
fun obtain thy cs ts = apsnd snd
|
haftmann@34246
|
426 |
(Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
|
haftmann@29947
|
427 |
|
haftmann@32101
|
428 |
fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
|
haftmann@29947
|
429 |
let
|
haftmann@31063
|
430 |
val pp = Syntax.pp_global thy;
|
haftmann@30942
|
431 |
val ct = cterm_of proto_ct;
|
haftmann@31063
|
432 |
val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
|
haftmann@30947
|
433 |
(Thm.term_of ct);
|
haftmann@31125
|
434 |
val thm = preprocess_conv thy ct;
|
haftmann@30942
|
435 |
val ct' = Thm.rhs_of thm;
|
haftmann@30942
|
436 |
val t' = Thm.term_of ct';
|
haftmann@30947
|
437 |
val vs = Term.add_tfrees t' [];
|
haftmann@30947
|
438 |
val consts = fold_aterms
|
haftmann@30947
|
439 |
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
|
haftmann@32544
|
440 |
val (algebra', eqngr') = obtain thy consts [t'];
|
haftmann@32544
|
441 |
in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
|
haftmann@30947
|
442 |
|
haftmann@30947
|
443 |
fun simple_evaluator evaluator algebra eqngr vs t ct =
|
haftmann@30947
|
444 |
evaluator algebra eqngr vs t;
|
haftmann@29947
|
445 |
|
haftmann@30942
|
446 |
fun eval_conv thy =
|
haftmann@30942
|
447 |
let
|
haftmann@30947
|
448 |
fun conclude_evaluation thm2 thm1 =
|
haftmann@30942
|
449 |
let
|
haftmann@31125
|
450 |
val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
|
haftmann@30942
|
451 |
in
|
haftmann@30942
|
452 |
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
|
haftmann@30942
|
453 |
error ("could not construct evaluation proof:\n"
|
wenzelm@32111
|
454 |
^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
|
haftmann@30942
|
455 |
end;
|
haftmann@30947
|
456 |
in gen_eval thy I conclude_evaluation end;
|
haftmann@29947
|
457 |
|
haftmann@32101
|
458 |
fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
|
haftmann@32101
|
459 |
(K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
|
haftmann@31125
|
460 |
|
haftmann@37417
|
461 |
fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
|
haftmann@37417
|
462 |
|
haftmann@31125
|
463 |
|
haftmann@31125
|
464 |
(** setup **)
|
haftmann@31125
|
465 |
|
haftmann@31125
|
466 |
val setup =
|
haftmann@31125
|
467 |
let
|
haftmann@31125
|
468 |
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
|
haftmann@32064
|
469 |
fun add_del_attribute_parser add del =
|
haftmann@31998
|
470 |
Attrib.add_del (mk_attribute add) (mk_attribute del);
|
haftmann@32064
|
471 |
fun both f g thm = f thm #> g thm;
|
haftmann@31125
|
472 |
in
|
haftmann@32064
|
473 |
Attrib.setup @{binding code_unfold} (add_del_attribute_parser
|
haftmann@32064
|
474 |
(both Codegen.add_unfold add_unfold) (both Codegen.del_unfold del_unfold))
|
haftmann@32064
|
475 |
"preprocessing equations for code generators"
|
haftmann@32064
|
476 |
#> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
|
haftmann@31998
|
477 |
"preprocessing equations for code generator"
|
haftmann@32064
|
478 |
#> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
|
haftmann@31998
|
479 |
"postprocessing equations for code generator"
|
haftmann@32064
|
480 |
#> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
|
haftmann@32064
|
481 |
"pre- and postprocessing equations for code generator"
|
haftmann@31125
|
482 |
end;
|
haftmann@31125
|
483 |
|
haftmann@31125
|
484 |
val _ =
|
wenzelm@36970
|
485 |
Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
|
wenzelm@36970
|
486 |
Keyword.diag (Scan.succeed
|
haftmann@31125
|
487 |
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
|
haftmann@31125
|
488 |
(print_codeproc o Toplevel.theory_of)));
|
haftmann@29947
|
489 |
|
haftmann@29947
|
490 |
end; (*struct*)
|