Philip Feniuk (Jan 06 2025 at 10:57): Philip Feniuk (Jan 06 2025 at 10:57):Hey there,
I'm currently working on my bachelor thesis. One part of this thesis is the comparison of a partially proven algorithm, that is exported through code generation, with other implementations. The programming language of choice is Scala, as there already exists a library containing some of those other implementations. The proof I am referring to can be found here PROOF.
I've never worked with Isabelle before, therefore I naively exported the desired code by adding
export_code TD_Interp_solve in Scala module_name TopDownSolver
At the end.
See:
image.png
This worked out fine. I have copy pasted the generated implementation into a dedicated Scala package.
# Problem
My sbt (scala build tool) environment refuses to compile the code. The reason can be seen in the screenshot below. The case class Char and the abstract sealed class char only differ in one upper- respectively lower-case letter. The proof uses a single string literal at a high level Code.abort, which a could just remove, but this feels wrong.
My current workaround is to just rename one of the classes. This works but is also a rather dirty solution, so I wondered if there is a more elegant solution to this problem? Or did I incorrectly export the desired code?
As for now, thanks for your time and help.
irvin (Jan 06 2025 at 12:43):Could you not use a string literal directly
definition
"a = STR ''test'' "
If you need char i think you'll have to rename but otherwise your case doesnt seem to use char.
object Scratch {
def a : String = "test"
} /* object Scratch */
Nice, this works. Thank you! What would be the reason to use String.implode rather than a direct String literal?
irvin (Jan 06 2025 at 13:10):String.implode is a function. STR ''foo '' is syntax sugar.
Last updated: Feb 28 2025 at 08:24 UTC