author | haftmann |
Wed, 27 Feb 2008 21:41:06 +0100 | |
changeset 26168 | 3bd9ac4e0b97 |
parent 26037 | 8bf9e480a7b8 |
child 26242 | d64510d3c7b7 |
permissions | -rw-r--r-- |
22525 | 1 |
(* Title: HOL/Library/Eval.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* A simple term evaluation mechanism *} |
|
7 |
||
8 |
theory Eval |
|
26037 | 9 |
imports |
26168 | 10 |
RType |
26037 | 11 |
Code_Index (* this theory is just imported for a term_of setup *) |
22525 | 12 |
begin |
13 |
||
25763 | 14 |
subsection {* Term representation *} |
15 |
||
26020 | 16 |
subsubsection {* Definitions *} |
17 |
||
18 |
datatype "term" = dummy_term |
|
25763 | 19 |
|
26020 | 20 |
definition |
26168 | 21 |
Const :: "message_string \<Rightarrow> rtype \<Rightarrow> term" |
26020 | 22 |
where |
23 |
"Const _ _ = dummy_term" |
|
25763 | 24 |
|
26020 | 25 |
definition |
26 |
App :: "term \<Rightarrow> term \<Rightarrow> term" |
|
27 |
where |
|
28 |
"App _ _ = dummy_term" |
|
29 |
||
30 |
code_datatype Const App |
|
25763 | 31 |
|
26168 | 32 |
|
26020 | 33 |
subsubsection {* Class @{term term_of} *} |
34 |
||
26168 | 35 |
class term_of = rtype + |
36 |
constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> rtype" |
|
26020 | 37 |
fixes term_of :: "'a \<Rightarrow> term" |
38 |
||
39 |
lemma term_of_anything: "term_of x \<equiv> t" |
|
40 |
by (rule eq_reflection) (cases "term_of x", cases t, simp) |
|
25763 | 41 |
|
42 |
ML {* |
|
26020 | 43 |
structure Eval = |
25763 | 44 |
struct |
45 |
||
46 |
fun mk_term f g (Const (c, ty)) = |
|
47 |
@{term Const} $ Message_String.mk c $ g ty |
|
48 |
| mk_term f g (t1 $ t2) = |
|
49 |
@{term App} $ mk_term f g t1 $ mk_term f g t2 |
|
50 |
| mk_term f g (Free v) = f v; |
|
51 |
||
26020 | 52 |
fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t; |
22525 | 53 |
|
54 |
end; |
|
55 |
*} |
|
56 |
||
57 |
setup {* |
|
58 |
let |
|
26020 | 59 |
fun add_term_of_def ty vs tyco thy = |
22525 | 60 |
let |
26020 | 61 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
62 |
$ Free ("x", ty); |
|
63 |
val rhs = @{term "undefined \<Colon> term"}; |
|
64 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
65 |
in |
|
25536 | 66 |
thy |
26020 | 67 |
|> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) |
68 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
69 |
|-> (fn eq => Specification.definition (NONE, (("", []), eq))) |
|
25569 | 70 |
|> snd |
71 |
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
72 |
|> LocalTheory.exit |
|
73 |
|> ProofContext.theory_of |
|
26020 | 74 |
end; |
75 |
fun interpretator (tyco, (raw_vs, _)) thy = |
|
76 |
let |
|
26168 | 77 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
26020 | 78 |
val constrain_sort = |
79 |
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
80 |
val vs = (map o apsnd) constrain_sort raw_vs; |
|
81 |
val ty = Type (tyco, map TFree vs); |
|
82 |
in |
|
83 |
thy |
|
26168 | 84 |
|> RType.perhaps_add_def tyco |
85 |
|> not has_inst ? add_term_of_def ty vs tyco |
|
26020 | 86 |
end; |
87 |
in |
|
26168 | 88 |
Code.type_interpretation interpretator |
26020 | 89 |
end |
22525 | 90 |
*} |
91 |
||
26020 | 92 |
setup {* |
93 |
let |
|
94 |
fun mk_term_of_eq ty vs tyco (c, tys) = |
|
95 |
let |
|
96 |
val t = list_comb (Const (c, tys ---> ty), |
|
97 |
map Free (Name.names Name.context "a" tys)); |
|
98 |
in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term |
|
99 |
(fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) |
|
26168 | 100 |
(RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t) |
26020 | 101 |
end; |
102 |
fun prove_term_of_eq ty eq thy = |
|
103 |
let |
|
104 |
val cty = Thm.ctyp_of thy ty; |
|
105 |
val (arg, rhs) = pairself (Thm.cterm_of thy) eq; |
|
106 |
val thm = @{thm term_of_anything} |
|
107 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
108 |
|> Thm.varifyT; |
|
109 |
in |
|
110 |
thy |
|
111 |
|> Code.add_func thm |
|
112 |
end; |
|
113 |
fun interpretator (tyco, (raw_vs, raw_cs)) thy = |
|
114 |
let |
|
115 |
val constrain_sort = |
|
116 |
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
117 |
val vs = (map o apsnd) constrain_sort raw_vs; |
|
118 |
val cs = (map o apsnd o map o map_atyps) |
|
119 |
(fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; |
|
120 |
val ty = Type (tyco, map TFree vs); |
|
121 |
val eqs = map (mk_term_of_eq ty vs tyco) cs; |
|
122 |
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
123 |
in |
|
124 |
thy |
|
125 |
|> Code.del_funcs const |
|
126 |
|> fold (prove_term_of_eq ty) eqs |
|
127 |
end; |
|
128 |
in |
|
129 |
Code.type_interpretation interpretator |
|
25569 | 130 |
end |
26020 | 131 |
*} |
23062 | 132 |
|
25763 | 133 |
subsubsection {* Code generator setup *} |
134 |
||
135 |
lemmas [code func del] = term.recs term.cases term.size |
|
136 |
lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" .. |
|
26037 | 137 |
|
26168 | 138 |
lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" .. |
26037 | 139 |
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
140 |
lemma [code func, code func del]: "(term_of \<Colon> index \<Rightarrow> term) = term_of" .. |
|
26020 | 141 |
lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
22525 | 142 |
|
25763 | 143 |
code_type "term" |
144 |
(SML "Term.term") |
|
145 |
||
26020 | 146 |
code_const Const and App |
147 |
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") |
|
22525 | 148 |
|
26037 | 149 |
code_const "term_of \<Colon> index \<Rightarrow> term" |
150 |
(SML "HOLogic.mk'_number/ HOLogic.indexT") |
|
151 |
||
152 |
code_const "term_of \<Colon> message_string \<Rightarrow> term" |
|
153 |
(SML "Message'_String.mk") |
|
154 |
||
155 |
||
25763 | 156 |
subsection {* Evaluation setup *} |
22525 | 157 |
|
158 |
ML {* |
|
159 |
signature EVAL = |
|
160 |
sig |
|
24587 | 161 |
val eval_ref: (unit -> term) option ref |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
162 |
val eval_term: theory -> term -> term |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
163 |
val evaluate: Proof.context -> term -> unit |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
164 |
val evaluate': string -> Proof.context -> term -> unit |
26020 | 165 |
val evaluate_cmd: string option -> string -> Toplevel.state -> unit |
22525 | 166 |
end; |
167 |
||
26020 | 168 |
structure Eval : EVAL = |
22525 | 169 |
struct |
170 |
||
26020 | 171 |
open Eval; |
172 |
||
24587 | 173 |
val eval_ref = ref (NONE : (unit -> term) option); |
22525 | 174 |
|
26020 | 175 |
fun eval_term thy t = |
176 |
t |
|
177 |
|> Eval.mk_term_of (fastype_of t) |
|
178 |
|> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t []) |
|
179 |
|> Code.postprocess_term thy; |
|
24280 | 180 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
181 |
val evaluators = [ |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
182 |
("code", eval_term), |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
183 |
("SML", Codegen.eval_term), |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
184 |
("normal_form", Nbe.norm_term) |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
185 |
]; |
22525 | 186 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
187 |
fun gen_evaluate evaluators ctxt t = |
24280 | 188 |
let |
189 |
val thy = ProofContext.theory_of ctxt; |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
190 |
val (evls, evl) = split_last evaluators; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
191 |
val t' = case get_first (fn f => try (f thy) t) evls |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
192 |
of SOME t' => t' |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
193 |
| NONE => evl thy t; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
194 |
val ty' = Term.type_of t'; |
24920 | 195 |
val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'), |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
196 |
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, |
24920 | 197 |
Pretty.quote (Syntax.pretty_typ ctxt ty')]; |
24280 | 198 |
in Pretty.writeln p end; |
199 |
||
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
200 |
val evaluate = gen_evaluate (map snd evaluators); |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
201 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
202 |
fun evaluate' name = gen_evaluate |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
203 |
[(the o AList.lookup (op =) evaluators) name]; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
204 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
205 |
fun evaluate_cmd some_name raw_t state = |
22525 | 206 |
let |
22804 | 207 |
val ctxt = Toplevel.context_of state; |
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24423
diff
changeset
|
208 |
val t = Syntax.read_term ctxt raw_t; |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
209 |
in case some_name |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
210 |
of NONE => evaluate ctxt t |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
211 |
| SOME name => evaluate' name ctxt t |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
212 |
end; |
22525 | 213 |
|
214 |
end; |
|
215 |
*} |
|
216 |
||
22804 | 217 |
ML {* |
218 |
OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
219 |
(Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")") |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
220 |
-- OuterParse.term |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
221 |
>> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
222 |
(Eval.evaluate_cmd some_name t))); |
22804 | 223 |
*} |
224 |
||
26032 | 225 |
print_translation {* |
226 |
let |
|
227 |
val term = Const ("<TERM>", dummyT); |
|
228 |
fun tr1' [_, _] = term; |
|
229 |
fun tr2' [] = term; |
|
230 |
in |
|
231 |
[(@{const_syntax Const}, tr1'), |
|
232 |
(@{const_syntax App}, tr1'), |
|
233 |
(@{const_syntax dummy_term}, tr2')] |
|
234 |
end |
|
235 |
*} |
|
236 |
||
26168 | 237 |
hide (open) const term_of |
26032 | 238 |
hide const Const App dummy_term |
26020 | 239 |
|
22665 | 240 |
end |