merged
authorwenzelm
Wed, 15 Sep 2010 16:22:12 +0200
changeset 39400 e8b94d51fa85
parent 39399 267235a14938 (diff)
parent 39391 f1d6ede54862 (current diff)
child 39405 4a6243de74b9
merged
--- a/src/HOL/IsaMakefile	Wed Sep 15 16:06:52 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 15 16:22:12 2010 +0200
@@ -1011,6 +1011,7 @@
   ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
   ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
   ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
+  ex/Normalization_by_Evaluation.thy					\
   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
   ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
   ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
--- a/src/HOL/ex/NormalForm.thy	Wed Sep 15 16:06:52 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-(*  Authors:  Klaus Aehlig, Tobias Nipkow *)
-
-header {* Testing implementation of normalization by evaluation *}
-
-theory NormalForm
-imports Complex_Main
-begin
-
-lemma "True" by normalization
-lemma "p \<longrightarrow> True" by normalization
-declare disj_assoc [code nbe]
-lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-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
-
-primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
-   "add Z = id"
- | "add (S m) = S o add m"
-
-primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
-   "add2 Z n = n"
- | "add2 (S m) n = S(add2 m n)"
-
-declare add2.simps [code]
-lemma [code nbe]: "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 :: "n \<Rightarrow> n \<Rightarrow> n" where
-   "mul Z = (%n. Z)"
- | "mul (S m) = (%n. add (mul m n) n)"
-
-primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
-   "mul2 Z n = Z"
- | "mul2 (S m) n = add2 n (mul2 m n)"
-
-primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
-   "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 "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
-lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
-lemma "[] @ xs = xs" by normalization
-lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
-
-lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
-  by normalization rule+
-lemma "rev [a, b, c] = [c, b, a]" by normalization
-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])"
-lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" 
-  by normalization
-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 = P"
-lemma "let x = y in [x, x] = [y, y]" by normalization
-lemma "Let y (%x. [x,x]) = [y, y]" by normalization
-normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
-lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
-normal_form "filter (%x. x) ([True,False,x]@xs)"
-normal_form "filter Not ([True,False,x]@xs)"
-
-lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
-lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
-lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
-
-lemma "last [a, b, c] = c" by normalization
-lemma "last ([a, b, c] @ xs) = last (c # 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
-lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
-lemma "max (Suc 0) 0 = Suc 0" by normalization
-lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
-normal_form "Suc 0 \<in> set ms"
-
-lemma "f = f" by normalization
-lemma "f x = f x" by normalization
-lemma "(f o g) x = f (g x)" by normalization
-lemma "(f o id) x = f x" by normalization
-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))))"
-
-(* handling of type classes in connection with equality *)
-
-lemma "map f [x, y] = [f x, f y]" by normalization
-lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
-lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
-lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
-lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
-
-end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Wed Sep 15 16:22:12 2010 +0200
@@ -0,0 +1,131 @@
+(*  Authors:  Klaus Aehlig, Tobias Nipkow *)
+
+header {* Testing implementation of normalization by evaluation *}
+
+theory Normalization_by_Evaluation
+imports Complex_Main
+begin
+
+lemma "True" by normalization
+lemma "p \<longrightarrow> True" by normalization
+declare disj_assoc [code nbe]
+lemma "((P | Q) | R) = (P | (Q | R))" by normalization
+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
+
+primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "add Z = id"
+ | "add (S m) = S o add m"
+
+primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "add2 Z n = n"
+ | "add2 (S m) n = S(add2 m n)"
+
+declare add2.simps [code]
+lemma [code nbe]: "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 :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "mul Z = (%n. Z)"
+ | "mul (S m) = (%n. add (mul m n) n)"
+
+primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "mul2 Z n = Z"
+ | "mul2 (S m) n = add2 n (mul2 m n)"
+
+primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
+   "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 "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
+lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
+lemma "[] @ xs = xs" by normalization
+lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
+
+lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
+  by normalization rule+
+lemma "rev [a, b, c] = [c, b, a]" by normalization
+value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
+value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
+lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" 
+  by normalization
+value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
+lemma "let x = y in [x, x] = [y, y]" by normalization
+lemma "Let y (%x. [x,x]) = [y, y]" by normalization
+value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
+value [nbe] "filter (%x. x) ([True,False,x]@xs)"
+value [nbe] "filter Not ([True,False,x]@xs)"
+
+lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
+lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
+lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
+
+lemma "last [a, b, c] = c" by normalization
+lemma "last ([a, b, c] @ xs) = last (c # 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
+lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
+lemma "max (Suc 0) 0 = Suc 0" by normalization
+lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
+value [nbe] "Suc 0 \<in> set ms"
+
+lemma "f = f" by normalization
+lemma "f x = f x" by normalization
+lemma "(f o g) x = f (g x)" by normalization
+lemma "(f o id) x = f x" by normalization
+value [nbe] "(\<lambda>x. x)"
+
+(* Church numerals: *)
+
+value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+
+(* handling of type classes in connection with equality *)
+
+lemma "map f [x, y] = [f x, f y]" by normalization
+lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
+lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
+lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
+lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
+
+end
--- a/src/HOL/ex/ROOT.ML	Wed Sep 15 16:06:52 2010 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Sep 15 16:22:12 2010 +0200
@@ -8,7 +8,7 @@
   "Efficient_Nat_examples",
   "FuncSet",
   "Eval_Examples",
