[isabelle] Questions concerning (Haskell) code generation



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;
};

}


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.