author | haftmann |
Wed, 15 Sep 2010 15:31:32 +0200 | |
changeset 39401 | 887f4218a39a |
parent 39387 | 6608c4838ff9 |
child 39403 | aad9f3cfa1d9 |
permissions | -rw-r--r-- |
32657 | 1 |
(* Title: HOL/Code_Evaluation.thy |
28228 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Term evaluation using the generic code generator *} |
|
6 |
||
32657 | 7 |
theory Code_Evaluation |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
8 |
imports Plain Typerep Code_Numeral |
28228 | 9 |
begin |
10 |
||
11 |
subsection {* Term representation *} |
|
12 |
||
13 |
subsubsection {* Terms and class @{text term_of} *} |
|
14 |
||
15 |
datatype "term" = dummy_term |
|
16 |
||
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
17 |
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where |
28228 | 18 |
"Const _ _ = dummy_term" |
19 |
||
28661 | 20 |
definition App :: "term \<Rightarrow> term \<Rightarrow> term" where |
28228 | 21 |
"App _ _ = dummy_term" |
22 |
||
23 |
code_datatype Const App |
|
24 |
||
28335 | 25 |
class term_of = typerep + |
31031 | 26 |
fixes term_of :: "'a \<Rightarrow> term" |
28228 | 27 |
|
28 |
lemma term_of_anything: "term_of x \<equiv> t" |
|
29 |
by (rule eq_reflection) (cases "term_of x", cases t, simp) |
|
30 |
||
31191 | 31 |
definition valapp :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) |
31178 | 32 |
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where |
31191 | 33 |
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))" |
31178 | 34 |
|
32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset
|
35 |
lemma valapp_code [code, code_unfold]: |
31191 | 36 |
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))" |
37 |
by (simp only: valapp_def fst_conv snd_conv) |
|
31178 | 38 |
|
28228 | 39 |
|
40 |
subsubsection {* @{text term_of} instances *} |
|
41 |
||
32344 | 42 |
instantiation "fun" :: (typerep, typerep) term_of |
43 |
begin |
|
44 |
||
45 |
definition |
|
46 |
"term_of (f \<Colon> 'a \<Rightarrow> 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') |
|
47 |
[Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" |
|
48 |
||
49 |
instance .. |
|
50 |
||
51 |
end |
|
52 |
||
28228 | 53 |
setup {* |
54 |
let |
|
31139 | 55 |
fun add_term_of tyco raw_vs thy = |
28228 | 56 |
let |
31139 | 57 |
val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
58 |
val ty = Type (tyco, map TFree vs); |
|
28228 | 59 |
val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
60 |
$ Free ("x", ty); |
|
61 |
val rhs = @{term "undefined \<Colon> term"}; |
|
62 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
28243 | 63 |
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
64 |
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; |
|
28228 | 65 |
in |
66 |
thy |
|
38348
cf7b2121ad9d
moved instantiation target formally to class_target.ML
haftmann
parents:
36176
diff
changeset
|
67 |
|> Class.instantiation ([tyco], vs, @{sort term_of}) |
28228 | 68 |
|> `(fn lthy => Syntax.check_term lthy eq) |
28965 | 69 |
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
28228 | 70 |
|> snd |
31139 | 71 |
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
28228 | 72 |
end; |
31139 | 73 |
fun ensure_term_of (tyco, (raw_vs, _)) thy = |
74 |
let |
|
75 |
val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) |
|
76 |
andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
77 |
in if need_inst then add_term_of tyco raw_vs thy else thy end; |
28228 | 78 |
in |
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
34028
diff
changeset
|
79 |
Code.datatype_interpretation ensure_term_of |
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
34028
diff
changeset
|
80 |
#> Code.abstype_interpretation ensure_term_of |
28228 | 81 |
end |
82 |
*} |
|
83 |
||
84 |
setup {* |
|
85 |
let |
|
31139 | 86 |
fun mk_term_of_eq thy ty vs tyco (c, tys) = |
28228 | 87 |
let |
88 |
val t = list_comb (Const (c, tys ---> ty), |
|
89 |
map Free (Name.names Name.context "a" tys)); |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35366
diff
changeset
|
90 |
val (arg, rhs) = |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35366
diff
changeset
|
91 |
pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35366
diff
changeset
|
92 |
(t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) |
31139 | 93 |
val cty = Thm.ctyp_of thy ty; |
94 |
in |
|
95 |
@{thm term_of_anything} |
|
96 |
|> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35366
diff
changeset
|
97 |
|> Thm.varifyT_global |
28228 | 98 |
end; |
31139 | 99 |
fun add_term_of_code tyco raw_vs raw_cs thy = |
28228 | 100 |
let |
31746
75fe3304015c
code equation observes default sort constraints for types
haftmann
parents:
31594
diff
changeset
|
101 |
val algebra = Sign.classes_of thy; |
75fe3304015c
code equation observes default sort constraints for types
haftmann
parents:
31594
diff
changeset
|
102 |
val vs = map (fn (v, sort) => |
75fe3304015c
code equation observes default sort constraints for types
haftmann
parents:
31594
diff
changeset
|
103 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
31139 | 104 |
val ty = Type (tyco, map TFree vs); |
105 |
val cs = (map o apsnd o map o map_atyps) |
|
106 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
|
107 |
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
108 |
val eqs = map (mk_term_of_eq thy ty vs tyco) cs; |
|
109 |
in |
|
110 |
thy |
|
111 |
|> Code.del_eqns const |
|
112 |
|> fold Code.add_eqn eqs |
|
113 |
end; |
|
114 |
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = |
|
115 |
let |
|
116 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
117 |
in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; |
28228 | 118 |
in |
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
34028
diff
changeset
|
119 |
Code.datatype_interpretation ensure_term_of_code |
28228 | 120 |
end |
121 |
*} |
|
122 |
||
35366 | 123 |
setup {* |
124 |
let |
|
125 |
fun mk_term_of_eq thy ty vs tyco abs ty_rep proj = |
|
126 |
let |
|
127 |
val arg = Var (("x", 0), ty); |
|
128 |
val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $ |
|
129 |
(HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg)) |
|
130 |
|> Thm.cterm_of thy; |
|
131 |
val cty = Thm.ctyp_of thy ty; |
|
132 |
in |
|
133 |
@{thm term_of_anything} |
|
134 |
|> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs] |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35366
diff
changeset
|
135 |
|> Thm.varifyT_global |
35366 | 136 |
end; |
137 |
fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy = |
|
138 |
let |
|
139 |
val algebra = Sign.classes_of thy; |
|
140 |
val vs = map (fn (v, sort) => |
|
141 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
|
142 |
val ty = Type (tyco, map TFree vs); |
|
143 |
val ty_rep = map_atyps |
|
144 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; |
|
145 |
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
146 |
val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj; |
|
147 |
in |
|
148 |
thy |
|
149 |
|> Code.del_eqns const |
|
150 |
|> Code.add_eqn eq |
|
151 |
end; |
|
152 |
fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy = |
|
153 |
let |
|
154 |
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
|
155 |
in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end; |
|
156 |
in |
|
157 |
Code.abstype_interpretation ensure_term_of_code |
|
158 |
end |
|
159 |
*} |
|
160 |
||
28228 | 161 |
|
39274
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
162 |
instantiation String.literal :: term_of |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
163 |
begin |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
164 |
|
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
165 |
definition |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
166 |
"term_of s = App (Const (STR ''STR'') |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
167 |
(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
168 |
Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
169 |
|
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
170 |
instance .. |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
171 |
|
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
172 |
end |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
38857
diff
changeset
|
173 |
|
28228 | 174 |
subsubsection {* Code generator setup *} |
175 |
||
28562 | 176 |
lemmas [code del] = term.recs term.cases term.size |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38348
diff
changeset
|
177 |
lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" .. |
28228 | 178 |
|
28562 | 179 |
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. |
180 |
lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
181 |
lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" .. |
30427 | 182 |
lemma [code, code del]: |
32657 | 183 |
"(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" .. |
30427 | 184 |
lemma [code, code del]: |
32657 | 185 |
"(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" .. |
28228 | 186 |
|
32657 | 187 |
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c = |
28243 | 188 |
(let (n, m) = nibble_pair_of_char c |
32657 | 189 |
in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
190 |
(Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))" |
|
28243 | 191 |
by (subst term_of_anything) rule |
192 |
||
28228 | 193 |
code_type "term" |
31031 | 194 |
(Eval "Term.term") |
28228 | 195 |
|
196 |
code_const Const and App |
|
31594 | 197 |
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))") |
28228 | 198 |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
199 |
code_const "term_of \<Colon> String.literal \<Rightarrow> term" |
33632
6ea8a4cce9e7
repaired broken code_const for term_of [String.literal]
haftmann
parents:
33553
diff
changeset
|
200 |
(Eval "HOLogic.mk'_literal") |
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset
|
201 |
|
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset
|
202 |
code_reserved Eval HOLogic |
28228 | 203 |
|
204 |
||
31178 | 205 |
subsubsection {* Syntax *} |
206 |
||
31191 | 207 |
definition termify :: "'a \<Rightarrow> term" where |
208 |
[code del]: "termify x = dummy_term" |
|
209 |
||
210 |
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where |
|
211 |
"valtermify x \<equiv> (x, \<lambda>u. termify x)" |
|
31178 | 212 |
|
213 |
setup {* |
|
214 |
let |
|
215 |
fun map_default f xs = |
|
216 |
let val ys = map f xs |
|
217 |
in if exists is_some ys |
|
218 |
then SOME (map2 the_default xs ys) |
|
219 |
else NONE |
|
220 |
end; |
|
221 |
fun subst_termify_app (Const (@{const_name termify}, T), [t]) = |
|
222 |
if not (Term.has_abs t) |
|
223 |
then if fold_aterms (fn Const _ => I | _ => K false) t true |
|
31191 | 224 |
then SOME (HOLogic.reflect_term t) |
31178 | 225 |
else error "Cannot termify expression containing variables" |
226 |
else error "Cannot termify expression containing abstraction" |
|
227 |
| subst_termify_app (t, ts) = case map_default subst_termify ts |
|
228 |
of SOME ts' => SOME (list_comb (t, ts')) |
|
229 |
| NONE => NONE |
|
230 |
and subst_termify (Abs (v, T, t)) = (case subst_termify t |
|
231 |
of SOME t' => SOME (Abs (v, T, t')) |
|
232 |
| NONE => NONE) |
|
233 |
| subst_termify t = subst_termify_app (strip_comb t) |
|
234 |
fun check_termify ts ctxt = map_default subst_termify ts |
|
235 |
|> Option.map (rpair ctxt) |
|
236 |
in |
|
237 |
Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) |
|
238 |
end; |
|
239 |
*} |
|
240 |
||
241 |
locale term_syntax |
|
242 |
begin |
|
243 |
||
31191 | 244 |
notation App (infixl "<\<cdot>>" 70) |
245 |
and valapp (infixl "{\<cdot>}" 70) |
|
31178 | 246 |
|
247 |
end |
|
248 |
||
249 |
interpretation term_syntax . |
|
250 |
||
31191 | 251 |
no_notation App (infixl "<\<cdot>>" 70) |
252 |
and valapp (infixl "{\<cdot>}" 70) |
|
253 |
||
254 |
||
255 |
subsection {* Numeric types *} |
|
256 |
||
257 |
definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where |
|
258 |
"term_of_num two = (\<lambda>_. dummy_term)" |
|
259 |
||
260 |
lemma (in term_syntax) term_of_num_code [code]: |
|
261 |
"term_of_num two k = (if k = 0 then termify Int.Pls |
|
262 |
else (if k mod two = 0 |
|
263 |
then termify Int.Bit0 <\<cdot>> term_of_num two (k div two) |
|
264 |
else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))" |
|
265 |
by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def) |
|
266 |
||
267 |
lemma (in term_syntax) term_of_nat_code [code]: |
|
268 |
"term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n" |
|
269 |
by (simp only: term_of_anything) |
|
270 |
||
271 |
lemma (in term_syntax) term_of_int_code [code]: |
|
272 |
"term_of (k::int) = (if k = 0 then termify (0 :: int) |
|
273 |
else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k |
|
274 |
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) (- k)))" |
|
275 |
by (simp only: term_of_anything) |
|
276 |
||
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
277 |
lemma (in term_syntax) term_of_code_numeral_code [code]: |
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
278 |
"term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k" |
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31191
diff
changeset
|
279 |
by (simp only: term_of_anything) |
31191 | 280 |
|
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
281 |
|
31191 | 282 |
subsection {* Obfuscate *} |
31178 | 283 |
|
284 |
print_translation {* |
|
285 |
let |
|
286 |
val term = Const ("<TERM>", dummyT); |
|
287 |
fun tr1' [_, _] = term; |
|
288 |
fun tr2' [] = term; |
|
289 |
in |
|
290 |
[(@{const_syntax Const}, tr1'), |
|
291 |
(@{const_syntax App}, tr1'), |
|
292 |
(@{const_syntax dummy_term}, tr2')] |
|
293 |
end |
|
294 |
*} |
|
295 |
||
296 |
||
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
297 |
subsection {* Evaluation setup *} |
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
298 |
|
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
299 |
ML {* |
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
300 |
signature CODE_EVALUATION = |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
301 |
sig |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
302 |
val eval_term: theory -> term -> term |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
303 |
val put_term: (unit -> term) -> Proof.context -> Proof.context |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
304 |
val tracing: string -> 'a -> 'a |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
305 |
end; |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
306 |
|
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
307 |
structure Code_Evaluation : CODE_EVALUATION = |
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
308 |
struct |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
309 |
|
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
310 |
structure Evaluation = Proof_Data ( |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
311 |
type T = unit -> term |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
312 |
fun init _ () = error "Evaluation" |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
313 |
); |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
314 |
val put_term = Evaluation.put; |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
315 |
|
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
316 |
fun tracing s x = (Output.tracing s; x); |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
317 |
|
39401 | 318 |
fun eval_term thy t = Code_Runtime.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term") |
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
319 |
I thy (HOLogic.mk_term_of (fastype_of t) t) []; |
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
320 |
|
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
321 |
end |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
322 |
*} |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
323 |
|
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
324 |
setup {* |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
325 |
Value.add_evaluator ("code", Code_Evaluation.eval_term o ProofContext.theory_of) |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
326 |
*} |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
327 |
|
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
328 |
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
329 |
[code del]: "tracing s x = x" |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
330 |
|
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
331 |
code_const "tracing :: String.literal => 'a => 'a" |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
332 |
(Eval "Code'_Evaluation.tracing") |
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
333 |
|
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset
|
334 |
code_reserved Eval Code_Evaluation |
31178 | 335 |
|
39387
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
336 |
hide_const dummy_term App valapp |
6608c4838ff9
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
haftmann
parents:
39274
diff
changeset
|
337 |
hide_const (open) Const termify valtermify term_of term_of_num tracing |
28228 | 338 |
|
339 |
end |