# HG changeset patch # User haftmann # Date 1186393519 -7200 # Node ID 119128bdb804dc6b4e44dd586c43a20b7abcaea8 # Parent 1a4607b7ad24245b7ec8734c8fc9c4203c4dd3ca removed diff -r 1a4607b7ad24 -r 119128bdb804 src/Tools/Nbe/Nbe.thy --- a/src/Tools/Nbe/Nbe.thy Fri Aug 03 22:50:40 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,168 +0,0 @@ -(* 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 - -lemma [code inline]: "If b f g = bool_case f g b" by auto -lemma [code func]: "null xs \ (case xs of [] \ True | _ \ False)" -by (cases xs) auto - - -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 - -normal_form "f" -normal_form "f x" -normal_form "(f o g) x" -normal_form "(f o id) x" -normal_form "id" -normal_form "\x. x" - -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 "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]" - -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 "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 \ True | S x \ 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 \ 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 "(%(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]" - -normal_form "Suc 0 \ set ms" - -(* 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 -lemma "null [x] = False" by normalization \ No newline at end of file diff -r 1a4607b7ad24 -r 119128bdb804 src/Tools/Nbe/nbe_eval.ML --- a/src/Tools/Nbe/nbe_eval.ML Fri Aug 03 22:50:40 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,327 +0,0 @@ -(* 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: -- 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 = - Const of string * Univ list (*uninterpreted constants*) - | Free of string * Univ list (*free (uninterpreted) variables*) - | BVar of int * Univ list (*bound named variables*) - | Abs of (int * (Univ list -> Univ)) * Univ list - (*abstractions as functions*) - val apply: Univ -> Univ -> Univ - - val univs_ref: Univ list ref - val lookup_fun: CodegenNames.const -> Univ - - (*preconditions: no Vars/TVars in term*) - val eval: theory -> 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 = - Const of string * Univ list (*named constructors*) - | Free of string * Univ list (*free variables*) - | BVar of int * Univ list (*bound named variables*) - | Abs of (int * (Univ list -> Univ)) * Univ list - (*functions*); - -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_Functions = 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 [] : Univ list ref; - -local - -val tab_ref = ref NONE : Univ Symtab.table option ref; - -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") - (!trace) s; - val _ = tab_ref := NONE; - val univs = case !univs_ref of [] => error "compile_univs" | univs => univs; - in cs ~~ univs end; - -end; (*local*) - - -(** printing ML syntax **) - -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 ^ ")"; - -fun ml_Val v s = "val " ^ v ^ " = " ^ s; -fun ml_Let ds e = "let\n" ^ space_implode "\n" ds ^ " in " ^ e ^ " end"; - -val ml_string = ML_Syntax.print_string; -fun ml_pair e1 e2 = "(" ^ e1 ^ ", " ^ e2 ^ ")"; -fun ml_list es = "[" ^ commas es ^ "]"; - -fun ml_cases t cs = - "(case " ^ t ^ " of " ^ space_implode " |" (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")"; - -fun ml_fundefs ([(name, [([], e)])]) = - "val " ^ name ^ " = " ^ e ^ "\n" - | ml_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; - - -(** nbe specific syntax **) - -local - 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 - -fun nbe_const c args = ml_app Eval_Const (ml_pair (ml_string c) (ml_list args)); - -fun nbe_fun 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_bound v = "v_" ^ v; - -fun nbe_apps e es = - Library.foldr (fn (s, e) => ml_app (ml_app Eval_apply e) s) (es, e); - -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 = ml_Val (nbe_fun c) (ml_app Eval_lookup_fun (ml_string c)); - -val nbe_value = "value"; - -end; - - -(** assembling and compiling of terms etc. **) - -open BasicCodegenThingol; - -(* greetings to Tarski *) - -fun assemble_iterm thy is_fun num_args = - let - fun of_iterm t = - let - 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 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_fun num_args (c, eqns) = - let - 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) = - ([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 assemble_eqnss thy is_fun [] = ([], "") - | assemble_eqnss thy is_fun eqnss = - let - val cs = map fst eqnss; - 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; - -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; - -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 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 code = - let - fun compile' stmts tab = - let - 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 *) - -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 (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 (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 (t as Abs _) typidx = - typidx - |> 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 t = - let - 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; diff -r 1a4607b7ad24 -r 119128bdb804 src/Tools/Nbe/nbe_package.ML --- a/src/Tools/Nbe/nbe_package.ML Fri Aug 03 22:50:40 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -(* 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 - |> 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;