Email Gateway (Aug 18 2022 at 19:16): Email Gateway (Aug 18 2022 at 19:16):From: René Thiemann <Rene.Thiemann@uibk.ac.at>
Dear all,
I recently tried to use the Scala code generator again, and stumbled over the following two problems:
1) There are too few brackets:
definition problem
where "problem b opt \<equiv> b \<or> (case opt of
None \<Rightarrow> True | Some _ \<Rightarrow> False)"
export_code problem in Scala module_name Problem file "Problem.scala"
yields
object Problem {
def problem[A](b: Boolean, opt: Option[A]): Boolean =
b || opt match {
case None => true
case Some(_) => false
}
} /* object Problem */
which does not compile, since it must be
def problem[A](b: Boolean, opt: Option[A]): Boolean =
b || (opt match {
case None => true
case Some(_) => false
})
} /* object Problem */
I believe that this is easy to fix in the formatter.
2) If I try to extract full IsaFoR, then an additional error occurs:
Ceta.scala:4887: error: Implementation restriction: case classes cannot have more than 22 parameters.
Googling a bit on this problem showed that the problem cannot be solved easily on the Scala-side:
"As a subclass of Product, case classes can't have more than 22 parameters
No real workaround, except to stop abusing classes with this many params :)"
So, is there a solution on the code-generator side, or do I have to adapt my theories?
Best regards,
René
Email Gateway (Aug 18 2022 at 19:16):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
congratulations, you have found a bug! To circumvent it, wait for the
next Isabelle release or help yourself with something like
code_const HOL.conj and HOL.disj
(Scala "!(_ && _)" and "!(_ || _)")
Similar adjustion could be necessary for other infix operators. See the
Tutorial On Code Generation for details.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 19:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,
Wow! How does your logic specification and your Scala code look like?
Maybe something can be done by tweaking the specification…
Florian
signature.asc
Email Gateway (Aug 18 2022 at 19:17):From: René Thiemann <rene.thiemann@uibk.ac.at>
Thanks,
René
Last updated: Apr 24 2024 at 20:16 UTC