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