author  haftmann 
Sun, 09 Mar 2008 07:57:30 +0100  
changeset 26242  d64510d3c7b7 
parent 26168  3bd9ac4e0b97 
child 26267  ba710daf77a7 
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 

26020  16 
subsubsection {* Definitions *} 
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 

26020  33 
subsubsection {* Class @{term term_of} *} 
34 

26168  35 
class term_of = rtype + 
26020  36 
fixes term_of :: "'a \<Rightarrow> term" 
37 

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

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

25763  40 

41 
ML {* 

26020  42 
structure Eval = 
25763  43 
struct 
44 

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

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

47 
 mk_term f g (t1 $ t2) = 

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

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

50 

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

53 
end; 

54 
*} 

55 

56 
setup {* 

57 
let 

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

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

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

64 
in 

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

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

25569  69 
> snd 
70 
> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) 

71 
> LocalTheory.exit 

72 
> ProofContext.theory_of 

26020  73 
end; 
74 
fun interpretator (tyco, (raw_vs, _)) thy = 

75 
let 

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

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

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

81 
in 

82 
thy 

26168  83 
> RType.perhaps_add_def tyco 
84 
> not has_inst ? add_term_of_def ty vs tyco 

26020  85 
end; 
86 
in 

26168  87 
Code.type_interpretation interpretator 
26020  88 
end 
22525  89 
*} 
90 

26020  91 
setup {* 
92 
let 

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

94 
let 

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

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

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

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

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

102 
let 

103 
val cty = Thm.ctyp_of thy ty; 

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

105 
val thm = @{thm term_of_anything} 

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

107 
> Thm.varifyT; 

108 
in 

109 
thy 

110 
> Code.add_func thm 

111 
end; 

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

113 
let 

114 
val constrain_sort = 

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

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

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

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

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

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

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

122 
in 

123 
thy 

124 
> Code.del_funcs const 

125 
> fold (prove_term_of_eq ty) eqs 

126 
end; 

127 
in 

128 
Code.type_interpretation interpretator 

25569  129 
end 
26020  130 
*} 
23062  131 

25763  132 
subsubsection {* Code generator setup *} 
133 

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

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

26037  136 

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

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

25763  142 
code_type "term" 
143 
(SML "Term.term") 

144 

26020  145 
code_const Const and App 
146 
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") 

22525  147 

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

150 

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

152 
(SML "Message'_String.mk") 

153 

154 

25763  155 
subsection {* Evaluation setup *} 
22525  156 

157 
ML {* 

158 
signature EVAL = 

159 
sig 

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

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

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

163 
val evaluate': string > Proof.context > term > unit 
26020  164 
val evaluate_cmd: string option > string > Toplevel.state > unit 
22525  165 
end; 
166 

26020  167 
structure Eval : EVAL = 
22525  168 
struct 
169 

26020  170 
open Eval; 
171 

24587  172 
val eval_ref = ref (NONE : (unit > term) option); 
22525  173 

26020  174 
fun eval_term thy t = 
175 
t 

176 
> Eval.mk_term_of (fastype_of t) 

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

178 
> Code.postprocess_term thy; 

24280  179 

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

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

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

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

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

184 
]; 
22525  185 

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

186 
fun gen_evaluate evaluators ctxt t = 
24280  187 
let 
188 
val thy = ProofContext.theory_of ctxt; 

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

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

190 
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

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

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

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

195 
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, 
24920  196 
Pretty.quote (Syntax.pretty_typ ctxt ty')]; 
24280  197 
in Pretty.writeln p end; 
198 

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

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

200 

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

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

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

203 

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

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

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

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

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

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

211 
end; 
22525  212 

213 
end; 

214 
*} 

215 

22804  216 
ML {* 
217 
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

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

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

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

221 
(Eval.evaluate_cmd some_name t))); 
22804  222 
*} 
223 

26032  224 
print_translation {* 
225 
let 

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

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

228 
fun tr2' [] = term; 

229 
in 

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

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

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

233 
end 

234 
*} 

235 

26168  236 
hide (open) const term_of 
26032  237 
hide const Const App dummy_term 
26020  238 

22665  239 
end 