author  bulwahn 
Fri, 06 Nov 2009 08:11:58 +0100  
changeset 33473  3b275a0bf18c 
parent 32740  9dd0a2f83429 
child 33553  35f2b30593a8 
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 

67 
> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) 

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 
31139  79 
Code.type_interpretation ensure_term_of 
28228  80 
end 
81 
*} 

82 

83 
setup {* 

84 
let 

31139  85 
fun mk_term_of_eq thy ty vs tyco (c, tys) = 
28228  86 
let 
87 
val t = list_comb (Const (c, tys > ty), 

88 
map Free (Name.names Name.context "a" tys)); 

31139  89 
val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify) 
90 
(t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t  t => t) o HOLogic.reflect_term) t) 

91 
val cty = Thm.ctyp_of thy ty; 

92 
in 

93 
@{thm term_of_anything} 

94 
> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] 

95 
> Thm.varifyT 

28228  96 
end; 
31139  97 
fun add_term_of_code tyco raw_vs raw_cs thy = 
28228  98 
let 
31746
75fe3304015c
code equation observes default sort constraints for types
haftmann
parents:
31594
diff
changeset

99 
val algebra = Sign.classes_of thy; 
75fe3304015c
code equation observes default sort constraints for types
haftmann
parents:
31594
diff
changeset

100 
val vs = map (fn (v, sort) => 
75fe3304015c
code equation observes default sort constraints for types
haftmann
parents:
31594
diff
changeset

101 
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; 
31139  102 
val ty = Type (tyco, map TFree vs); 
103 
val cs = (map o apsnd o map o map_atyps) 

104 
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; 

105 
val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); 

106 
val eqs = map (mk_term_of_eq thy ty vs tyco) cs; 

107 
in 

108 
thy 

109 
> Code.del_eqns const 

110 
> fold Code.add_eqn eqs 

111 
end; 

112 
fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = 

113 
let 

114 
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

115 
in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end; 
28228  116 
in 
31139  117 
Code.type_interpretation ensure_term_of_code 
28228  118 
end 
119 
*} 

120 

121 

122 
subsubsection {* Code generator setup *} 

123 

28562  124 
lemmas [code del] = term.recs term.cases term.size 
125 
lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" .. 

28228  126 

28562  127 
lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" .. 
128 
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

129 
lemma [code, code del]: "(term_of \<Colon> String.literal \<Rightarrow> term) = term_of" .. 
30427  130 
lemma [code, code del]: 
32657  131 
"(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" .. 
30427  132 
lemma [code, code del]: 
32657  133 
"(Code_Evaluation.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of" .. 
28228  134 

32657  135 
lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Evaluation.term_of c = 
28243  136 
(let (n, m) = nibble_pair_of_char c 
32657  137 
in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) 
138 
(Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))" 

28243  139 
by (subst term_of_anything) rule 
140 

28228  141 
code_type "term" 
31031  142 
(Eval "Term.term") 
28228  143 

144 
code_const Const and App 

31594  145 
(Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))") 
28228  146 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

147 
code_const "term_of \<Colon> String.literal \<Rightarrow> term" 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

148 
(Eval "HOLogic.mk'_message'_string") 
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

149 

ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31031
diff
changeset

150 
code_reserved Eval HOLogic 
28228  151 

152 

31178  153 
subsubsection {* Syntax *} 
154 

31191  155 
definition termify :: "'a \<Rightarrow> term" where 
156 
[code del]: "termify x = dummy_term" 

157 

158 
abbreviation valtermify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where 

159 
"valtermify x \<equiv> (x, \<lambda>u. termify x)" 

31178  160 

161 
setup {* 

162 
let 

163 
fun map_default f xs = 

164 
let val ys = map f xs 

165 
in if exists is_some ys 

166 
then SOME (map2 the_default xs ys) 

167 
else NONE 

168 
end; 

169 
fun subst_termify_app (Const (@{const_name termify}, T), [t]) = 

170 
if not (Term.has_abs t) 

171 
then if fold_aterms (fn Const _ => I  _ => K false) t true 

31191  172 
then SOME (HOLogic.reflect_term t) 
31178  173 
else error "Cannot termify expression containing variables" 
174 
else error "Cannot termify expression containing abstraction" 

175 
 subst_termify_app (t, ts) = case map_default subst_termify ts 

176 
of SOME ts' => SOME (list_comb (t, ts')) 

