|
1 (* Title: HOL/Tools/value_command.ML |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 |
|
4 Generic value command for arbitrary evaluators, with default using nbe or SML. |
|
5 *) |
|
6 |
|
7 signature VALUE_COMMAND = |
|
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_Command : VALUE_COMMAND = |
|
16 struct |
|
17 |
|
18 fun default_value ctxt t = |
|
19 if null (Term.add_frees t []) |
|
20 then case try (Code_Evaluation.dynamic_value_strict ctxt) t of |
|
21 SOME t' => t' |
|
22 | NONE => Nbe.dynamic_value ctxt t |
|
23 else Nbe.dynamic_value ctxt t; |
|
24 |
|
25 structure Evaluator = Theory_Data |
|
26 ( |
|
27 type T = (string * (Proof.context -> term -> term)) list; |
|
28 val empty = [("default", default_value)]; |
|
29 val extend = I; |
|
30 fun merge data : T = AList.merge (op =) (K true) data; |
|
31 ) |
|
32 |
|
33 val add_evaluator = Evaluator.map o AList.update (op =); |
|
34 |
|
35 fun value_select name ctxt = |
|
36 case AList.lookup (op =) (Evaluator.get (Proof_Context.theory_of ctxt)) name |
|
37 of NONE => error ("No such evaluator: " ^ name) |
|
38 | SOME f => f ctxt; |
|
39 |
|
40 fun value ctxt = |
|
41 let |
|
42 val evaluators = Evaluator.get (Proof_Context.theory_of ctxt) |
|
43 in |
|
44 if null evaluators |
|
45 then error "No evaluators" |
|
46 else (snd o snd o split_last) evaluators ctxt |
|
47 end; |
|
48 |
|
49 fun value_maybe_select some_name = |
|
50 case some_name |
|
51 of NONE => value |
|
52 | SOME name => value_select name; |
|
53 |
|
54 fun value_cmd some_name modes raw_t state = |
|
55 let |
|
56 val ctxt = Toplevel.context_of state; |
|
57 val t = Syntax.read_term ctxt raw_t; |
|
58 val t' = value_maybe_select some_name ctxt t; |
|
59 val ty' = Term.type_of t'; |
|
60 val ctxt' = Variable.auto_fixes t' ctxt; |
|
61 val p = Print_Mode.with_modes modes (fn () => |
|
62 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
|
63 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); |
|
64 in Pretty.writeln p end; |
|
65 |
|
66 val opt_modes = |
|
67 Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; |
|
68 |
|
69 val opt_evaluator = |
|
70 Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"}) |
|
71 |
|
72 val _ = |
|
73 Outer_Syntax.command @{command_keyword value} "evaluate and print term" |
|
74 (opt_evaluator -- opt_modes -- Parse.term |
|
75 >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t))); |
|
76 |
|
77 val _ = Theory.setup |
|
78 (Thy_Output.antiquotation @{binding value} |
|
79 (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) |
|
80 (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context |
|
81 (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source |
|
82 [style (value_maybe_select some_name context t)])) |
|
83 #> add_evaluator ("simp", Code_Simp.dynamic_value) |
|
84 #> add_evaluator ("nbe", Nbe.dynamic_value) |
|
85 #> add_evaluator ("code", Code_Evaluation.dynamic_value_strict)); |
|
86 |
|
87 end; |