author | haftmann |
Fri, 16 Mar 2007 21:32:07 +0100 | |
changeset 22451 | 989182f660e0 |
parent 22423 | c1836b14c63a |
child 22473 | 753123c89d72 |
permissions | -rw-r--r-- |
21046 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Setup of code generator tools *} |
|
6 |
||
7 |
theory Code_Generator |
|
8 |
imports HOL |
|
9 |
begin |
|
10 |
||
22385 | 11 |
subsection {* SML code generator setup *} |
21046 | 12 |
|
13 |
types_code |
|
14 |
"bool" ("bool") |
|
15 |
attach (term_of) {* |
|
16 |
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
|
17 |
*} |
|
18 |
attach (test) {* |
|
19 |
fun gen_bool i = one_of [false, true]; |
|
20 |
*} |
|
21 |
"prop" ("bool") |
|
22 |
attach (term_of) {* |
|
23 |
fun term_of_prop b = |
|
24 |
HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); |
|
25 |
*} |
|
26 |
||
27 |
consts_code |
|
28 |
"Trueprop" ("(_)") |
|
29 |
"True" ("true") |
|
30 |
"False" ("false") |
|
31 |
"Not" ("not") |
|
32 |
"op |" ("(_ orelse/ _)") |
|
33 |
"op &" ("(_ andalso/ _)") |
|
34 |
"HOL.If" ("(if _/ then _/ else _)") |
|
35 |
||
36 |
setup {* |
|
37 |
let |
|
38 |
||
39 |
fun eq_codegen thy defs gr dep thyname b t = |
|
40 |
(case strip_comb t of |
|
41 |
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE |
|
42 |
| (Const ("op =", _), [t, u]) => |
|
43 |
let |
|
44 |
val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); |
|
45 |
val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); |
|
46 |
val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) |
|
47 |
in |
|
48 |
SOME (gr''', Codegen.parens |
|
49 |
(Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu])) |
|
50 |
end |
|
51 |
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen |
|
52 |
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) |
|
53 |
| _ => NONE); |
|
54 |
||
55 |
in |
|
56 |
||
57 |
Codegen.add_codegen "eq_codegen" eq_codegen |
|
58 |
||
59 |
end |
|
60 |
*} |
|
61 |
||
62 |
text {* Evaluation *} |
|
63 |
||
22099 | 64 |
method_setup evaluation = {* |
21046 | 65 |
let |
66 |
||
67 |
fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule |
|
68 |
(Drule.goals_conv (equal i) Codegen.evaluation_conv)); |
|
69 |
||
22099 | 70 |
in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end |
71 |
*} "solve goal by evaluation" |
|
21046 | 72 |
|
73 |
||
74 |
subsection {* Generic code generator setup *} |
|
75 |
||
21904 | 76 |
text {* operational equality for code generation *} |
77 |
||
22385 | 78 |
class eq (attach "op =") = notes reflexive |
21904 | 79 |
|
80 |
||
81 |
text {* equality for Haskell *} |
|
82 |
||
83 |
code_class eq |
|
84 |
(Haskell "Eq" where "op =" \<equiv> "(==)") |
|
85 |
||
86 |
code_const "op =" |
|
87 |
(Haskell infixl 4 "==") |
|
88 |
||
89 |
||
22423 | 90 |
text {* type bool *} |
91 |
||
92 |
code_datatype True False |
|
21904 | 93 |
|
94 |
lemma [code func]: |
|
95 |
shows "(False \<and> x) = False" |
|
96 |
and "(True \<and> x) = x" |
|
97 |
and "(x \<and> False) = False" |
|
98 |
and "(x \<and> True) = x" by simp_all |
|
99 |
||
100 |
lemma [code func]: |
|
101 |
shows "(False \<or> x) = x" |
|
102 |
and "(True \<or> x) = True" |
|
103 |
and "(x \<or> False) = x" |
|
104 |
and "(x \<or> True) = True" by simp_all |
|
105 |
||
106 |
lemma [code func]: |
|
107 |
shows "(\<not> True) = False" |
|
108 |
and "(\<not> False) = True" by (rule HOL.simp_thms)+ |
|
109 |
||
110 |
lemmas [code func] = imp_conv_disj |
|
111 |
||
112 |
lemmas [code func] = if_True if_False |
|
113 |
||
114 |
instance bool :: eq .. |
|
115 |
||
116 |
lemma [code func]: |
|
117 |
"True = P \<longleftrightarrow> P" by simp |
|
118 |
||
119 |
lemma [code func]: |
|
120 |
"False = P \<longleftrightarrow> \<not> P" by simp |
|
121 |
||
122 |
lemma [code func]: |
|
123 |
"P = True \<longleftrightarrow> P" by simp |
|
124 |
||
125 |
lemma [code func]: |
|
126 |
"P = False \<longleftrightarrow> \<not> P" by simp |
|
127 |
||
128 |
code_type bool |
|
129 |
(SML "bool") |
|
130 |
(OCaml "bool") |
|
131 |
(Haskell "Bool") |
|
132 |
||
133 |
code_instance bool :: eq |
|
134 |
(Haskell -) |
|
135 |
||
136 |
code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" |
|
137 |
(Haskell infixl 4 "==") |
|
138 |
||
139 |
code_const True and False and Not and "op &" and "op |" and If |
|
140 |
(SML "true" and "false" and "not" |
|
141 |
and infixl 1 "andalso" and infixl 0 "orelse" |
|
142 |
and "!(if (_)/ then (_)/ else (_))") |
|
143 |
(OCaml "true" and "false" and "not" |
|
144 |
and infixl 4 "&&" and infixl 2 "||" |
|
145 |
and "!(if (_)/ then (_)/ else (_))") |
|
146 |
(Haskell "True" and "False" and "not" |
|
147 |
and infixl 3 "&&" and infixl 2 "||" |
|
148 |
and "!(if (_)/ then (_)/ else (_))") |
|
149 |
||
150 |
code_reserved SML |
|
151 |
bool true false not |
|
152 |
||
153 |
code_reserved OCaml |
|
154 |
bool true false not |
|
155 |
||
156 |
||
22423 | 157 |
text {* type prop *} |
158 |
||
159 |
code_datatype Trueprop "prop" |
|
160 |
||
161 |
||
162 |
text {* type itself *} |
|
21046 | 163 |
|
22423 | 164 |
code_datatype "TYPE('a)" |
165 |
||
166 |
||
167 |
text {* prevent unfolding of quantifier definitions *} |
|
168 |
||
169 |
lemma [code func]: |
|
170 |
"Ex = Ex" |
|
171 |
"All = All" |
|
172 |
by rule+ |
|
21046 | 173 |
|
174 |
||
175 |
text {* code generation for arbitrary as exception *} |
|
176 |
||
177 |
setup {* |
|
178 |
CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")" |
|
21904 | 179 |
#> CodegenSerializer.add_undefined "OCaml" "arbitrary" "(failwith \"arbitrary\")" |
21046 | 180 |
*} |
181 |
||
182 |
code_const arbitrary |
|
21110 | 183 |
(Haskell "error/ \"arbitrary\"") |
21046 | 184 |
|
21079 | 185 |
code_reserved SML Fail |
21904 | 186 |
code_reserved OCaml failwith |
21046 | 187 |
|
188 |
||
21378 | 189 |
subsection {* Evaluation oracle *} |
190 |
||
191 |
ML {* |
|
22099 | 192 |
structure HOL_Eval: |
21378 | 193 |
sig |
22004 | 194 |
val reff: bool option ref |
195 |
val prop: theory -> term -> term |
|
22099 | 196 |
end = |
21378 | 197 |
struct |
198 |
||
22004 | 199 |
val reff : bool option ref = ref NONE; |
21378 | 200 |
|
22004 | 201 |
fun prop thy t = |
21869 | 202 |
if CodegenPackage.eval_term thy |
22004 | 203 |
(("HOL_Eval.reff", reff), t) |
21869 | 204 |
then HOLogic.true_const |
22004 | 205 |
else HOLogic.false_const |
206 |
||
22099 | 207 |
end |
21869 | 208 |
*} |
21378 | 209 |
|
22099 | 210 |
oracle eval_oracle ("term") = {* |
211 |
fn thy => fn t => Logic.mk_equals (t, HOL_Eval.prop thy t) |
|
21869 | 212 |
*} |
21378 | 213 |
|
22099 | 214 |
method_setup eval = {* |
215 |
let |
|
21378 | 216 |
|
217 |
fun conv ct = |
|
22099 | 218 |
let val {thy, t, ...} = rep_cterm ct |
219 |
in eval_oracle thy t end; |
|
21378 | 220 |
|
22099 | 221 |
fun eval_tac i = Tactical.PRIMITIVE (Drule.fconv_rule |
21546 | 222 |
(Drule.goals_conv (equal i) (HOLogic.Trueprop_conv conv))); |
21378 | 223 |
|
22099 | 224 |
in Method.no_args (Method.SIMPLE_METHOD' (eval_tac THEN' rtac TrueI)) end |
225 |
*} "solve goal by evaluation" |
|
21378 | 226 |
|
227 |
||
228 |
subsection {* Normalization by evaluation *} |
|
21046 | 229 |
|
22099 | 230 |
method_setup normalization = {* |
21046 | 231 |
let |
232 |
fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule |
|
21546 | 233 |
(Drule.goals_conv (equal i) (HOLogic.Trueprop_conv |
21149 | 234 |
NBE.normalization_conv))); |
21046 | 235 |
in |
22099 | 236 |
Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl])) |
237 |
end |
|
238 |
*} "solve goal by normalization" |
|
239 |
||
21046 | 240 |
|
21059 | 241 |
text {* lazy @{const If} *} |
242 |
||
243 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21378
diff
changeset
|
244 |
if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where |
21059 | 245 |
"if_delayed b f g = (if b then f True else g False)" |
246 |
||
247 |
lemma [code func]: |
|
248 |
shows "if_delayed True f g = f True" |
|
249 |
and "if_delayed False f g = g False" |
|
250 |
unfolding if_delayed_def by simp_all |
|
251 |
||
252 |
lemma [normal pre, symmetric, normal post]: |
|
253 |
"(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)" |
|
254 |
unfolding if_delayed_def .. |
|
255 |
||
256 |
||
21454 | 257 |
hide (open) const if_delayed |
21046 | 258 |
|
22099 | 259 |
end |