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.

Thanks.

> @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é
-- 
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






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