author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 29272  fb3ccf499df5 
child 30022  1d8b8fa19074 
permissions  rwrr 
24590  1 
(* Title: Tools/nbe.ML 
24155  2 
Authors: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen 
3 

24839  4 
Normalization by evaluation, based on generic code generator. 
24155  5 
*) 
6 

7 
signature NBE = 

8 
sig 

25101  9 
val norm_conv: cterm > thm 
10 
val norm_term: theory > term > term 

11 

25204  12 
datatype Univ = 
26064  13 
Const of int * Univ list (*named (uninterpreted) constants*) 
25924  14 
 Free of string * Univ list (*free (uninterpreted) variables*) 
15 
 DFree of string * int (*free (uninterpreted) dictionary parameters*) 

24155  16 
 BVar of int * Univ list 
28350  17 
 Abs of (int * (Univ list > Univ)) * Univ list 
25924  18 
val apps: Univ > Univ list > Univ (*explicit applications*) 
25944  19 
val abss: int > (Univ list > Univ) > Univ 
28337  20 
(*abstractions as closures*) 
28350  21 
val same: Univ > Univ > bool 
24155  22 

25204  23 
val univs_ref: (unit > Univ list > Univ list) option ref 
24155  24 
val trace: bool ref 
25924  25 

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

26 
val setup: theory > theory 
24155  27 
end; 
28 

29 
structure Nbe: NBE = 

30 
struct 

31 

32 
(* generic nonsense *) 

33 

34 
val trace = ref false; 

35 
fun tracing f x = if !trace then (Output.tracing (f x); x) else x; 

36 

37 

38 
(** the semantical universe **) 

39 

40 
(* 

41 
Functions are given by their semantical function value. To avoid 

42 
trouble with the MLtype system, these functions have the most 

43 
generic type, that is "Univ list > Univ". The calling convention is 

44 
that the arguments come as a list, the last argument first. In 

45 
other words, a function call that usually would look like 

46 

47 
f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n) 

48 

49 
would be in our convention called as 

50 

51 
f [x_n,..,x_2,x_1] 

52 

53 
Moreover, to handle functions that are still waiting for some 

54 
arguments we have additionally a list of arguments collected to far 

55 
and the number of arguments we're still waiting for. 

56 
*) 

57 

25204  58 
datatype Univ = 
26064  59 
Const of int * Univ list (*named (uninterpreted) constants*) 
24155  60 
 Free of string * Univ list (*free variables*) 
25924  61 
 DFree of string * int (*free (uninterpreted) dictionary parameters*) 
27499  62 
 BVar of int * Univ list (*bound variables, named*) 
24155  63 
 Abs of (int * (Univ list > Univ)) * Univ list 
27499  64 
(*abstractions as closures*); 
24155  65 

28350  66 
fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys 
67 
 same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys 

68 
 same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l 

69 
 same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys 

70 
 same _ _ = false 

71 
and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys); 

72 

24155  73 
(* constructor functions *) 
74 

25944  75 
fun abss n f = Abs ((n, f), []); 
25924  76 
fun apps (Abs ((n, f), xs)) ys = let val k = n  length ys in 
27499  77 
case int_ord (k, 0) 
78 
of EQUAL => f (ys @ xs) 

79 
 LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end 

80 
 GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*) 

81 
end 

25924  82 
 apps (Const (name, xs)) ys = Const (name, ys @ xs) 
83 
 apps (Free (name, xs)) ys = Free (name, ys @ xs) 

27499  84 
 apps (BVar (n, xs)) ys = BVar (n, ys @ xs); 
24155  85 

86 

87 
(** assembling and compiling ML code from terms **) 

88 

89 
(* abstract ML syntax *) 

90 

91 
infix 9 `$` `$$`; 

92 
fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")"; 

25101  93 
fun e `$$` [] = e 
94 
 e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")"; 

24590  95 
fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")"; 
24155  96 

97 
fun ml_cases t cs = 

98 
"(case " ^ t ^ " of " ^ space_implode "  " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")"; 

25944  99 
fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end"; 
28337  100 
fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")"; 
24155  101 

