lf-scala should account for case-insensitive name clashes in MMT theories

[ComFreek]

Currently in LATIN2 we have a theory Nat containing two constant declarations named Nat and nat. This will produce something along the lines of

object Nat extends TheoryScala {
  object nat extends ConstantScala { /* ... */ }
  object Nat extends ConstantScala { /* ... */ }
}

which is a problem on case-insensitive filenames.

[tkw1536]

I thought we were escaping filenames already with "$" in front of capital letters. Right @florian-rabe ?

[ComFreek]

We do, however, this is not about our filenames. This is about the Scala object/class names being equivalent modulo case and hence the Scala-generated filenames.

[florian-rabe]

Escapes in the generated Scala code would be annoying.

For theories, the issue basically never comes up. But the exporter generates a nested object per constant, constants often have names that only differ in capitalization, and I believe Scala generates class files for those nested objects.

Would the problem go away if we replace

object nat ...

with

val nat = new {...}

?

[ComFreek]

@florian-rabe Yes, indeed val fixes it:

val nat: ConstantScala = new ConstantScala {
  /* ... */
}

val Nat: ConstantScala = new ConstantScala {
  /* ... */
}