[isabelle-dev] Isabelle_10-Sep-2013

[C. Diekmann]

Hi Florian,


> I am not sure whether I get your intention right, but I guess you want
> to print natural numbers from generated Scala code.

Yes, I have hand-written code and generated code. The generated code
is wrapped, let's say in class Wrapper. I export many generated tuples
of functions that are all wrapped (by hand) in the same generic
Wrapper. In my hand-written code, I call Wrapper's toString often,
which might end up in printing generated datatypes. I give you a
sketch of my generic prettyprinter (which already features an
Isabelle2013 workaround) and Wrapper.

//hand-written
protected class Wrapper[A](generated_code: tuple_of_generated_functions[A])
  with PrettyPrinter[A]
{
  def a: A = generated_code.function_a
  def b: A = generated_code.function_b
}

//hand-written
protected trait PrettyPrinter[A]
{
    this: Wrapper[A] =>

    final def myToString: String = {
      val value: A = a
      val str: String = value.toString
      // fix introduced by Isabelle2013
      // case objects are now case classes
      // instead of printing "Unassigned()", let's print "Unassigned"
      if (str.endsWith("()"))
        str.dropRight("()".length)
      else
        str
   }

}

//hand-written
//using generated Isabelle code:
new Wrapper[String](GENERATED_CODE.the_generated_tuple_with_the_functions1)
new Wrapper[Nat](GENERATED_CODE.the_generated_tuple_with_the_functions2)

//generated by Isabelle
val a = GENERATED_CODE.the_generated_tuple_with_the_functions1[String]
= (function_a, function_b)
val b = GENERATED_CODE.the_generated_tuple_with_the_functions2[Nat] =
(function_a, function_b)
....
println(a.myToString) // works
println(b.myToString) // gives "Nata(X)"

> Two possible hints:
>
> a) There is a conversion from Isabelle nat to Scala builtin BigInt which
> maybe is useful.
>
> b) Also you could add an implicit conversion Nat > String to your Scala
> code without a need to patch the generated code.

I guess both solutions are not satisfying. I tried the following hack
in the PrettyPrinter

val str = if (value.isInstanceOf[Nat.nat])
                  integer_of_nat(value.asInstanceOf[Nat.nat]).toString
              else
                  value.toString

However, if the nat is nested somewhere, this also fails. For example,
my following test case fails:
"Subnet(Nata(1))" did not equal "Subnet(1)"

The best and object oriented correct way would be to add the
  final case class Nata(a: BigInt) extends nat {override def toString
= a.toString}
directly to Nata, where it is defined.

Any suggestions?

Also, I hope presenting my generic wrapper facade for generated code
helps a bit. It servers well for 6k lines of hand-written Scala and
2.5k lines of generated Scala.

  Cornelius