author  haftmann 
Wed, 02 Jan 2008 15:14:15 +0100  
changeset 25763  474f8ba9dfa9 
parent 25691  8f8d83af100a 
child 25864  11f531354852 
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 
abbreviation 

25 
Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" where 

26 
"Fun ty1 ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]" 

27 

28 
locale (open) pure_term_syntax =  {* FIXME drop this *} 

29 
fixes pure_term_Type :: "message_string \<Rightarrow> typ list \<Rightarrow> typ" (infixl "{\<struct>}" 120) 

30 
and pure_term_TFree :: "vname \<Rightarrow> sort \<Rightarrow> typ" ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117) 

31 
and pure_term_Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 114) 

32 

33 
parse_translation {* 

34 
let 

35 
fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys 

36 
 Type_tr ts = raise TERM ("Type_tr", ts); 

37 
fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort 

38 
 TFree_tr ts = raise TERM ("TFree_tr", ts); 

39 
fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2 

40 
 Fun_tr ts = raise TERM("Fun_tr", ts); 

41 
in [ 

42 
("\\<^fixed>pure_term_Type", Type_tr), 

43 
("\\<^fixed>pure_term_TFree", TFree_tr), 

44 
("\\<^fixed>pure_term_Fun", Fun_tr) 

45 
] end 

46 
*} 

47 

48 
notation (output) 

49 
Type (infixl "{\<struct>}" 120) 

50 
and 

51 
TFree ("\<lbrace>_\<Colon>_\<rbrace>" [118, 118] 117) 

52 
and 

53 
Fun (infixr "\<rightarrow>" 114) 

54 

55 
ML {* 

56 
structure Eval_Aux = 

57 
struct 

58 

59 
val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk; 

60 

61 
fun mk_typ f (Type (tyco, tys)) = 

62 
@{term Type} $ Message_String.mk tyco 

63 
$ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys) 

64 
 mk_typ f (TFree v) = 

65 
f v; 

66 

67 
end; 

68 
*} 

69 

70 

71 
subsubsection {* Class @{text typ_of} *} 

22525  72 

23062  73 
class typ_of = 
74 
fixes typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ" 

22525  75 

76 
ML {* 

25763  77 
structure Eval_Aux = 
22525  78 
struct 
79 

25763  80 
open Eval_Aux; 
81 

82 
fun mk_typ_of ty = 

22525  83 
Const (@{const_name typ_of}, Term.itselfT ty > @{typ typ}) 
84 
$ Logic.mk_type ty; 

85 

25536  86 
end 
22525  87 
*} 
88 

89 
setup {* 

90 
let 

25763  91 
open Eval_Aux; 
25536  92 
fun define_typ_of ty lthy = 
93 
let 

94 
val lhs = Const (@{const_name typ_of}, Term.itselfT ty > @{typ typ}) 

95 
$ Free ("T", Term.itselfT ty); 

25763  96 
val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty; 
25603  97 
val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) 
25536  98 
in lthy > Specification.definition (NONE, (("", []), eq)) end; 
99 
fun interpretator tyco thy = 

100 
let 

101 
val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of}; 

102 
val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts)); 

103 
in 

104 
thy 

25569  105 
> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of}) 
106 
> define_typ_of ty 

107 
> snd 

108 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 

109 
> LocalTheory.exit 

110 
> ProofContext.theory_of 

25536  111 
end; 
112 
in TypedefPackage.interpretation interpretator end 

22525  113 
*} 
114 

25536  115 
instantiation "prop" :: typ_of 
116 
begin 

117 

25666  118 
definition 
119 
"typ_of (T\<Colon>prop itself) = Type (STR ''prop'') []" 

25536  120 

121 
instance .. 

122 

123 
end 

124 

125 
instantiation itself :: (typ_of) typ_of 

126 
begin 

127 

128 
definition 

25666  129 
"typ_of (T\<Colon>'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\<Colon>typ_of)]" 
25536  130 

131 
instance .. 

132 

133 
end 

134 

135 
instantiation set :: (typ_of) typ_of 

136 
begin 

137 

138 
definition 

25666  139 
"typ_of (T\<Colon>'a set itself) = Type (STR ''set'') [typ_of TYPE('a\<Colon>typ_of)]" 
25536  140 

141 
instance .. 

142 

143 
end 

144 

22525  145 

25763  146 
subsubsection {* Code generator setup *} 
147 

148 
lemma [code func]: 

149 
includes pure_term_syntax 

150 
shows "tyco1 {\<struct>} tys1 = tyco2 {\<struct>} tys2 \<longleftrightarrow> tyco1 = tyco2 

151 
\<and> list_all2 (op =) tys1 tys2" 

152 
by (auto simp add: list_all2_eq [symmetric]) 

153 

154 
code_type "typ" 

155 
(SML "Term.typ") 

156 

157 
code_const Type and TFree 

158 
(SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)") 

159 