177 
 NONE => NONE 

178 
and subst_termify (Abs (v, T, t)) = (case subst_termify t 

179 
of SOME t' => SOME (Abs (v, T, t')) 

180 
 NONE => NONE) 

181 
 subst_termify t = subst_termify_app (strip_comb t) 

182 
fun check_termify ts ctxt = map_default subst_termify ts 

183 
> Option.map (rpair ctxt) 

184 
in 

185 
Context.theory_map (Syntax.add_term_check 0 "termify" check_termify) 

186 
end; 

187 
*} 

188 

189 
locale term_syntax 

190 
begin 

191 

31191  192 
notation App (infixl "<\<cdot>>" 70) 
193 
and valapp (infixl "{\<cdot>}" 70) 

31178  194 

195 
end 

196 

197 
interpretation term_syntax . 

198 

31191  199 
no_notation App (infixl "<\<cdot>>" 70) 
200 
and valapp (infixl "{\<cdot>}" 70) 

201 

202 

203 
subsection {* Numeric types *} 

204 

205 
definition term_of_num :: "'a\<Colon>{semiring_div} \<Rightarrow> 'a\<Colon>{semiring_div} \<Rightarrow> term" where 

206 
"term_of_num two = (\<lambda>_. dummy_term)" 

207 

208 
lemma (in term_syntax) term_of_num_code [code]: 

209 
"term_of_num two k = (if k = 0 then termify Int.Pls 

210 
else (if k mod two = 0 

211 
then termify Int.Bit0 <\<cdot>> term_of_num two (k div two) 

212 
else termify Int.Bit1 <\<cdot>> term_of_num two (k div two)))" 

213 
by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def) 

214 

215 
lemma (in term_syntax) term_of_nat_code [code]: 

216 
"term_of (n::nat) = termify (number_of :: int \<Rightarrow> nat) <\<cdot>> term_of_num (2::nat) n" 

217 
by (simp only: term_of_anything) 

218 

219 
lemma (in term_syntax) term_of_int_code [code]: 

220 
"term_of (k::int) = (if k = 0 then termify (0 :: int) 

221 
else if k > 0 then termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) k 

222 
else termify (uminus :: int \<Rightarrow> int) <\<cdot>> (termify (number_of :: int \<Rightarrow> int) <\<cdot>> term_of_num (2::int) ( k)))" 

223 
by (simp only: term_of_anything) 

224 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

225 
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

226 
"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

227 
by (simp only: term_of_anything) 
31191  228 

229 
subsection {* Obfuscate *} 

31178  230 

231 
print_translation {* 

232 
let 

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

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

235 
fun tr2' [] = term; 

236 
in 

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

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

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

240 
end 

241 
*} 

242 

31191  243 
hide const dummy_term App valapp 
244 
hide (open) const Const termify valtermify term_of term_of_num 

31178  245 

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

246 
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

247 

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

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

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

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

251 

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

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

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

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

255 

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

256 
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

257 

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

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

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

260 

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

261 
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

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

263 

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

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

265 
code_reserved Eval Code_Evaluation 
31178  266 

28228  267 
subsection {* Evaluation setup *} 
268 

269 
ML {* 

270 
signature EVAL = 

271 
sig 

32740  272 
val eval_ref: (unit > term) option Unsynchronized.ref 
28228  273 
val eval_term: theory > term > term 
274 
end; 

275 

276 
structure Eval : EVAL = 

277 
struct 

278 

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

281 
fun eval_term thy t = 

31139  282 
Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) []; 
28228  283 

284 
end; 

285 
*} 

286 

287 
setup {* 

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

289 
*} 

290 

291 
end 