--- a/NEWS Fri May 09 08:13:36 2014 +0200
+++ b/NEWS Fri May 09 08:13:37 2014 +0200
@@ -204,8 +204,11 @@
*** HOL ***
+* Command and antiquotation ''value'' are hardcoded against nbe and
+ML now. Minor INCOMPATIBILITY.
+
* Separate command ''approximate'' for approximative computation
-in Decision_Procs/Approximation. Minor INCOMPATBILITY.
+in Decision_Procs/Approximation. Minor INCOMPATIBILITY.
* Adjustion of INF and SUP operations:
* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
--- a/src/Doc/Codegen/Evaluation.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Fri May 09 08:13:37 2014 +0200
@@ -90,18 +90,12 @@
value %quote "42 / (12 :: rat)"
text {*
- \noindent By default @{command value} tries all available evaluation
- techniques and prints the result of the first succeeding one. A particular
- technique may be specified in square brackets, e.g.
-*}
+ \noindent @{command value} tries first to evaluate using ML, falling
+ back to normalization by evaluation if this fails.
-value %quote [nbe] "42 / (12 :: rat)"
-
-text {*
To employ dynamic evaluation in the document generation, there is also
- a @{text value} antiquotation. By default, it also tries all available evaluation
- techniques and prints the result of the first succeeding one, unless a particular
- technique is specified in square brackets.
+ a @{text value} antiquotation with the same evaluation techniques
+ as @{command value}.
Static evaluation freezes the code generator configuration at a
certain point and uses this context whenever evaluation is issued
@@ -172,10 +166,7 @@
\fontsize{9pt}{12pt}\selectfont
\begin{tabular}{ll||c|c|c}
& & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
- \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
- & interactive evaluation
- & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
- \tabularnewline
+ \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
& evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
& property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri May 09 08:13:37 2014 +0200
@@ -2114,7 +2114,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
+ @@{command (HOL) value} modes? @{syntax term}
;
@@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -2144,13 +2144,8 @@
\item @{command (HOL) "value"}~@{text t} evaluates and prints a
term; optionally @{text modes} can be specified, which are appended
to the current print mode; see \secref{sec:print-modes}.
- Internally, the evaluation is performed by registered evaluators,
- which are invoked sequentially until a result is returned.
- Alternatively a specific evaluator can be selected using square
- brackets; typical evaluators use the current set of code equations
- to normalize and include @{text simp} for fully symbolic evaluation
- using the simplifier, @{text nbe} for \emph{normalization by
- evaluation} and \emph{code} for code generation in SML.
+ Evaluation is tried first using ML, falling
+ back to normalization by evaluation if this fails.
\item @{command (HOL) "values"}~@{text t} enumerates a set
comprehension by evaluation and prints its values up to the given
--- a/src/HOL/Code_Evaluation.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Fri May 09 08:13:37 2014 +0200
@@ -158,11 +158,6 @@
ML_file "~~/src/HOL/Tools/value.ML"
-setup {*
- Value.add_evaluator ("nbe", Nbe.dynamic_value)
- #> Value.add_evaluator ("code", Code_Evaluation.dynamic_value_strict)
-*}
-
subsection {* Generic reification *}
--- a/src/HOL/IMP/Abs_Int1_parity.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Fri May 09 08:13:37 2014 +0200
@@ -134,7 +134,7 @@
definition "test1_parity =
''x'' ::= N 1;;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
-value [code] "show_acom (the(AI_parity test1_parity))"
+value "show_acom (the(AI_parity test1_parity))"
definition "test2_parity =
''x'' ::= N 1;;
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri May 09 08:13:37 2014 +0200
@@ -100,12 +100,12 @@
WHILE Less (V ''x'') (N 1)
DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')"
-value [code] "list (AI_const test1_const Top)"
-value [code] "list (AI_const test2_const Top)"
-value [code] "list (AI_const test3_const Top)"
-value [code] "list (AI_const test4_const Top)"
-value [code] "list (AI_const test5_const Top)"
-value [code] "list (AI_const test6_const Top)"
-value [code] "list (AI_const test7_const Top)"
+value "list (AI_const test1_const Top)"
+value "list (AI_const test2_const Top)"
+value "list (AI_const test3_const Top)"
+value "list (AI_const test4_const Top)"
+value "list (AI_const test5_const Top)"
+value "list (AI_const test6_const Top)"
+value "list (AI_const test7_const Top)"
end
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri May 09 08:13:37 2014 +0200
@@ -213,22 +213,22 @@
"list_up bot = bot" |
"list_up (Up x) = Up(list x)"
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
-value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
+value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
+value "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
+value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
(Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
+value "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
(Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
+value "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
(Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
+value "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
(Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
(Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
+value "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
(Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
-value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
+value "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
(Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
definition "test_ivl1 =
@@ -236,7 +236,7 @@
IF Less (V ''x'') (V ''y'')
THEN ''y'' ::= Plus (V ''y'') (V ''x'')
ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
-value [code] "list_up(AI_ivl test_ivl1 Top)"
+value "list_up(AI_ivl test_ivl1 Top)"
value "list_up (AI_ivl test3_const Top)"
@@ -247,24 +247,24 @@
definition "test2_ivl =
''y'' ::= N 7;;
WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
-value [code] "list_up(AI_ivl test2_ivl Top)"
+value "list_up(AI_ivl test2_ivl Top)"
definition "test3_ivl =
''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
WHILE Less (V ''x'') (N 11)
DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
-value [code] "list_up(AI_ivl test3_ivl Top)"
+value "list_up(AI_ivl test3_ivl Top)"
definition "test4_ivl =
''x'' ::= N 0;; ''y'' ::= N 0;;
WHILE Less (V ''x'') (N 1001)
DO (''y'' ::= V ''x'';; ''x'' ::= Plus (V ''x'') (N 1))"
-value [code] "list_up(AI_ivl test4_ivl Top)"
+value "list_up(AI_ivl test4_ivl Top)"
text{* Nontermination not detected: *}
definition "test5_ivl =
''x'' ::= N 0;;
WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
-value [code] "list_up(AI_ivl test5_ivl Top)"
+value "list_up(AI_ivl test5_ivl Top)"
end
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri May 09 08:13:37 2014 +0200
@@ -200,8 +200,8 @@
and aval_ivl' = aval'
proof qed (auto simp: iter'_pfp_above)
-value [code] "list_up(AI_ivl' test3_ivl Top)"
-value [code] "list_up(AI_ivl' test4_ivl Top)"
-value [code] "list_up(AI_ivl' test5_ivl Top)"
+value "list_up(AI_ivl' test3_ivl Top)"
+value "list_up(AI_ivl' test4_ivl Top)"
+value "list_up(AI_ivl' test5_ivl Top)"
end
--- a/src/HOL/Library/Extended_Real.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri May 09 08:13:37 2014 +0200
@@ -2444,10 +2444,10 @@
(* A small list of simple arithmetic expressions *)
-value [code] "- \<infinity> :: ereal"
-value [code] "\<bar>-\<infinity>\<bar> :: ereal"
-value [code] "4 + 5 / 4 - ereal 2 :: ereal"
-value [code] "ereal 3 < \<infinity>"
-value [code] "real (\<infinity>::ereal) = 0"
+value "- \<infinity> :: ereal"
+value "\<bar>-\<infinity>\<bar> :: ereal"
+value "4 + 5 / 4 - ereal 2 :: ereal"
+value "ereal 3 < \<infinity>"
+value "real (\<infinity>::ereal) = 0"
end
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Fri May 09 08:13:37 2014 +0200
@@ -452,8 +452,8 @@
values [random_dseq 1, 3, 3] 10 "{(xs, ys, zs::int list). append xs ys zs}"
values [random_dseq 1, 1, 4] 10 "{(xs, ys, zs::int list). append xs ys zs}"
-value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
-value [code] "Predicate.the (slice ([]::int list))"
+value "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])"
+value "Predicate.the (slice ([]::int list))"
text {* tricky case with alternative rules *}
@@ -830,7 +830,7 @@
code_pred divmod_rel .
thm divmod_rel.equation
-value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
+value "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
subsection {* Transforming predicate logic into logic programs *}
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri May 09 08:13:37 2014 +0200
@@ -183,7 +183,7 @@
quickcheck[tester = smart_exhaustive]
oops
-value [code] "prop_regex a_sol"
+value "prop_regex a_sol"
end
--- a/src/HOL/Tools/value.ML Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/Tools/value.ML Fri May 09 08:13:37 2014 +0200
@@ -1,53 +1,30 @@
-(* Title: Tools/value.ML
+(* Title: HOL/Tools/value.ML
Author: Florian Haftmann, TU Muenchen
-Generic value command for arbitrary evaluators.
+Evaluation using nbe or SML.
*)
signature VALUE =
sig
val value: Proof.context -> term -> term
- val value_select: string -> Proof.context -> term -> term
- val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
- val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
+ val value_cmd: string list -> string -> Toplevel.state -> unit
end;
structure Value : VALUE =
struct
-structure Evaluator = Theory_Data
-(
- type T = (string * (Proof.context -> term -> term)) list;
- val empty = [];
- val extend = I;
- fun merge data : T = AList.merge (op =) (K true) data;
-)
-
-val add_evaluator = Evaluator.map o AList.update (op =);
-
-fun value_select name ctxt =
- case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
- of NONE => error ("No such evaluator: " ^ name)
- | SOME f => f ctxt;
+fun value ctxt t =
+ if null (Term.add_frees t [])
+ then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
+ SOME t' => t'
+ | NONE => Nbe.dynamic_value ctxt t
+ else Nbe.dynamic_value ctxt t;
-fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
- in if null evaluators then error "No evaluators"
- else let val (evaluators, (_, evaluator)) = split_last evaluators
- in case get_first (fn (_, f) => try (f ctxt) t) evaluators
- of SOME t' => t'
- | NONE => evaluator ctxt t
- end end;
-
-fun value_maybe_select some_name =
- case some_name
- of NONE => value
- | SOME name => value_select name;
-
-fun value_cmd some_name modes raw_t state =
+fun value_cmd modes raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
- val t' = value_maybe_select some_name ctxt t;
+ val t' = value ctxt t;
val ty' = Term.type_of t';
val ctxt' = Variable.auto_fixes t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
@@ -63,14 +40,14 @@
val _ =
Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
- (opt_evaluator -- opt_modes -- Parse.term
- >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
+ (opt_modes -- Parse.term
+ >> (fn (modes, t) => Toplevel.keep (value_cmd modes t)));
val _ = Context.>> (Context.map_theory
(Thy_Output.antiquotation @{binding value}
- (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
- (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
+ (Term_Style.parse -- Args.term)
+ (fn {source, context, ...} => fn (style, t) => Thy_Output.output context
(Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
- [style (value_maybe_select some_name context t)]))));
+ [style (value context t)]))));
end;
--- a/src/HOL/ex/Eval_Examples.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Fri May 09 08:13:37 2014 +0200
@@ -25,36 +25,20 @@
text {* term evaluation *}
value "(Suc 2 + 1) * 4"
-value [code] "(Suc 2 + 1) * 4"
-value [nbe] "(Suc 2 + 1) * 4"
value "(Suc 2 + Suc 0) * Suc 3"
-value [code] "(Suc 2 + Suc 0) * Suc 3"
-value [nbe] "(Suc 2 + Suc 0) * Suc 3"
value "nat 100"
-value [code] "nat 100"
-value [nbe] "nat 100"
value "(10::int) \<le> 12"
-value [code] "(10::int) \<le> 12"
-value [nbe] "(10::int) \<le> 12"
value "max (2::int) 4"
-value [code] "max (2::int) 4"
-value [nbe] "max (2::int) 4"
value "of_int 2 / of_int 4 * (1::rat)"
-value [code] "of_int 2 / of_int 4 * (1::rat)"
-value [nbe] "of_int 2 / of_int 4 * (1::rat)"
value "[] :: nat list"
-value [code] "[] :: nat list"
-value [nbe] "[] :: nat list"
value "[(nat 100, ())]"
-value [code] "[(nat 100, ())]"
-value [nbe] "[(nat 100, ())]"
text {* a fancy datatype *}
@@ -67,7 +51,5 @@
| Blubb "('a, 'b) foo"
value "Bla (Bar (4::nat) [Suc 0])"
-value [code] "Bla (Bar (4::nat) [Suc 0])"
-value [nbe] "Bla (Bar (4::nat) [Suc 0])"
end
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Fri May 09 08:13:37 2014 +0200
@@ -68,20 +68,20 @@
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])"
+value "rev (a#b#cs) = rev cs @ [b, a]"
+value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value "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"
+value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value "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"
+value "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)"
+value "filter (%x. x) ([True,False,x]@xs)"
+value "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
@@ -106,7 +106,7 @@
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"
+value "Suc 0 \<in> set ms"
(* non-left-linear patterns, equality by extensionality *)
@@ -115,13 +115,13 @@
lemma "(f o g) x = f (g x)" by normalization
lemma "(f o id) x = f x" by normalization
lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
-value [nbe] "(\<lambda>x. x)"
+value "(\<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))))"
+value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
(* handling of type classes in connection with equality *)
--- a/src/HOL/ex/Parallel_Example.thy Fri May 09 08:13:36 2014 +0200
+++ b/src/HOL/ex/Parallel_Example.thy Fri May 09 08:13:37 2014 +0200
@@ -93,7 +93,7 @@
(\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
in (computation_primes (), Parallel.join c))"
-value [code] "computation_future ()"
+value "computation_future ()"
definition computation_factorise :: "nat \<Rightarrow> nat list" where
"computation_factorise = Debug.timing (STR ''factorise'') factorise"
@@ -102,7 +102,7 @@
"computation_parallel _ = Debug.timing (STR ''overall computation'')
(Parallel.map computation_factorise) [20000..<20100]"
-value [code] "computation_parallel ()"
+value "computation_parallel ()"
end