28350  102 
fun ml_and [] = "true" 
103 
 ml_and [x] = x 

104 
 ml_and xs = "(" ^ space_implode " andalso " xs ^ ")"; 

105 
fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")"; 

106 

24155  107 
fun ml_list es = "[" ^ commas es ^ "]"; 
108 

109 
fun ml_fundefs ([(name, [([], e)])]) = 

110 
"val " ^ name ^ " = " ^ e ^ "\n" 

111 
 ml_fundefs (eqs :: eqss) = 

112 
let 

113 
fun fundef (name, eqs) = 

114 
let 

115 
fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e 

116 
in space_implode "\n  " (map eqn eqs) end; 

117 
in 

118 
(prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss 

26931  119 
> cat_lines 
24155  120 
> suffix "\n" 
121 
end; 

122 

25944  123 
(* nbe specific syntax and sandbox communication *) 
124 

125 
val univs_ref = ref (NONE : (unit > Univ list > Univ list) option); 

24155  126 

127 
local 

28350  128 
val prefix = "Nbe."; 
129 
val name_ref = prefix ^ "univs_ref"; 

130 
val name_const = prefix ^ "Const"; 

131 
val name_abss = prefix ^ "abss"; 

132 
val name_apps = prefix ^ "apps"; 

133 
val name_same = prefix ^ "same"; 

24155  134 
in 
135 

25944  136 
val univs_cookie = (name_ref, univs_ref); 
137 

28337  138 
fun nbe_fun 0 "" = "nbe_value" 
139 
 nbe_fun i c = "c_" ^ translate_string (fn "." => "_"  c => c) c ^ "_" ^ string_of_int i; 

25101  140 
fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n; 
24155  141 
fun nbe_bound v = "v_" ^ v; 
28337  142 
fun nbe_default v = "w_" ^ v; 
24155  143 

25924  144 
(*note: these three are the "turning spots" where proper argument order is established!*) 
145 
fun nbe_apps t [] = t 

146 
 nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; 

28337  147 
fun nbe_apps_local i c ts = nbe_fun i c `$` ml_list (rev ts); 
148 
fun nbe_apps_constr idx_of c ts = 

149 
let 

150 
val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ c ^ "*)" 

151 
else string_of_int (idx_of c); 

152 
in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end; 

25924  153 

24155  154 
fun nbe_abss 0 f = f `$` ml_list [] 
25944  155 
 nbe_abss n f = name_abss `$$` [string_of_int n, f]; 
24155  156 

28350  157 
fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")"; 
158 

24155  159 
end; 
160 

28054  161 
open Basic_Code_Thingol; 
24155  162 

25865  163 
(* code generation *) 
24155  164 

26064  165 
fun assemble_eqnss idx_of deps eqnss = 
25944  166 
let 
167 
fun prep_eqns (c, (vs, eqns)) = 

25924  168 
let 
25944  169 
val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs; 
28337  170 
val num_args = length dicts + ((length o fst o hd) eqns); 
25944  171 
in (c, (num_args, (dicts, eqns))) end; 
172 
val eqnss' = map prep_eqns eqnss; 

173 

174 
fun assemble_constapp c dss ts = 

175 
let 

176 
val ts' = (maps o map) assemble_idict dss @ ts; 

177 
in case AList.lookup (op =) eqnss' c 

28337  178 
of SOME (num_args, _) => if num_args <= length ts' 
179 
then let val (ts1, ts2) = chop num_args ts' 

180 
in nbe_apps (nbe_apps_local 0 c ts1) ts2 

181 
end else nbe_apps (nbe_abss num_args (nbe_fun 0 c)) ts' 

25944  182 
 NONE => if member (op =) deps c 
28337  183 
then nbe_apps (nbe_fun 0 c) ts' 
184 
else nbe_apps_constr idx_of c ts' 

25924  185 
end 
25944  186 
and assemble_idict (DictConst (inst, dss)) = 
187 
assemble_constapp inst dss [] 

188 
 assemble_idict (DictVar (supers, (v, (n, _)))) = 

189 
fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n); 

