[isabelle] Scala codegen error: need NatO, natT, and NatC


There are Scala identifier naming differences between when 'module_name' is used (the problem), and when 'module_name' isn't used (which works). I get a valid warning that classes 'nat' and 'Nat' differ only in case. It tells me:

/warning: Class test_mod$Nat differs only in case from test_mod$nat. Such classes will overwrite one another on case-insensitive filesystems./

I'll include the theory below, but before that, I turn this into a feature request, described by the subject line.

What works when I specify no module name is this:

object Nat {
abstract sealed class nat
final case class Nata(a: BigInt) extends nat

What doesn't work, when 'module_name' is used is this:

object test_mod {
abstract sealed class nat
final case class Nat(a: BigInt) extends nat

That the name 'Nata' works is good, but my proposed naming scheme would use a name that would be more meaningful to me.

Putting everything in one object is convenient for easy importing, but I can see a use for not specifying a module, which would be that Scala objects would be organized like the HOL logic is.

It would be nice, to have the same names so I can go back and forth without renaming. My proposal is as above, with 'nat' as an example:

NatO, for the nat object,

natT, for the top level nat class, and

NatC, for the nat constructor/class

The theory is below.



theory test_export_code
imports Complex_Main "~~/src/HOL/Library/Code_Target_Nat"

fun nat_natlist_op :: "nat => nat list => nat list" where
  "nat_natlist_op m []       = []"
 |"nat_natlist_op m (n # nl) = (m + n) # nat_natlist_op m nl"

value "nat_natlist_op 3 [2,3,4]"

export_code nat_natlist_op in Scala file "src/test_no_mod.scala"

export_code nat_natlist_op
  in Scala module_name test_mod file "src/test_mod.scala"


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