[isabelle] Haskell code generator problem, upper-case type variables



Hi all,

I have a problem with the Haskell code generator. It generates
upper-case type variables, that are not accepted by ghci 6.4.10.
Is this problem known? Is there any workaround (ghci configuration?)
other than working through all theories and only using lowe-case
type-variables, which I definitely do not want?

Regards, Peter
Below follows an example:

Consider the following dummy definition:
-------------
theory Scratch
imports Main Efficient_Nat
begin
  definition test_fun :: "('a \<Rightarrow> 'S) \<Rightarrow> 'a
\<Rightarrow> ('S\<times>'S)"
    where "test_fun f x = (f x, f x)"

  export_code test_fun in Haskell file "~/devel/isabelle/generated_hs/"

-------------

The generated file, Scratch.hs looks like this:

{-# OPTIONS_GHC -fglasgow-exts #-}

module Scratch where {

import qualified Nat;

test_fun :: forall a S. (a -> S) -> a -> (S, S);
test_fun f x = (f x, f x);

}

------------------

However, ghci as of version 6.10.4 seems not to accept the upper-case
type variable in the functions signature: (With a lower-case s,
everything works fine)

GHCi, version 6.10.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
Prelude> :load Scratch.hs
[1 of 2] Compiling Nat              ( Nat.hs, interpreted )
[2 of 2] Compiling Scratch          ( Scratch.hs, interpreted )

Scratch.hs:7:21: parse error on input `S'
Failed, modules loaded: Nat.










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