25924  190 

28350  191 
fun assemble_iterm constapp = 
24155  192 
let 
28350  193 
fun of_iterm match_cont t = 
25944  194 
let 
28054  195 
val (t', ts) = Code_Thingol.unfold_app t 
28350  196 
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end 
197 
and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts 

198 
 of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts 

199 
 of_iapp match_cont ((v, _) `> t) ts = 

200 
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts 

201 
 of_iapp match_cont (ICase (((t, _), cs), t0)) ts = 

202 
nbe_apps (ml_cases (of_iterm NONE t) 

203 
(map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs 

204 
@ [("_", case match_cont of SOME s => s  NONE => of_iterm NONE t0)])) ts 

25944  205 
in of_iterm end; 
24155  206 

28350  207 
fun subst_nonlin_vars args = 
208 
let 

209 
val vs = (fold o Code_Thingol.fold_varnames) 

210 
(fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args []; 

211 
val names = Name.make_context (map fst vs); 

212 
fun declare v k ctxt = let val vs = Name.invents ctxt v k 

213 
in (vs, fold Name.declare vs ctxt) end; 

214 
val (vs_renames, _) = fold_map (fn (v, k) => if k > 1 

215 
then declare v (k  1) #>> (fn vs => (v, vs)) 

216 
else pair (v, [])) vs names; 

217 
val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames; 

218 
fun subst_vars (t as IConst _) samepairs = (t, samepairs) 

219 
 subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v 

220 
of SOME v' => (IVar v', AList.delete (op =) v samepairs) 

221 
 NONE => (t, samepairs)) 

222 
 subst_vars (t1 `$ t2) samepairs = samepairs 

223 
> subst_vars t1 

224 
>> subst_vars t2 

225 
>> (op `$) 

226 
 subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs; 

227 
val (args', _) = fold_map subst_vars args samepairs; 

228 
in (samepairs, args') end; 

229 

28337  230 
fun assemble_eqn c dicts default_args (i, (args, rhs)) = 
231 
let 

232 
val is_eval = (c = ""); 

233 
val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args); 

234 
val match_cont = if is_eval then NONE else SOME default_rhs; 

28350  235 
val assemble_arg = assemble_iterm 
236 
(fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE; 

237 
val assemble_rhs = assemble_iterm assemble_constapp match_cont ; 

238 
val (samepairs, args') = subst_nonlin_vars args; 

239 
val s_args = map assemble_arg args'; 

240 
val s_rhs = if null samepairs then assemble_rhs rhs 

241 
else ml_if (ml_and (map (uncurry nbe_same) samepairs)) 

242 
(assemble_rhs rhs) default_rhs; 

28337  243 
val eqns = if is_eval then 
28350  244 
[([ml_list (rev (dicts @ s_args))], s_rhs)] 
28337  245 
else 
28350  246 
[([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs), 
28337  247 
([ml_list (rev (dicts @ default_args))], default_rhs)] 
248 
in (nbe_fun i c, eqns) end; 

249 

25944  250 
fun assemble_eqns (c, (num_args, (dicts, eqns))) = 
251 
let 

28337  252 
val default_args = map nbe_default 
253 
(Name.invent_list [] "a" (num_args  length dicts)); 

254 
val eqns' = map_index (assemble_eqn c dicts default_args) eqns 

255 
@ (if c = "" then [] else [(nbe_fun (length eqns) c, 

256 
[([ml_list (rev (dicts @ default_args))], 

257 
nbe_apps_constr idx_of c (dicts @ default_args))])]); 

258 
in (eqns', nbe_abss num_args (nbe_fun 0 c)) end; 

24155  259 

25944  260 
val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; 
28337  261 
val deps_vars = ml_list (map (nbe_fun 0) deps); 
262 
in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end; 

25944  263 

264 
(* code compilation *) 

265 

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

266 
fun compile_eqnss _ gr raw_deps [] = [] 
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset

267 
 compile_eqnss ctxt gr raw_deps eqnss = 
24155  268 
let 
26064  269 
val (deps, deps_vals) = split_list (map_filter 
270 
(fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps); 

271 
val idx_of = raw_deps 

272 
> map (fn dep => (dep, snd (Graph.get_node gr dep))) 

273 
> AList.lookup (op =) 

274 
> (fn f => the o f); 

275 
val s = assemble_eqnss idx_of deps eqnss; 

24155  276 
val cs = map fst eqnss; 
25944  277 
in 
278 
s 

279 
> 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

280 
> ML_Context.evaluate ctxt 
25944  281 
(Output.tracing o enclose "\ncompiler echo:\n" "\n\n", 
282 
Output.tracing o enclose "\n compiler echo (with error):\n" "\n\n") 

283 
(!trace) univs_cookie 

284 
> (fn f => f deps_vals) 

285 
> (fn univs => cs ~~ univs) 

286 
end; 

25190  287 

25944  288 
(* preparing function equations *) 
24155  289 

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

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

292 
 eqns_of_stmt (const, Code_Thingol.Fun (_, ((vs, _), eqns))) = 
25101  293 
[(const, (vs, map fst eqns))] 
28054  294 
 eqns_of_stmt (_, Code_Thingol.Datatypecons _) = 
25101  295 
[] 
28054  296 
 eqns_of_stmt (_, Code_Thingol.Datatype _) = 
25101  297 
[] 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

298 
 eqns_of_stmt (class, Code_Thingol.Class (_, (v, (superclasses, classops)))) = 
25101  299 
let 
300 
val names = map snd superclasses @ map fst classops; 

301 
val params = Name.invent_list [] "d" (length names); 

302 
fun mk (k, name) = 

303 
(name, ([(v, [])], 

304 
[([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))])); 

305 
in map_index mk names end 

28054  306 
 eqns_of_stmt (_, Code_Thingol.Classrel _) = 
25101  307 
[] 
28054  308 
 eqns_of_stmt (_, Code_Thingol.Classparam _) = 
25101  309 
[] 
28054  310 
 eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) = 
25101  311 
[(inst, (arities, [([], IConst (class, ([], [])) `$$ 
312 
map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts 

313 
@ map (IConst o snd o fst) instops)]))]; 

