author  haftmann 
Thu, 04 Oct 2007 19:41:49 +0200  
changeset 24835  8c26128f8997 
parent 24659  6b7ac2a43df8 
child 24867  e5b55d7be9bb 
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 

24280  9 
imports Main Pure_term 
22525  10 
begin 
11 

22527  12 
subsection {* @{text typ_of} class *} 
22525  13 

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

22525  16 

17 
ML {* 

18 
structure TypOf = 

19 
struct 

20 

21 
val class_typ_of = Sign.intern_class @{theory} "typ_of"; 

22 

23 
fun term_typ_of_type ty = 

24 
Const (@{const_name typ_of}, Term.itselfT ty > @{typ typ}) 

25 
$ Logic.mk_type ty; 

26 

27 
fun mk_typ_of_def ty = 

28 
let 

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

30 
$ Free ("x", Term.itselfT ty) 

31 
val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty 

32 
in Logic.mk_equals (lhs, rhs) end; 

33 

34 
end; 

35 
*} 

36 

24587  37 
instance "prop" :: typ_of 
38 
"typ_of T \<equiv> STR ''prop'' {\<struct>} []" .. 

39 

23062  40 
instance itself :: (typ_of) typ_of 
41 
"typ_of T \<equiv> STR ''itself'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" .. 

42 

24587  43 
instance set :: (typ_of) typ_of 
44 
"typ_of T \<equiv> STR ''set'' {\<struct>} [typ_of TYPE('a\<Colon>typ_of)]" .. 

23062  45 

23020  46 
instance int :: typ_of 
47 
"typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" .. 

48 

22525  49 
setup {* 
50 
let 

51 
fun mk arities _ thy = 

52 
(maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def 

53 
(Type (tyco, 

54 
map TFree (Name.names Name.context "'a" asorts))))]) arities, thy); 

55 
fun hook specs = 

24219  56 
DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac []) 
22525  57 
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) 
24621  58 
[TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func)) 
24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24621
diff
changeset

59 
in DatatypeCodegen.add_codetypes_hook hook end 
22525  60 
*} 
61 

62 

22527  63 
subsection {* @{text term_of} class *} 
22525  64 

65 
class term_of = typ_of + 

23062  66 
constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> typ" 
22525  67 
fixes term_of :: "'a \<Rightarrow> term" 
68 

69 
ML {* 

70 
structure TermOf = 

71 
struct 

72 

73 
local 

74 
fun term_term_of ty = 

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

76 
in 

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

78 
fun mk_terms_of_defs vs (tyco, cs) = 

79 
let 

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

81 
fun mk_eq c = 

82 
let 

83 
val lhs : term = term_term_of dty $ c; 

84 
val rhs : term = Pure_term.mk_term 

85 
(fn (v, ty) => term_term_of ty $ Free (v, ty)) 

86 
(Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c 

87 
in 

88 
HOLogic.mk_eq (lhs, rhs) 

89 
end; 

90 
in map mk_eq cs end; 

91 
fun mk_term_of t = 

92 
term_term_of (Term.fastype_of t) $ t; 

93 
end; 

94 

95 
end; 

96 
*} 

97 

98 
setup {* 

99 
let 

100 
fun thy_note ((name, atts), thms) = 

101 
PureThy.add_thmss [((name, thms), atts)] #> (fn [thms] => pair (name, thms)); 

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

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

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24381
diff
changeset

104 
fun mk arities css _ thy = 
22525  105 
let 
106 
val (_, asorts, _) :: _ = arities; 

107 
val vs = Name.names Name.context "'a" asorts; 

108 
val defs = map (TermOf.mk_terms_of_defs vs) css; 

109 
val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs; 

110 
in 

111 
thy 

112 
> PrimrecPackage.gen_primrec thy_note thy_def "" defs' 

113 
> snd 

114 
end; 

115 
fun hook specs = 

24659  116 
if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I 
22525  117 
else 
24219  118 
DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac []) 
22525  119 
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) 
120 
[TermOf.class_term_of] ((K o K o pair) []) mk 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24621
diff
changeset

121 
in DatatypeCodegen.add_codetypes_hook hook end 
22525  122 
*} 
123 

23062  124 
abbreviation 
125 
intT :: "typ" 

126 
where 

127 
"intT \<equiv> STR ''IntDef.int'' {\<struct>} []" 

128 

23133  129 
abbreviation 
130 
bitT :: "typ" 

131 
where 

132 
"bitT \<equiv> STR ''Numeral.bit'' {\<struct>} []" 

133 

23062  134 
function 
135 
mk_int :: "int \<Rightarrow> term" 

136 
where 

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

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

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

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

23062  142 
by pat_completeness auto 
143 
termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div) 

144 

145 
instance int :: term_of 

23133  146 
"term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" .. 
23062  147 

148 

22804  149 
text {* Adaption for @{typ ml_string}s *} 
22525  150 

22845  151 
lemmas [code func, code func del] = term_of_ml_string_def 
22525  152 

153 

154 
subsection {* Evaluation infrastructure *} 

155 

156 
ML {* 

157 
signature EVAL = 

158 
sig 

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

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

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

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

163 
val evaluate_cmd: string option > Toplevel.state > unit 
22525  164 
end; 
165 

24280  166 
structure Eval = 
22525  167 
struct 
168 

24587  169 
val eval_ref = ref (NONE : (unit > term) option); 
22525  170 

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

171 
fun eval_invoke thy code ((_, ty), t) deps _ = 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

172 
CodePackage.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) []; 
24280  173 

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

174 
fun eval_term thy = 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

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

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

177 
#> Code.postprocess_term thy; 
24280  178 

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

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

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

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

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

183 
]; 
22525  184 

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

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

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

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

189 
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

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

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

192 
val ty' = Term.type_of t'; 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

193 
val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

194 
Pretty.fbrk, Pretty.str "::", Pretty.brk 1, 
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset

195 
Pretty.quote (ProofContext.pretty_typ ctxt ty')]; 
24280  196 
in Pretty.writeln p end; 
197 

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

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

199 

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

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

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

202 

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

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

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

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

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

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

210 
end; 
22525  211 

212 
end; 

213 
*} 

214 

22804  215 
ML {* 
216 
val valueP = 

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 
val _ = OuterSyntax.add_parsers [valueP]; 

224 
*} 

225 

22665  226 
end 