author  haftmann 
Wed, 09 Apr 2008 08:10:09 +0200  
changeset 26587  58fb6e033c00 
parent 26267  ba710daf77a7 
child 26591  74b3c93f2428 
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 

26037  9 
imports 
26168  10 
RType 
26037  11 
Code_Index (* this theory is just imported for a term_of setup *) 
22525  12 
begin 
13 

25763  14 
subsection {* Term representation *} 
15 

26587  16 
subsubsection {* Terms and class @{text term_of} *} 
26020  17 

18 
datatype "term" = dummy_term 

25763  19 

26020  20 
definition 
26168  21 
Const :: "message_string \<Rightarrow> rtype \<Rightarrow> term" 
26020  22 
where 
23 
"Const _ _ = dummy_term" 

25763  24 

26020  25 
definition 
26 
App :: "term \<Rightarrow> term \<Rightarrow> term" 

27 
where 

28 
"App _ _ = dummy_term" 

29 

30 
code_datatype Const App 

25763  31 

26168  32 
class term_of = rtype + 
26020  33 
fixes term_of :: "'a \<Rightarrow> term" 
34 

35 
lemma term_of_anything: "term_of x \<equiv> t" 

36 
by (rule eq_reflection) (cases "term_of x", cases t, simp) 

25763  37 

38 
ML {* 

26020  39 
structure Eval = 
25763  40 
struct 
41 

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

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

44 
 mk_term f g (t1 $ t2) = 

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

26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26242
diff
changeset

46 
 mk_term f g (Free v) = f v 
26587  47 
 mk_term f g (Bound i) = Bound i 
48 
 mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t); 

25763  49 

26020  50 
fun mk_term_of ty t = Const (@{const_name term_of}, ty > @{typ term}) $ t; 
22525  51 

52 
end; 

53 
*} 

54 

26587  55 

56 
subsubsection {* @{text term_of} instances *} 

57 