24155  314 

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

315 
fun compile_stmts ctxt stmts_deps = 
25101  316 
let 
317 
val names = map (fst o fst) stmts_deps; 

318 
val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps; 

319 
val eqnss = maps (eqns_of_stmt o fst) stmts_deps; 

26064  320 
val refl_deps = names_deps 
25190  321 
> maps snd 
322 
> distinct (op =) 

26064  323 
> fold (insert (op =)) names; 
324 
fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name 

325 
then (gr, (maxidx, idx_tab)) 

326 
else (Graph.new_node (name, (NONE, maxidx)) gr, 

327 
(maxidx + 1, Inttab.update_new (maxidx, name) idx_tab)); 

25190  328 
fun compile gr = eqnss 
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset

329 
> compile_eqnss ctxt gr refl_deps 
25190  330 
> rpair gr; 
25101  331 
in 
26064  332 
fold new_node refl_deps 
333 
#> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps 

334 
#> compile 

335 
#> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ)))) 

25101  336 
end; 
24155  337 

28706  338 
fun ensure_stmts ctxt naming program = 
25101  339 
let 
26064  340 
fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names 
341 
then (gr, (maxidx, idx_tab)) 

342 
else (gr, (maxidx, idx_tab)) 

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

343 
> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name), 
27103  344 
Graph.imm_succs program name)) names); 
28706  345 
in 
346 
fold_rev add_stmts (Graph.strong_conn program) 

347 
#> pair naming 

348 
end; 

24155  349 

25944  350 

351 
(** evaluation **) 

352 

353 
(* term evaluation *) 

354 

28296  355 
fun eval_term ctxt gr deps ((vs, ty) : typscheme, t) = 
25924  356 
let 
28054  357 
val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t [] 
25924  358 
val frees' = map (fn v => Free (v, [])) frees; 
359 
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs; 

360 
in 

