author  bulwahn 
Fri, 10 Sep 2010 10:59:09 +0200  
changeset 39274  b17ffa965223 
parent 38857  97775f3e8722 
child 39387  6608c4838ff9 
permissions  rwrr 
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 

281 
subsection {* Obfuscate *} 

31178  282 

283 
print_translation {* 

284 
let 

285 
val term = Const ("<TERM>", dummyT); 

286 
fun tr1' [_, _] = term; 

287 
fun tr2' [] = term; 

288 
in 

289 
[(@{const_syntax Const}, tr1'), 

290 
(@{const_syntax App}, tr1'), 

291 
(@{const_syntax dummy_term}, tr2')] 

292 
end 

293 
*} 

294 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35845
diff
changeset

295 
hide_const dummy_term App valapp 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35845
diff
changeset

296 
hide_const (open) Const termify valtermify term_of term_of_num 
31178  297 

33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

298 
subsection {* Tracing of generated and evaluated code *} 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

299 

3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

300 
definition tracing :: "String.literal => 'a => 'a" 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

301 
where 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

302 
[code del]: "tracing s x = x" 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

303 

3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

304 
ML {* 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

305 
structure Code_Evaluation = 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

306 
struct 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

307 

3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

308 
fun tracing s x = (Output.tracing s; x) 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

309 

3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

310 
end 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

311 
*} 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

312 

3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

313 
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

314 
(Eval "Code'_Evaluation.tracing") 
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

315 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35845
diff
changeset

316 
hide_const (open) tracing 
33473
3b275a0bf18c
adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents:
32740
diff
changeset

317 
code_reserved Eval Code_Evaluation 
31178  318 

28228  319 
subsection {* Evaluation setup *} 
320 

321 
ML {* 

322 
signature EVAL = 

323 
sig 

32740  324 
val eval_ref: (unit > term) option Unsynchronized.ref 
28228  325 
val eval_term: theory > term > term 
326 
end; 

327 

328 
structure Eval : EVAL = 

329 
struct 

330 

32740  331 
val eval_ref = Unsynchronized.ref (NONE : (unit > term) option); 
28228  332 

333 
fun eval_term thy t = 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33632
diff
changeset

334 
Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) []; 
28228  335 

336 
end; 

337 
*} 

338 

339 
setup {* 

340 
Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of) 

341 
*} 

342 

343 
end 