author  haftmann 
Thu, 31 Jan 2008 11:44:43 +0100  
changeset 26020  ffe1a032d24b 
parent 26011  d55224947082 
child 26032  377b7aa0b5b5 
permissions  rwrr 
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 

26020  311 
hide (open) const Type TFree Const App dummy_term typ_of term_of 
312 

22665  313 
end 