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

[Tobias Nipkow]

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.

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

Tobias

> Florian Haftmann can say if he feels like supporting this deviation from hard
> and fast Isabelle conventions about Isabelle theories names: capitalized words
> (usually in singular) that are separated by underscore. Moreover locale / class
> names are in lower case, like most material within a theory body.
> 
> I occasioanlly see users making theory names lower case and locale names
> capitalized, probably in imitation of Java packages and classes.  Bad
> consequences will come from that, as can be seen here.
> 
> The Prover IDE should probably point to such confusions via some funny
> highlighting, but it is just one more feature to be taken care of, and there are
> more pressing things to do.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev