205 exists (fn th => member (op =) (foldr add_term_consts |
205 exists (fn th => member (op =) (foldr add_term_consts |
206 [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths |
206 [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths |
207 then remove_suc_clause thy ths else ths |
207 then remove_suc_clause thy ths else ths |
208 end; |
208 end; |
209 |
209 |
210 fun lift_obj_eq f thy = |
210 fun lift_obj_eq f thy thms = |
211 map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) |
211 thms |
212 #> f thy |
212 |> try ( |
213 #> map (fn thm => thm RS @{thm eq_reflection}) |
213 map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) |
214 #> map (Conv.fconv_rule Drule.beta_eta_conversion) |
214 #> f thy |
|
215 #> map (fn thm => thm RS @{thm eq_reflection}) |
|
216 #> map (Conv.fconv_rule Drule.beta_eta_conversion)) |
|
217 |> the_default thms |
215 *} |
218 *} |
216 |
219 |
217 setup {* |
220 setup {* |
218 Codegen.add_preprocessor eqn_suc_preproc |
221 Codegen.add_preprocessor eqn_suc_preproc |
219 #> Codegen.add_preprocessor clause_suc_preproc |
222 #> Codegen.add_preprocessor clause_suc_preproc |
220 #> Code.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) |
223 #> Code.add_preproc ("eqn_Suc", lift_obj_eq eqn_suc_preproc) |
221 #> Code.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) |
224 #> Code.add_preproc ("clause_Suc", lift_obj_eq clause_suc_preproc) |
222 *} |
225 *} |
223 (*>*) |
226 (*>*) |
224 |
227 |
225 |
|
226 subsection {* Target language setup *} |
228 subsection {* Target language setup *} |
227 |
229 |
228 text {* |
230 text {* |
229 We map @{typ nat} to target language integers, where we |
231 For ML, we map @{typ nat} to target language integers, where we |
230 assert that values are always non-negative. |
232 assert that values are always non-negative. |
231 *} |
233 *} |
232 |
234 |
233 code_type nat |
235 code_type nat |
234 (SML "int") |
236 (SML "int") |
235 (OCaml "Big'_int.big'_int") |
237 (OCaml "Big'_int.big'_int") |
236 (Haskell "Integer") |
|
237 |
238 |
238 types_code |
239 types_code |
239 nat ("int") |
240 nat ("int") |
240 attach (term_of) {* |
241 attach (term_of) {* |
241 val term_of_nat = HOLogic.mk_number HOLogic.natT; |
242 val term_of_nat = HOLogic.mk_number HOLogic.natT; |
245 let val n = random_range 0 i |
246 let val n = random_range 0 i |
246 in (n, fn () => term_of_nat n) end; |
247 in (n, fn () => term_of_nat n) end; |
247 *} |
248 *} |
248 |
249 |
249 text {* |
250 text {* |
|
251 For Haskell we define our own @{typ nat} type. The reason |
|
252 is that we have to distinguish type class instances |
|
253 for @{typ nat} and @{typ int}. |
|
254 *} |
|
255 |
|
256 code_include Haskell "Nat" {* |
|
257 newtype Nat = Nat Integer deriving (Show, Eq); |
|
258 |
|
259 instance Num Nat where { |
|
260 fromInteger k = Nat (if k >= 0 then k else 0); |
|
261 Nat n + Nat m = Nat (n + m); |
|
262 Nat n - Nat m = fromInteger (n - m); |
|
263 Nat n * Nat m = Nat (n * m); |
|
264 abs n = n; |
|
265 signum _ = 1; |
|
266 negate n = error "negate Nat"; |
|
267 }; |
|
268 |
|
269 instance Ord Nat where { |
|
270 Nat n <= Nat m = n <= m; |
|
271 Nat n < Nat m = n < m; |
|
272 }; |
|
273 |
|
274 instance Real Nat where { |
|
275 toRational (Nat n) = toRational n; |
|
276 }; |
|
277 |
|
278 instance Enum Nat where { |
|
279 toEnum k = fromInteger (toEnum k); |
|
280 fromEnum (Nat n) = fromEnum n; |
|
281 }; |
|
282 |
|
283 instance Integral Nat where { |
|
284 toInteger (Nat n) = n; |
|
285 divMod n m = quotRem n m; |
|
286 quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m; |
|
287 }; |
|
288 *} |
|
289 |
|
290 code_reserved Haskell Nat |
|
291 |
|
292 code_type nat |
|
293 (Haskell "Nat") |
|
294 |
|
295 code_instance nat :: eq |
|
296 (Haskell -) |
|
297 |
|
298 text {* |
250 Natural numerals. |
299 Natural numerals. |
251 *} |
300 *} |
252 |
301 |
253 lemma [code inline]: |
302 lemma [code inline, symmetric, code post]: |
254 "nat (number_of i) = number_nat_inst.number_of_nat i" |
303 "nat (number_of i) = number_nat_inst.number_of_nat i" |
255 -- {* this interacts as desired with @{thm nat_number_of_def} *} |
304 -- {* this interacts as desired with @{thm nat_number_of_def} *} |
256 by (simp add: number_nat_inst.number_of_nat) |
305 by (simp add: number_nat_inst.number_of_nat) |
257 |
306 |
258 setup {* |
307 setup {* |
259 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat} |
308 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat} |
260 false false) ["SML", "OCaml", "Haskell"] |
309 true false) ["SML", "OCaml", "Haskell"] |
261 *} |
310 *} |
262 |
311 |
263 text {* |
312 text {* |
264 Since natural numbers are implemented |
313 Since natural numbers are implemented |
265 using integers, the coercion function @{const "of_nat"} of type |
314 using integers in ML, the coercion function @{const "of_nat"} of type |
266 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function. |
315 @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function. |
267 For the @{const "nat"} function for converting an integer to a natural |
316 For the @{const "nat"} function for converting an integer to a natural |
268 number, we give a specific implementation using an ML function that |
317 number, we give a specific implementation using an ML function that |
269 returns its input value, provided that it is non-negative, and otherwise |
318 returns its input value, provided that it is non-negative, and otherwise |
270 returns @{text "0"}. |
319 returns @{text "0"}. |
283 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" |
332 "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)" |
284 by auto |
333 by auto |
285 |
334 |
286 lemma of_nat_int [code unfold]: |
335 lemma of_nat_int [code unfold]: |
287 "of_nat = int" by (simp add: int_def) |
336 "of_nat = int" by (simp add: int_def) |
|
337 declare of_nat_int [symmetric, code post] |
288 |
338 |
289 code_const int |
339 code_const int |
290 (SML "_") |
340 (SML "_") |
291 (OCaml "_") |
341 (OCaml "_") |
292 (Haskell "_") |
|
293 |
|
294 code_const nat |
|
295 (SML "IntInf.max/ (/0,/ _)") |
|
296 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int") |
|
297 (Haskell "max 0") |
|
298 |
342 |
299 consts_code |
343 consts_code |
300 int ("(_)") |
344 int ("(_)") |
301 nat ("\<module>nat") |
345 nat ("\<module>nat") |
302 attach {* |
346 attach {* |
303 fun nat i = if i < 0 then 0 else i; |
347 fun nat i = if i < 0 then 0 else i; |
304 *} |
348 *} |
305 |
349 |
|
350 code_const nat |
|
351 (SML "IntInf.max/ (/0,/ _)") |
|
352 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int") |
|
353 |
|
354 text {* For Haskell, things are slightly different again. *} |
|
355 |
|
356 code_const int and nat |
|
357 (Haskell "toInteger" and "fromInteger") |
306 |
358 |
307 text {* Conversion from and to indices. *} |
359 text {* Conversion from and to indices. *} |
|
360 |
|
361 code_const index_of_nat |
|
362 (SML "IntInf.toInt") |
|
363 (OCaml "Big'_int.int'_of'_big'_int") |
|
364 (Haskell "toEnum") |
308 |
365 |
309 code_const nat_of_index |
366 code_const nat_of_index |
310 (SML "IntInf.fromInt") |
367 (SML "IntInf.fromInt") |
311 (OCaml "Big'_int.big'_int'_of'_int") |
368 (OCaml "Big'_int.big'_int'_of'_int") |
312 (Haskell "toInteger") |
369 (Haskell "fromEnum") |
313 |
|
314 code_const index_of_nat |
|
315 (SML "IntInf.toInt") |
|
316 (OCaml "Big'_int.int'_of'_big'_int") |
|
317 (Haskell "fromInteger") |
|
318 |
|
319 |
370 |
320 text {* Using target language arithmetic operations whenever appropriate *} |
371 text {* Using target language arithmetic operations whenever appropriate *} |
321 |
372 |
322 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" |
373 code_const "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" |
323 (SML "IntInf.+ ((_), (_))") |
374 (SML "IntInf.+ ((_), (_))") |