-  "NormalForm"
+  "Normalization_by_Evaluation"
 ];
 
 use_thys [
--- a/src/Pure/Isar/code.ML	Wed Sep 15 16:06:52 2010 +0200
+++ b/src/Pure/Isar/code.ML	Wed Sep 15 16:22:12 2010 +0200
@@ -89,16 +89,14 @@
 signature CODE_DATA =
 sig
   type T
-  val change: theory -> (T -> T) -> T
-  val change_yield: theory -> (T -> 'a * T) -> 'a * T
+  val change: theory option -> (T -> T) -> T
+  val change_yield: theory option -> (T -> 'a * T) -> 'a * T
 end;
 
 signature PRIVATE_CODE =
 sig
   include CODE
   val declare_data: Object.T -> serial
-  val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> ('a -> 'a) -> 'a
   val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
     -> theory -> ('a -> 'b * 'a) -> 'b * 'a
 end;
@@ -310,8 +308,6 @@
       ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
   in result end;
 
-fun change_data ops theory f = change_yield_data ops theory (f #> pair ()) |> snd;
-
 end; (*local*)
 
 
@@ -1277,8 +1273,10 @@
 
 val data_op = (kind, Data, dest);
 
-val change = Code.change_data data_op;
-fun change_yield thy = Code.change_yield_data data_op thy;
+fun change_yield (SOME thy) f = Code.change_yield_data data_op thy f
+  | change_yield NONE f = f Data.empty
+
+fun change some_thy f = snd (change_yield some_thy (pair () o f));
 
 end;
 
--- a/src/Tools/Code/code_preproc.ML	Wed Sep 15 16:06:52 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Sep 15 16:22:12 2010 +0200
@@ -23,7 +23,7 @@
   val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
   val pretty: theory -> code_graph -> Pretty.T
-  val obtain: theory -> string list -> term list -> code_algebra * code_graph
+  val obtain: bool -> theory -> string list -> term list -> code_algebra * code_graph
   val dynamic_eval_conv: theory
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
   val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
@@ -422,8 +422,8 @@
 
 (** retrieval and evaluation interfaces **)
 
-fun obtain thy consts ts = apsnd snd
-  (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts));
+fun obtain ignore_cache thy consts ts = apsnd snd
+  (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy) (extend_arities_eqngr thy consts ts));
 
 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
 
@@ -437,7 +437,7 @@
     val (vs', t') = dest_cterm ct';
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
-    val (algebra', eqngr') = obtain thy consts [t'];
+    val (algebra', eqngr') = obtain false thy consts [t'];
   in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
 
 fun dynamic_eval_conv thy =
@@ -457,15 +457,12 @@
 
 fun static_eval_conv thy consts conv =
   let
-    val (algebra, eqngr) = obtain thy consts [];
-    fun conv' ct =
-      let
-        val (vs, t) = dest_cterm ct;
-      in
-        Conv.tap_thy (fn thy => (preprocess_conv thy)
-          then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
-      end;
-  in conv' end;
+    val (algebra, eqngr) = obtain true thy consts [];
+  in
+    Conv.tap_thy (fn thy => (preprocess_conv thy)
+      then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
+      then_conv (postprocess_conv thy))
+  end;
 
 
 (** setup **)
--- a/src/Tools/Code/code_thingol.ML	Wed Sep 15 16:06:52 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 15 16:22:12 2010 +0200
@@ -832,15 +832,11 @@
   val empty = (empty_naming, Graph.empty);
 );
 
-fun cache_generation thy (algebra, eqngr) f name =
-  Program.change_yield thy (fn naming_program => (NONE, naming_program)
-    |> f thy algebra eqngr name
-    |-> (fn name => fn (_, naming_program) => (name, naming_program)));
-
-fun transient_generation thy (algebra, eqngr) f name =
-  (NONE, (empty_naming, Graph.empty))
-  |> f thy algebra eqngr name
-  |-> (fn name => fn (_, naming_program) => (name, naming_program));
+fun invoke_generation ignore_cache thy (algebra, eqngr) f name =
+  Program.change_yield (if ignore_cache then NONE else SOME thy)
+    (fn naming_program => (NONE, naming_program)
+      |> f thy algebra eqngr name
+      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
 
 
 (* program generation *)
@@ -853,10 +849,9 @@
       in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr permissive);
-    val invoke_generation = if permissive
-      then transient_generation else cache_generation
   in
-    invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs
+    invoke_generation (not permissive) thy (Code_Preproc.obtain false thy cs [])
+      generate_consts cs
     |-> project_consts
   end;
 
@@ -892,7 +887,7 @@
 fun base_evaluator thy evaluator algebra eqngr vs t =
   let
     val (((naming, program), (((vs', ty'), t'), deps)), _) =
-      cache_generation thy (algebra, eqngr) ensure_value t;
+      invoke_generation false thy (algebra, eqngr) ensure_value t;
     val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
   in evaluator naming program ((vs'', (vs', ty')), t') deps end;
 
@@ -926,7 +921,7 @@
 
 fun code_depgr thy consts =
   let
-    val (_, eqngr) = Code_Preproc.obtain thy consts [];
+    val (_, eqngr) = Code_Preproc.obtain true thy consts [];
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.subgraph (member (op =) all_consts) eqngr end;
 
--- a/src/Tools/nbe.ML	Wed Sep 15 16:06:52 2010 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 15 16:22:12 2010 +0200
@@ -8,6 +8,7 @@
 sig
   val dynamic_eval_conv: conv
   val dynamic_eval_value: theory -> term -> term
+  val static_eval_conv: theory -> string list -> conv
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
@@ -228,9 +229,9 @@
 
 (* nbe specific syntax and sandbox communication *)
 
-structure Univs = Proof_Data(
+structure Univs = Proof_Data (
   type T = unit -> Univ list -> Univ list
-  fun init thy () = error "Univs"
+  fun init _ () = error "Univs"
 );
 val put_result = Univs.put;
 
@@ -377,15 +378,16 @@
   in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
 
 
-(* code compilation *)
+(* compile equations *)
 
-fun compile_eqnss ctxt gr raw_deps [] = []
-  | compile_eqnss ctxt gr raw_deps eqnss =
+fun compile_eqnss thy nbe_program raw_deps [] = []
+  | compile_eqnss thy nbe_program raw_deps eqnss =
       let
+        val ctxt = ProofContext.init_global thy;
         val (deps, deps_vals) = split_list (map_filter
-          (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps);
+          (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
         val idx_of = raw_deps
-          |> map (fn dep => (dep, snd (Graph.get_node gr dep)))
+          |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
           |> AList.lookup (op =)
           |> (fn f => the o f);
         val s = assemble_eqnss idx_of deps eqnss;
@@ -400,7 +402,7 @@
       end;
 
 
-(* preparing function equations *)
+(* extract equations from statements *)
 
 fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
       []
@@ -428,7 +430,16 @@
         map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
         @ map (IConst o snd o fst) classparam_instances)]))];
 
-fun compile_stmts ctxt stmts_deps =
+
+(* compile whole programs *)
+
+fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) =
+  if can (Graph.get_node nbe_program) name
+  then (nbe_program, (maxidx, idx_tab))
+  else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
+    (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
+
+fun compile_stmts thy stmts_deps =
   let
     val names = map (fst o fst) stmts_deps;
     val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
@@ -437,26 +448,22 @@
       |> maps snd
       |> distinct (op =)
       |> fold (insert (op =)) names;
-    fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name
-      then (gr, (maxidx, idx_tab))
-      else (Graph.new_node (name, (NONE, maxidx)) gr,
-        (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
-    fun compile gr = eqnss
-      |> compile_eqnss ctxt gr refl_deps
-      |> rpair gr;
+    fun compile nbe_program = eqnss
+      |> compile_eqnss thy nbe_program refl_deps
+      |> rpair nbe_program;
   in
-    fold new_node refl_deps
+    fold ensure_const_idx refl_deps
     #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
       #> compile
       #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
   end;
 
-fun ensure_stmts ctxt program =
+fun compile_program thy program =
   let
-    fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
-      then (gr, (maxidx, idx_tab))
-      else (gr, (maxidx, idx_tab))
-        |> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name),
+    fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
+      then (nbe_program, (maxidx, idx_tab))
+      else (nbe_program, (maxidx, idx_tab))
+        |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
           Graph.imm_succs program name)) names);
   in
     fold_rev add_stmts (Graph.strong_conn program)
@@ -465,20 +472,20 @@
 
 (** evaluation **)
 
-(* term evaluation *)
+(* term evaluation by compilation *)
 
-fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
+fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
   let 
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in
     ("", (vs, [([], t)]))
-    |> singleton (compile_eqnss ctxt gr deps)
+    |> singleton (compile_eqnss thy nbe_program deps)
     |> snd
     |> (fn t => apps t (rev dict_frees))
   end;
 
 
-(* reification *)
+(* reconstruction *)
 
 fun typ_of_itype program vs (ityco `%% itys) =
       let
@@ -525,6 +532,29 @@
   in of_univ 0 t 0 |> fst end;
 
 
+(* evaluation with type reconstruction *)
+
+fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+  let
+    val ctxt = Syntax.init_pretty_global thy;
+    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
+    val ty' = typ_of_itype program vs0 ty;
+    fun type_infer t = singleton
+      (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
+      (Type.constraint ty' t);
+    fun check_tvars t =
+      if null (Term.add_tvars t []) then t
+      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
+  in
+    compile_term thy nbe_program deps (vs, t)
+    |> term_of_univ thy program idx_tab
+    |> traced (fn t => "Normalized:\n" ^ string_of_term t)
+    |> type_infer
+    |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
+    |> check_tvars
+    |> traced (fn _ => "---\n")
+  end;
+
 (* function store *)
 
 structure Nbe_Functions = Code_Data
@@ -533,46 +563,15 @@
   val empty = (Graph.empty, (0, Inttab.empty));
 );
 
-
-(* compilation, evaluation and reification *)
-
-fun compile_eval thy program =
+fun compile ignore_cache thy program =
   let
-    val ctxt = ProofContext.init_global thy;
-    val (gr, (_, idx_tab)) =
-      Nbe_Functions.change thy (ensure_stmts ctxt program);
-  in fn vs_t => fn deps =>
-    vs_t
-    |> eval_term ctxt gr deps
-    |> term_of_univ thy program idx_tab
-  end;
+    val (nbe_program, (_, idx_tab)) =
+      Nbe_Functions.change (if ignore_cache then NONE else SOME thy)
+        (compile_program thy program);
+  in (nbe_program, idx_tab) end;
 
 
-(* evaluation with type reconstruction *)
-
-fun normalize thy program ((vs0, (vs, ty)), t) deps =
-  let
-    val ctxt = Syntax.init_pretty_global thy;
-    val ty' = typ_of_itype program vs0 ty;
-    fun type_infer t =
-      singleton
-        (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
-        (Type.constraint ty' t);
-    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
-    fun check_tvars t =
-      if null (Term.add_tvars t []) then t
-      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
-  in
-    compile_eval thy program (vs, t) deps
-    |> traced (fn t => "Normalized:\n" ^ string_of_term t)
-    |> type_infer
-    |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
-    |> check_tvars
-    |> traced (fn _ => "---\n")
-  end;
-
-
-(* evaluation oracle *)
+(* dynamic evaluation oracle *)
 
 fun mk_equals thy lhs raw_rhs =
   let
@@ -582,10 +581,12 @@
   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
-    mk_equals thy ct (normalize thy program vsp_ty_t deps))));
+  (Thm.add_oracle (Binding.name "normalization_by_evaluation",
+    fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
+      mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
 
-fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
+fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
+  raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
 
 fun no_frees_rew rew t =
   let
@@ -597,41 +598,22 @@
     |> curry (Term.betapplys o swap) frees
   end;
 
-val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
-  (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
+val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
+  (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
+    (K (fn program => oracle thy program (compile false thy program))))));
 
 fun dynamic_eval_value thy = lift_triv_classes_rew thy
-  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
+  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
+    (K (fn program => eval_term thy program (compile false thy program)))));
+
+fun static_eval_conv thy consts = Code_Simp.no_frees_conv
+  (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
+    (K (fn program => oracle thy program (compile true thy program)))));
 
 
-(* evaluation command *)
-
-fun norm_print_term ctxt modes t =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val t' = dynamic_eval_value thy t;
-    val ty' = Term.type_of t';
-    val ctxt' = Variable.auto_fixes t ctxt;
-    val p = Print_Mode.with_modes modes (fn () =>
-      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
-  in Pretty.writeln p end;
-
-
-(** Isar setup **)
-
-fun norm_print_term_cmd (modes, s) state =
-  let val ctxt = Toplevel.context_of state
-  in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
+(** setup **)
 
 val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
 
-val opt_modes =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-
-val _ =
-  Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
-    (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
-
 end;
  
\ No newline at end of file