# HG changeset patch
# User haftmann
# Date 1409469041 -7200
# Node ID f54a8a4134d32aa4baff4fad08a25566f637d452
# Parent  7f232ae7de7cb148eb3c1940674c75d7abf37a82
restored generic value slot, retaining default behaviour and separate approximate command

diff -r 7f232ae7de7c -r f54a8a4134d3 NEWS
--- a/NEWS	Sun Aug 31 09:10:40 2014 +0200
+++ b/NEWS	Sun Aug 31 09:10:41 2014 +0200
@@ -17,6 +17,10 @@
 
 *** HOL ***
 
+* Command and antiquotation "value" provide different evaluation slots (again),
+where the previous strategy (nbe after ML) serves as default.
+Minor INCOMPATIBILITY.
+
 * New (co)datatype package:
   - Renamed theorems:
       disc_corec ~> corec_disc
diff -r 7f232ae7de7c -r f54a8a4134d3 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Sun Aug 31 09:10:40 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Sun Aug 31 09:10:41 2014 +0200
@@ -93,6 +93,12 @@
   \noindent @{command value} tries first to evaluate using ML, falling
   back to normalization by evaluation if this fails.
 
+  A particular technique may be specified in square brackets, e.g.
+*}
+
+value %quote [nbe] "42 / (12 :: rat)"
+
+text {*
   To employ dynamic evaluation in the document generation, there is also
   a @{text value} antiquotation with the same evaluation techniques 
   as @{command value}.
@@ -166,7 +172,10 @@
   \fontsize{9pt}{12pt}\selectfont
   \begin{tabular}{ll||c|c|c}
     & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
-    \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
+    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
+      & interactive evaluation 
+      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
+      \tabularnewline
     & 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}
diff -r 7f232ae7de7c -r f54a8a4134d3 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Aug 31 09:10:40 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Aug 31 09:10:41 2014 +0200
@@ -2127,7 +2127,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) value} modes? @{syntax term}
+    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
     ;
 
     @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -2159,6 +2159,11 @@
   to the current print mode; see \secref{sec:print-modes}.
   Evaluation is tried first using ML, falling
   back to normalization by evaluation if this fails.
+  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.
 
   \item @{command (HOL) "values"}~@{text t} enumerates a set
   comprehension by evaluation and prints its values up to the given
diff -r 7f232ae7de7c -r f54a8a4134d3 src/HOL/Tools/value.ML
--- a/src/HOL/Tools/value.ML	Sun Aug 31 09:10:40 2014 +0200
+++ b/src/HOL/Tools/value.ML	Sun Aug 31 09:10:41 2014 +0200
@@ -1,30 +1,61 @@
 (*  Title:      HOL/Tools/value.ML
     Author:     Florian Haftmann, TU Muenchen
 
-Evaluation using nbe or SML.
+Generic value command for arbitrary evaluators, with default using nbe or SML.
 *)
 
 signature VALUE =
 sig
   val value: Proof.context -> term -> term
-  val value_cmd: string list -> string -> Toplevel.state -> unit
+  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
 end;
 
 structure Value : VALUE =
 struct
 
-fun value ctxt t =
+fun default_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_cmd modes raw_t state =
+structure Evaluator = Theory_Data
+(
+  type T = (string * (Proof.context -> term -> term)) list;
+  val empty = [("default", default_value)];
+  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 =
+  let
+    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
+  in
+    if null evaluators
+    then error "No evaluators"
+    else (snd o snd o split_last) evaluators ctxt
+  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 =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
-    val t' = value ctxt t;
+    val t' = value_maybe_select some_name ctxt t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
     val p = Print_Mode.with_modes modes (fn () =>
@@ -35,16 +66,23 @@
 val opt_modes =
   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
 
+val opt_evaluator =
+  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
+  
 val _ =
   Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
-    (opt_modes -- Parse.term
-      >> (fn (modes, t) => Toplevel.keep (value_cmd modes t)));
+    (opt_evaluator -- opt_modes -- Parse.term
+      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
 val _ = Context.>> (Context.map_theory
   (Thy_Output.antiquotation @{binding value}
-    (Term_Style.parse -- Args.term)
-    (fn {source, context, ...} => fn (style, t) => Thy_Output.output context
+    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
+    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
       (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
-        [style (value context t)]))));
+        [style (value_maybe_select some_name context t)]))
+  #> add_evaluator ("simp", Code_Simp.dynamic_value)
+  #> add_evaluator ("nbe", Nbe.dynamic_value)
+  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict))
+);
 
 end;