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