--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Nbe/nbe_eval.ML Mon Jul 23 15:16:35 2007 +0200
@@ -0,0 +1,318 @@
+(* Title: Tools/Nbe/Nbe_Eval.ML
+ ID: $Id$
+ Authors: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
+
+Evaluation mechanisms for normalization by evaluation.
+*)
+
+(*
+FIXME:
+- implement purge operation proper
+- get rid of BVar (?) - it is only used tor terms to be evaluated, not for functions
+*)
+
+signature NBE_EVAL =
+sig
+ datatype Univ =
+ Constr of string * Univ list (*named constructors*)
+ | Var of string * Univ list (*free variables*)
+ | BVar of int * Univ list (*bound named variables*)
+ | Fun of (Univ list -> Univ) * Univ list * int
+ (*functions*)
+ val apply: Univ -> Univ -> Univ
+
+ val univs_ref: (CodegenNames.const * Univ) list ref
+ val compile_univs: string -> (CodegenNames.const * Univ) list
+ val lookup_fun: CodegenNames.const -> Univ
+
+ (*preconditions: no Vars/TVars in term*)
+ val eval: theory -> CodegenFuncgr.T -> term -> term
+
+ val trace: bool ref
+end;
+
+structure Nbe_Eval: NBE_EVAL =
+struct
+
+
+(* generic non-sense *)
+
+val trace = ref false;
+fun tracing f x = if !trace then (Output.tracing (f x); x) else x;
+
+(** the semantical universe **)
+
+(*
+ Functions are given by their semantical function value. To avoid
+ trouble with the ML-type system, these functions have the most
+ generic type, that is "Univ list -> Univ". The calling convention is
+ that the arguments come as a list, the last argument first. In
+ other words, a function call that usually would look like
+
+ f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n)
+
+ would be in our convention called as
+
+ f [x_n,..,x_2,x_1]
+
+ Moreover, to handle functions that are still waiting for some
+ arguments we have additionally a list of arguments collected to far
+ 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
+ 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*)
+ | BVar of int * Univ list (*bound named variables*)
+ | Fun of (Univ list -> Univ) * Univ list * int
+ (*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)
+ | apply (BVar (name, args)) x = BVar (name, x :: args);
+
+
+(** global functions **)
+
+structure Nbe_Data = CodeDataFun
+(struct
+ type T = Univ Symtab.table;
+ val empty = Symtab.empty;
+ fun merge _ = Symtab.merge (K true);
+ fun purge _ _ _ = Symtab.empty;
+end);
+
+
+(** sandbox communication **)
+
+val univs_ref = ref [] : (string * Univ) list ref;
+
+fun compile_univs "" = []
+ | compile_univs raw_s =
+ let
+ val _ = univs_ref := [];
+ val s = "Nbe_Eval.univs_ref := " ^ raw_s;
+ val _ = tracing (fn () => "\n---generated code:\n" ^ s) ();
+ 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")
+ (!trace) s;
+ val univs = case !univs_ref of [] => error "compile_univs" | univs => univs;
+ in univs end;
+
+val tab_ref = ref Symtab.empty : Univ Symtab.table ref;
+fun lookup_fun s = (the o Symtab.lookup (! tab_ref)) s;
+
+
+(** printing ML syntax **)
+
+structure S =
+struct
+
+(* generic basics *)
+
+fun app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
+fun apps s ss = Library.foldl (uncurry app) (s, ss);
+fun abs v e = "(fn" ^ v ^ " => " ^ e ^ ")";
+
+fun Val v s = "val " ^ v ^ " = " ^ s;
+fun Let ds e = "let\n" ^ space_implode "\n" ds ^ " in " ^ e ^ " end";
+
+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) =
+ 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 *)
+
+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";
+
+in
+
+(* nbe specific syntax *)
+
+fun nbe_constr c args = app Eval_Constr (tup [string c, list args]);
+
+fun nbe_const c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
+
+fun nbe_free 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"]);
+
+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_lookup c = Val (nbe_const c) (app Eval_lookup_fun (string c));
+
+end;
+
+end;
+
+
+(** assembling and compiling ML representation of terms **)
+
+fun assemble_term thy is_global local_arity =
+ let
+ fun of_term 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
+ 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;
+
+fun assemble_fun thy is_global local_arity (c, eqns) =
+ let
+ val assemble_arg = assemble_term thy (K false) (K NONE);
+ val assemble_rhs = assemble_term thy is_global local_arity;
+ 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);
+ in map assemble_eqn eqns @ [default_eqn] end;
+
+fun compile _ _ [] = []
+ | compile _ _ [(_, [])] = []
+ | compile thy is_global fundefs =
+ 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;
+
+
+(** evaluation with greetings to Tarski **)
+
+(* conversion and evaluation *)
+
+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;
+
+
+(* ensure global functions *)
+
+fun ensure_funs thy funcgr t =
+ 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 =
+ 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;
+
+
+(* re-conversion *)
+
+fun term_of_univ thy t =
+ let
+ 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 =
+ 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
+ | of_univ bounds (BVar (name, ts)) typidx =
+ of_apps bounds (Bound (bounds - name - 1), ts) typidx
+ | of_univ bounds (F as Fun _) typidx =
+ typidx
+ |> of_univ (bounds + 1) (apply F (BVar (bounds, [])))
+ |-> (fn t' => pair (Abs ("u", dummyT, t')))
+ in of_univ 0 t 0 |> fst end;
+
+
+(* interface *)
+
+fun eval thy funcgr t =
+ let
+ val tab = ensure_funs thy funcgr t;
+ val u = univ_of_term thy (Symtab.lookup tab) t;
+ in term_of_univ thy u end;;
+
+end;