--- a/src/Tools/Nbe/Nbe.thy Thu Jul 26 21:51:37 2007 +0200
+++ b/src/Tools/Nbe/Nbe.thy Fri Jul 27 10:09:44 2007 +0200
@@ -39,7 +39,13 @@
hide (open) const if_delayed
-lemma "True" by normalization
+lemma [code func]: "null xs \<longleftrightarrow> (case xs of [] \<Rightarrow> True | _ \<Rightarrow> False)"
+apply (cases xs) apply auto done
+
+normal_form "null [x]"
+
+lemma "True"
+by normalization
lemma "x = x" by normalization
lemma "True \<or> False"
by normalization
@@ -93,11 +99,12 @@
lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
-lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
-lemma "split (%x y. x) (a, b) = a" by normalization
-lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
-
-lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
+normal_form "f"
+normal_form "f x"
+normal_form "(f o g) x"
+normal_form "(f o id) x"
+normal_form "id"
+normal_form "\<lambda>x. x"
lemma "[] @ [] = []" by normalization
lemma "[] @ xs = xs" by normalization
@@ -110,24 +117,10 @@
normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
-normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
-normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
-normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs"
-normal_form "let x = y::'x in [x,x]"
-normal_form "Let y (%x. [x,x])"
-normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
-normal_form "(%(x,y). add x y) (S z,S z)"
normal_form "filter (%x. x) ([True,False,x]@xs)"
normal_form "filter Not ([True,False,x]@xs)"
normal_form "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]"
-normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]"
-normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
-
-lemma "last [a, b, c] = c"
- by normalization
-lemma "last ([a, b, c] @ xs) = (if null xs then c else last xs)"
- by normalization
lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
lemma "(-4::int) * 2 = -8" by normalization
@@ -140,19 +133,36 @@
lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
lemma "4 - 42 * abs (3 + (-7\<Colon>int)) = -164" by normalization
lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
-lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
-lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
+
+lemma "last [a, b, c] = c"
+ by normalization
+lemma "last ([a, b, c] @ xs) = (if null xs then c else last xs)"
+ by normalization
+
+lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
+lemma "split (%x y. x) (a, b) = a" by normalization
+lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
+lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z"
+by normalization
+normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
+normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs"
+normal_form "let x = y::'x in [x,x]"
+normal_form "Let y (%x. [x,x])"
+normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+normal_form "(%(x,y). add x y) (S z,S z)"
+normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]"
+normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
normal_form "Suc 0 \<in> set ms"
-normal_form "f"
-normal_form "f x"
-normal_form "(f o g) x"
-normal_form "(f o id) x"
-normal_form "\<lambda>x. x"
-
(* Church numerals: *)
normal_form "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+
+
+
+lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
+lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
--- a/src/Tools/Nbe/nbe_eval.ML Thu Jul 26 21:51:37 2007 +0200
+++ b/src/Tools/Nbe/nbe_eval.ML Fri Jul 27 10:09:44 2007 +0200
@@ -7,26 +7,26 @@
(*
FIXME:
-- implement purge operation proper
-- get rid of BVar (?) - it is only used tor terms to be evaluated, not for functions
+- get rid of BVar (?) - it is only used for terms to be evaluated, not for functions
+- proper purge operation - preliminary for...
+- really incremental code generation
*)
signature NBE_EVAL =
sig
datatype Univ =
- Constr of string * Univ list (*named constructors*)
- | Var of string * Univ list (*free variables*)
+ Const of string * Univ list (*uninterpreted constants*)
+ | Free of string * Univ list (*free (uninterpreted) variables*)
| BVar of int * Univ list (*bound named variables*)
- | Fun of (Univ list -> Univ) * Univ list * int
- (*functions*)
+ | Abs of (int * (Univ list -> Univ)) * Univ list
+ (*abstractions as functions*)
val apply: Univ -> Univ -> Univ
- val univs_ref: (CodegenNames.const * Univ) list ref
- val compile_univs: string -> (CodegenNames.const * Univ) list
+ val univs_ref: Univ list ref
val lookup_fun: CodegenNames.const -> Univ
(*preconditions: no Vars/TVars in term*)
- val eval: theory -> CodegenFuncgr.T -> term -> term
+ val eval: theory -> term -> term
val trace: bool ref
end;
@@ -60,28 +60,28 @@
and the number of arguments we're still waiting for.
(?) Finally, it might happen, that a function does not get all the
- arguments it needs. In this case the function must provide means to
+ arguments it needs. In this case the function must provide means to
present itself as a string. As this might be a heavy-wight
operation, we delay it. (?)
*)
datatype Univ =
- Constr of string * Univ list (*named constructors*)
- | Var of string * Univ list (*free variables*)
+ Const of string * Univ list (*named constructors*)
+ | Free of string * Univ list (*free variables*)
| BVar of int * Univ list (*bound named variables*)
- | Fun of (Univ list -> Univ) * Univ list * int
+ | Abs of (int * (Univ list -> Univ)) * Univ list
(*functions*);
-fun apply (Fun (f, xs, 1)) x = f (x :: xs)
- | apply (Fun (f, xs, n)) x = Fun (f, x :: xs, n - 1)
- | apply (Constr (name, args)) x = Constr (name, x :: args)
- | apply (Var (name, args)) x = Var (name, x :: args)
+fun apply (Abs ((1, f), xs)) x = f (x :: xs)
+ | apply (Abs ((n, f), xs)) x = Abs ((n - 1, f), x :: xs)
+ | apply (Const (name, args)) x = Const (name, x :: args)
+ | apply (Free (name, args)) x = Free (name, x :: args)
| apply (BVar (name, args)) x = BVar (name, x :: args);
(** global functions **)
-structure Nbe_Data = CodeDataFun
+structure Nbe_Functions = CodeDataFun
(struct
type T = Univ Symtab.table;
val empty = Symtab.empty;
@@ -92,194 +92,202 @@
(** sandbox communication **)
-val univs_ref = ref [] : (string * Univ) list ref;
+val univs_ref = ref [] : Univ list ref;
+
+local
+
+val tab_ref = ref NONE : Univ Symtab.table option ref;
-fun compile_univs "" = []
- | compile_univs raw_s =
+in
+
+fun lookup_fun s = case ! tab_ref
+ of NONE => error "compile_univs"
+ | SOME tab => (the o Symtab.lookup tab) s;
+
+fun compile_univs tab ([], _) = []
+ | compile_univs tab (cs, raw_s) =
let
val _ = univs_ref := [];
val s = "Nbe_Eval.univs_ref := " ^ raw_s;
val _ = tracing (fn () => "\n---generated code:\n" ^ s) ();
+ val _ = tab_ref := SOME tab; (*FIXME hide proper*)
val _ = use_text "" (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
- Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
+ Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
(!trace) s;
+ val _ = tab_ref := NONE;
val univs = case !univs_ref of [] => error "compile_univs" | univs => univs;
- in univs end;
+ in cs ~~ univs end;
-val tab_ref = ref Symtab.empty : Univ Symtab.table ref;
-fun lookup_fun s = (the o Symtab.lookup (! tab_ref)) s;
+end; (*local*)
(** printing ML syntax **)
-structure S =
-struct
+fun ml_app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
+fun ml_apps s ss = Library.foldl (uncurry ml_app) (s, ss);
+fun ml_abs v e = "(fn" ^ v ^ " => " ^ e ^ ")";
-(* generic basics *)
+fun ml_Val v s = "val " ^ v ^ " = " ^ s;
+fun ml_Let ds e = "let\n" ^ space_implode "\n" ds ^ " in " ^ e ^ " end";
-fun app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
-fun apps s ss = Library.foldl (uncurry app) (s, ss);
-fun abs v e = "(fn" ^ v ^ " => " ^ e ^ ")";
+val ml_string = ML_Syntax.print_string;
+fun ml_pair e1 e2 = "(" ^ e1 ^ ", " ^ e2 ^ ")";
+fun ml_list es = "[" ^ commas es ^ "]";
-fun Val v s = "val " ^ v ^ " = " ^ s;
-fun Let ds e = "let\n" ^ space_implode "\n" ds ^ " in " ^ e ^ " end";
+fun ml_cases t cs =
+ "(case " ^ t ^ " of " ^ space_implode " |" (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")";
-val string = ML_Syntax.print_string;
-fun tup es = "(" ^ commas es ^ ")";
-fun list es = "[" ^ commas es ^ "]";
-
-fun fundefs (eqs :: eqss) =
- let
- fun fundef (name, eqs) =
+fun ml_fundefs ([(name, [([], e)])]) =
+ "val " ^ name ^ " = " ^ e ^ "\n"
+ | ml_fundefs (eqs :: eqss) =
let
- fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
- in space_implode "\n | " (map eqn eqs) end;
- in
- (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
- |> space_implode "\n"
- |> suffix "\n"
- end;
+ fun fundef (name, eqs) =
+ let
+ fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
+ in space_implode "\n | " (map eqn eqs) end;
+ in
+ (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
+ |> space_implode "\n"
+ |> suffix "\n"
+ end;
-(* runtime names *)
+(** nbe specific syntax **)
local
-
-val Eval = "Nbe_Eval.";
-val Eval_Constr = Eval ^ "Constr";
-val Eval_apply = Eval ^ "apply";
-val Eval_Fun = Eval ^ "Fun";
-val Eval_lookup_fun = Eval ^ "lookup_fun";
-
+ val Eval = "Nbe_Eval.";
+ val Eval_Const = Eval ^ "Const";
+ val Eval_Free = Eval ^ "Free";
+ val Eval_apply = Eval ^ "apply";
+ val Eval_Abs = Eval ^ "Abs";
+ val Eval_lookup_fun = Eval ^ "lookup_fun";
in
-(* nbe specific syntax *)
+fun nbe_const c args = ml_app Eval_Const (ml_pair (ml_string c) (ml_list args));
-fun nbe_constr c args = app Eval_Constr (tup [string c, list args]);
+fun nbe_fun c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
-fun nbe_const c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
+fun nbe_free v = ml_app Eval_Free (ml_pair (ml_string v) (ml_list []));
-fun nbe_free v = "v_" ^ v;
+fun nbe_bound v = "v_" ^ v;
fun nbe_apps e es =
- Library.foldr (fn (s, e) => app (app Eval_apply e) s) (es, e);
-
-fun nbe_abs (v, e) =
- app Eval_Fun (tup [abs (list [nbe_free v]) e, list [], "1"]);
+ Library.foldr (fn (s, e) => ml_app (ml_app Eval_apply e) s) (es, e);
-fun nbe_fun (c, 0) = tup [string c, app (nbe_const c) (list [])]
- | nbe_fun (c, n) = tup [string c,
- app Eval_Fun (tup [nbe_const c, list [], string_of_int n])];
+fun nbe_abss 0 f = ml_app f (ml_list [])
+ | nbe_abss n f = ml_app Eval_Abs (ml_pair (ml_pair (string_of_int n) f) (ml_list []));
-fun nbe_lookup c = Val (nbe_const c) (app Eval_lookup_fun (string c));
+fun nbe_lookup c = ml_Val (nbe_fun c) (ml_app Eval_lookup_fun (ml_string c));
-end;
+val nbe_value = "value";
end;
-(** assembling and compiling ML representation of terms **)
+(** assembling and compiling of terms etc. **)
+
+open BasicCodegenThingol;
-fun assemble_term thy is_global local_arity =
+(* greetings to Tarski *)
+
+fun assemble_iterm thy is_fun num_args =
let
- fun of_term t =
+ fun of_iterm t =
let
- val (t', ts) = strip_comb t
- in of_termapp t' (fold (cons o of_term) ts []) end
- and of_termapp (Const cexpr) ts =
- let
- val c = (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cexpr;
- in case local_arity c
+ val (t', ts) = CodegenThingol.unfold_app t
+ in of_itermapp t' (fold (cons o of_iterm) ts []) end
+ and of_itermapp (IConst (c, (dss, _))) ts =
+ (case num_args c
of SOME n => if n <= length ts
then let val (args2, args1) = chop (length ts - n) ts
- in S.nbe_apps (S.app (S.nbe_const c) (S.list args1)) args2
- end else S.nbe_constr c ts
- | NONE => if is_global c then S.nbe_apps (S.nbe_const c) ts
- else S.nbe_constr c ts
- end
- | of_termapp (Free (v, _)) ts = S.nbe_apps (S.nbe_free v) ts
- | of_termapp (Abs abs) ts =
- let
- val (v', t') = Syntax.variant_abs abs;
- in S.nbe_apps (S.nbe_abs (v', of_term t')) ts end;
- in of_term end;
+ in nbe_apps (ml_app (nbe_fun c) (ml_list args1)) args2
+ end else nbe_const c ts
+ | NONE => if is_fun c then nbe_apps (nbe_fun c) ts
+ else nbe_const c ts)
+ | of_itermapp (IVar v) ts = nbe_apps (nbe_bound v) ts
+ | of_itermapp ((v, _) `|-> t) ts =
+ nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm t))) ts
+ | of_itermapp (ICase (((t, _), cs), t0)) ts =
+ nbe_apps (ml_cases (of_iterm t) (map (pairself of_iterm) cs
+ @ [("_", of_iterm t0)])) ts
+ in of_iterm end;
-fun assemble_fun thy is_global local_arity (c, eqns) =
+fun assemble_fun thy is_fun num_args (c, eqns) =
let
- val assemble_arg = assemble_term thy (K false) (K NONE);
- val assemble_rhs = assemble_term thy is_global local_arity;
+ val assemble_arg = assemble_iterm thy (K false) (K NONE);
+ val assemble_rhs = assemble_iterm thy is_fun num_args;
fun assemble_eqn (args, rhs) =
- ([S.list (map assemble_arg (rev args))], assemble_rhs rhs);
- val default_params = map S.nbe_free
- (Name.invent_list [] "a" ((the o local_arity) c));
- val default_eqn = ([S.list default_params], S.nbe_constr c default_params);
+ ([ml_list (map assemble_arg (rev args))], assemble_rhs rhs);
+ val default_params = map nbe_bound
+ (Name.invent_list [] "a" ((the o num_args) c));
+ val default_eqn = ([ml_list default_params], nbe_const c default_params);
in map assemble_eqn eqns @ [default_eqn] end;
-fun compile _ _ [] = []
- | compile _ _ [(_, [])] = []
- | compile thy is_global fundefs =
+fun assemble_eqnss thy is_fun [] = ([], "")
+ | assemble_eqnss thy is_fun eqnss =
let
- val eqnss = (map o apsnd o map) (apfst (snd o strip_comb) o Logic.dest_equals
- o Logic.unvarify o prop_of) fundefs;
val cs = map fst eqnss;
- val arities = cs ~~ map (fn (_, (args, rhs) :: _) => length args) eqnss;
- val used_cs = fold (fold (fold_aterms (fn Const cexpr =>
- insert (op =) ((CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cexpr)
- | _ => I)) o map snd o snd) eqnss [];
- val bind_globals = map S.nbe_lookup (filter is_global used_cs);
- val bind_locals = S.fundefs (map S.nbe_const cs ~~ map
- (assemble_fun thy is_global (AList.lookup (op =) arities)) eqnss);
- val result = S.list (map S.nbe_fun arities);
- in compile_univs (S.Let (bind_globals @ [bind_locals]) result) end;
+ val num_args = cs ~~ map (fn (_, (args, rhs) :: _) => length args) eqnss;
+ val funs = fold (fold (CodegenThingol.fold_constnames
+ (insert (op =))) o map snd o snd) eqnss [];
+ val bind_funs = map nbe_lookup (filter is_fun funs);
+ val bind_locals = ml_fundefs (map nbe_fun cs ~~ map
+ (assemble_fun thy is_fun (AList.lookup (op =) num_args)) eqnss);
+ val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
+ in (cs, ml_Let (bind_funs @ [bind_locals]) result) end;
-
-(** evaluation with greetings to Tarski **)
+fun assemble_eval thy is_fun t =
+ let
+ val funs = CodegenThingol.fold_constnames (insert (op =)) t [];
+ val frees = CodegenThingol.fold_unbound_varnames (insert (op =)) t [];
+ val bind_funs = map nbe_lookup (filter is_fun funs);
+ val bind_value = ml_fundefs [(nbe_value, [([ml_list (map nbe_bound frees)],
+ assemble_iterm thy is_fun (K NONE) t)])];
+ val result = ml_list [ml_app nbe_value (ml_list (map nbe_free frees))];
+ in ([nbe_value], ml_Let (bind_funs @ [bind_value]) result) end;
-(* conversion and evaluation *)
+fun eqns_of_stmt (name, CodegenThingol.Fun ([], _)) =
+ NONE
+ | eqns_of_stmt (name, CodegenThingol.Fun (eqns, _)) =
+ SOME (name, eqns)
+ | eqns_of_stmt (_, CodegenThingol.Datatypecons _) =
+ NONE
+ | eqns_of_stmt (_, CodegenThingol.Datatype _) =
+ NONE
+ | eqns_of_stmt (_, CodegenThingol.Class _) =
+ NONE
+ | eqns_of_stmt (_, CodegenThingol.Classrel _) =
+ NONE
+ | eqns_of_stmt (_, CodegenThingol.Classop _) =
+ NONE
+ | eqns_of_stmt (_, CodegenThingol.Classinst _) =
+ NONE;
-fun univ_of_term thy lookup_fun =
- let
- fun of_term vars t =
- let
- val (t', ts) = strip_comb t
- in
- Library.foldl (uncurry apply)
- (of_termapp vars t', map (of_term vars) ts)
- end
- and of_termapp vars (Const cexpr) =
- let
- val s = (CodegenNames.const thy o CodegenConsts.const_of_cexpr thy) cexpr;
- in the_default (Constr (s, [])) (lookup_fun s) end
- | of_termapp vars (Free (v, _)) =
- the_default (Var (v, [])) (AList.lookup (op =) vars v)
- | of_termapp vars (Abs abs) =
- let
- val (v', t') = Syntax.variant_abs abs;
- in Fun (fn [x] => of_term (AList.update (op =) (v', x) vars) t', [], 1) end;
- in of_term [] end;
+fun compile_stmts thy is_fun =
+ map_filter eqns_of_stmt
+ #> assemble_eqnss thy is_fun
+ #> compile_univs (Nbe_Functions.get thy);
+
+fun eval_term thy is_fun =
+ assemble_eval thy is_fun
+ #> compile_univs (Nbe_Functions.get thy)
+ #> the_single
+ #> snd;
(* ensure global functions *)
-fun ensure_funs thy funcgr t =
+fun ensure_funs thy code =
let
- fun consts_of thy t =
- fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t []
- val consts = consts_of thy t;
- fun compile' eqs tab =
+ fun compile' stmts tab =
let
- val _ = tab_ref := tab;
- val compiled = compile thy (Symtab.defined tab) eqs;
- in Nbe_Data.change thy (fold Symtab.update compiled) end;
- val nbe_tab = Nbe_Data.get thy;
- in
- CodegenFuncgr.deps funcgr consts
- |> (map o filter_out) (Symtab.defined nbe_tab o CodegenNames.const thy)
- |> filter_out null
- |> (map o map) (fn c => (CodegenNames.const thy c, CodegenFuncgr.funcs funcgr c))
- |> tracing (fn funs => "new definitions: " ^ (commas o maps (map fst)) funs)
- |> (fn funs => fold compile' funs nbe_tab)
- end;
+ val compiled = compile_stmts thy (Symtab.defined tab) stmts;
+ in Nbe_Functions.change thy (fold Symtab.update compiled) end;
+ val nbe_tab = Nbe_Functions.get thy;
+ val stmtss =
+ map (AList.make (Graph.get_node code)) (rev (Graph.strong_conn code))
+ |> (map o filter_out) (Symtab.defined nbe_tab o fst)
+ in fold compile' stmtss nbe_tab end;
(* re-conversion *)
@@ -289,30 +297,31 @@
fun of_apps bounds (t, ts) =
fold_map (of_univ bounds) ts
#>> (fn ts' => list_comb (t, rev ts'))
- and of_univ bounds (Constr (name, ts)) typidx =
+ and of_univ bounds (Const (name, ts)) typidx =
let
val SOME (const as (c, _)) = CodegenNames.const_rev thy name;
val T = CodegenData.default_typ thy const;
val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, S)) T;
val typidx' = typidx + maxidx_of_typ T' + 1;
- in of_apps bounds (Const (c, T'), ts) typidx' end
- | of_univ bounds (Var (name, ts)) typidx =
- of_apps bounds (Free (name, dummyT), ts) typidx
+ in of_apps bounds (Term.Const (c, T'), ts) typidx' end
+ | of_univ bounds (Free (name, ts)) typidx =
+ of_apps bounds (Term.Free (name, dummyT), ts) typidx
| of_univ bounds (BVar (name, ts)) typidx =
of_apps bounds (Bound (bounds - name - 1), ts) typidx
- | of_univ bounds (F as Fun _) typidx =
+ | of_univ bounds (t as Abs _) typidx =
typidx
- |> of_univ (bounds + 1) (apply F (BVar (bounds, [])))
- |-> (fn t' => pair (Abs ("u", dummyT, t')))
+ |> of_univ (bounds + 1) (apply t (BVar (bounds, [])))
+ |-> (fn t' => pair (Term.Abs ("u", dummyT, t')))
in of_univ 0 t 0 |> fst end;
(* interface *)
-fun eval thy funcgr t =
+fun eval thy t =
let
- val tab = ensure_funs thy funcgr t;
- val u = univ_of_term thy (Symtab.lookup tab) t;
+ val (code, t') = CodegenPackage.compile_term thy t;
+ val tab = ensure_funs thy code;
+ val u = eval_term thy (Symtab.defined tab) t';
in term_of_univ thy u end;;
end;
--- a/src/Tools/Nbe/nbe_package.ML Thu Jul 26 21:51:37 2007 +0200
+++ b/src/Tools/Nbe/nbe_package.ML Fri Jul 27 10:09:44 2007 +0200
@@ -86,7 +86,7 @@
in
t
|> tracing (fn t => "Input:\n" ^ Display.raw_string_of_term t)
- |> Nbe_Eval.eval thy funcgr
+ |> Nbe_Eval.eval thy
|> tracing (fn t => "Normalized:\n" ^ setmp show_types true Display.raw_string_of_term t)
|> tracing (fn _ => "Term type:\n" ^ Display.raw_string_of_typ ty)
|> anno_vars