Email Gateway (Aug 18 2022 at 14:08): Email Gateway (Aug 18 2022 at 14:08):From: Peter Lammich <peter.lammich@uni-muenster.de>
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.
Last updated: Apr 24 2024 at 08:20 UTC