[isabelle] Code generator: overloaded numeric constants



Hi Florian,

I was demoing the code generator here at Galois, and someone wanted to see what kind of Haskell code was generated for overloaded arithmetic. We tried this example:

  theory Int_ex
  imports Main Code_Integer
  begin

  definition
    "foo (x::'a::{number,plus,times}) y = x + 2 * y"

  export_code foo in Haskell
    module_name Int_ex
    file "IntCode"

It was able to generate Haskell code, but the code itself is very strange:

  module Int_ex where {


  class Plus a where {
    plus :: a -> a -> a;
  };

  class Times a where {
    times :: a -> a -> a;
  };

  class Number a where {
    number_of :: Integer -> a;
  };

  foo :: forall a. (Plus a, Times a, Number a) => a -> a -> a;
  foo x y =
plus x (times (number_of (error "Bit0" (error "Bit1" (error "Pls")))) y);

  }

Notice that in the definition of foo uses the "error" function and Isabelle's internal datatype for integers. I had hoped the Haskell definition would instead be:

  foo x y =
    plus x (times (number_of 2) y);

Should I be including a different adaptation theory here?

Thanks,
-john

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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