author | chaieb |
Mon, 25 Feb 2008 11:59:57 +0100 | |
changeset 26125 | 345465cc9e79 |
parent 26037 | 8bf9e480a7b8 |
child 26168 | 3bd9ac4e0b97 |
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 |
10 |
ATP_Linkup Code_Message |
|
11 |
Code_Index (* this theory is just imported for a term_of setup *) |
|
22525 | 12 |
begin |
13 |
||
25763 | 14 |
subsection {* Type reflection *} |
15 |
||
16 |
subsubsection {* Definition *} |
|
17 |
||
18 |
types vname = message_string; |
|
19 |
types "class" = message_string; |
|
20 |
types sort = "class list" |
|
21 |
||
22 |
datatype "typ" = |
|
23 |
Type message_string "typ list" |
|
24 |
| TFree vname sort |
|
25 |
||
26 |
ML {* |
|
26020 | 27 |
structure Eval = |
25763 | 28 |
struct |
29 |
||
30 |
val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk; |
|
31 |
||
32 |
fun mk_typ f (Type (tyco, tys)) = |
|
33 |
@{term Type} $ Message_String.mk tyco |
|
34 |
$ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys) |
|
35 |
| mk_typ f (TFree v) = |
|
36 |
f v; |
|
37 |
||
38 |
end; |
|
39 |
*} |
|
40 |
||
41 |
||
42 |
subsubsection {* Class @{text typ_of} *} |
|
22525 | 43 |
|
23062 | 44 |
class typ_of = |
45 |
fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ" |
|
22525 | 46 |
|
47 |
ML {* |
|
26020 | 48 |
structure Eval = |
22525 | 49 |
struct |
50 |
||
26020 | 51 |
open Eval; |
25763 | 52 |
|
53 |
fun mk_typ_of ty = |
|
22525 | 54 |
Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) |
55 |
$ Logic.mk_type ty; |
|
56 |
||
26020 | 57 |
fun add_typ_of_def tyco thy = |
58 |
let |
|
59 |
val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of}; |
|
60 |
val vs = Name.names Name.context "'a" sorts; |
|
61 |
val ty = Type (tyco, map TFree vs); |
|
62 |
val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) |
|
63 |
$ Free ("T", Term.itselfT ty); |
|
64 |
val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty; |
|
65 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
66 |
in |
|
67 |
thy |
|
68 |
|> TheoryTarget.instantiation ([tyco], vs, @{sort typ_of}) |
|
69 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
70 |
|-> (fn eq => Specification.definition (NONE, (("", []), eq))) |
|
71 |
|> snd |
|
72 |
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
73 |
|> LocalTheory.exit |
|
74 |
|> ProofContext.theory_of |
|
75 |
end; |
|
76 |
||
25536 | 77 |
end |
22525 | 78 |
*} |
79 |
||
26020 | 80 |
(*setup {* |
22525 | 81 |
let |
26020 | 82 |
open Eval; |
83 |
in |
|
84 |
Eval.add_typ_of_def @{type_name prop} |
|
26037 | 85 |
#> Eval.add_typ_of_def @{type_name fun} |
26020 | 86 |
#> Eval.add_typ_of_def @{type_name itself} |
87 |
#> Eval.add_typ_of_def @{type_name bool} |
|
88 |
#> Eval.add_typ_of_def @{type_name set} |
|
89 |
#> TypedefPackage.interpretation Eval.add_typ_of_def |
|
25536 | 90 |
end |
26020 | 91 |
*}*) |
22525 | 92 |
|
25763 | 93 |
subsubsection {* Code generator setup *} |
94 |
||
95 |
lemma [code func]: |
|
26020 | 96 |
"Type tyco1 tys1 = Type tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2 |
25763 | 97 |
\<and> list_all2 (op =) tys1 tys2" |
98 |
by (auto simp add: list_all2_eq [symmetric]) |
|
99 |
||
100 |
code_type "typ" |
|
101 |
(SML "Term.typ") |
|
102 |
||
103 |
code_const Type and TFree |
|
104 |
(SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)") |
|
105 |
||
106 |
code_reserved SML Term |
|
107 |
||
108 |
||
109 |
subsection {* Term representation *} |
|
110 |
||
26020 | 111 |
subsubsection {* Definitions *} |
112 |
||
113 |
datatype "term" = dummy_term |
|
25763 | 114 |
|
26020 | 115 |
definition |
116 |
Const :: "message_string \<Rightarrow> typ \<Rightarrow> term" |
|
117 |
where |
|
118 |
"Const _ _ = dummy_term" |
|
25763 | 119 |
|
26020 | 120 |
definition |
121 |
App :: "term \<Rightarrow> term \<Rightarrow> term" |
|
122 |
where |
|
123 |
"App _ _ = dummy_term" |
|
124 |
||
125 |
code_datatype Const App |
|
25763 | 126 |
|
26020 | 127 |
subsubsection {* Class @{term term_of} *} |
128 |
||
129 |
class term_of = typ_of + |
|
130 |
constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ" |
|
131 |
fixes term_of :: "'a \<Rightarrow> term" |
|
132 |
||
133 |
lemma term_of_anything: "term_of x \<equiv> t" |
|
134 |
by (rule eq_reflection) (cases "term_of x", cases t, simp) |
|
25763 | 135 |
|
136 |
ML {* |
|
26020 | 137 |
structure Eval = |
25763 | 138 |
struct |
139 |
||
26020 | 140 |
open Eval; |
25763 | 141 |
|
142 |
fun mk_term f g (Const (c, ty)) = |
|
143 |
@{term Const} $ Message_String.mk c $ g ty |
|
144 |
| mk_term f g (t1 $ t2) = |
|
145 |
@{term App} $ mk_term f g t1 $ mk_term f g t2 |
|
146 |
| mk_term f g (Free v) = f v; |
|
147 |
||
26020 | 148 |
fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t; |
22525 | 149 |
|
150 |
end; |
|
151 |
*} |
|
152 |
||
153 |
setup {* |
|
154 |
let |
|
26020 | 155 |
fun has_no_inst tyco sort thy = |
156 |
not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) |
|
157 |
sort); |
|
158 |
fun add_term_of_def ty vs tyco thy = |
|
22525 | 159 |
let |
26020 | 160 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
161 |
$ Free ("x", ty); |
|
162 |
val rhs = @{term "undefined \<Colon> term"}; |
|
163 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
164 |
in |
|
25536 | 165 |
thy |
26020 | 166 |
|> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) |
167 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
168 |
|-> (fn eq => Specification.definition (NONE, (("", []), eq))) |
|
25569 | 169 |
|> snd |
170 |
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
171 |
|> LocalTheory.exit |
|
172 |
|> ProofContext.theory_of |
|
26020 | 173 |
end; |
174 |
fun interpretator (tyco, (raw_vs, _)) thy = |
|
175 |
let |
|
176 |
val constrain_sort = |
|
177 |
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
178 |
val vs = (map o apsnd) constrain_sort raw_vs; |
|
179 |
val ty = Type (tyco, map TFree vs); |
|
180 |
in |
|
181 |
thy |
|
182 |
|> `(has_no_inst tyco @{sort typ_of}) |
|
183 |
|-> (fn no_typ_of => no_typ_of ? Eval.add_typ_of_def tyco) |
|
184 |
|> `(has_no_inst tyco @{sort term_of}) |
|
185 |
|-> (fn no_term_of => no_term_of ? add_term_of_def ty vs tyco) |
|
186 |
end; |
|
187 |
in |
|
26037 | 188 |
Eval.add_typ_of_def @{type_name fun} |
189 |
#> Code.type_interpretation interpretator |
|
26020 | 190 |
end |
22525 | 191 |
*} |
192 |
||
26020 | 193 |
setup {* |
194 |
let |
|
195 |
fun mk_term_of_eq ty vs tyco (c, tys) = |
|
196 |
let |
|
197 |
val t = list_comb (Const (c, tys ---> ty), |
|
198 |
map Free (Name.names Name.context "a" tys)); |
|
199 |
in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term |
|
200 |
(fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) |
|
201 |
(Eval.mk_typ (fn (v, sort) => Eval.mk_typ_of (TFree (v, sort)))) t) |
|
202 |
end; |
|
203 |
fun prove_term_of_eq ty eq thy = |
|
204 |
let |
|
205 |
val cty = Thm.ctyp_of thy ty; |
|
206 |
val (arg, rhs) = pairself (Thm.cterm_of thy) eq; |
|
207 |
val thm = @{thm term_of_anything} |
|
208 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
209 |
|> Thm.varifyT; |
|
210 |
in |
|
211 |
thy |
|
212 |
|> Code.add_func thm |
|
213 |
end; |
|
214 |
fun interpretator (tyco, (raw_vs, raw_cs)) thy = |
|
215 |
let |
|
216 |
val constrain_sort = |
|
217 |
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
218 |
val vs = (map o apsnd) constrain_sort raw_vs; |
|
219 |
val cs = (map o apsnd o map o map_atyps) |
|
220 |
(fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; |
|
221 |
val ty = Type (tyco, map TFree vs); |
|
222 |
val eqs = map (mk_term_of_eq ty vs tyco) cs; |
|
223 |
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
224 |
in |
|
225 |
thy |
|
226 |
|> Code.del_funcs const |
|
227 |
|> fold (prove_term_of_eq ty) eqs |
|
228 |
end; |
|
229 |
in |
|
230 |
Code.type_interpretation interpretator |
|
25569 | 231 |
end |
26020 | 232 |
*} |
23062 | 233 |
|
25763 | 234 |
subsubsection {* Code generator setup *} |
235 |
||
236 |
lemmas [code func del] = term.recs term.cases term.size |
|
237 |
lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" .. |
|
26037 | 238 |
|
239 |
lemma [code func, code func del]: "(term_of \<Colon> typ \<Rightarrow> term) = term_of" .. |
|
240 |
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
|
241 |
lemma [code func, code func del]: "(term_of \<Colon> index \<Rightarrow> term) = term_of" .. |
|
26020 | 242 |
lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
22525 | 243 |
|
25763 | 244 |
code_type "term" |
245 |
(SML "Term.term") |
|
246 |
||
26020 | 247 |
code_const Const and App |
248 |
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") |
|
22525 | 249 |
|
26037 | 250 |
code_const "term_of \<Colon> index \<Rightarrow> term" |
251 |
(SML "HOLogic.mk'_number/ HOLogic.indexT") |
|
252 |
||
253 |
code_const "term_of \<Colon> message_string \<Rightarrow> term" |
|
254 |
(SML "Message'_String.mk") |
|
255 |
||
256 |
||
25763 | 257 |
subsection {* Evaluation setup *} |
22525 | 258 |
|
259 |
ML {* |
|
260 |
signature EVAL = |
|
261 |
sig |
|
24587 | 262 |
val eval_ref: (unit -> term) option ref |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
263 |
val eval_term: theory -> term -> term |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
264 |
val evaluate: Proof.context -> term -> unit |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
265 |
val evaluate': string -> Proof.context -> term -> unit |
26020 | 266 |
val evaluate_cmd: string option -> string -> Toplevel.state -> unit |
22525 | 267 |
end; |
268 |
||
26020 | 269 |
structure Eval : EVAL = |
22525 | 270 |
struct |
271 |
||
26020 | 272 |
open Eval; |
273 |
||
24587 | 274 |
val eval_ref = ref (NONE : (unit -> term) option); |
22525 | 275 |
|
26020 | 276 |
fun eval_term thy t = |
277 |
t |
|
278 |
|> Eval.mk_term_of (fastype_of t) |
|
279 |
|> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t []) |
|
280 |
|> Code.postprocess_term thy; |
|
24280 | 281 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
282 |
val evaluators = [ |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
283 |
("code", eval_term), |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
284 |
("SML", Codegen.eval_term), |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
285 |
("normal_form", Nbe.norm_term) |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
286 |
]; |
22525 | 287 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
288 |
fun gen_evaluate evaluators ctxt t = |
24280 | 289 |
let |
290 |
val thy = ProofContext.theory_of ctxt; |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
291 |
val (evls, evl) = split_last evaluators; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
292 |
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
|
293 |
of SOME t' => t' |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
294 |
| NONE => evl thy t; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
295 |
val ty' = Term.type_of t'; |
24920 | 296 |
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
|
297 |
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, |
24920 | 298 |
Pretty.quote (Syntax.pretty_typ ctxt ty')]; |
24280 | 299 |
in Pretty.writeln p end; |
300 |
||
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
301 |
val evaluate = gen_evaluate (map snd evaluators); |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
302 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
303 |
fun evaluate' name = gen_evaluate |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
304 |
[(the o AList.lookup (op =) evaluators) name]; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
305 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
306 |
fun evaluate_cmd some_name raw_t state = |
22525 | 307 |
let |
22804 | 308 |
val ctxt = Toplevel.context_of state; |
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24423
diff
changeset
|
309 |
val t = Syntax.read_term ctxt raw_t; |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
310 |
in case some_name |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
311 |
of NONE => evaluate ctxt t |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
312 |
| SOME name => evaluate' name ctxt t |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
313 |
end; |
22525 | 314 |
|
315 |
end; |
|
316 |
*} |
|
317 |
||
22804 | 318 |
ML {* |
319 |
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
|
320 |
(Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")") |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
321 |
-- OuterParse.term |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
322 |
>> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
323 |
(Eval.evaluate_cmd some_name t))); |
22804 | 324 |
*} |
325 |
||
26032 | 326 |
print_translation {* |
327 |
let |
|
328 |
val term = Const ("<TERM>", dummyT); |
|
329 |
fun tr1' [_, _] = term; |
|
330 |
fun tr2' [] = term; |
|
331 |
in |
|
332 |
[(@{const_syntax Const}, tr1'), |
|
333 |
(@{const_syntax App}, tr1'), |
|
334 |
(@{const_syntax dummy_term}, tr2')] |
|
335 |
end |
|
336 |
*} |
|
337 |
||
338 |
hide (open) const Type TFree typ_of term_of |
|
339 |
hide const Const App dummy_term |
|
26020 | 340 |
|
22665 | 341 |
end |