[isabelle-dev] Isabelle_10-Sep-2013

C. Diekmann diekmann at in.tum.de
Thu Sep 12 15:28:30 CEST 2013


thanks Florian and Makarius for your help.

>> * Discontinued theories Code_Integer and Efficient_Nat by a more
>> fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
>> Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
>> generation for details.  INCOMPATIBILITY.

Finally, I tested the Scala code generation with my existing Scala
application. The biggest change is the Code_Target_Nat. It causes
minor changes to the code. Overall, few changes had to be made to
replace the generated Scala code of Isabelle2013 with
Isabelle_10-Sep-2013. However, there is one incompatibility I cannot
fix easily.
The generated code contains the following definition:

  final case class Nata(a: BigInt) extends nat

In the old version, when printing for example the natural number 42, I
got "42". Now I get "Nata(42)". I don't see an easy way to fix this
without touching the generated code (except modifying my code
everywhere where a nat is printed which induces a lot of code smell).
The following change to the generated code is, as far as I can see,
the best solution:

  final case class Nata(a: BigInt) extends nat {override def toString
= a.toString}

Maybe this could be added to the generated code? I know that this
simple suggestion might be very hard to implement in the code
generator but it would really really help to increase the usability of
the generated code.


More information about the isabelle-dev mailing list