haftmann@37743
|
1 |
(* Title: Tools/value.ML
|
haftmann@28227
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@28227
|
3 |
|
haftmann@28952
|
4 |
Generic value command for arbitrary evaluators.
|
haftmann@28227
|
5 |
*)
|
haftmann@28227
|
6 |
|
haftmann@28227
|
7 |
signature VALUE =
|
haftmann@28227
|
8 |
sig
|
haftmann@28227
|
9 |
val value: Proof.context -> term -> term
|
haftmann@28227
|
10 |
val value_select: string -> Proof.context -> term -> term
|
haftmann@28227
|
11 |
val value_cmd: string option -> string list -> string -> Toplevel.state -> unit
|
haftmann@28227
|
12 |
val add_evaluator: string * (Proof.context -> term -> term) -> theory -> theory
|
bulwahn@44482
|
13 |
val setup : theory -> theory
|
haftmann@28227
|
14 |
end;
|
haftmann@28227
|
15 |
|
haftmann@28227
|
16 |
structure Value : VALUE =
|
haftmann@28227
|
17 |
struct
|
haftmann@28227
|
18 |
|
wenzelm@33522
|
19 |
structure Evaluator = Theory_Data
|
wenzelm@33522
|
20 |
(
|
haftmann@28227
|
21 |
type T = (string * (Proof.context -> term -> term)) list;
|
haftmann@28227
|
22 |
val empty = [];
|
haftmann@28227
|
23 |
val extend = I;
|
wenzelm@33522
|
24 |
fun merge data : T = AList.merge (op =) (K true) data;
|
haftmann@28227
|
25 |
)
|
haftmann@28227
|
26 |
|
haftmann@28227
|
27 |
val add_evaluator = Evaluator.map o AList.update (op =);
|
haftmann@28227
|
28 |
|
haftmann@28227
|
29 |
fun value_select name ctxt =
|
wenzelm@43232
|
30 |
case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name
|
haftmann@28227
|
31 |
of NONE => error ("No such evaluator: " ^ name)
|
haftmann@28227
|
32 |
| SOME f => f ctxt;
|
haftmann@28227
|
33 |
|
wenzelm@43232
|
34 |
fun value ctxt t = let val evaluators = Evaluator.get (Proof_Context.theory_of ctxt)
|
haftmann@28227
|
35 |
in if null evaluators then error "No evaluators"
|
haftmann@28227
|
36 |
else let val (evaluators, (_, evaluator)) = split_last evaluators
|
haftmann@28227
|
37 |
in case get_first (fn (_, f) => try (f ctxt) t) evaluators
|
haftmann@28227
|
38 |
of SOME t' => t'
|
haftmann@28227
|
39 |
| NONE => evaluator ctxt t
|
haftmann@28227
|
40 |
end end;
|
haftmann@28227
|
41 |
|
bulwahn@44482
|
42 |
fun value_maybe_select some_name =
|
bulwahn@44482
|
43 |
case some_name
|
bulwahn@44482
|
44 |
of NONE => value
|
bulwahn@44482
|
45 |
| SOME name => value_select name;
|
bulwahn@44482
|
46 |
|
haftmann@28227
|
47 |
fun value_cmd some_name modes raw_t state =
|
haftmann@28227
|
48 |
let
|
haftmann@28227
|
49 |
val ctxt = Toplevel.context_of state;
|
haftmann@28227
|
50 |
val t = Syntax.read_term ctxt raw_t;
|
bulwahn@44482
|
51 |
val t' = value_maybe_select some_name ctxt t;
|
haftmann@28227
|
52 |
val ty' = Term.type_of t';
|
haftmann@31218
|
53 |
val ctxt' = Variable.auto_fixes t' ctxt;
|
wenzelm@37154
|
54 |
val p = Print_Mode.with_modes modes (fn () =>
|
haftmann@28227
|
55 |
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
haftmann@28227
|
56 |
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
haftmann@28227
|
57 |
in Pretty.writeln p end;
|
haftmann@28227
|
58 |
|
wenzelm@36970
|
59 |
val opt_modes =
|
wenzelm@47823
|
60 |
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
|
haftmann@28227
|
61 |
|
bulwahn@44482
|
62 |
val opt_evaluator =
|
wenzelm@47823
|
63 |
Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
|
bulwahn@44482
|
64 |
|
wenzelm@36970
|
65 |
val _ =
|
wenzelm@36970
|
66 |
Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
|
bulwahn@44482
|
67 |
(opt_evaluator -- opt_modes -- Parse.term
|
wenzelm@36970
|
68 |
>> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
|
wenzelm@36970
|
69 |
(value_cmd some_name modes t)));
|
haftmann@28227
|
70 |
|
bulwahn@44482
|
71 |
val antiq_setup =
|
wenzelm@44500
|
72 |
Thy_Output.antiquotation @{binding value}
|
bulwahn@44482
|
73 |
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
|
bulwahn@44482
|
74 |
(fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
|
bulwahn@44482
|
75 |
(Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
|
bulwahn@44482
|
76 |
[style (value_maybe_select some_name context t)]));
|
bulwahn@44482
|
77 |
|
bulwahn@44482
|
78 |
val setup = antiq_setup;
|
bulwahn@44482
|
79 |
|
haftmann@28227
|
80 |
end;
|