src/Pure/Tools/value.ML
author haftmann
Tue Sep 16 09:21:22 2008 +0200 (2008-09-16)
changeset 28227 77221ee0f7b9
permissions -rw-r--r--
generic value command
     1 (*  Title:      Pure/Tools/value.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Value command for different evaluators.
     6 *)
     7 
     8 signature VALUE =
     9 sig
    10   val value: Proof.context -> term -> term
    11   val value_select: string -> Proof.context -> term -> term
    12   val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    13   val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    14 end;
    15 
    16 structure Value : VALUE =
    17 struct
    18 
    19 structure Evaluator = TheoryDataFun(
    20   type T = (string * (Proof.context -> term -> term)) list;
    21   val empty = [];
    22   val copy = I;
    23   val extend = I;
    24   fun merge pp = AList.merge (op =) (K true);
    25 )
    26 
    27 val add_evaluator = Evaluator.map o AList.update (op =);
    28 
    29 fun value_select name ctxt =
    30   case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
    31    of NONE => error ("No such evaluator: " ^ name)
    32     | SOME f => f ctxt;
    33 
    34 fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
    35   in if null evaluators then error "No evaluators"
    36   else let val (evaluators, (_, evaluator)) = split_last evaluators
    37     in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    38      of SOME t' => t'
    39       | NONE => evaluator ctxt t
    40   end end;
    41 
    42 fun value_cmd some_name modes raw_t state =
    43   let
    44     val ctxt = Toplevel.context_of state;
    45     val t = Syntax.read_term ctxt raw_t;
    46     val t' = case some_name
    47      of NONE => value ctxt t
    48       | SOME name => value_select name ctxt t;
    49     val ty' = Term.type_of t';
    50     val ctxt' = Variable.auto_fixes t ctxt;
    51     val p = PrintMode.with_modes modes (fn () =>
    52       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    53         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    54   in Pretty.writeln p end;
    55 
    56 local structure P = OuterParse and K = OuterKeyword in
    57 
    58 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    59 
    60 val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
    61   (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
    62     >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    63         (value_cmd some_name modes t)));
    64 
    65 end; (*local*)
    66 
    67 end;