author | haftmann |
Thu, 25 Sep 2008 09:28:08 +0200 | |
changeset 28350 | 715163ec93c0 |
parent 28337 | 93964076e7b8 |
child 28423 | 9fc3befd8191 |
permissions | -rw-r--r-- |
24590 | 1 |
(* Title: Tools/nbe.ML |
24155 | 2 |
ID: $Id$ |
3 |
Authors: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen |
|
4 |
||
24839 | 5 |
Normalization by evaluation, based on generic code generator. |
24155 | 6 |
*) |
7 |
||
8 |
signature NBE = |
|
9 |
sig |
|
25101 | 10 |
val norm_conv: cterm -> thm |
11 |
val norm_term: theory -> term -> term |
|
12 |
||
25204 | 13 |
datatype Univ = |
26064 | 14 |
Const of int * Univ list (*named (uninterpreted) constants*) |
25924 | 15 |
| Free of string * Univ list (*free (uninterpreted) variables*) |
16 |
| DFree of string * int (*free (uninterpreted) dictionary parameters*) |
|
24155 | 17 |
| BVar of int * Univ list |
28350 | 18 |
| Abs of (int * (Univ list -> Univ)) * Univ list |
25924 | 19 |
val apps: Univ -> Univ list -> Univ (*explicit applications*) |
25944 | 20 |
val abss: int -> (Univ list -> Univ) -> Univ |
28337 | 21 |
(*abstractions as closures*) |
28350 | 22 |
val same: Univ -> Univ -> bool |
24155 | 23 |
|
25204 | 24 |
val univs_ref: (unit -> Univ list -> Univ list) option ref |
24155 | 25 |
val trace: bool ref |
25924 | 26 |
|
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
27 |
val setup: theory -> theory |
24155 | 28 |
end; |
29 |
||
30 |
structure Nbe: NBE = |
|
31 |
struct |
|
32 |
||
33 |
(* generic non-sense *) |
|
34 |
||
35 |
val trace = ref false; |
|
36 |
fun tracing f x = if !trace then (Output.tracing (f x); x) else x; |
|
37 |
||
38 |
||
39 |
(** the semantical universe **) |
|
40 |
||
41 |
(* |
|
42 |
Functions are given by their semantical function value. To avoid |
|
43 |
trouble with the ML-type system, these functions have the most |
|
44 |
generic type, that is "Univ list -> Univ". The calling convention is |
|
45 |
that the arguments come as a list, the last argument first. In |
|
46 |
other words, a function call that usually would look like |
|
47 |
||
48 |
f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n) |
|
49 |
||
50 |
would be in our convention called as |
|
51 |
||
52 |
f [x_n,..,x_2,x_1] |
|
53 |
||
54 |
Moreover, to handle functions that are still waiting for some |
|
55 |
arguments we have additionally a list of arguments collected to far |
|
56 |
and the number of arguments we're still waiting for. |
|
57 |
*) |
|
58 |
||
25204 | 59 |
datatype Univ = |
26064 | 60 |
Const of int * Univ list (*named (uninterpreted) constants*) |
24155 | 61 |
| Free of string * Univ list (*free variables*) |
25924 | 62 |
| DFree of string * int (*free (uninterpreted) dictionary parameters*) |
27499 | 63 |
| BVar of int * Univ list (*bound variables, named*) |
24155 | 64 |
| Abs of (int * (Univ list -> Univ)) * Univ list |
27499 | 65 |
(*abstractions as closures*); |
24155 | 66 |
|
28350 | 67 |
fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys |
68 |
| same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys |
|
69 |
| same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l |
|
70 |
| same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys |
|
71 |
| same _ _ = false |
|
72 |
and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys); |
|
73 |
||
24155 | 74 |
(* constructor functions *) |
75 |
||
25944 | 76 |
fun abss n f = Abs ((n, f), []); |
25924 | 77 |
fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in |
27499 | 78 |
case int_ord (k, 0) |
79 |
of EQUAL => f (ys @ xs) |
|
80 |
| LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end |
|
81 |
| GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*) |
|
82 |
end |
|
25924 | 83 |
| apps (Const (name, xs)) ys = Const (name, ys @ xs) |
84 |
| apps (Free (name, xs)) ys = Free (name, ys @ xs) |
|
27499 | 85 |
| apps (BVar (n, xs)) ys = BVar (n, ys @ xs); |
24155 | 86 |
|
87 |
||
88 |
(** assembling and compiling ML code from terms **) |
|
89 |
||
90 |
(* abstract ML syntax *) |
|
91 |
||
92 |
infix 9 `$` `$$`; |
|
93 |
fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")"; |
|
25101 | 94 |
fun e `$$` [] = e |
95 |
| e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")"; |
|
24590 | 96 |
fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")"; |
24155 | 97 |
|
98 |
fun ml_cases t cs = |
|
99 |
"(case " ^ t ^ " of " ^ space_implode " | " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")"; |
|
25944 | 100 |
fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end"; |
28337 | 101 |
fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")"; |
24155 | 102 |
|
28350 | 103 |
fun ml_and [] = "true" |
104 |
| ml_and [x] = x |
|
105 |
| ml_and xs = "(" ^ space_implode " andalso " xs ^ ")"; |
|
106 |
fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")"; |
|
107 |
||
24155 | 108 |
fun ml_list es = "[" ^ commas es ^ "]"; |
109 |
||
110 |
fun ml_fundefs ([(name, [([], e)])]) = |
|
111 |
"val " ^ name ^ " = " ^ e ^ "\n" |
|
112 |
| ml_fundefs (eqs :: eqss) = |
|
113 |
let |
|
114 |
fun fundef (name, eqs) = |
|
115 |
let |
|
116 |
fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e |
|
117 |
in space_implode "\n | " (map eqn eqs) end; |
|
118 |
in |
|
119 |
(prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss |
|
26931 | 120 |
|> cat_lines |
24155 | 121 |
|> suffix "\n" |
122 |
end; |
|
123 |
||
25944 | 124 |
(* nbe specific syntax and sandbox communication *) |
125 |
||
126 |
val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option); |
|
24155 | 127 |
|
128 |
local |
|
28350 | 129 |
val prefix = "Nbe."; |
130 |
val name_ref = prefix ^ "univs_ref"; |
|
131 |
val name_const = prefix ^ "Const"; |
|
132 |
val name_abss = prefix ^ "abss"; |
|
133 |
val name_apps = prefix ^ "apps"; |
|
134 |
val name_same = prefix ^ "same"; |
|
24155 | 135 |
in |
136 |
||
25944 | 137 |
val univs_cookie = (name_ref, univs_ref); |
138 |
||
28337 | 139 |
fun nbe_fun 0 "" = "nbe_value" |
140 |
| nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i; |
|
25101 | 141 |
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n; |
24155 | 142 |
fun nbe_bound v = "v_" ^ v; |
28337 | 143 |
fun nbe_default v = "w_" ^ v; |
24155 | 144 |
|
25924 | 145 |
(*note: these three are the "turning spots" where proper argument order is established!*) |
146 |
fun nbe_apps t [] = t |
|
147 |
| nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; |
|
28337 | 148 |
fun nbe_apps_local i c ts = nbe_fun i c `$` ml_list (rev ts); |
149 |
fun nbe_apps_constr idx_of c ts = |
|
150 |
let |
|
151 |
val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ c ^ "*)" |
|
152 |
else string_of_int (idx_of c); |
|
153 |
in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end; |
|
25924 | 154 |
|
24155 | 155 |
fun nbe_abss 0 f = f `$` ml_list [] |
25944 | 156 |
| nbe_abss n f = name_abss `$$` [string_of_int n, f]; |
24155 | 157 |
|
28350 | 158 |
fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")"; |
159 |
||
24155 | 160 |
end; |
161 |
||
28054 | 162 |
open Basic_Code_Thingol; |
24155 | 163 |
|
25865 | 164 |
(* code generation *) |
24155 | 165 |
|
26064 | 166 |
fun assemble_eqnss idx_of deps eqnss = |
25944 | 167 |
let |
168 |
fun prep_eqns (c, (vs, eqns)) = |
|
25924 | 169 |
let |
25944 | 170 |
val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; |
28337 | 171 |
val num_args = length dicts + ((length o fst o hd) eqns); |
25944 | 172 |
in (c, (num_args, (dicts, eqns))) end; |
173 |
val eqnss' = map prep_eqns eqnss; |
|
174 |
||
175 |
fun assemble_constapp c dss ts = |
|
176 |
let |
|
177 |
val ts' = (maps o map) assemble_idict dss @ ts; |
|
178 |
in case AList.lookup (op =) eqnss' c |
|
28337 | 179 |
of SOME (num_args, _) => if num_args <= length ts' |
180 |
then let val (ts1, ts2) = chop num_args ts' |
|
181 |
in nbe_apps (nbe_apps_local 0 c ts1) ts2 |
|
182 |
end else nbe_apps (nbe_abss num_args (nbe_fun 0 c)) ts' |
|
25944 | 183 |
| NONE => if member (op =) deps c |
28337 | 184 |
then nbe_apps (nbe_fun 0 c) ts' |
185 |
else nbe_apps_constr idx_of c ts' |
|
25924 | 186 |
end |
25944 | 187 |
and assemble_idict (DictConst (inst, dss)) = |
188 |
assemble_constapp inst dss [] |
|
189 |
| assemble_idict (DictVar (supers, (v, (n, _)))) = |
|
190 |
fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n); |
|
25924 | 191 |
|
28350 | 192 |
fun assemble_iterm constapp = |
24155 | 193 |
let |
28350 | 194 |
fun of_iterm match_cont t = |
25944 | 195 |
let |
28054 | 196 |
val (t', ts) = Code_Thingol.unfold_app t |
28350 | 197 |
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end |
198 |
and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts |
|
199 |
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts |
|
200 |
| of_iapp match_cont ((v, _) `|-> t) ts = |
|
201 |
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts |
|
202 |
| of_iapp match_cont (ICase (((t, _), cs), t0)) ts = |
|
203 |
nbe_apps (ml_cases (of_iterm NONE t) |
|
204 |
(map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs |
|
205 |
@ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts |
|
25944 | 206 |
in of_iterm end; |
24155 | 207 |
|
28350 | 208 |
fun subst_nonlin_vars args = |
209 |
let |
|
210 |
val vs = (fold o Code_Thingol.fold_varnames) |
|
211 |
(fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args []; |
|
212 |
val names = Name.make_context (map fst vs); |
|
213 |
fun declare v k ctxt = let val vs = Name.invents ctxt v k |
|
214 |
in (vs, fold Name.declare vs ctxt) end; |
|
215 |
val (vs_renames, _) = fold_map (fn (v, k) => if k > 1 |
|
216 |
then declare v (k - 1) #>> (fn vs => (v, vs)) |
|
217 |
else pair (v, [])) vs names; |
|
218 |
val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; |
|
219 |
fun subst_vars (t as IConst _) samepairs = (t, samepairs) |
|
220 |
| subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v |
|
221 |
of SOME v' => (IVar v', AList.delete (op =) v samepairs) |
|
222 |
| NONE => (t, samepairs)) |
|
223 |
| subst_vars (t1 `$ t2) samepairs = samepairs |
|
224 |
|> subst_vars t1 |
|
225 |
||>> subst_vars t2 |
|
226 |
|>> (op `$) |
|
227 |
| subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs; |
|
228 |
val (args', _) = fold_map subst_vars args samepairs; |
|
229 |
in (samepairs, args') end; |
|
230 |
||
28337 | 231 |
fun assemble_eqn c dicts default_args (i, (args, rhs)) = |
232 |
let |
|
233 |
val is_eval = (c = ""); |
|
234 |
val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args); |
|
235 |
val match_cont = if is_eval then NONE else SOME default_rhs; |
|
28350 | 236 |
val assemble_arg = assemble_iterm |
237 |
(fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE; |
|
238 |
val assemble_rhs = assemble_iterm assemble_constapp match_cont ; |
|
239 |
val (samepairs, args') = subst_nonlin_vars args; |
|
240 |
val s_args = map assemble_arg args'; |
|
241 |
val s_rhs = if null samepairs then assemble_rhs rhs |
|
242 |
else ml_if (ml_and (map (uncurry nbe_same) samepairs)) |
|
243 |
(assemble_rhs rhs) default_rhs; |
|
28337 | 244 |
val eqns = if is_eval then |
28350 | 245 |
[([ml_list (rev (dicts @ s_args))], s_rhs)] |
28337 | 246 |
else |
28350 | 247 |
[([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs), |
28337 | 248 |
([ml_list (rev (dicts @ default_args))], default_rhs)] |
249 |
in (nbe_fun i c, eqns) end; |
|
250 |
||
25944 | 251 |
fun assemble_eqns (c, (num_args, (dicts, eqns))) = |
252 |
let |
|
28337 | 253 |
val default_args = map nbe_default |
254 |
(Name.invent_list [] "a" (num_args - length dicts)); |
|
255 |
val eqns' = map_index (assemble_eqn c dicts default_args) eqns |
|
256 |
@ (if c = "" then [] else [(nbe_fun (length eqns) c, |
|
257 |
[([ml_list (rev (dicts @ default_args))], |
|
258 |
nbe_apps_constr idx_of c (dicts @ default_args))])]); |
|
259 |
in (eqns', nbe_abss num_args (nbe_fun 0 c)) end; |
|
24155 | 260 |
|
25944 | 261 |
val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; |
28337 | 262 |
val deps_vars = ml_list (map (nbe_fun 0) deps); |
263 |
in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end; |
|
25944 | 264 |
|
265 |
(* code compilation *) |
|
266 |
||
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
267 |
fun compile_eqnss _ gr raw_deps [] = [] |
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
268 |
| compile_eqnss ctxt gr raw_deps eqnss = |
24155 | 269 |
let |
26064 | 270 |
val (deps, deps_vals) = split_list (map_filter |
271 |
(fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps); |
|
272 |
val idx_of = raw_deps |
|
273 |
|> map (fn dep => (dep, snd (Graph.get_node gr dep))) |
|
274 |
|> AList.lookup (op =) |
|
275 |
|> (fn f => the o f); |
|
276 |
val s = assemble_eqnss idx_of deps eqnss; |
|
24155 | 277 |
val cs = map fst eqnss; |
25944 | 278 |
in |
279 |
s |
|
280 |
|> tracing (fn s => "\n--- code to be evaluated:\n" ^ s) |
|
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
281 |
|> ML_Context.evaluate ctxt |
25944 | 282 |
(Output.tracing o enclose "\n---compiler echo:\n" "\n---\n", |
283 |
Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n") |
|
284 |
(!trace) univs_cookie |
|
285 |
|> (fn f => f deps_vals) |
|
286 |
|> (fn univs => cs ~~ univs) |
|
287 |
end; |
|
25190 | 288 |
|
25944 | 289 |
(* preparing function equations *) |
24155 | 290 |
|
28054 | 291 |
fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) = |
25101 | 292 |
[] |
28054 | 293 |
| eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) = |
25101 | 294 |
[(const, (vs, map fst eqns))] |
28054 | 295 |
| eqns_of_stmt (_, Code_Thingol.Datatypecons _) = |
25101 | 296 |
[] |
28054 | 297 |
| eqns_of_stmt (_, Code_Thingol.Datatype _) = |
25101 | 298 |
[] |
28054 | 299 |
| eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) = |
25101 | 300 |
let |
301 |
val names = map snd superclasses @ map fst classops; |
|
302 |
val params = Name.invent_list [] "d" (length names); |
|
303 |
fun mk (k, name) = |
|
304 |
(name, ([(v, [])], |
|
305 |
[([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))])); |
|
306 |
in map_index mk names end |
|
28054 | 307 |
| eqns_of_stmt (_, Code_Thingol.Classrel _) = |
25101 | 308 |
[] |
28054 | 309 |
| eqns_of_stmt (_, Code_Thingol.Classparam _) = |
25101 | 310 |
[] |
28054 | 311 |
| eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) = |
25101 | 312 |
[(inst, (arities, [([], IConst (class, ([], [])) `$$ |
313 |
map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts |
|
314 |
@ map (IConst o snd o fst) instops)]))]; |
|
24155 | 315 |
|
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
316 |
fun compile_stmts ctxt stmts_deps = |
25101 | 317 |
let |
318 |
val names = map (fst o fst) stmts_deps; |
|
319 |
val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps; |
|
320 |
val eqnss = maps (eqns_of_stmt o fst) stmts_deps; |
|
26064 | 321 |
val refl_deps = names_deps |
25190 | 322 |
|> maps snd |
323 |
|> distinct (op =) |
|
26064 | 324 |
|> fold (insert (op =)) names; |
325 |
fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name |
|
326 |
then (gr, (maxidx, idx_tab)) |
|
327 |
else (Graph.new_node (name, (NONE, maxidx)) gr, |
|
328 |
(maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); |
|
25190 | 329 |
fun compile gr = eqnss |
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
330 |
|> compile_eqnss ctxt gr refl_deps |
25190 | 331 |
|> rpair gr; |
25101 | 332 |
in |
26064 | 333 |
fold new_node refl_deps |
334 |
#> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps |
|
335 |
#> compile |
|
336 |
#-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ)))) |
|
25101 | 337 |
end; |
24155 | 338 |
|
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
339 |
fun ensure_stmts ctxt program = |
25101 | 340 |
let |
26064 | 341 |
fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names |
342 |
then (gr, (maxidx, idx_tab)) |
|
343 |
else (gr, (maxidx, idx_tab)) |
|
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
344 |
|> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name), |
27103 | 345 |
Graph.imm_succs program name)) names); |
346 |
in fold_rev add_stmts (Graph.strong_conn program) end; |
|
24155 | 347 |
|
25944 | 348 |
|
349 |
(** evaluation **) |
|
350 |
||
351 |
(* term evaluation *) |
|
352 |
||
28296 | 353 |
fun eval_term ctxt gr deps ((vs, ty) : typscheme, t) = |
25924 | 354 |
let |
28054 | 355 |
val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t [] |
25924 | 356 |
val frees' = map (fn v => Free (v, [])) frees; |
357 |
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs; |
|
358 |
in |
|
25935 | 359 |
("", (vs, [(map IVar frees, t)])) |
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
360 |
|> singleton (compile_eqnss ctxt gr deps) |
25924 | 361 |
|> snd |
362 |
|> (fn t => apps t (rev (dict_frees @ frees'))) |
|
363 |
end; |
|
24155 | 364 |
|
24839 | 365 |
(* reification *) |
24155 | 366 |
|
26064 | 367 |
fun term_of_univ thy idx_tab t = |
24155 | 368 |
let |
25101 | 369 |
fun take_until f [] = [] |
370 |
| take_until f (x::xs) = if f x then [] else x :: take_until f xs; |
|
26064 | 371 |
fun is_dict (Const (idx, _)) = |
372 |
let |
|
373 |
val c = the (Inttab.lookup idx_tab idx); |
|
374 |
in |
|
28054 | 375 |
(is_some o Code_Name.class_rev thy) c |
376 |
orelse (is_some o Code_Name.classrel_rev thy) c |
|
377 |
orelse (is_some o Code_Name.instance_rev thy) c |
|
26064 | 378 |
end |
25101 | 379 |
| is_dict (DFree _) = true |
380 |
| is_dict _ = false; |
|
24155 | 381 |
fun of_apps bounds (t, ts) = |
382 |
fold_map (of_univ bounds) ts |
|
383 |
#>> (fn ts' => list_comb (t, rev ts')) |
|
26064 | 384 |
and of_univ bounds (Const (idx, ts)) typidx = |
24155 | 385 |
let |
25101 | 386 |
val ts' = take_until is_dict ts; |
28054 | 387 |
val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx; |
26970 | 388 |
val (_, T) = Code.default_typ thy c; |
26739 | 389 |
val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; |
24155 | 390 |
val typidx' = typidx + maxidx_of_typ T' + 1; |
25101 | 391 |
in of_apps bounds (Term.Const (c, T'), ts') typidx' end |
24155 | 392 |
| of_univ bounds (Free (name, ts)) typidx = |
393 |
of_apps bounds (Term.Free (name, dummyT), ts) typidx |
|
27499 | 394 |
| of_univ bounds (BVar (n, ts)) typidx = |
395 |
of_apps bounds (Bound (bounds - n - 1), ts) typidx |
|
24155 | 396 |
| of_univ bounds (t as Abs _) typidx = |
397 |
typidx |
|
25924 | 398 |
|> of_univ (bounds + 1) (apps t [BVar (bounds, [])]) |
24155 | 399 |
|-> (fn t' => pair (Term.Abs ("u", dummyT, t'))) |
400 |
in of_univ 0 t 0 |> fst end; |
|
401 |
||
25101 | 402 |
(* function store *) |
403 |
||
404 |
structure Nbe_Functions = CodeDataFun |
|
405 |
( |
|
26064 | 406 |
type T = (Univ option * int) Graph.T * (int * string Inttab.table); |
407 |
val empty = (Graph.empty, (0, Inttab.empty)); |
|
27609 | 408 |
fun purge thy cs (gr, (maxidx, idx_tab)) = |
409 |
let |
|
410 |
val cs_exisiting = |
|
28054 | 411 |
map_filter (Code_Name.const_rev thy) (Graph.keys gr); |
27609 | 412 |
val dels = (Graph.all_preds gr |
28054 | 413 |
o map (Code_Name.const thy) |
27609 | 414 |
o filter (member (op =) cs_exisiting) |
415 |
) cs; |
|
416 |
in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end; |
|
25101 | 417 |
); |
418 |
||
419 |
(* compilation, evaluation and reification *) |
|
420 |
||
27103 | 421 |
fun compile_eval thy program vs_ty_t deps = |
26064 | 422 |
let |
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
423 |
val ctxt = ProofContext.init thy; |
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
424 |
val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts ctxt program); |
26064 | 425 |
in |
426 |
vs_ty_t |
|
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset
|
427 |
|> eval_term ctxt gr deps |
26064 | 428 |
|> term_of_univ thy idx_tab |
429 |
end; |
|
25101 | 430 |
|
24155 | 431 |
(* evaluation with type reconstruction *) |
432 |
||
27103 | 433 |
fun eval thy t program vs_ty_t deps = |
24155 | 434 |
let |
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
435 |
fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty) |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
436 |
| t => t); |
28054 | 437 |
val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy); |
24347 | 438 |
val ty = type_of t; |
26739 | 439 |
val type_free = AList.lookup (op =) |
440 |
(map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t [])); |
|
441 |
val type_frees = Term.map_aterms |
|
442 |
(fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t); |
|
27264 | 443 |
fun type_infer t = |
444 |
singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I |
|
445 |
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) |
|
446 |
(TypeInfer.constrain ty t); |
|
24155 | 447 |
fun check_tvars t = if null (Term.term_tvars t) then t else |
448 |
error ("Illegal schematic type variables in normalized term: " |
|
26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset
|
449 |
^ setmp show_types true (Syntax.string_of_term_global thy) t); |
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset
|
450 |
val string_of_term = setmp show_types true (Syntax.string_of_term_global thy); |
24155 | 451 |
in |
27103 | 452 |
compile_eval thy program vs_ty_t deps |
25167 | 453 |
|> tracing (fn t => "Normalized:\n" ^ string_of_term t) |
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
454 |
|> subst_triv_consts |
26739 | 455 |
|> type_frees |
25167 | 456 |
|> tracing (fn t => "Vars typed:\n" ^ string_of_term t) |
26739 | 457 |
|> type_infer |
25167 | 458 |
|> tracing (fn t => "Types inferred:\n" ^ string_of_term t) |
26739 | 459 |
|> check_tvars |
25101 | 460 |
|> tracing (fn t => "---\n") |
24155 | 461 |
end; |
462 |
||
463 |
(* evaluation oracle *) |
|
464 |
||
28290 | 465 |
val (_, norm_oracle) = Context.>>> (Context.map_theory_result |
466 |
(Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) => |
|
467 |
Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps))))); |
|
24155 | 468 |
|
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
469 |
fun add_triv_classes thy = |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
470 |
let |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
471 |
val inters = curry (Sorts.inter_sort (Sign.classes_of thy)) |
28054 | 472 |
(Code_Unit.triv_classes thy); |
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
473 |
fun map_sorts f = (map_types o map_atyps) |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
474 |
(fn TVar (v, sort) => TVar (v, f sort) |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
475 |
| TFree (v, sort) => TFree (v, f sort)); |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
476 |
in map_sorts inters end; |
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset
|
477 |
|
24839 | 478 |
fun norm_conv ct = |
24155 | 479 |
let |
480 |
val thy = Thm.theory_of_cterm ct; |
|
28290 | 481 |
fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps); |
26739 | 482 |
fun evaluator t = (add_triv_classes thy t, evaluator' t); |
28054 | 483 |
in Code_Thingol.eval_conv thy evaluator ct end; |
24155 | 484 |
|
26739 | 485 |
fun norm_term thy t = |
24839 | 486 |
let |
27103 | 487 |
fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps; |
26739 | 488 |
fun evaluator t = (add_triv_classes thy t, evaluator' t); |
28054 | 489 |
in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end; |
24839 | 490 |
|
24155 | 491 |
(* evaluation command *) |
492 |
||
493 |
fun norm_print_term ctxt modes t = |
|
494 |
let |
|
495 |
val thy = ProofContext.theory_of ctxt; |
|
24839 | 496 |
val t' = norm_term thy t; |
497 |
val ty' = Term.type_of t'; |
|
26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset
|
498 |
val ctxt' = Variable.auto_fixes t ctxt; |
24634 | 499 |
val p = PrintMode.with_modes modes (fn () => |
26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset
|
500 |
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset
|
501 |
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); |
24155 | 502 |
in Pretty.writeln p end; |
503 |
||
504 |
||
505 |
(** Isar setup **) |
|
506 |
||
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24493
diff
changeset
|
507 |
fun norm_print_term_cmd (modes, s) state = |
24155 | 508 |
let val ctxt = Toplevel.context_of state |
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24493
diff
changeset
|
509 |
in norm_print_term ctxt modes (Syntax.read_term ctxt s) end; |
24155 | 510 |
|
28290 | 511 |
val setup = |
512 |
Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of); |
|
24155 | 513 |
|
514 |
local structure P = OuterParse and K = OuterKeyword in |
|
515 |
||
516 |
val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; |
|
517 |
||
24867 | 518 |
val _ = |
24155 | 519 |
OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag |
28227 | 520 |
(opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd)); |
24155 | 521 |
|
522 |
end; |
|
523 |
||
524 |
end; |
|
28337 | 525 |