160 
code_reserved SML Term 

161 

162 

163 

164 
subsection {* Term representation *} 

165 

166 
subsubsection {* Definition *} 

167 

168 
datatype "term" = 

169 
Const message_string "typ" (infix "\<Colon>\<subseteq>" 112) 

170 
 Fix vname "typ" (infix ":\<epsilon>" 112) 

171 
 App "term" "term" (infixl "\<bullet>" 110) 

172 
 Abs "vname \<times> typ" "term" (infixr "\<mapsto>" 111) 

173 
 Bnd nat 

174 

175 
code_datatype Const App Fix 

176 

177 
abbreviation 

178 
Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where 

179 
"t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts" 

180 
abbreviation 

181 
Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where 

182 
"vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t" 

183 

184 
ML {* 

185 
structure Eval_Aux = 

186 
struct 

187 

188 
open Eval_Aux; 

189 

190 
fun mk_term f g (Const (c, ty)) = 

191 
@{term Const} $ Message_String.mk c $ g ty 

192 
 mk_term f g (t1 $ t2) = 

193 
@{term App} $ mk_term f g t1 $ mk_term f g t2 

194 
 mk_term f g (Free v) = f v; 

195 

196 
end; 

197 
*} 

198 

199 

200 
subsubsection {* Class @{text term_of} *} 

22525  201 

202 
class term_of = typ_of + 

23062  203 
constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ" 
22525  204 
fixes term_of :: "'a \<Rightarrow> term" 
205 

206 
ML {* 

25763  207 
structure Eval_Aux = 
22525  208 
struct 
209 

25763  210 
open Eval_Aux; 
211 

22525  212 
local 
213 
fun term_term_of ty = 

214 
Const (@{const_name term_of}, ty > @{typ term}); 

215 
in 

216 
val class_term_of = Sign.intern_class @{theory} "term_of"; 

217 
fun mk_terms_of_defs vs (tyco, cs) = 

218 
let 

219 
val dty = Type (tyco, map TFree vs); 

220 
fun mk_eq c = 

221 
let 

222 
val lhs : term = term_term_of dty $ c; 

25763  223 
val rhs : term = mk_term 
22525  224 
(fn (v, ty) => term_term_of ty $ Free (v, ty)) 
25763  225 
(mk_typ (fn (v, sort) => mk_typ_of (TFree (v, sort)))) c 
22525  226 
in 
25559  227 
HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) 
22525  228 
end; 
229 
in map mk_eq cs end; 

230 
fun mk_term_of t = 

231 
term_term_of (Term.fastype_of t) $ t; 

232 
end; 

233 

234 
end; 

235 
*} 

236 

237 
setup {* 

238 
let 

25763  239 
open Eval_Aux; 
22525  240 
fun thy_note ((name, atts), thms) = 
241 
PureThy.add_thmss [((name, thms), atts)] #> (fn [thms] => pair (name, thms)); 

242 
fun thy_def ((name, atts), t) = 

243 
PureThy.add_defs_i false [((name, t), atts)] #> (fn [thm] => pair (name, thm)); 

25536  244 
fun prep_dtyp thy vs tyco = 
245 
let 

246 
val (_, cs) = DatatypePackage.the_datatype_spec thy tyco; 

247 
val prep_typ = map_atyps (fn TFree (v, sort) => 

248 
TFree (v, (the o AList.lookup (op =) vs) v)); 

249 
fun prep_c (c, tys) = list_comb (Const (c, tys > Type (tyco, map TFree vs)), 

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

251 
in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end; 

252 
fun prep thy tycos = 

22525  253 
let 
25536  254 
val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; 
255 
val tyco = hd tycos; 

256 
val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco; 

257 
val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos; 

258 
fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> 

259 
fold add_tycos tys 

260 
 add_tycos _ = I; 

261 
val dep_tycos = [] > fold add_tycos all_typs > subtract (op =) tycos; 

262 
val sorts = map (inter_sort o snd) vs_proto; 

263 
val vs = map fst vs_proto ~~ sorts; 

264 
val css = map (prep_dtyp thy vs) tycos; 

25763  265 
val defs = map (mk_terms_of_defs vs) css; 
25536  266 
in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos 
267 
andalso not (tycos = [@{type_name typ}]) 

25559  268 
then SOME (sorts, defs) 
25536  269 
else NONE 
22525  270 
end; 
25559  271 
fun prep' ctxt proto_eqs = 
272 
let 

25603  273 
val eqs as eq :: _ = map (Syntax.check_term ctxt) proto_eqs; 
25559  274 
val (Free (v, ty), _) = 
275 
(strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; 

276 
in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end; 

277 
fun primrec primrecs ctxt = 

278 
let 

279 
val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs); 

280 
in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end; 

25536  281 
fun interpretator tycos thy = case prep thy tycos 
282 
of SOME (sorts, defs) => 

283 
thy 

25569  284 
> TheoryTarget.instantiation (tycos, sorts, @{sort term_of}) 
285 
> primrec defs 

286 
> snd 

287 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 

288 
> LocalTheory.exit 

289 
> ProofContext.theory_of 

25536  290 
 NONE => thy; 
291 
in DatatypePackage.interpretation interpretator end 

22525  292 
*} 
293 

25666  294 
abbreviation (in pure_term_syntax) (input) 
23062  295 
intT :: "typ" 
296 
where 

25666  297 
"intT \<equiv> Type (STR ''IntDef.int'') []" 
23062  298 

25666  299 
abbreviation (in pure_term_syntax) (input) 
23133  300 
bitT :: "typ" 
301 
where 

25666  302 
"bitT \<equiv> Type (STR ''Numeral.bit'') []" 
23133  303 

25666  304 
function (in pure_term_syntax) 
23062  305 
mk_int :: "int \<Rightarrow> term" 
306 
where 

307 
"mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT 

308 
else if k = 1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT 

309 
else let (l, m) = divAlg (k, 2) 

23133  310 
in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet> 
311 
(if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))" 

