[isabelle] Scala generator



Dear all,

after updating our theories to Isabelle 2011 we wanted to try out the Scala code generator, but unfortunately we have some problems since the generated code does not compile (it complies for other languages like Haskell and OCaml).

A simplified example is attached (theory file and generated scala file), and scala 2.8 complains as follows:

Test.scala:25: error: type mismatch;
found   : (List[(A, Nat.nat)]) => Boolean
required: Boolean
   (a: List[(A, Nat.nat)]) =>
                           ^
one error found


In the full generated code (20000 lines of Scala), we also detected other compilation problems

Ceta.scala:13427: error: ambiguous implicit values:
both method poly_carrier_rat in object Ceta of type => Ceta.poly_carrier[Ceta.rat] and method max_ordered_monoid_add_rat in object Ceta of type => Ceta.max_ordered_monoid_add[Ceta.rat]
match expected type Ceta.non_strict_order[Ceta.rat]
  (mat_ge[rat],

but we have not yet simplified and localized the exact problem.


Any help is appreciated,
René
--
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

Attachment: Test.scala
Description: Binary data

Attachment: Test.thy
Description: Binary data



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