# HG changeset patch # User haftmann # Date 1185196595 -7200 # Node ID 6d81e2ef69f772676bedfbb1ec6cba397904718b # Parent 6a98d0826dafc99d22d4fa3254ae6792ef589ac1 added nbe implementation heading for dictionaries diff -r 6a98d0826daf -r 6d81e2ef69f7 src/Tools/Nbe/Nbe.thy --- /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 \ (bool \ 'a) \ (bool \ 'a) \ '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 (\_. x) (\_. y)" + unfolding if_delayed_def .. + +hide (open) const if_delayed + +lemma "True" by normalization +lemma "x = x" by normalization +lemma "True \ False" +by normalization +lemma "True \ p" by normalization +lemma "p \ 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 \ n \ n" + add2 :: "n \ n \ n" + mul :: "n \ n \ n" + mul2 :: "n \ n \ n" + exp :: "n \ n \ 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 \ True | S x \ 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 \ False | Some y \ True) [None, Some ()]" +normal_form "case xs of [] \ True | x#xs \ False" +normal_form "map (%x. case x of None \ False | Some y \ True) xs" +normal_form "let x = y::'x in [x,x]" +normal_form "Let y (%x. [x,x])" +normal_form "case n of Z \ True | S x \ 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 \ False | Some y \ 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\int)) = -164" by normalization +lemma "(if (0\nat) \ (x\nat) then 0\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 \ set ms" + +normal_form "f" +normal_form "f x" +normal_form "(f o g) x" +normal_form "(f o id) x" +normal_form "\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))))" diff -r 6a98d0826daf -r 6d81e2ef69f7 src/Tools/Nbe/nbe_eval.ML --- /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; diff -r 6a98d0826daf -r 6d81e2ef69f7 src/Tools/Nbe/nbe_package.ML --- /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;