author  haftmann 
Wed, 22 Oct 2008 14:15:45 +0200  
changeset 28663  bd8438543bf2 
parent 28423  9fc3befd8191 
child 28706  3fef773ae6b1 
permissions  rwrr 
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 nonsense *) 

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 MLtype 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 "\ncompiler 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 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

291 
fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) = 
25101  292 
[] 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

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 
[] 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

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 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

367 
fun term_of_univ thy program 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; 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

371 
fun is_dict (Const (idx, _)) = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

372 
of Code_Thingol.Class _ => true 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

373 
 Code_Thingol.Classrel _ => true 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

374 
 Code_Thingol.Classinst _ => true 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

375 
 _ => false) 
25101  376 
 is_dict (DFree _) = true 
377 
 is_dict _ = false; 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

378 
fun const_of_idx idx = (case (Graph.get_node program o the o Inttab.lookup idx_tab) idx 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

379 
of Code_Thingol.Fun (c, _) => c 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

380 
 Code_Thingol.Datatypecons (c, _) => c 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

381 
 Code_Thingol.Classparam (c, _) => c); 
24155  382 
fun of_apps bounds (t, ts) = 
383 
fold_map (of_univ bounds) ts 

384 
#>> (fn ts' => list_comb (t, rev ts')) 

26064  385 
and of_univ bounds (Const (idx, ts)) typidx = 
24155  386 
let 
25101  387 
val ts' = take_until is_dict ts; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

388 
val c = const_of_idx idx; 
28423  389 
val (_, T) = Code.default_typscheme thy c; 
26739  390 
val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; 
24155  391 
val typidx' = typidx + maxidx_of_typ T' + 1; 
25101  392 
in of_apps bounds (Term.Const (c, T'), ts') typidx' end 
24155  393 
 of_univ bounds (Free (name, ts)) typidx = 
394 
of_apps bounds (Term.Free (name, dummyT), ts) typidx 

27499  395 
 of_univ bounds (BVar (n, ts)) typidx = 
396 
of_apps bounds (Bound (bounds  n  1), ts) typidx 

24155  397 
 of_univ bounds (t as Abs _) typidx = 
398 
typidx 

25924  399 
> of_univ (bounds + 1) (apps t [BVar (bounds, [])]) 
24155  400 
> (fn t' => pair (Term.Abs ("u", dummyT, t'))) 
401 
in of_univ 0 t 0 > fst end; 

402 

25101  403 
(* function store *) 
404 

405 
structure Nbe_Functions = CodeDataFun 

406 
( 

26064  407 
type T = (Univ option * int) Graph.T * (int * string Inttab.table); 
408 
val empty = (Graph.empty, (0, Inttab.empty)); 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

409 
fun purge thy cs (gr, (maxidx, idx_tab)) = empty (*FIXME 
27609  410 
let 
411 
val cs_exisiting = 

28054  412 
map_filter (Code_Name.const_rev thy) (Graph.keys gr); 
27609  413 
val dels = (Graph.all_preds gr 
28054  414 
o map (Code_Name.const thy) 
27609  415 
o filter (member (op =) cs_exisiting) 
416 
) cs; 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

417 
in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end*); 
25101  418 
); 
419 

420 
(* compilation, evaluation and reification *) 

421 

27103  422 
fun compile_eval thy program vs_ty_t deps = 
26064  423 
let 
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset

424 
val ctxt = ProofContext.init thy; 
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset

425 
val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts ctxt program); 
26064  426 
in 
427 
vs_ty_t 

28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset

428 
> eval_term ctxt gr deps 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

429 
> term_of_univ thy program idx_tab 
26064  430 
end; 
25101  431 

24155  432 
(* evaluation with type reconstruction *) 
433 

27103  434 
fun eval thy t program vs_ty_t deps = 
24155  435 
let 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

436 
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

437 
 t => t); 
