[isabelle] Haskabelle configuration



Dear Haskabelle developers,

I am trying to import some Haskell code using Haskabelle for Isabelle2011-1. So far, I ran into the following two problems:

1. Bound variable names clash with previous constant names.
For example, in the following Haskell program

f = \x -> x
g = f
h f = (f, g)

f is bound in h's definition, but also defined previously.

Haskabelle generates the following definitions in Isabelle:

definition f where "f = (% x . x)"
definition g where "g = f"
fun h where "h f = (f, g)"

Obviously, this is not what I want, because h's definition now "pattern-matches" on the constant f, but it should actually be as follows:

fun h where "!!f. h f = (f, g)"

The same problem also occurs with predefined constants from the Isabelle library. I suggest that Haskabelle explicitly adds the universal quantification to all bound variables that occur on the left-hand equation of a function definition such that it need not know which names are used.

Is there some other way than manually renaming all such variables in the Haskell code? This is something I actually want to avoid.


2. do notation
Apparently, Haskabelle has some undocumented support for do notation and monads. At least, this is what I gather from the files in ex/ and the error message for the following program:

f = do {
  x <- [1,2];
  y <- [x + 1];
  [y]
}

haskabelle_bin: Do syntax is used without sufficient type information!

What type information do I have to add (and where) such that such examples compile? Actually, I would have expected that no type information were necessary, because Isabelle's parser setup for do notation in Library/Monad_Syntax should resolve the operations correctly.
Can I configure Haskabelle to use that setup?

Thanks for any help,
Andreas


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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