--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Nbe/Nbe.thy Mon Jul 23 15:16:35 2007 +0200
@@ -0,0 +1,158 @@
+(* ID: $Id$
+ Authors: Klaus Aehlig, Tobias Nipkow
+*)
+
+header {* Alternativ implementation of "normalization by evaluation" for HOL, including test examples *}
+
+theory Nbe
+imports Main
+uses
+ "~~/src/Tools/Nbe/nbe_eval.ML"
+ "~~/src/Tools/Nbe/nbe_package.ML"
+begin
+
+ML {* reset Toplevel.debug *}
+
+setup Nbe_Package.setup
+
+method_setup normalization = {*
+ Method.no_args (Method.SIMPLE_METHOD'
+ (CONVERSION (ObjectLogic.judgment_conv Nbe_Package.normalization_conv)
+ THEN' resolve_tac [TrueI, refl]))
+*} "solve goal by normalization"
+
+
+text {* lazy @{const If} *}
+
+definition
+ if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ [code func del]: "if_delayed b f g = (if b then f True else g False)"
+
+lemma [code func]:
+ shows "if_delayed True f g = f True"
+ and "if_delayed False f g = g False"
+ unfolding if_delayed_def by simp_all
+
+lemma [normal pre, symmetric, normal post]:
+ "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
+ unfolding if_delayed_def ..
+
+hide (open) const if_delayed
+
+lemma "True" by normalization
+lemma "x = x" by normalization
+lemma "True \<or> False"
+by normalization
+lemma "True \<or> p" by normalization
+lemma "p \<longrightarrow> True"
+by normalization
+declare disj_assoc [code func]
+lemma "((P | Q) | R) = (P | (Q | R))" by normalization
+declare disj_assoc [code func del]
+lemma "0 + (n::nat) = n" by normalization
+lemma "0 + Suc n = Suc n" by normalization
+lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
+lemma "~((0::nat) < (0::nat))" by normalization
+
+datatype n = Z | S n
+consts
+ add :: "n \<Rightarrow> n \<Rightarrow> n"
+ add2 :: "n \<Rightarrow> n \<Rightarrow> n"
+ mul :: "n \<Rightarrow> n \<Rightarrow> n"
+ mul2 :: "n \<Rightarrow> n \<Rightarrow> n"
+ exp :: "n \<Rightarrow> n \<Rightarrow> n"
+primrec
+ "add Z = id"
+ "add (S m) = S o add m"
+primrec
+ "add2 Z n = n"
+ "add2 (S m) n = S(add2 m n)"
+
+lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
+ by(induct n) auto
+lemma [code]: "add2 n (S m) = S (add2 n m)"
+ by(induct n) auto
+lemma [code]: "add2 n Z = n"
+ by(induct n) auto
+
+lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
+lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
+lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
+
+primrec
+ "mul Z = (%n. Z)"
+ "mul (S m) = (%n. add (mul m n) n)"
+primrec
+ "mul2 Z n = Z"
+ "mul2 (S m) n = add2 n (mul2 m n)"
+primrec
+ "exp m Z = S Z"
+ "exp m (S n) = mul (exp m n) m"
+
+lemma "mul2 (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 "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
+
+lemma "[] @ [] = []" by normalization
+lemma "[] @ xs = xs" by normalization
+normal_form "[a, b, c] @ xs = a # b # c # xs"
+normal_form "map f [x,y,z::'x] = [f x, f y, f z]"
+normal_form "map (%f. f True) [id, g, Not] = [True, g True, False]"
+normal_form "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
+normal_form "rev [a, b, c] = [c, b, a]"
+normal_form "rev (a#b#cs) = rev cs @ [b, a]"
+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
+lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
+lemma "(2::int) + 3 = 5" by normalization
+lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
+lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
+lemma "(2::int) < 3" by normalization
+lemma "(2::int) <= 3" by normalization
+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
+
+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))))"
--- /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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Nbe/nbe_package.ML Mon Jul 23 15:16:35 2007 +0200
@@ -0,0 +1,166 @@
+(* Title: Tools/Nbe/nbe_package.ML
+ ID: $Id$
+ Authors: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
+
+Toplevel theory interface for normalization by evaluation.
+*)
+
+signature NBE_PACKAGE =
+sig
+ val normalization_conv: cterm -> thm
+ val setup: theory -> theory
+ val trace: bool ref
+end;
+
+structure Nbe_Package: NBE_PACKAGE =
+struct
+
+val trace = ref false;
+fun tracing f x = if !trace then (Output.tracing (f x); x) else x;
+
+
+(** data setup **)
+
+(* preproc and postproc attributes *)
+
+structure Nbe_Rewrite = TheoryDataFun
+(
+ type T = thm list * thm list
+ val empty = ([], []);
+ val copy = I;
+ val extend = I;
+ fun merge _ ((pres1,posts1), (pres2,posts2)) =
+ (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2))
+);
+
+val setup_rewrite =
+ let
+ fun map_data f = Context.mapping (Nbe_Rewrite.map f) I;
+ fun attr_pre (thy, thm) =
+ ((map_data o apfst) (insert Thm.eq_thm thm) thy, thm)
+ fun attr_post (thy, thm) =
+ ((map_data o apsnd) (insert Thm.eq_thm thm) thy, thm)
+ val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre
+ || Args.$$$ "post" >> K attr_post));
+ in
+ Attrib.add_attributes
+ [("normal", attr, "declare rewrite theorems for normalization")]
+ end;
+
+fun the_pres thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val pres = (map (LocalDefs.meta_rewrite_rule ctxt) o fst) (Nbe_Rewrite.get thy)
+ in pres end
+
+fun apply_posts thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (Nbe_Rewrite.get thy)
+ in MetaSimplifier.rewrite false posts end
+
+(* theorem store *)
+
+structure Funcgr = CodegenFuncgrRetrieval (val rewrites = the_pres);
+
+
+(** norm by eval **)
+
+local
+
+fun eval_term thy funcgr t =
+ let
+ fun subst_Frees [] = I
+ | subst_Frees inst =
+ Term.map_aterms (fn (t as Free (s, _)) => the_default t (AList.lookup (op =) inst s)
+ | t => t);
+ val anno_vars =
+ subst_Frees (map (fn (s, T) => (s, Free (s, T))) (Term.add_frees t []))
+ #> subst_Vars (map (fn (ixn, T) => (ixn, Var (ixn, T))) (Term.add_vars t []))
+ fun check_tvars t = if null (Term.term_tvars t) then t else
+ error ("Illegal schematic type variables in normalized term: "
+ ^ setmp show_types true (Sign.string_of_term thy) t);
+ val ty = type_of t;
+ fun constrain t =
+ singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
+ in
+ t
+ |> tracing (fn t => "Input:\n" ^ Display.raw_string_of_term t)
+ |> Nbe_Eval.eval thy funcgr
+ |> 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
+ |> tracing (fn t => "Vars typed:\n" ^ setmp show_types true Display.raw_string_of_term t)
+ |> tracing (fn t => setmp show_types true (Sign.string_of_term thy) t)
+ |> constrain
+ |> tracing (fn t => "Types inferred:\n" ^ setmp show_types true Display.raw_string_of_term t)
+ |> check_tvars
+ end;
+
+(* evaluation oracle *)
+
+exception Normalization of CodegenFuncgr.T * term;
+
+fun normalization_oracle (thy, Normalization (funcgr, t)) =
+ Logic.mk_equals (t, eval_term thy funcgr t);
+
+fun normalization_invoke thy funcgr t =
+ Thm.invoke_oracle_i thy "Nbe.normalization" (thy, Normalization (funcgr, t));
+
+in
+
+(* interface *)
+
+val setup_oracle = Theory.add_oracle ("normalization", normalization_oracle)
+
+fun normalization_conv ct =
+ let
+ val thy = Thm.theory_of_cterm ct;
+ fun mk funcgr drop_classes ct thm1 =
+ let
+ val t = Thm.term_of ct;
+ val thm2 = normalization_invoke thy funcgr t;
+ val thm3 = apply_posts thy (Thm.rhs_of thm2);
+ val thm23 = drop_classes (Thm.transitive thm2 thm3);
+ in
+ Thm.transitive thm1 thm23 handle THM _ =>
+ error ("normalization_conv - could not construct proof:\n"
+ ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
+ end;
+ in fst (Funcgr.make_term thy mk ct) end;
+
+fun norm_print_term ctxt modes t =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val ct = Thm.cterm_of thy t;
+ val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
+ val ty = Term.type_of t';
+ val p = Library.setmp print_mode (modes @ ! print_mode) (fn () =>
+ Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
+ in Pretty.writeln p end;
+
+fun norm_print_term_cmd (modes, raw_t) state =
+ let val ctxt = Toplevel.context_of state
+ in norm_print_term ctxt modes (ProofContext.read_term ctxt raw_t) end;
+
+end; (*local*)
+
+
+(* Isar setup *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val nbeP =
+ OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
+ (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
+
+end;
+
+val setup = setup_rewrite #> setup_oracle;
+
+val _ = OuterSyntax.add_parsers [nbeP];
+
+end;