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