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



Hi Peter,

> 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?

I must admit that this problem slipped into Isabelle 2009 accidentally.
For Haskell there is no workaround since lower/upper case distinction is
essential to distinguish between type constructors and type variables.

One workaround could be to redeclare each code theorem with lower case
type variables, in our toy example:

definition test_fun :: "('a \<Rightarrow> 'S) \<Rightarrow> 'a
\<Rightarrow> ('S\<times>'S)"
    where "test_fun f x = (f x, f x)"

declare test_fun_def [where ?'S = 's, standard, code]

but this is not convincing either.

If you really bother substituting all type variables e.g. by means of a
perl one-liner, let me know, and I will provide you with a patch for the
Isabelle 2009 sources.

Hope this helps
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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