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