restored generic value slot, retaining default behaviour and separate approximate command
authorhaftmann
Sun Aug 31 09:10:41 2014 +0200 (2014-08-31)
changeset 58100f54a8a4134d3
parent 58099 7f232ae7de7c
child 58101 e7ebe5554281
restored generic value slot, retaining default behaviour and separate approximate command
NEWS
src/Doc/Codegen/Evaluation.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Tools/value.ML
     1.1 --- a/NEWS	Sun Aug 31 09:10:40 2014 +0200
     1.2 +++ b/NEWS	Sun Aug 31 09:10:41 2014 +0200
     1.3 @@ -17,6 +17,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Command and antiquotation "value" provide different evaluation slots (again),
     1.8 +where the previous strategy (nbe after ML) serves as default.
     1.9 +Minor INCOMPATIBILITY.
    1.10 +
    1.11  * New (co)datatype package:
    1.12    - Renamed theorems:
    1.13        disc_corec ~> corec_disc
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Sun Aug 31 09:10:40 2014 +0200
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sun Aug 31 09:10:41 2014 +0200
     2.3 @@ -93,6 +93,12 @@
     2.4    \noindent @{command value} tries first to evaluate using ML, falling
     2.5    back to normalization by evaluation if this fails.
     2.6  
     2.7 +  A particular technique may be specified in square brackets, e.g.
     2.8 +*}
     2.9 +
    2.10 +value %quote [nbe] "42 / (12 :: rat)"
    2.11 +
    2.12 +text {*
    2.13    To employ dynamic evaluation in the document generation, there is also
    2.14    a @{text value} antiquotation with the same evaluation techniques 
    2.15    as @{command value}.
    2.16 @@ -166,7 +172,10 @@
    2.17    \fontsize{9pt}{12pt}\selectfont
    2.18    \begin{tabular}{ll||c|c|c}
    2.19      & & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline
    2.20 -    \multirow{4}{1ex}{\rotatebox{90}{dynamic}}
    2.21 +    \multirow{5}{1ex}{\rotatebox{90}{dynamic}}
    2.22 +      & interactive evaluation 
    2.23 +      & @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"}
    2.24 +      \tabularnewline
    2.25      & plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5}
    2.26      & evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline
    2.27      & property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5}
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Aug 31 09:10:40 2014 +0200
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Aug 31 09:10:41 2014 +0200
     3.3 @@ -2127,7 +2127,7 @@
     3.4    \end{matharray}
     3.5  
     3.6    @{rail \<open>
     3.7 -    @@{command (HOL) value} modes? @{syntax term}
     3.8 +    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
     3.9      ;
    3.10  
    3.11      @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
    3.12 @@ -2159,6 +2159,11 @@
    3.13    to the current print mode; see \secref{sec:print-modes}.
    3.14    Evaluation is tried first using ML, falling
    3.15    back to normalization by evaluation if this fails.
    3.16 +  Alternatively a specific evaluator can be selected using square
    3.17 +  brackets; typical evaluators use the current set of code equations
    3.18 +  to normalize and include @{text simp} for fully symbolic evaluation
    3.19 +  using the simplifier, @{text nbe} for \emph{normalization by
    3.20 +  evaluation} and \emph{code} for code generation in SML.
    3.21  
    3.22    \item @{command (HOL) "values"}~@{text t} enumerates a set
    3.23    comprehension by evaluation and prints its values up to the given
     4.1 --- a/src/HOL/Tools/value.ML	Sun Aug 31 09:10:40 2014 +0200
     4.2 +++ b/src/HOL/Tools/value.ML	Sun Aug 31 09:10:41 2014 +0200
     4.3 @@ -1,30 +1,61 @@
     4.4  (*  Title:      HOL/Tools/value.ML
     4.5      Author:     Florian Haftmann, TU Muenchen
     4.6  
     4.7 -Evaluation using nbe or SML.
     4.8 +Generic value command for arbitrary evaluators, with default using nbe or SML.
     4.9  *)
    4.10  
    4.11  signature VALUE =
    4.12  sig
    4.13    val value: Proof.context -> term -> term
    4.14 -  val value_cmd: string list -> string -> Toplevel.state -> unit
    4.15 +  val value_select: string -> Proof.context -> term -> term
    4.16 +  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    4.17 +  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    4.18  end;
    4.19  
    4.20  structure Value : VALUE =
    4.21  struct
    4.22  
    4.23 -fun value ctxt t =
    4.24 +fun default_value ctxt t =
    4.25    if null (Term.add_frees t [])
    4.26    then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
    4.27      SOME t' => t'
    4.28    | NONE => Nbe.dynamic_value ctxt t
    4.29    else Nbe.dynamic_value ctxt t;
    4.30  
    4.31 -fun value_cmd modes raw_t state =
    4.32 +structure Evaluator = Theory_Data
    4.33 +(
    4.34 +  type T = (string * (Proof.context -> term -> term)) list;
    4.35 +  val empty = [("default", default_value)];
    4.36 +  val extend = I;
    4.37 +  fun merge data : T = AList.merge (op =) (K true) data;
    4.38 +)
    4.39 +
    4.40 +val add_evaluator = Evaluator.map o AList.update (op =);
    4.41 +
    4.42 +fun value_select name ctxt =
    4.43 +  case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    4.44 +   of NONE => error ("No such evaluator: " ^ name)
    4.45 +    | SOME f => f ctxt;
    4.46 +
    4.47 +fun value ctxt =
    4.48 +  let
    4.49 +    val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    4.50 +  in
    4.51 +    if null evaluators
    4.52 +    then error "No evaluators"
    4.53 +    else (snd o snd o split_last) evaluators ctxt
    4.54 +  end;
    4.55 +
    4.56 +fun value_maybe_select some_name =
    4.57 +  case some_name
    4.58 +    of NONE => value
    4.59 +     | SOME name => value_select name;
    4.60 +  
    4.61 +fun value_cmd some_name modes raw_t state =
    4.62    let
    4.63      val ctxt = Toplevel.context_of state;
    4.64      val t = Syntax.read_term ctxt raw_t;
    4.65 -    val t' = value ctxt t;
    4.66 +    val t' = value_maybe_select some_name ctxt t;
    4.67      val ty' = Term.type_of t';
    4.68      val ctxt' = Variable.auto_fixes t' ctxt;
    4.69      val p = Print_Mode.with_modes modes (fn () =>
    4.70 @@ -35,16 +66,23 @@
    4.71  val opt_modes =
    4.72    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
    4.73  
    4.74 +val opt_evaluator =
    4.75 +  Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
    4.76 +  
    4.77  val _ =
    4.78    Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
    4.79 -    (opt_modes -- Parse.term
    4.80 -      >> (fn (modes, t) => Toplevel.keep (value_cmd modes t)));
    4.81 +    (opt_evaluator -- opt_modes -- Parse.term
    4.82 +      >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
    4.83  
    4.84  val _ = Context.>> (Context.map_theory
    4.85    (Thy_Output.antiquotation @{binding value}
    4.86 -    (Term_Style.parse -- Args.term)
    4.87 -    (fn {source, context, ...} => fn (style, t) => Thy_Output.output context
    4.88 +    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    4.89 +    (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    4.90        (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    4.91 -        [style (value context t)]))));
    4.92 +        [style (value_maybe_select some_name context t)]))
    4.93 +  #> add_evaluator ("simp", Code_Simp.dynamic_value)
    4.94 +  #> add_evaluator ("nbe", Nbe.dynamic_value)
    4.95 +  #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict))
    4.96 +);
    4.97  
    4.98  end;