# HG changeset patch # User wenzelm # Date 1284560532 -7200 # Node ID e8b94d51fa85a187fa7d7c838789209a09b0bff8 # Parent 267235a1493805a168584d4bee979de7eb52fb91# Parent f1d6ede54862efb1847d2fda4b955bbdc829a156 merged diff -r f1d6ede54862 -r e8b94d51fa85 src/HOL/IsaMakefile --- 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 \ diff -r f1d6ede54862 -r e8b94d51fa85 src/HOL/ex/NormalForm.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 \ 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 \ n \ n" where - "add Z = id" - | "add (S m) = S o add m" - -primrec add2 :: "n \ n \ 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 \ n \ n" where - "mul Z = (%n. Z)" - | "mul (S m) = (%n. add (mul m n) n)" - -primrec mul2 :: "n \ n \ n" where - "mul2 Z n = Z" - | "mul2 (S m) n = add2 n (mul2 m n)" - -primrec exp :: "n \ n \ 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 \ True | S x \ 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 \ False | Some y \ True) [None, Some ()] = [False, True]" - by normalization -normal_form "case xs of [] \ True | x#xs \ False" -normal_form "map (%x. case x of None \ False | Some y \ 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 \ True | S x \ 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 \ False | Some y \ 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\int)) = -164" by normalization -lemma "(if (0\nat) \ (x\nat) then 0\nat else x) = 0" by normalization -lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization -lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization -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 \ 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 "(\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 \ 'a\semigroup_add, f y]" by normalization -lemma "map f [x \ 'a\semigroup_add, y] = [f x, f y]" by normalization -lemma "(map f [x \ 'a\semigroup_add, y], w \ 'b\finite) = ([f x, f y], w)" by normalization - -end diff -r f1d6ede54862 -r e8b94d51fa85 src/HOL/ex/Normalization_by_Evaluation.thy --- /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 \ 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 \ n \ n" where + "add Z = id" + | "add (S m) = S o add m" + +primrec add2 :: "n \ n \ 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 \ n \ n" where + "mul Z = (%n. Z)" + | "mul (S m) = (%n. add (mul m n) n)" + +primrec mul2 :: "n \ n \ n" where + "mul2 Z n = Z" + | "mul2 (S m) n = add2 n (mul2 m n)" + +primrec exp :: "n \ n \ 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 \ True | S x \ 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 \ False | Some y \ True) [None, Some ()] = [False, True]" + by normalization +value [nbe] "case xs of [] \ True | x#xs \ False" +value [nbe] "map (%x. case x of None \ False | Some y \ 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 \ True | S x \ 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 \ False | Some y \ 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\int)) = -164" by normalization +lemma "(if (0\nat) \ (x\nat) then 0\nat else x) = 0" by normalization +lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization +lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization +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 \ 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] "(\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 \ 'a\semigroup_add, f y]" by normalization +lemma "map f [x \ 'a\semigroup_add, y] = [f x, f y]" by normalization +lemma "(map f [x \ 'a\semigroup_add, y], w \ 'b\finite) = ([f x, f y], w)" by normalization + +end diff -r f1d6ede54862 -r e8b94d51fa85 src/HOL/ex/ROOT.ML --- 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 [ diff -r f1d6ede54862 -r e8b94d51fa85 src/Pure/Isar/code.ML --- 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; diff -r f1d6ede54862 -r e8b94d51fa85 src/Tools/Code/code_preproc.ML --- 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 **) diff -r f1d6ede54862 -r e8b94d51fa85 src/Tools/Code/code_thingol.ML --- 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; diff -r f1d6ede54862 -r e8b94d51fa85 src/Tools/nbe.ML --- 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