Re: [isabelle] Problem with Scala code generation



Hi René,

> 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 */

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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