author | haftmann |
Thu, 09 Oct 2008 08:47:27 +0200 | |
changeset 28537 | 1e84256d1a8a |
parent 28512 | f29fecd6ddaa |
child 28562 | 4e74209f113e |
permissions | -rw-r--r-- |
24285 | 1 |
(* Title: HOL/Code_Setup.thy |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann |
|
4 |
*) |
|
5 |
||
28400 | 6 |
header {* Setup of code generators and related tools *} |
24285 | 7 |
|
8 |
theory Code_Setup |
|
9 |
imports HOL |
|
28400 | 10 |
begin |
11 |
||
12 |
subsection {* Generic code generator foundation *} |
|
13 |
||
14 |
text {* Datatypes *} |
|
15 |
||
16 |
code_datatype True False |
|
17 |
||
18 |
code_datatype "TYPE('a\<Colon>{})" |
|
19 |
||
20 |
code_datatype Trueprop "prop" |
|
21 |
||
22 |
text {* Code equations *} |
|
23 |
||
24 |
lemma [code func]: |
|
25 |
shows "False \<and> x \<longleftrightarrow> False" |
|
26 |
and "True \<and> x \<longleftrightarrow> x" |
|
27 |
and "x \<and> False \<longleftrightarrow> False" |
|
28 |
and "x \<and> True \<longleftrightarrow> x" by simp_all |
|
29 |
||
30 |
lemma [code func]: |
|
31 |
shows "False \<or> x \<longleftrightarrow> x" |
|
32 |
and "True \<or> x \<longleftrightarrow> True" |
|
33 |
and "x \<or> False \<longleftrightarrow> x" |
|
34 |
and "x \<or> True \<longleftrightarrow> True" by simp_all |
|
35 |
||
36 |
lemma [code func]: |
|
37 |
shows "\<not> True \<longleftrightarrow> False" |
|
38 |
and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+ |
|
39 |
||
40 |
lemmas [code func] = Let_def if_True if_False |
|
41 |
||
42 |
lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj |
|
43 |
||
44 |
text {* Equality *} |
|
45 |
||
46 |
context eq |
|
24285 | 47 |
begin |
48 |
||
28400 | 49 |
lemma equals_eq [code inline, code func]: "op = \<equiv> eq" |
50 |
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) |
|
51 |
||
28512 | 52 |
declare eq [code unfold, code inline del] |
53 |
||
28400 | 54 |
declare equals_eq [symmetric, code post] |
55 |
||
56 |
end |
|
57 |
||
58 |
declare simp_thms(6) [code nbe] |
|
59 |
||
60 |
hide (open) const eq |
|
61 |
hide const eq |
|
62 |
||
63 |
setup {* |
|
64 |
Code_Unit.add_const_alias @{thm equals_eq} |
|
65 |
*} |
|
66 |
||
67 |
text {* Cases *} |
|
68 |
||
69 |
lemma Let_case_cert: |
|
70 |
assumes "CASE \<equiv> (\<lambda>x. Let x f)" |
|
71 |
shows "CASE x \<equiv> f x" |
|
72 |
using assms by simp_all |
|
73 |
||
74 |
lemma If_case_cert: |
|
75 |
includes meta_conjunction_syntax |
|
76 |
assumes "CASE \<equiv> (\<lambda>b. If b f g)" |
|
77 |
shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)" |
|
78 |
using assms by simp_all |
|
79 |
||
80 |
setup {* |
|
81 |
Code.add_case @{thm Let_case_cert} |
|
82 |
#> Code.add_case @{thm If_case_cert} |
|
83 |
#> Code.add_undefined @{const_name undefined} |
|
84 |
*} |
|
85 |
||
86 |
code_abort undefined |
|
87 |
||
88 |
||
89 |
subsection {* Generic code generator preprocessor *} |
|
90 |
||
91 |
setup {* |
|
92 |
Code.map_pre (K HOL_basic_ss) |
|
93 |
#> Code.map_post (K HOL_basic_ss) |
|
94 |
*} |
|
95 |
||
24285 | 96 |
|
28400 | 97 |
subsection {* Generic code generator target languages *} |
98 |
||
99 |
text {* type bool *} |
|
100 |
||
101 |
code_type bool |
|
102 |
(SML "bool") |
|
103 |
(OCaml "bool") |
|
104 |
(Haskell "Bool") |
|
105 |
||
106 |
code_const True and False and Not and "op &" and "op |" and If |
|
107 |
(SML "true" and "false" and "not" |
|
108 |
and infixl 1 "andalso" and infixl 0 "orelse" |
|
109 |
and "!(if (_)/ then (_)/ else (_))") |
|
110 |
(OCaml "true" and "false" and "not" |
|
111 |
and infixl 4 "&&" and infixl 2 "||" |
|
112 |
and "!(if (_)/ then (_)/ else (_))") |
|
113 |
(Haskell "True" and "False" and "not" |
|
114 |
and infixl 3 "&&" and infixl 2 "||" |
|
115 |
and "!(if (_)/ then (_)/ else (_))") |
|
116 |
||
117 |
code_reserved SML |
|
118 |
bool true false not |
|
119 |
||
120 |
code_reserved OCaml |
|
121 |
bool not |
|
122 |
||
123 |
text {* using built-in Haskell equality *} |
|
124 |
||
125 |
code_class eq |
|
126 |
(Haskell "Eq" where "eq_class.eq" \<equiv> "(==)") |
|
127 |
||
128 |
code_const "eq_class.eq" |
|
129 |
(Haskell infixl 4 "==") |
|
130 |
||
131 |
code_const "op =" |
|
132 |
(Haskell infixl 4 "==") |
|
133 |
||
134 |
text {* undefined *} |
|
135 |
||
136 |
code_const undefined |
|
28512 | 137 |
(SML "!(raise/ Fail/ \"undefined\")") |
28400 | 138 |
(OCaml "failwith/ \"undefined\"") |
139 |
(Haskell "error/ \"undefined\"") |
|
140 |
||
141 |
||
142 |
subsection {* SML code generator setup *} |
|
24285 | 143 |
|
144 |
types_code |
|
145 |
"bool" ("bool") |
|
146 |
attach (term_of) {* |
|
147 |
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
|
148 |
*} |
|
149 |
attach (test) {* |
|
25885 | 150 |
fun gen_bool i = |
151 |
let val b = one_of [false, true] |
|
152 |
in (b, fn () => term_of_bool b) end; |
|
24285 | 153 |
*} |
154 |
"prop" ("bool") |
|
155 |
attach (term_of) {* |
|
156 |
fun term_of_prop b = |
|
157 |
HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); |
|
158 |
*} |
|
159 |
||
160 |
consts_code |
|
161 |
"Trueprop" ("(_)") |
|
162 |
"True" ("true") |
|
163 |
"False" ("false") |
|
164 |
"Not" ("Bool.not") |
|
165 |
"op |" ("(_ orelse/ _)") |
|
166 |
"op &" ("(_ andalso/ _)") |
|
167 |
"If" ("(if _/ then _/ else _)") |
|
168 |
||
169 |
setup {* |
|
170 |
let |
|
171 |
||
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
172 |
fun eq_codegen thy defs dep thyname b t gr = |
24285 | 173 |
(case strip_comb t of |
174 |
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE |
|
175 |
| (Const ("op =", _), [t, u]) => |
|
176 |
let |
|
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
177 |
val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr; |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
178 |
val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr'; |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
179 |
val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr''; |
24285 | 180 |
in |
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
181 |
SOME (Codegen.parens |
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
182 |
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''') |
24285 | 183 |
end |
184 |
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen |
|
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28512
diff
changeset
|
185 |
thy defs dep thyname b (Codegen.eta_expand t ts 2) gr) |
24285 | 186 |
| _ => NONE); |
187 |
||
188 |
in |
|
189 |
Codegen.add_codegen "eq_codegen" eq_codegen |
|
190 |
end |
|
191 |
*} |
|
192 |
||
24463
841c2e24761f
Smaller size and fewer iterations for quickcheck.
berghofe
parents:
24293
diff
changeset
|
193 |
|
28400 | 194 |
subsection {* Evaluation and normalization by evaluation *} |
24285 | 195 |
|
27103 | 196 |
ML {* |
197 |
structure Eval_Method = |
|
198 |
struct |
|
199 |
||
200 |
val eval_ref : (unit -> bool) option ref = ref NONE; |
|
201 |
||
202 |
end; |
|
203 |
*} |
|
204 |
||
28290 | 205 |
oracle eval_oracle = {* fn ct => |
206 |
let |
|
207 |
val thy = Thm.theory_of_cterm ct; |
|
208 |
val t = Thm.term_of ct; |
|
209 |
in |
|
210 |
if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy |
|
211 |
(HOLogic.dest_Trueprop t) [] |
|
212 |
then ct |
|
213 |
else @{cprop True} (*dummy*) |
|
214 |
end |
|
24285 | 215 |
*} |
216 |
||
217 |
method_setup eval = {* |
|
218 |
let |
|
219 |
fun eval_tac thy = |
|
28290 | 220 |
CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i) |
24285 | 221 |
in |
222 |
Method.ctxt_args (fn ctxt => |
|
223 |
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt))) |
|
224 |
end |
|
225 |
*} "solve goal by evaluation" |
|
226 |
||
227 |
||
28400 | 228 |
method_setup evaluation = {* |
229 |
Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI)) |
|
230 |
*} "solve goal by evaluation" |
|
231 |
||
24285 | 232 |
|
233 |
method_setup normalization = {* |
|
234 |
Method.no_args (Method.SIMPLE_METHOD' |
|
25962 | 235 |
(CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) |
236 |
THEN' (fn k => TRY (rtac TrueI k)) |
|
25866 | 237 |
)) |
24285 | 238 |
*} "solve goal by normalization" |
239 |
||
28400 | 240 |
|
241 |
subsection {* Quickcheck *} |
|
242 |
||
243 |
quickcheck_params [size = 5, iterations = 50] |
|
244 |
||
24285 | 245 |
end |