author | wenzelm |
Sat, 04 Oct 2008 16:05:09 +0200 | |
changeset 28500 | 4b79e5d3d0aa |
parent 28400 | 89904cfd41c3 |
child 28512 | f29fecd6ddaa |
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 |
||
52 |
declare equals_eq [symmetric, code post] |
|
53 |
||
54 |
end |
|
55 |
||
56 |
declare simp_thms(6) [code nbe] |
|
57 |
||
58 |
hide (open) const eq |
|
59 |
hide const eq |
|
60 |
||
61 |
setup {* |
|
62 |
Code_Unit.add_const_alias @{thm equals_eq} |
|
63 |
*} |
|
64 |
||
65 |
text {* Cases *} |
|
66 |
||
67 |
lemma Let_case_cert: |
|
68 |
assumes "CASE \<equiv> (\<lambda>x. Let x f)" |
|
69 |
shows "CASE x \<equiv> f x" |
|
70 |
using assms by simp_all |
|
71 |
||
72 |
lemma If_case_cert: |
|
73 |
includes meta_conjunction_syntax |
|
74 |
assumes "CASE \<equiv> (\<lambda>b. If b f g)" |
|
75 |
shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)" |
|
76 |
using assms by simp_all |
|
77 |
||
78 |
setup {* |
|
79 |
Code.add_case @{thm Let_case_cert} |
|
80 |
#> Code.add_case @{thm If_case_cert} |
|
81 |
#> Code.add_undefined @{const_name undefined} |
|
82 |
*} |
|
83 |
||
84 |
code_abort undefined |
|
85 |
||
86 |
||
87 |
subsection {* Generic code generator preprocessor *} |
|
88 |
||
89 |
setup {* |
|
90 |
Code.map_pre (K HOL_basic_ss) |
|
91 |
#> Code.map_post (K HOL_basic_ss) |
|
92 |
*} |
|
93 |
||
24285 | 94 |
|
28400 | 95 |
subsection {* Generic code generator target languages *} |
96 |
||
97 |
text {* type bool *} |
|
98 |
||
99 |
code_type bool |
|
100 |
(SML "bool") |
|
101 |
(OCaml "bool") |
|
102 |
(Haskell "Bool") |
|
103 |
||
104 |
code_const True and False and Not and "op &" and "op |" and If |
|
105 |
(SML "true" and "false" and "not" |
|
106 |
and infixl 1 "andalso" and infixl 0 "orelse" |
|
107 |
and "!(if (_)/ then (_)/ else (_))") |
|
108 |
(OCaml "true" and "false" and "not" |
|
109 |
and infixl 4 "&&" and infixl 2 "||" |
|
110 |
and "!(if (_)/ then (_)/ else (_))") |
|
111 |
(Haskell "True" and "False" and "not" |
|
112 |
and infixl 3 "&&" and infixl 2 "||" |
|
113 |
and "!(if (_)/ then (_)/ else (_))") |
|
114 |
||
115 |
code_reserved SML |
|
116 |
bool true false not |
|
117 |
||
118 |
code_reserved OCaml |
|
119 |
bool not |
|
120 |
||
121 |
text {* using built-in Haskell equality *} |
|
122 |
||
123 |
code_class eq |
|
124 |
(Haskell "Eq" where "eq_class.eq" \<equiv> "(==)") |
|
125 |
||
126 |
code_const "eq_class.eq" |
|
127 |
(Haskell infixl 4 "==") |
|
128 |
||
129 |
code_const "op =" |
|
130 |
(Haskell infixl 4 "==") |
|
131 |
||
132 |
text {* undefined *} |
|
133 |
||
134 |
code_const undefined |
|
135 |
(SML "raise/ Fail/ \"undefined\"") |
|
136 |
(OCaml "failwith/ \"undefined\"") |
|
137 |
(Haskell "error/ \"undefined\"") |
|
138 |
||
139 |
||
140 |
subsection {* SML code generator setup *} |
|
24285 | 141 |
|
142 |
types_code |
|
143 |
"bool" ("bool") |
|
144 |
attach (term_of) {* |
|
145 |
fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const; |
|
146 |
*} |
|
147 |
attach (test) {* |
|
25885 | 148 |
fun gen_bool i = |
149 |
let val b = one_of [false, true] |
|
150 |
in (b, fn () => term_of_bool b) end; |
|
24285 | 151 |
*} |
152 |
"prop" ("bool") |
|
153 |
attach (term_of) {* |
|
154 |
fun term_of_prop b = |
|
155 |
HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); |
|
156 |
*} |
|
157 |
||
158 |
consts_code |
|
159 |
"Trueprop" ("(_)") |
|
160 |
"True" ("true") |
|
161 |
"False" ("false") |
|
162 |
"Not" ("Bool.not") |
|
163 |
"op |" ("(_ orelse/ _)") |
|
164 |
"op &" ("(_ andalso/ _)") |
|
165 |
"If" ("(if _/ then _/ else _)") |
|
166 |
||
167 |
setup {* |
|
168 |
let |
|
169 |
||
170 |
fun eq_codegen thy defs gr dep thyname b t = |
|
171 |
(case strip_comb t of |
|
172 |
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE |
|
173 |
| (Const ("op =", _), [t, u]) => |
|
174 |
let |
|
175 |
val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t); |
|
176 |
val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u); |
|
177 |
val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT) |
|
178 |
in |
|
179 |
SOME (gr''', Codegen.parens |
|
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
25962
diff
changeset
|
180 |
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu])) |
24285 | 181 |
end |
182 |
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen |
|
183 |
thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) |
|
184 |
| _ => NONE); |
|
185 |
||
186 |
in |
|
187 |
Codegen.add_codegen "eq_codegen" eq_codegen |
|
188 |
end |
|
189 |
*} |
|
190 |
||
24463
841c2e24761f
Smaller size and fewer iterations for quickcheck.
berghofe
parents:
24293
diff
changeset
|
191 |
|
28400 | 192 |
subsection {* Evaluation and normalization by evaluation *} |
24285 | 193 |
|
27103 | 194 |
ML {* |
195 |
structure Eval_Method = |
|
196 |
struct |
|
197 |
||
198 |
val eval_ref : (unit -> bool) option ref = ref NONE; |
|
199 |
||
200 |
end; |
|
201 |
*} |
|
202 |
||
28290 | 203 |
oracle eval_oracle = {* fn ct => |
204 |
let |
|
205 |
val thy = Thm.theory_of_cterm ct; |
|
206 |
val t = Thm.term_of ct; |
|
207 |
in |
|
208 |
if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy |
|
209 |
(HOLogic.dest_Trueprop t) [] |
|
210 |
then ct |
|
211 |
else @{cprop True} (*dummy*) |
|
212 |
end |
|
24285 | 213 |
*} |
214 |
||
215 |
method_setup eval = {* |
|
216 |
let |
|
217 |
fun eval_tac thy = |
|
28290 | 218 |
CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i) |
24285 | 219 |
in |
220 |
Method.ctxt_args (fn ctxt => |
|
221 |
Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt))) |
|
222 |
end |
|
223 |
*} "solve goal by evaluation" |
|
224 |
||
225 |
||
28400 | 226 |
method_setup evaluation = {* |
227 |
Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI)) |
|
228 |
*} "solve goal by evaluation" |
|
229 |
||
24285 | 230 |
|
231 |
method_setup normalization = {* |
|
232 |
Method.no_args (Method.SIMPLE_METHOD' |
|
25962 | 233 |
(CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) |
234 |
THEN' (fn k => TRY (rtac TrueI k)) |
|
25866 | 235 |
)) |
24285 | 236 |
*} "solve goal by normalization" |
237 |
||
28400 | 238 |
|
239 |
subsection {* Quickcheck *} |
|
240 |
||
241 |
quickcheck_params [size = 5, iterations = 50] |
|
242 |
||
24285 | 243 |
end |