src/HOL/Tools/value_command.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66345 882abe912da9
child 67149 e61557884799
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/value_command.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Generic value command for arbitrary evaluators, with default using nbe or SML.
     5 *)
     6 
     7 signature VALUE_COMMAND =
     8 sig
     9   val value: Proof.context -> term -> term
    10   val value_select: string -> Proof.context -> term -> term
    11   val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    12   val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    13 end;
    14 
    15 structure Value_Command : VALUE_COMMAND =
    16 struct
    17 
    18 fun default_value ctxt t =
    19   if null (Term.add_frees t [])
    20   then Code_Evaluation.dynamic_value_strict ctxt t
    21   else Nbe.dynamic_value ctxt t;
    22 
    23 structure Evaluator = Theory_Data
    24 (
    25   type T = (string * (Proof.context -> term -> term)) list;
    26   val empty = [("default", default_value)];
    27   val extend = I;
    28   fun merge data : T = AList.merge (op =) (K true) data;
    29 )
    30 
    31 val add_evaluator = Evaluator.map o AList.update (op =);
    32 
    33 fun value_select name ctxt =
    34   case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
    35    of NONE => error ("No such evaluator: " ^ name)
    36     | SOME f => f ctxt;
    37 
    38 fun value ctxt =
    39   let
    40     val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
    41   in
    42     if null evaluators
    43     then error "No evaluators"
    44     else (snd o snd o split_last) evaluators ctxt
    45   end;
    46 
    47 fun value_maybe_select some_name =
    48   case some_name
    49     of NONE => value
    50      | SOME name => value_select name;
    51   
    52 fun value_cmd some_name modes raw_t state =
    53   let
    54     val ctxt = Toplevel.context_of state;
    55     val t = Syntax.read_term ctxt raw_t;
    56     val t' = value_maybe_select some_name ctxt t;
    57     val ty' = Term.type_of t';
    58     val ctxt' = Variable.auto_fixes t' ctxt;
    59     val p = Print_Mode.with_modes modes (fn () =>
    60       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    61         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    62   in Pretty.writeln p end;
    63 
    64 val opt_modes =
    65   Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
    66 
    67 val opt_evaluator =
    68   Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
    69   
    70 val _ =
    71   Outer_Syntax.command @{command_keyword value} "evaluate and print term"
    72     (opt_evaluator -- opt_modes -- Parse.term
    73       >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
    74 
    75 val _ = Theory.setup
    76   (Thy_Output.antiquotation @{binding value}
    77     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
    78     (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
    79       (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
    80         [style (value_maybe_select some_name context t)]))
    81   #> add_evaluator ("simp", Code_Simp.dynamic_value)
    82   #> add_evaluator ("nbe", Nbe.dynamic_value)
    83   #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict));
    84 
    85 end;