Email Gateway (Aug 19 2022 at 16:51): Email Gateway (Aug 19 2022 at 16:51):From: Gottfried Barrow <igbi@gmx.com>
Hi,
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.
Thanks,
GB
(***************)
theory test_export_code
imports Complex_Main "~~/src/HOL/Library/Code_Target_Nat"
begin
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"
end
Email Gateway (Aug 19 2022 at 16:51):From: Gottfried Barrow <igbi@gmx.com>
Naming schemes take a lot of brainstorming. I guess the real conflict is
between 'nat' as a class/type, and 'Nat' as a class/constructor. Here's
my new vote for this example:
Nat for object,
natT or natD for class/type, and
Nat for class/constructor.
I think that constructors are used more than type annotation.
Regards,
GB
Email Gateway (Aug 19 2022 at 16:53):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gottfried,
using »code_identifier«, you can explicitly control the naming of
identifiers in generated code. The syntax is described in the Isar
reference manual and the theories in src/HOL contain various examples.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:53):From: Gottfried Barrow <igbi@gmx.com>
Florian,
Thanks. I'll use that someday, but all this led to several additional
things. I hadn't considered the 'Eval' export_code option. The first
section of codegen.pdf speaks of the four languages, so I missed that
'Eval' was an option. I saw 'Eval' the other day in the Isar reference
manual, and now I've used it. It's more in line with what I've recently
been focusing, which is a high-powered 'value'.
Reading your section 6 in codegen.pdf led me to your Parallel.thy. I
experimented with 'Parallel.fork' and 'Parallel.join'. All that looks
like it should be useful. I got a particular function, for a particular
value, down from 4.5s to about 1s, by forking on the values of a list.
Doing that with a 'fun' in a THY is good.
Thanks,
GB
Last updated: May 07 2024 at 01:07 UTC