[isabelle-dev] Code export to Haskell and lower-case theory names

[Makarius]

On Fri, 29 Mar 2013, Tobias Nipkow wrote:

> Am 29/03/2013 11:24, schrieb Makarius:
>> On Thu, 28 Mar 2013, Manuel Eberl wrote:
>>
>>> I just noticed that when exporting code to Haskell, there is a complication
>>> when some of the theories involved have lower-case names. The code export
>>> itself will work with no error or warning, but when ghc/ghci are invoked on
>>> the generated code, they will report the lower-case module name of the module
>>> that corresponds to the theory as a parse error, as Haskell apparently does
>>> not allow lower-case module names.
>>>
>>> Is this a known issue, or even intended behaviour? I think the code export
>>> tool should automatically rename this to an upper case version, similarly to
>>> what it does with name clashes and Unicode tokens in identifiers, or at least
>>> abort with an error message.
>
> Manuel is absolutely right. If you translate into a language with certain rules
> you have to obey those rules. Which the translator into Haskell mostly does:
> types are capitalized (despite the fact that they are typically lower case in
> Isabelle, nothing bad comes of it), function names are lowered where needed,
> type variables are called a, not 'a, etc. But theory/module names are not
> capitalized. An omission.

So that's something to be refined by Florian Haftmann.


> This has got nothing to do with Isabelle's informal conventions but is 
> all about the target language's formal rules.

The conventions about theory names and locale/class names are not that 
informal.  If you violate them systematically, certain name space policies 
will break down.  That is then a "general user error".


 	Makarius