--- 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