*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Questions concerning (Haskell) code generation*From*: René Neumann <lists at necoro.eu>*Date*: Sat, 10 Dec 2011 22:54:10 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:7.0.1) Gecko/20111031 Thunderbird/7.0.1

Hi, I have two questions regarding the Haskell-code generation in Isabelle 2011-1: 1.) It is in someway possible to make the generated code have an explicit export list? So something like export_code bla foo [export] in Haskell module_name Code file - that results in the following module definition module Code (bla, foo) where ...? The reason is, that w/o an explicit export list the compiler assumes that all functions are exported and therefore does not inline them or uses other code optimizations (see [1]). For my test-case this makes indeed a huge difference: without export list: -------------------- benchmarking fully 200 collecting 100 samples, 1 iterations each, in estimated 33.55970 s mean: 337.4847 ms, lb 336.8887 ms, ub 338.2864 ms, ci 0.950 std dev: 3.518088 ms, lb 2.850222 ms, ub 5.044390 ms, ci 0.950 with export list: ----------------- benchmarking fully 200 collecting 100 samples, 1 iterations each, in estimated 30.92251 s mean: 103.9187 us, lb 99.45309 us, ub 119.4683 us, ci 0.950 std dev: 37.75363 us, lb 11.42921 us, ub 84.93836 us, ci 0.950 Note the difference of 300ms vs. 0.1ms. 2.) I noted that when using "Efficient_Nat", I got two new types for natural numbers in code: Natural and Nat. The code of both looks nearly identical (see attached files) and also only one of them (Nat) is used throughout the rest of the code. Is there a deeper reason behind having them both? Or is it the result of some refactoring and forgetting to remove the old version? Thanks :) René

{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} module Nat where { newtype Nat = Nat Integer deriving (Eq, Show, Read); instance Num Nat where { fromInteger k = Nat (if k >= 0 then k else 0); Nat n + Nat m = Nat (n + m); Nat n - Nat m = fromInteger (n - m); Nat n * Nat m = Nat (n * m); abs n = n; signum _ = 1; negate n = error "negate Nat"; }; instance Ord Nat where { Nat n <= Nat m = n <= m; Nat n < Nat m = n < m; }; instance Real Nat where { toRational (Nat n) = toRational n; }; instance Enum Nat where { toEnum k = fromInteger (toEnum k); fromEnum (Nat n) = fromEnum n; }; instance Integral Nat where { toInteger (Nat n) = n; divMod n m = quotRem n m; quotRem (Nat n) (Nat m) | (m == 0) = (0, Nat n) | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m; }; }

{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-} module Natural where { import Data.Array.ST; newtype Natural = Natural Integer deriving (Eq, Show, Read); instance Num Natural where { fromInteger k = Natural (if k >= 0 then k else 0); Natural n + Natural m = Natural (n + m); Natural n - Natural m = fromInteger (n - m); Natural n * Natural m = Natural (n * m); abs n = n; signum _ = 1; negate n = error "negate Natural"; }; instance Ord Natural where { Natural n <= Natural m = n <= m; Natural n < Natural m = n < m; }; instance Ix Natural where { range (Natural n, Natural m) = map Natural (range (n, m)); index (Natural n, Natural m) (Natural q) = index (n, m) q; inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q; rangeSize (Natural n, Natural m) = rangeSize (n, m); }; instance Real Natural where { toRational (Natural n) = toRational n; }; instance Enum Natural where { toEnum k = fromInteger (toEnum k); fromEnum (Natural n) = fromEnum n; }; instance Integral Natural where { toInteger (Natural n) = n; divMod n m = quotRem n m; quotRem (Natural n) (Natural m) | (m == 0) = (0, Natural n) | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m; }; }

**Follow-Ups**:**Re: [isabelle] Questions concerning (Haskell) code generation***From:*Florian Haftmann

- Previous by Date: [isabelle] CfP: Only one week left for submitting abstracts to TAP 2012 (International Conference on Test and Proofs
- Next by Date: [isabelle] Elbe 1.41 Update
- Previous by Thread: [isabelle] CfP: Only one week left for submitting abstracts to TAP 2012 (International Conference on Test and Proofs
- Next by Thread: Re: [isabelle] Questions concerning (Haskell) code generation
- Cl-isabelle-users December 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list