--- a/src/Pure/Tools/value.ML Wed Dec 03 09:53:58 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Title: Pure/Tools/value.ML
- ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-
-Value command for different evaluators.
-*)
-
-signature VALUE =
-sig
- val value: Proof.context -> term -> term
- val value_select: string -> Proof.context -> term -> term
- val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
- val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
-end;
-
-structure Value : VALUE =
-struct
-
-structure Evaluator = TheoryDataFun(
- type T = (string * (Proof.context -> term -> term)) list;
- val empty = [];
- val copy = I;
- val extend = I;
- fun merge pp = AList.merge (op =) (K true);
-)
-
-val add_evaluator = Evaluator.map o AList.update (op =);
-
-fun value_select name ctxt =
- case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
- of NONE => error ("No such evaluator: " ^ name)
- | SOME f => f ctxt;
-
-fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
- in if null evaluators then error "No evaluators"
- else let val (evaluators, (_, evaluator)) = split_last evaluators
- in case get_first (fn (_, f) => try (f ctxt) t) evaluators
- of SOME t' => t'
- | NONE => evaluator ctxt t
- end end;
-
-fun value_cmd some_name modes raw_t state =
- let
- val ctxt = Toplevel.context_of state;
- val t = Syntax.read_term ctxt raw_t;
- val t' = case some_name
- of NONE => value ctxt t
- | SOME name => value_select name ctxt t;
- val ty' = Term.type_of t';
- val ctxt' = Variable.auto_fixes t ctxt;
- val p = PrintMode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
- in Pretty.writeln p end;
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-
-val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
- (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
- >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
- (value_cmd some_name modes t)));
-
-end; (*local*)
-
-end;