author | wenzelm |
Tue, 02 Sep 2008 14:10:45 +0200 | |
changeset 28083 | 103d9282a946 |
parent 28054 | 2b84d34c5d02 |
child 28084 | a05ca48ef263 |
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 |
27368 | 10 |
Plain |
26168 | 11 |
RType |
26037 | 12 |
Code_Index (* this theory is just imported for a term_of setup *) |
22525 | 13 |
begin |
14 |
||
25763 | 15 |
subsection {* Term representation *} |
16 |
||
26587 | 17 |
subsubsection {* Terms and class @{text term_of} *} |
26020 | 18 |
|
19 |
datatype "term" = dummy_term |
|
25763 | 20 |
|
26020 | 21 |
definition |
26168 | 22 |
Const :: "message_string \<Rightarrow> rtype \<Rightarrow> term" |
26020 | 23 |
where |
24 |
"Const _ _ = dummy_term" |
|
25763 | 25 |
|
26020 | 26 |
definition |
27 |
App :: "term \<Rightarrow> term \<Rightarrow> term" |
|
28 |
where |
|
29 |
"App _ _ = dummy_term" |
|
30 |
||
31 |
code_datatype Const App |
|
25763 | 32 |
|
26168 | 33 |
class term_of = rtype + |
26020 | 34 |
fixes term_of :: "'a \<Rightarrow> term" |
35 |
||
36 |
lemma term_of_anything: "term_of x \<equiv> t" |
|
37 |
by (rule eq_reflection) (cases "term_of x", cases t, simp) |
|
25763 | 38 |
|
39 |
ML {* |
|
26020 | 40 |
structure Eval = |
25763 | 41 |
struct |
42 |
||
43 |
fun mk_term f g (Const (c, ty)) = |
|
44 |
@{term Const} $ Message_String.mk c $ g ty |
|
45 |
| mk_term f g (t1 $ t2) = |
|
46 |
@{term App} $ mk_term f g t1 $ mk_term f g t2 |
|
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26242
diff
changeset
|
47 |
| mk_term f g (Free v) = f v |
26587 | 48 |
| mk_term f g (Bound i) = Bound i |
49 |
| mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t); |
|
25763 | 50 |
|
26020 | 51 |
fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t; |
22525 | 52 |
|
53 |
end; |
|
54 |
*} |
|
55 |
||
26587 | 56 |
|
57 |
subsubsection {* @{text term_of} instances *} |
|
58 |
||
22525 | 59 |
setup {* |
60 |
let |
|
26020 | 61 |
fun add_term_of_def ty vs tyco thy = |
22525 | 62 |
let |
26020 | 63 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
64 |
$ Free ("x", ty); |
|
65 |
val rhs = @{term "undefined \<Colon> term"}; |
|
66 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
67 |
in |
|
25536 | 68 |
thy |
26020 | 69 |
|> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) |
70 |
|> `(fn lthy => Syntax.check_term lthy eq) |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
28054
diff
changeset
|
71 |
|-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq))) |
25569 | 72 |
|> snd |
73 |
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
|
74 |
|> LocalTheory.exit |
|
75 |
|> ProofContext.theory_of |
|
26020 | 76 |
end; |
77 |
fun interpretator (tyco, (raw_vs, _)) thy = |
|
78 |
let |
|
26168 | 79 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
26020 | 80 |
val constrain_sort = |
81 |
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
82 |
val vs = (map o apsnd) constrain_sort raw_vs; |
|
83 |
val ty = Type (tyco, map TFree vs); |
|
84 |
in |
|
85 |
thy |
|
26168 | 86 |
|> RType.perhaps_add_def tyco |
87 |
|> not has_inst ? add_term_of_def ty vs tyco |
|
26020 | 88 |
end; |
89 |
in |
|
26168 | 90 |
Code.type_interpretation interpretator |
26020 | 91 |
end |
22525 | 92 |
*} |
93 |
||
26020 | 94 |
setup {* |
95 |
let |
|
96 |
fun mk_term_of_eq ty vs tyco (c, tys) = |
|
97 |
let |
|
98 |
val t = list_comb (Const (c, tys ---> ty), |
|
99 |
map Free (Name.names Name.context "a" tys)); |
|
100 |
in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term |
|
101 |
(fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) |
|
26168 | 102 |
(RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t) |
26020 | 103 |
end; |
104 |
fun prove_term_of_eq ty eq thy = |
|
105 |
let |
|
106 |
val cty = Thm.ctyp_of thy ty; |
|
107 |
val (arg, rhs) = pairself (Thm.cterm_of thy) eq; |
|
108 |
val thm = @{thm term_of_anything} |
|
109 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
110 |
|> Thm.varifyT; |
|
111 |
in |
|
112 |
thy |
|
113 |
|> Code.add_func thm |
|
114 |
end; |
|
115 |
fun interpretator (tyco, (raw_vs, raw_cs)) thy = |
|
116 |
let |
|
117 |
val constrain_sort = |
|
118 |
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
119 |
val vs = (map o apsnd) constrain_sort raw_vs; |
|
120 |
val cs = (map o apsnd o map o map_atyps) |
|
121 |
(fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; |
|
122 |
val ty = Type (tyco, map TFree vs); |
|
123 |
val eqs = map (mk_term_of_eq ty vs tyco) cs; |
|
124 |
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
125 |
in |
|
126 |
thy |
|
127 |
|> Code.del_funcs const |
|
128 |
|> fold (prove_term_of_eq ty) eqs |
|
129 |
end; |
|
130 |
in |
|
131 |
Code.type_interpretation interpretator |
|
25569 | 132 |
end |
26020 | 133 |
*} |
23062 | 134 |
|
26587 | 135 |
|
25763 | 136 |
subsubsection {* Code generator setup *} |
137 |
||
138 |
lemmas [code func del] = term.recs term.cases term.size |
|
139 |
lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" .. |
|
26037 | 140 |
|
26168 | 141 |
lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" .. |
26037 | 142 |
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
143 |
lemma [code func, code func del]: "(term_of \<Colon> index \<Rightarrow> term) = term_of" .. |
|
26020 | 144 |
lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. |
22525 | 145 |
|
25763 | 146 |
code_type "term" |
147 |
(SML "Term.term") |
|
148 |
||
26020 | 149 |
code_const Const and App |
150 |
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") |
|
22525 | 151 |
|
26037 | 152 |
code_const "term_of \<Colon> index \<Rightarrow> term" |
153 |
(SML "HOLogic.mk'_number/ HOLogic.indexT") |
|
154 |
||
155 |
code_const "term_of \<Colon> message_string \<Rightarrow> term" |
|
156 |
(SML "Message'_String.mk") |
|
157 |
||
158 |
||
26587 | 159 |
subsubsection {* Syntax *} |
160 |
||
161 |
print_translation {* |
|
162 |
let |
|
163 |
val term = Const ("<TERM>", dummyT); |
|
164 |
fun tr1' [_, _] = term; |
|
165 |
fun tr2' [] = term; |
|
166 |
in |
|
167 |
[(@{const_syntax Const}, tr1'), |
|
168 |
(@{const_syntax App}, tr1'), |
|
169 |
(@{const_syntax dummy_term}, tr2')] |
|
170 |
end |
|
171 |
*} |
|
172 |
setup {* |
|
173 |
Sign.declare_const [] ("rterm_of", @{typ "'a \<Rightarrow> 'b"}, NoSyn) |
|
174 |
#> snd |
|
175 |
*} |
|
176 |
||
177 |
notation (output) |
|
178 |
rterm_of ("\<guillemotleft>_\<guillemotright>") |
|
179 |
||
27681 | 180 |
locale rterm_syntax = |
26587 | 181 |
fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>") |
182 |
||
183 |
parse_translation {* |
|
184 |
let |
|
185 |
fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t |
|
186 |
| rterm_of_tr ts = raise TERM ("rterm_of_tr", ts); |
|
187 |
in |
|
26591 | 188 |
[(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)] |
26587 | 189 |
end |
190 |
*} |
|
191 |
||
192 |
setup {* |
|
193 |
let |
|
194 |
val subst_rterm_of = Eval.mk_term |
|
195 |
(fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) |
|
196 |
(RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))); |
|
197 |
fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t |
|
198 |
| subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = |
|
199 |
error ("illegal number of arguments for " ^ quote @{const_name rterm_of}) |
|
200 |
| subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts); |
|
201 |
fun subst_rterm_of'' t = |
|
202 |
let |
|
203 |
val t' = subst_rterm_of' (strip_comb t); |
|
204 |
in if t aconv t' |
|
205 |
then NONE |
|
206 |
else SOME t' |
|
207 |
end; |
|
208 |
fun check_rterm_of ts ctxt = |
|
209 |
let |
|
210 |
val ts' = map subst_rterm_of'' ts; |
|
211 |
in if exists is_some ts' |
|
212 |
then SOME (map2 the_default ts ts', ctxt) |
|
213 |
else NONE |
|
214 |
end; |
|
215 |
in |
|
216 |
Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of) |
|
217 |
end; |
|
218 |
*} |
|
219 |
||
220 |
hide const dummy_term |
|
221 |
hide (open) const Const App |
|
222 |
hide (open) const term_of |
|
223 |
||
224 |
||
25763 | 225 |
subsection {* Evaluation setup *} |
22525 | 226 |
|
227 |
ML {* |
|
228 |
signature EVAL = |
|
229 |
sig |
|
26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26242
diff
changeset
|
230 |
val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term |
24587 | 231 |
val eval_ref: (unit -> term) option ref |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
232 |
val eval_term: theory -> term -> term |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
233 |
val evaluate: Proof.context -> term -> unit |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
234 |
val evaluate': string -> Proof.context -> term -> unit |
26020 | 235 |
val evaluate_cmd: string option -> string -> Toplevel.state -> unit |
22525 | 236 |
end; |
237 |
||
26020 | 238 |
structure Eval : EVAL = |
22525 | 239 |
struct |
240 |
||
26020 | 241 |
open Eval; |
242 |
||
24587 | 243 |
val eval_ref = ref (NONE : (unit -> term) option); |
22525 | 244 |
|
26020 | 245 |
fun eval_term thy t = |
246 |
t |
|
247 |
|> Eval.mk_term_of (fastype_of t) |
|
28054 | 248 |
|> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t []) |
26020 | 249 |
|> Code.postprocess_term thy; |
24280 | 250 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
251 |
val evaluators = [ |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
252 |
("code", eval_term), |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
253 |
("SML", Codegen.eval_term), |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
254 |
("normal_form", Nbe.norm_term) |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
255 |
]; |
22525 | 256 |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
257 |
fun gen_evaluate evaluators ctxt t = |
24280 | 258 |
let |
259 |
val thy = ProofContext.theory_of ctxt; |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
260 |
val (evls, evl) = split_last evaluators; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
261 |
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
|
262 |
of SOME t' => t' |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
263 |
| NONE => evl thy t; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
264 |
val ty' = Term.type_of t'; |
24920 | 265 |
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
|
266 |
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, |
24920 | 267 |
Pretty.quote (Syntax.pretty_typ ctxt ty')]; |
24280 | 268 |
in Pretty.writeln p end; |
269 |
||
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
270 |
val evaluate = gen_evaluate (map snd evaluators); |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
271 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
272 |
fun evaluate' name = gen_evaluate |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
273 |
[(the o AList.lookup (op =) evaluators) name]; |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
274 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
275 |
fun evaluate_cmd some_name raw_t state = |
22525 | 276 |
let |
22804 | 277 |
val ctxt = Toplevel.context_of state; |
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24423
diff
changeset
|
278 |
val t = Syntax.read_term ctxt raw_t; |
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
279 |
in case some_name |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
280 |
of NONE => evaluate ctxt t |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
281 |
| SOME name => evaluate' name ctxt t |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
282 |
end; |
22525 | 283 |
|
284 |
end; |
|
285 |
*} |
|
286 |
||
22804 | 287 |
ML {* |
288 |
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
|
289 |
(Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")") |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
290 |
-- OuterParse.term |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
291 |
>> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep |
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
292 |
(Eval.evaluate_cmd some_name t))); |
22804 | 293 |
*} |
294 |
||
26032 | 295 |
end |