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