src/Tools/value.ML
author wenzelm
Sun Nov 08 18:43:42 2009 +0100 (2009-11-08)
changeset 33522 737589bb9bb8
parent 31218 fa54c1e614df
child 36960 01594f816e3a
permissions -rw-r--r--
adapted Theory_Data;
tuned;
     1 (*  Title:      Pure/Tools/value.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Generic value command for arbitrary evaluators.
     5 *)
     6 
     7 signature VALUE =
     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 : VALUE =
    16 struct
    17 
    18 structure Evaluator = Theory_Data
    19 (
    20   type T = (string * (Proof.context -> term -> term)) list;
    21   val empty = [];
    22   val extend = I;
    23   fun merge data : T = AList.merge (op =) (K true) data;
    24 )
    25 
    26 val add_evaluator = Evaluator.map o AList.update (op =);
    27 
    28 fun value_select name ctxt =
    29   case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
    30    of NONE => error ("No such evaluator: " ^ name)
    31     | SOME f => f ctxt;
    32 
    33 fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
    34   in if null evaluators then error "No evaluators"
    35   else let val (evaluators, (_, evaluator)) = split_last evaluators
    36     in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    37      of SOME t' => t'
    38       | NONE => evaluator ctxt t
    39   end end;
    40 
    41 fun value_cmd some_name modes raw_t state =
    42   let
    43     val ctxt = Toplevel.context_of state;
    44     val t = Syntax.read_term ctxt raw_t;
    45     val t' = case some_name
    46      of NONE => value ctxt t
    47       | SOME name => value_select name ctxt t;
    48     val ty' = Term.type_of t';
    49     val ctxt' = Variable.auto_fixes t' ctxt;
    50     val p = PrintMode.with_modes modes (fn () =>
    51       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    52         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    53   in Pretty.writeln p end;
    54 
    55 local structure P = OuterParse and K = OuterKeyword in
    56 
    57 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    58 
    59 val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
    60   (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
    61     >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    62         (value_cmd some_name modes t)));
    63 
    64 end; (*local*)
    65 
    66 end;