25935  361 
("", (vs, [(map IVar frees, t)])) 
28274
9873697fa411
ML_Context.evaluate: proper context (for ML environment);
wenzelm
parents:
28227
diff
changeset

362 
> singleton (compile_eqnss ctxt gr deps) 
25924  363 
> snd 
364 
> (fn t => apps t (rev (dict_frees @ frees'))) 

365 
end; 

24155  366 

24839  367 
(* reification *) 
24155  368 

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

369 
fun term_of_univ thy program idx_tab t = 
24155  370 
let 
25101  371 
fun take_until f [] = [] 
372 
 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

373 
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

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

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

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

377 
 _ => false) 
25101  378 
 is_dict (DFree _) = true 
379 
 is_dict _ = false; 

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

380 
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

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

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

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

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

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

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

27499  397 
 of_univ bounds (BVar (n, ts)) typidx = 
398 
of_apps bounds (Bound (bounds  n  1), ts) typidx 

24155  399 
 of_univ bounds (t as Abs _) typidx = 
400 
typidx 

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

404 

25101  405 
(* function store *) 
406 

407 
structure Nbe_Functions = CodeDataFun 

408 
( 

28706  409 
type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table)); 
410 
val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty))); 

411 
fun purge thy cs (naming, (gr, (maxidx, idx_tab))) = 

27609  412 
let 
28706  413 
val names_delete = cs 
414 
> map_filter (Code_Thingol.lookup_const naming) 

415 
> filter (can (Graph.get_node gr)) 

416 
> Graph.all_preds gr; 

417 
val gr' = Graph.del_nodes names_delete gr; 

418 
in (naming, (gr', (maxidx, idx_tab))) end; 

25101  419 
); 
420 

421 
(* compilation, evaluation and reification *) 

422 

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

425 
val ctxt = ProofContext.init thy; 
28706  426 
val (_, (gr, (_, idx_tab))) = 
427 
Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd); 

26064  428 
in 
429 
vs_ty_t 

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

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

431 
> term_of_univ thy program idx_tab 
26064  432 
end; 
25101  433 

24155  434 
(* evaluation with type reconstruction *) 
435 

28706  436 
fun eval thy t naming program vs_ty_t deps = 
24155  437 
let 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26739
diff
changeset

438 
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

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

444 
val type_frees = Term.map_aterms 

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

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

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

449 
(TypeInfer.constrain ty t); 

29272  450 
fun check_tvars t = if null (Term.add_tvars t []) then t else 
24155  451 
error ("Illegal schematic type variables in normalized term: " 
26952
df36f4c52ee8
command 'normal_form': proper context via Variable.auto_fixes;
wenzelm
parents:
26931
diff
changeset

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

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

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

466 
(* evaluation oracle *) 

467 

28290  468 
val (_, norm_oracle) = Context.>>> (Context.map_theory_result 
28706  469 
(Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) => 
470 
Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps))))); 

24155  471 

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

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

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

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

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

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

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

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

480 

24839  481 
fun norm_conv ct = 
24155  482 
let 
483 
val thy = Thm.theory_of_cterm ct; 

28706  484 
fun evaluator' t naming program vs_ty_t deps = 
485 
norm_oracle (thy, t, naming, program, vs_ty_t, deps); 

26739  486 
fun evaluator t = (add_triv_classes thy t, evaluator' t); 
28054  487 
in Code_Thingol.eval_conv thy evaluator ct end; 
24155  488 

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

24155  495 
(* evaluation command *) 
496 

497 
fun norm_print_term ctxt modes t = 

498 
let 

499 
val thy = ProofContext.theory_of ctxt; 

24839  500 
val t' = norm_term thy t; 
501 
val ty' = Term.type_of t'; 

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

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

504 
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

505 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); 
24155  506 
in Pretty.writeln p end; 
507 

508 

509 
(** Isar setup **) 

510 

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

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

513 
in norm_print_term ctxt modes (Syntax.read_term ctxt s) end; 
24155  514 

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

24155  517 

518 
local structure P = OuterParse and K = OuterKeyword in 

519 

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

521 

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

526 
end; 

527 

528 
end; 

28337  529 