[isabelle-dev] Isabelle_10-Sep-2013

[C. Diekmann]

Hi,

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.

  Cornelius