src/Pure/Tools/value.ML
changeset 28227 77221ee0f7b9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/value.ML	Tue Sep 16 09:21:22 2008 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +(*  Title:      Pure/Tools/value.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Value command for different evaluators.
     1.9 +*)
    1.10 +
    1.11 +signature VALUE =
    1.12 +sig
    1.13 +  val value: Proof.context -> term -> term
    1.14 +  val value_select: string -> Proof.context -> term -> term
    1.15 +  val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
    1.16 +  val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
    1.17 +end;
    1.18 +
    1.19 +structure Value : VALUE =
    1.20 +struct
    1.21 +
    1.22 +structure Evaluator = TheoryDataFun(
    1.23 +  type T = (string * (Proof.context -> term -> term)) list;
    1.24 +  val empty = [];
    1.25 +  val copy = I;
    1.26 +  val extend = I;
    1.27 +  fun merge pp = AList.merge (op =) (K true);
    1.28 +)
    1.29 +
    1.30 +val add_evaluator = Evaluator.map o AList.update (op =);
    1.31 +
    1.32 +fun value_select name ctxt =
    1.33 +  case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
    1.34 +   of NONE => error ("No such evaluator: " ^ name)
    1.35 +    | SOME f => f ctxt;
    1.36 +
    1.37 +fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
    1.38 +  in if null evaluators then error "No evaluators"
    1.39 +  else let val (evaluators, (_, evaluator)) = split_last evaluators
    1.40 +    in case get_first (fn (_, f) => try (f ctxt) t) evaluators
    1.41 +     of SOME t' => t'
    1.42 +      | NONE => evaluator ctxt t
    1.43 +  end end;
    1.44 +
    1.45 +fun value_cmd some_name modes raw_t state =
    1.46 +  let
    1.47 +    val ctxt = Toplevel.context_of state;
    1.48 +    val t = Syntax.read_term ctxt raw_t;
    1.49 +    val t' = case some_name
    1.50 +     of NONE => value ctxt t
    1.51 +      | SOME name => value_select name ctxt t;
    1.52 +    val ty' = Term.type_of t';
    1.53 +    val ctxt' = Variable.auto_fixes t ctxt;
    1.54 +    val p = PrintMode.with_modes modes (fn () =>
    1.55 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    1.56 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
    1.57 +  in Pretty.writeln p end;
    1.58 +
    1.59 +local structure P = OuterParse and K = OuterKeyword in
    1.60 +
    1.61 +val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    1.62 +
    1.63 +val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
    1.64 +  (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
    1.65 +    >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    1.66 +        (value_cmd some_name modes t)));
    1.67 +
    1.68 +end; (*local*)
    1.69 +
    1.70 +end;