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