[isabelle] Problem with Scala code generation



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é




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