28054  438 
val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy); 
24347  439 
val ty = type_of t; 
26739  440 
val type_free = AList.lookup (op =) 
441 
(map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t [])); 

442 
val type_frees = Term.map_aterms 

443 
(fn (t as Term.Free (s, _)) => the_default t (type_free s)  t => t); 

27264  444 
fun type_infer t = 
445 
singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I 

446 
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0) 

447 
(TypeInfer.constrain ty t); 

24155  448 
fun check_tvars t = if null (Term.term_tvars t) then t else 
449 
error ("Illegal schematic type variables in normalized term: " 

26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset

450 
^ 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

451 
val string_of_term = setmp show_types true (Syntax.string_of_term_global thy); 
24155  452 
in 
27103  453 
compile_eval thy program vs_ty_t deps 
25167  454 
> tracing (fn t => "Normalized:\n" ^ string_of_term t) 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

455 
> subst_triv_consts 
26739  456 
> type_frees 
25167  457 
> tracing (fn t => "Vars typed:\n" ^ string_of_term t) 
26739  458 
> type_infer 
25167  459 
> tracing (fn t => "Types inferred:\n" ^ string_of_term t) 
26739  460 
> check_tvars 
25101  461 
> tracing (fn t => "\n") 
24155  462 
end; 
463 

464 
(* evaluation oracle *) 

465 

28290  466 
val (_, norm_oracle) = Context.>>> (Context.map_theory_result 
467 
(Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) => 

468 
Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps))))); 

24155  469 

26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

470 
fun add_triv_classes thy = 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

471 
let 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

472 
val inters = curry (Sorts.inter_sort (Sign.classes_of thy)) 
28054  473 
(Code_Unit.triv_classes thy); 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

474 
fun map_sorts f = (map_types o map_atyps) 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

475 
(fn TVar (v, sort) => TVar (v, f sort) 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

476 
 TFree (v, sort) => TFree (v, f sort)); 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

477 
in map_sorts inters end; 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

478 

24839  479 
fun norm_conv ct = 
24155  480 
let 
481 
val thy = Thm.theory_of_cterm ct; 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

482 
fun evaluator' t naming program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps); 
26739  483 
fun evaluator t = (add_triv_classes thy t, evaluator' t); 
28054  484 
in Code_Thingol.eval_conv thy evaluator ct end; 
24155  485 

26739  486 
fun norm_term thy t = 
24839  487 
let 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

488 
fun evaluator' t naming program vs_ty_t deps = eval thy t program vs_ty_t deps; 
26739  489 
fun evaluator t = (add_triv_classes thy t, evaluator' t); 
28054  490 
in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end; 
24839  491 

24155  492 
(* evaluation command *) 
493 

494 
fun norm_print_term ctxt modes t = 

495 
let 

496 
val thy = ProofContext.theory_of ctxt; 

24839  497 
val t' = norm_term thy t; 
498 
val ty' = Term.type_of t'; 

26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset

499 
val ctxt' = Variable.auto_fixes t ctxt; 
24634  500 
val p = PrintMode.with_modes modes (fn () => 
26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset

501 
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

502 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); 
24155  503 
in Pretty.writeln p end; 
504 

505 

506 
(** Isar setup **) 

507 

24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24493
diff
changeset

508 
fun norm_print_term_cmd (modes, s) state = 
24155  509 
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

510 
in norm_print_term ctxt modes (Syntax.read_term ctxt s) end; 
24155  511 

28290  512 
val setup = 
513 
Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of); 

24155  514 

515 
local structure P = OuterParse and K = OuterKeyword in 

516 

517 
val opt_modes = Scan.optional (P.$$$ "("  P.!!! (Scan.repeat1 P.xname  P.$$$ ")")) []; 

518 

24867  519 
val _ = 
24155  520 
OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag 
28227  521 
(opt_modes  P.term >> (Toplevel.keep o norm_print_term_cmd)); 
24155  522 

523 
end; 

524 

525 
end; 

28337  526 