--- 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 \<longleftrightarrow> (case xs of [] \<Rightarrow> True | _ \<Rightarrow> 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 \<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
-
-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
-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\<Colon>int)) = -164" by normalization
-lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>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 \<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"
-
-(* 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
--- 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;
--- 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;