9 sig |
9 sig |
10 val norm_conv: cterm -> thm |
10 val norm_conv: cterm -> thm |
11 val norm_term: theory -> term -> term |
11 val norm_term: theory -> term -> term |
12 |
12 |
13 datatype Univ = |
13 datatype Univ = |
14 Const of string * Univ list (*named (uninterpreted) constants*) |
14 Const of int * Univ list (*named (uninterpreted) constants*) |
15 | Free of string * Univ list (*free (uninterpreted) variables*) |
15 | Free of string * Univ list (*free (uninterpreted) variables*) |
16 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
16 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
17 | BVar of int * Univ list |
17 | BVar of int * Univ list |
18 | Abs of (int * (Univ list -> Univ)) * Univ list; |
18 | Abs of (int * (Univ list -> Univ)) * Univ list; |
19 val apps: Univ -> Univ list -> Univ (*explicit applications*) |
19 val apps: Univ -> Univ list -> Univ (*explicit applications*) |
54 arguments we have additionally a list of arguments collected to far |
54 arguments we have additionally a list of arguments collected to far |
55 and the number of arguments we're still waiting for. |
55 and the number of arguments we're still waiting for. |
56 *) |
56 *) |
57 |
57 |
58 datatype Univ = |
58 datatype Univ = |
59 Const of string * Univ list (*named (uninterpreted) constants*) |
59 Const of int * Univ list (*named (uninterpreted) constants*) |
60 | Free of string * Univ list (*free variables*) |
60 | Free of string * Univ list (*free variables*) |
61 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
61 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
62 | BVar of int * Univ list (*bound named variables*) |
62 | BVar of int * Univ list (*bound named variables*) |
63 | Abs of (int * (Univ list -> Univ)) * Univ list |
63 | Abs of (int * (Univ list -> Univ)) * Univ list |
64 (*abstractions as closures*); |
64 (*abstractions as closures*); |
74 else Abs ((k, f), ys @ xs) end (*note: reverse convention also for apps!*) |
74 else Abs ((k, f), ys @ xs) end (*note: reverse convention also for apps!*) |
75 | apps (Const (name, xs)) ys = Const (name, ys @ xs) |
75 | apps (Const (name, xs)) ys = Const (name, ys @ xs) |
76 | apps (Free (name, xs)) ys = Free (name, ys @ xs) |
76 | apps (Free (name, xs)) ys = Free (name, ys @ xs) |
77 | apps (BVar (name, xs)) ys = BVar (name, ys @ xs); |
77 | apps (BVar (name, xs)) ys = BVar (name, ys @ xs); |
78 |
78 |
79 (* universe graph *) |
|
80 |
|
81 type univ_gr = Univ option Graph.T; |
|
82 |
|
83 |
79 |
84 (** assembling and compiling ML code from terms **) |
80 (** assembling and compiling ML code from terms **) |
85 |
81 |
86 (* abstract ML syntax *) |
82 (* abstract ML syntax *) |
87 |
83 |
132 |
128 |
133 (*note: these three are the "turning spots" where proper argument order is established!*) |
129 (*note: these three are the "turning spots" where proper argument order is established!*) |
134 fun nbe_apps t [] = t |
130 fun nbe_apps t [] = t |
135 | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; |
131 | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; |
136 fun nbe_apps_local c ts = nbe_fun c `$` ml_list (rev ts); |
132 fun nbe_apps_local c ts = nbe_fun c `$` ml_list (rev ts); |
137 fun nbe_apps_constr c ts = |
133 fun nbe_apps_constr idx ts = |
138 name_const `$` ("(" ^ ML_Syntax.print_string c ^ ", " ^ ml_list (rev ts) ^ ")"); |
134 name_const `$` ("(" ^ string_of_int idx ^ ", " ^ ml_list (rev ts) ^ ")"); |
139 |
135 |
140 fun nbe_abss 0 f = f `$` ml_list [] |
136 fun nbe_abss 0 f = f `$` ml_list [] |
141 | nbe_abss n f = name_abss `$$` [string_of_int n, f]; |
137 | nbe_abss n f = name_abss `$$` [string_of_int n, f]; |
142 |
138 |
143 end; |
139 end; |
144 |
140 |
145 open BasicCodeThingol; |
141 open BasicCodeThingol; |
146 |
142 |
147 (* code generation *) |
143 (* code generation *) |
148 |
144 |
149 fun assemble_eqnss deps eqnss = |
145 fun assemble_eqnss idx_of deps eqnss = |
150 let |
146 let |
151 fun prep_eqns (c, (vs, eqns)) = |
147 fun prep_eqns (c, (vs, eqns)) = |
152 let |
148 let |
153 val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; |
149 val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; |
154 val num_args = length dicts + (length o fst o hd) eqns; |
150 val num_args = length dicts + (length o fst o hd) eqns; |
163 then let val (ts1, ts2) = chop n ts' |
159 then let val (ts1, ts2) = chop n ts' |
164 in nbe_apps (nbe_apps_local c ts1) ts2 |
160 in nbe_apps (nbe_apps_local c ts1) ts2 |
165 end else nbe_apps (nbe_abss n (nbe_fun c)) ts' |
161 end else nbe_apps (nbe_abss n (nbe_fun c)) ts' |
166 | NONE => if member (op =) deps c |
162 | NONE => if member (op =) deps c |
167 then nbe_apps (nbe_fun c) ts' |
163 then nbe_apps (nbe_fun c) ts' |
168 else nbe_apps_constr c ts' |
164 else nbe_apps_constr (idx_of c) ts' |
169 end |
165 end |
170 and assemble_idict (DictConst (inst, dss)) = |
166 and assemble_idict (DictConst (inst, dss)) = |
171 assemble_constapp inst dss [] |
167 assemble_constapp inst dss [] |
172 | assemble_idict (DictVar (supers, (v, (n, _)))) = |
168 | assemble_idict (DictVar (supers, (v, (n, _)))) = |
173 fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n); |
169 fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n); |
187 @ [("_", of_iterm t0)])) ts |
183 @ [("_", of_iterm t0)])) ts |
188 in of_iterm end; |
184 in of_iterm end; |
189 |
185 |
190 fun assemble_eqns (c, (num_args, (dicts, eqns))) = |
186 fun assemble_eqns (c, (num_args, (dicts, eqns))) = |
191 let |
187 let |
192 val assemble_arg = assemble_iterm (fn c => fn _ => fn ts => nbe_apps_constr c ts); |
188 val assemble_arg = assemble_iterm |
|
189 (fn c => fn _ => fn ts => nbe_apps_constr (idx_of c) ts); |
193 val assemble_rhs = assemble_iterm assemble_constapp; |
190 val assemble_rhs = assemble_iterm assemble_constapp; |
194 fun assemble_eqn (args, rhs) = |
191 fun assemble_eqn (args, rhs) = |
195 ([ml_list (rev (dicts @ map assemble_arg args))], assemble_rhs rhs); |
192 ([ml_list (rev (dicts @ map assemble_arg args))], assemble_rhs rhs); |
196 val default_args = map nbe_bound (Name.invent_list [] "a" num_args); |
193 val default_args = map nbe_bound (Name.invent_list [] "a" num_args); |
197 val default_eqn = ([ml_list (rev default_args)], nbe_apps_constr c default_args); |
194 val default_eqn = if c = "" then NONE |
|
195 else SOME ([ml_list (rev default_args)], |
|
196 nbe_apps_constr (idx_of c) default_args); |
198 in |
197 in |
199 ((nbe_fun c, map assemble_eqn eqns @ [default_eqn]), |
198 ((nbe_fun c, map assemble_eqn eqns @ the_list default_eqn), |
200 nbe_abss num_args (nbe_fun c)) |
199 nbe_abss num_args (nbe_fun c)) |
201 end; |
200 end; |
202 |
201 |
203 val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; |
202 val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; |
204 val deps_vars = ml_list (map nbe_fun deps); |
203 val deps_vars = ml_list (map nbe_fun deps); |
207 (* code compilation *) |
206 (* code compilation *) |
208 |
207 |
209 fun compile_eqnss gr raw_deps [] = [] |
208 fun compile_eqnss gr raw_deps [] = [] |
210 | compile_eqnss gr raw_deps eqnss = |
209 | compile_eqnss gr raw_deps eqnss = |
211 let |
210 let |
|
211 val (deps, deps_vals) = split_list (map_filter |
|
212 (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps); |
|
213 val idx_of = raw_deps |
|
214 |> map (fn dep => (dep, snd (Graph.get_node gr dep))) |
|
215 |> AList.lookup (op =) |
|
216 |> (fn f => the o f); |
|
217 val s = assemble_eqnss idx_of deps eqnss; |
212 val cs = map fst eqnss; |
218 val cs = map fst eqnss; |
213 val (deps, deps_vals) = raw_deps |
|
214 |> map_filter (fn dep => case Graph.get_node gr dep of NONE => NONE |
|
215 | SOME univ => SOME (dep, univ)) |
|
216 |> split_list; |
|
217 val s = assemble_eqnss deps eqnss; |
|
218 in |
219 in |
219 s |
220 s |
220 |> tracing (fn s => "\n--- code to be evaluated:\n" ^ s) |
221 |> tracing (fn s => "\n--- code to be evaluated:\n" ^ s) |
221 |> ML_Context.evaluate |
222 |> ML_Context.evaluate |
222 (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n", |
223 (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n", |
256 fun compile_stmts stmts_deps = |
257 fun compile_stmts stmts_deps = |
257 let |
258 let |
258 val names = map (fst o fst) stmts_deps; |
259 val names = map (fst o fst) stmts_deps; |
259 val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps; |
260 val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps; |
260 val eqnss = maps (eqns_of_stmt o fst) stmts_deps; |
261 val eqnss = maps (eqns_of_stmt o fst) stmts_deps; |
261 val deps = names_deps |
262 val refl_deps = names_deps |
262 |> maps snd |
263 |> maps snd |
263 |> distinct (op =) |
264 |> distinct (op =) |
264 |> subtract (op =) names; |
265 |> fold (insert (op =)) names; |
|
266 fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name |
|
267 then (gr, (maxidx, idx_tab)) |
|
268 else (Graph.new_node (name, (NONE, maxidx)) gr, |
|
269 (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); |
265 fun compile gr = eqnss |
270 fun compile gr = eqnss |
266 |> compile_eqnss gr deps |
271 |> compile_eqnss gr refl_deps |
267 |> rpair gr; |
272 |> rpair gr; |
268 in |
273 in |
269 fold (fn name => Graph.default_node (name, NONE)) names |
274 fold new_node refl_deps |
270 #> fold (fn name => Graph.default_node (name, NONE)) deps |
275 #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps |
271 #> fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps |
276 #> compile |
272 #> compile |
277 #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ)))) |
273 #-> fold (fn (name, univ) => Graph.map_node name (K (SOME univ))) |
|
274 end; |
278 end; |
275 |
279 |
276 fun ensure_stmts code = |
280 fun ensure_stmts code = |
277 let |
281 let |
278 fun add_stmts names gr = if exists ((can o Graph.get_node) gr) names then gr else gr |
282 fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names |
279 |> compile_stmts (map (fn name => ((name, Graph.get_node code name), |
283 then (gr, (maxidx, idx_tab)) |
|
284 else (gr, (maxidx, idx_tab)) |
|
285 |> compile_stmts (map (fn name => ((name, Graph.get_node code name), |
280 Graph.imm_succs code name)) names); |
286 Graph.imm_succs code name)) names); |
281 in fold_rev add_stmts (Graph.strong_conn code) end; |
287 in fold_rev add_stmts (Graph.strong_conn code) end; |
282 |
288 |
283 |
289 |
284 (** evaluation **) |
290 (** evaluation **) |
297 |> (fn t => apps t (rev (dict_frees @ frees'))) |
303 |> (fn t => apps t (rev (dict_frees @ frees'))) |
298 end; |
304 end; |
299 |
305 |
300 (* reification *) |
306 (* reification *) |
301 |
307 |
302 fun term_of_univ thy t = |
308 fun term_of_univ thy idx_tab t = |
303 let |
309 let |
304 fun take_until f [] = [] |
310 fun take_until f [] = [] |
305 | take_until f (x::xs) = if f x then [] else x :: take_until f xs; |
311 | take_until f (x::xs) = if f x then [] else x :: take_until f xs; |
306 fun is_dict (Const (c, _)) = |
312 fun is_dict (Const (idx, _)) = |
307 (is_some o CodeName.class_rev thy) c |
313 let |
308 orelse (is_some o CodeName.classrel_rev thy) c |
314 val c = the (Inttab.lookup idx_tab idx); |
309 orelse (is_some o CodeName.instance_rev thy) c |
315 in |
|
316 (is_some o CodeName.class_rev thy) c |
|
317 orelse (is_some o CodeName.classrel_rev thy) c |
|
318 orelse (is_some o CodeName.instance_rev thy) c |
|
319 end |
310 | is_dict (DFree _) = true |
320 | is_dict (DFree _) = true |
311 | is_dict _ = false; |
321 | is_dict _ = false; |
312 fun of_apps bounds (t, ts) = |
322 fun of_apps bounds (t, ts) = |
313 fold_map (of_univ bounds) ts |
323 fold_map (of_univ bounds) ts |
314 #>> (fn ts' => list_comb (t, rev ts')) |
324 #>> (fn ts' => list_comb (t, rev ts')) |
315 and of_univ bounds (Const (name, ts)) typidx = |
325 and of_univ bounds (Const (idx, ts)) typidx = |
316 let |
326 let |
317 val ts' = take_until is_dict ts; |
327 val ts' = take_until is_dict ts; |
318 val SOME c = CodeName.const_rev thy name; |
328 val c = (the o CodeName.const_rev thy o the o Inttab.lookup idx_tab) idx; |
319 val T = Code.default_typ thy c; |
329 val T = Code.default_typ thy c; |
320 val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T; |
330 val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T; |
321 val typidx' = typidx + maxidx_of_typ T' + 1; |
331 val typidx' = typidx + maxidx_of_typ T' + 1; |
322 in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
332 in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
323 | of_univ bounds (Free (name, ts)) typidx = |
333 | of_univ bounds (Free (name, ts)) typidx = |
332 |
342 |
333 (* function store *) |
343 (* function store *) |
334 |
344 |
335 structure Nbe_Functions = CodeDataFun |
345 structure Nbe_Functions = CodeDataFun |
336 ( |
346 ( |
337 type T = univ_gr; |
347 type T = (Univ option * int) Graph.T * (int * string Inttab.table); |
338 val empty = Graph.empty; |
348 val empty = (Graph.empty, (0, Inttab.empty)); |
339 fun merge _ = Graph.merge (K true); |
349 fun merge _ ((gr1, (maxidx1, idx_tab1)), (gr2, (maxidx2, idx_tab2))) = |
340 fun purge _ NONE _ = Graph.empty |
350 (Graph.merge (K true) (gr1, gr2), (IntInf.max (maxidx1, maxidx2), |
341 | purge NONE _ _ = Graph.empty |
351 Inttab.merge (K true) (idx_tab1, idx_tab2))); |
342 | purge (SOME thy) (SOME cs) gr = |
352 fun purge _ NONE _ = empty |
|
353 | purge NONE _ _ = empty |
|
354 | purge (SOME thy) (SOME cs) (gr, (maxidx, idx_tab)) = |
343 let |
355 let |
344 val cs_exisiting = |
356 val cs_exisiting = |
345 map_filter (CodeName.const_rev thy) (Graph.keys gr); |
357 map_filter (CodeName.const_rev thy) (Graph.keys gr); |
346 val dels = (Graph.all_preds gr |
358 val dels = (Graph.all_preds gr |
347 o map (CodeName.const thy) |
359 o map (CodeName.const thy) |
348 o filter (member (op =) cs_exisiting) |
360 o filter (member (op =) cs_exisiting) |
349 ) cs; |
361 ) cs; |
350 in Graph.del_nodes dels gr end; |
362 in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end; |
351 ); |
363 ); |
352 |
364 |
353 (* compilation, evaluation and reification *) |
365 (* compilation, evaluation and reification *) |
354 |
366 |
355 fun compile_eval thy code vs_ty_t deps = |
367 fun compile_eval thy code vs_ty_t deps = |
356 vs_ty_t |
368 let |
357 |> eval_term (Nbe_Functions.change thy (ensure_stmts code)) deps |
369 val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts code); |
358 |> term_of_univ thy; |
370 in |
|
371 vs_ty_t |
|
372 |> eval_term gr deps |
|
373 |> term_of_univ thy idx_tab |
|
374 end; |
359 |
375 |
360 (* evaluation with type reconstruction *) |
376 (* evaluation with type reconstruction *) |
361 |
377 |
362 fun eval thy code t vs_ty_t deps = |
378 fun eval thy code t vs_ty_t deps = |
363 let |
379 let |