22525  58 
setup {* 
59 
let 

26020  60 
fun add_term_of_def ty vs tyco thy = 
22525  61 
let 
26020  62 
val lhs = Const (@{const_name term_of}, ty > @{typ term}) 
63 
$ Free ("x", ty); 

64 
val rhs = @{term "undefined \<Colon> term"}; 

65 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 

66 
in 

25536  67 
thy 
26020  68 
> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) 
69 
> `(fn lthy => Syntax.check_term lthy eq) 

70 
> (fn eq => Specification.definition (NONE, (("", []), eq))) 

25569  71 
> snd 
72 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 

73 
> LocalTheory.exit 

74 
> ProofContext.theory_of 

26020  75 
end; 
76 
fun interpretator (tyco, (raw_vs, _)) thy = 

77 
let 

26168  78 
val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; 
26020  79 
val constrain_sort = 
80 
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; 

81 
val vs = (map o apsnd) constrain_sort raw_vs; 

82 
val ty = Type (tyco, map TFree vs); 

83 
in 

84 
thy 

26168  85 
> RType.perhaps_add_def tyco 
86 
> not has_inst ? add_term_of_def ty vs tyco 

26020  87 
end; 
88 
in 

26168  89 
Code.type_interpretation interpretator 
26020  90 
end 
22525  91 
*} 
92 

26020  93 
setup {* 
94 
let 

95 
fun mk_term_of_eq ty vs tyco (c, tys) = 

96 
let 

97 
val t = list_comb (Const (c, tys > ty), 

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

99 
in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty)  t => t) t, Eval.mk_term 

100 
(fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) 

26168  101 
(RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t) 
26020  102 
end; 
103 
fun prove_term_of_eq ty eq thy = 

104 
let 

105 
val cty = Thm.ctyp_of thy ty; 

106 
val (arg, rhs) = pairself (Thm.cterm_of thy) eq; 

107 
val thm = @{thm term_of_anything} 

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

109 
> Thm.varifyT; 

110 
in 

111 
thy 

112 
> Code.add_func thm 

113 
end; 

114 
fun interpretator (tyco, (raw_vs, raw_cs)) thy = 

115 
let 

116 
val constrain_sort = 

117 
curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; 

118 
val vs = (map o apsnd) constrain_sort raw_vs; 

119 
val cs = (map o apsnd o map o map_atyps) 

120 
(fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; 

121 
val ty = Type (tyco, map TFree vs); 

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

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

124 
in 

125 
thy 

126 
> Code.del_funcs const 

127 
> fold (prove_term_of_eq ty) eqs 

128 
end; 

129 
in 

130 
Code.type_interpretation interpretator 

25569  131 
end 
26020  132 
*} 
23062  133 

26587  134 

25763  135 
subsubsection {* Code generator setup *} 
136 

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

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

26037  139 

26168  140 
lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" .. 
26037  141 
lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" .. 
142 
lemma [code func, code func del]: "(term_of \<Colon> index \<Rightarrow> term) = term_of" .. 

26020  143 
lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" .. 
22525  144 

25763  145 
code_type "term" 
146 
(SML "Term.term") 

147 

26020  148 
code_const Const and App 
149 
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") 

22525  150 

26037  151 
code_const "term_of \<Colon> index \<Rightarrow> term" 
152 
(SML "HOLogic.mk'_number/ HOLogic.indexT") 

153 

154 
code_const "term_of \<Colon> message_string \<Rightarrow> term" 

155 
(SML "Message'_String.mk") 

156 

157 

26587  158 
subsubsection {* Syntax *} 
159 

160 
print_translation {* 

161 
let 

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

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

164 
fun tr2' [] = term; 

165 
in 

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

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

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

169 
end 

170 
*} 

171 
setup {* 

172 
Sign.declare_const [] ("rterm_of", @{typ "'a \<Rightarrow> 'b"}, NoSyn) 

173 
#> snd 

174 
*} 

175 

176 
notation (output) 

177 
rterm_of ("\<guillemotleft>_\<guillemotright>") 

178 

179 
locale (open) rterm_syntax = 

180 
fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>") 

181 

182 
parse_translation {* 

183 
let 

184 
fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t 

185 
 rterm_of_tr ts = raise TERM ("rterm_of_tr", ts); 

186 
in 

187 
[("\<^fixed>rterm_of_syntax", rterm_of_tr)] 

188 
end 

189 
*} 

190 

191 
setup {* 

192 
let 

193 
val subst_rterm_of = Eval.mk_term 

194 
(fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) 

195 
(RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))); 

196 
fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t 

197 
 subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = 

198 
error ("illegal number of arguments for " ^ quote @{const_name rterm_of}) 

199 
 subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts); 

200 
fun subst_rterm_of'' t = 

201 
let 

202 
val t' = subst_rterm_of' (strip_comb t); 

203 
in if t aconv t' 

204 
then NONE 

205 
else SOME t' 

206 
end; 

207 
fun check_rterm_of ts ctxt = 

208 
let 

209 
val ts' = map subst_rterm_of'' ts; 

210 
in if exists is_some ts' 

211 
then SOME (map2 the_default ts ts', ctxt) 

212 
else NONE 

213 
end; 

214 
in 

215 
Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of) 

216 
end; 

217 
*} 

218 

219 
hide const dummy_term 

220 
hide (open) const Const App 

221 
hide (open) const term_of 

222 

223 

25763  224 
subsection {* Evaluation setup *} 
22525  225 

226 
ML {* 

227 
signature EVAL = 

228 
sig 

26267
ba710daf77a7
added combinator for interpretation of construction of datatype
haftmann
parents:
26242
diff
changeset

229 
val mk_term: ((string * typ) > term) > (typ > term) > term > term 
24587  230 
val eval_ref: (unit > term) option ref 
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

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

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

233 
val evaluate': string > Proof.context > term > unit 
26020  234 
val evaluate_cmd: string option > string > Toplevel.state > unit 
22525  235 
end; 
236 

26020  237 
structure Eval : EVAL = 
22525  238 
struct 
239 

26020  240 
open Eval; 
241 

24587  242 
val eval_ref = ref (NONE : (unit > term) option); 
22525  243 

26020  244 
fun eval_term thy t = 
245 
t 

246 
> Eval.mk_term_of (fastype_of t) 

247 
> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t []) 

248 
> Code.postprocess_term thy; 

24280  249 

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

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

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

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

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

254 
]; 
22525  255 

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

256 
fun gen_evaluate evaluators ctxt t = 
24280  257 
let 
258 
val thy = ProofContext.theory_of ctxt; 

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

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

260 
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

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

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

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

265 
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, 
24920  266 
Pretty.quote (Syntax.pretty_typ ctxt ty')]; 
24280  267 
in Pretty.writeln p end; 
268 

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

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

270 

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

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

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

273 

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

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

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

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

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

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

281 
end; 
22525  282 

283 
end; 

284 
*} 

285 

22804  286 
ML {* 
287 
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

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

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

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

291 
(Eval.evaluate_cmd some_name t))); 
22804  292 
*} 
293 

26032  294 
end 