23062  312 
by pat_completeness auto 
25666  313 
termination (in pure_term_syntax) 
314 
by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div) 

315 

316 
declare pure_term_syntax.mk_int.simps [code func] 

317 

318 
definition (in pure_term_syntax) 

319 
"term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" 

320 

321 
declare pure_term_syntax.term_of_int_aux_def [code func] 

23062  322 

25569  323 
instantiation int :: term_of 
324 
begin 

325 

326 
definition 

25666  327 
"term_of = pure_term_syntax.term_of_int_aux" 
25569  328 

329 
instance .. 

330 

331 
end 

23062  332 

333 

25763  334 
subsubsection {* Code generator setup *} 
335 

336 
lemmas [code func del] = term.recs term.cases term.size 

337 
lemmas [code func del] = term_of_message_string.simps 

338 
lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" .. 

22525  339 

25763  340 
code_type "term" 
341 
(SML "Term.term") 

342 

343 
code_const Const and App and Fix 

344 
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)") 

22525  345 

346 

25763  347 
subsection {* Evaluation setup *} 
22525  348 

349 
ML {* 

350 
signature EVAL = 

351 
sig 

24587  352 
val eval_ref: (unit > term) option ref 
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

353 
val eval_term: theory > term > term 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

354 
val evaluate: Proof.context > term > unit 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

355 
val evaluate': string > Proof.context > term > unit 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

356 
val evaluate_cmd: string option > Toplevel.state > unit 
22525  357 
end; 
358 

24280  359 
structure Eval = 
22525  360 
struct 
361 

24587  362 
val eval_ref = ref (NONE : (unit > term) option); 
22525  363 

24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

364 
fun eval_invoke thy code ((_, ty), t) deps _ = 
24916  365 
CodeTarget.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) []; 
24280  366 

24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

367 
fun eval_term thy = 
25763  368 
Eval_Aux.mk_term_of 
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

369 
#> CodePackage.eval_term thy (eval_invoke thy) 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

370 
#> Code.postprocess_term thy; 
24280  371 

24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

372 
val evaluators = [ 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

373 
("code", eval_term), 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

374 
("SML", Codegen.eval_term), 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

375 
("normal_form", Nbe.norm_term) 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

376 
]; 
22525  377 

24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

378 
fun gen_evaluate evaluators ctxt t = 
24280  379 
let 
380 
val thy = ProofContext.theory_of ctxt; 

24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

381 
val (evls, evl) = split_last evaluators; 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

382 
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

383 
of SOME t' => t' 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

384 
 NONE => evl thy t; 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

385 
val ty' = Term.type_of t'; 
24920  386 
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

387 
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, 
24920  388 
Pretty.quote (Syntax.pretty_typ ctxt ty')]; 
24280  389 
in Pretty.writeln p end; 
390 

24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

391 
val evaluate = gen_evaluate (map snd evaluators); 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

392 

8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

393 
fun evaluate' name = gen_evaluate 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

394 
[(the o AList.lookup (op =) evaluators) name]; 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

395 

8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

396 
fun evaluate_cmd some_name raw_t state = 
22525  397 
let 
22804  398 
val ctxt = Toplevel.context_of state; 
24508
c8b82fec6447
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24423
diff
changeset

399 
val t = Syntax.read_term ctxt raw_t; 
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

400 
in case some_name 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

401 
of NONE => evaluate ctxt t 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

402 
 SOME name => evaluate' name ctxt t 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

403 
end; 
22525  404 

405 
end; 

406 
*} 

407 

22804  408 
ML {* 
409 
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

410 
(Scan.option (OuterParse.$$$ "("  OuterParse.name  OuterParse.$$$ ")") 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

411 
 OuterParse.term 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

412 
>> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

413 
(Eval.evaluate_cmd some_name t))); 
22804  414 
*} 
415 

22665  416 
end 