Re: [isabelle] Scala generator

> We have improved the Scala code generation to add parentheses around function literals as suggested,
> and provide a fix as changeset 3450e57264b3 in the development version.


> @Rene: I hope we can also identify and fix the other quirks with the Scala code generation; just provide us some further pointers.

Here is another one.

class class0 = fixes elem :: 'a
class class1 = class0
class class2 = class0
definition f :: "'a :: {class1, class2}" where "f \<equiv> elem"
export_code f in Scala file "Problem.scala"

Then the file Problem.scala is created:

object Problem {

trait class0[A] {
  val `Problem.elem`: A
def elem[A](implicit A: class0[A]): A = A.`Problem.elem`

trait class1[A] extends class0[A] {

trait class2[A] extends class0[A] {

def f[A: class1: class2]: A = elem[A] /* line 14 */

} /* object Problem */

which does not compile:
Problem.scala:14: error: ambiguous implicit values:
 both value evidence$1 of type Problem.class1[A]
 and value evidence$2 of type Problem.class2[A]
 match expected type Problem.class0[A]
def f[A: class1: class2]: A = elem[A]

René Thiemann                    mailto:rene.thiemann at
Computational Logic Group
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

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