Email Gateway (Aug 18 2022 at 17:09): Email Gateway (Aug 18 2022 at 17:09):From: Lukas Bulwahn <bulwahn@in.tum.de>
On 02/01/2011 03:23 PM, Christian Sternagel wrote:
I tried almost the same example and found that the reason for the
error is that a definitiondef myfun: Boolean = {
(_: Boolean) => true;
true
}is parsed as
def myfun: Boolean = {
(_: Boolean) => { true; true };
}by the scala compiler. I'm not sure whether this is intended from the
Scala side. However, a (hopefully) easy workaround in the Isabelle
setup is to provide additional parentheses around function literals.
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.
This changeset can possibly also be applied to the release version
Isabelle2011, for those which require it for Scala code generation.
@Rene: I hope we can also identify and fix the other quirks with the
Scala code generation; just provide us some further pointers.
Thank you all for the help identifying the problem.
Lukas
cheers
chris
On 02/01/2011 03:12 PM, bnord wrote:
Am 01.02.2011 14:46, schrieb René Thiemann:
we have not yet simplified and localized the exact problem
The problem seems to be that the code generator doesn't generate the
necessary "val ... = " parts for values that are not used anywhere and
the resulting anonymous function isn't a valid statement on it's own.A simpler example might be:
theory Test
imports Main
begindefinition myfun :: "bool"
where "myfun \<equiv> let x = \<lambda> l::bool. True
in True"export_code myfun in Scala file "Test.scala"
endwhich produces:
object Test {
def myfun: Boolean = {
(_: Boolean) => true;
true
}} /* object Test */
Thank
Email Gateway (Aug 18 2022 at 17:11):From: René Thiemann <rene.thiemann@uibk.ac.at>
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 elemA: 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é
Email Gateway (Aug 18 2022 at 17:11):From: Lukas Bulwahn <bulwahn@in.tum.de>
On 02/03/2011 08:07 AM, René Thiemann wrote:
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] {
valProblem.elem: A
}
def elemA: A = A.Problem.elemtrait 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]This can be only fixed by someone, who understands how type classes were
thought to be modelled as implicits, i.e., our code generation guru Florian.
Florian's thoughts have been partly recorded on
http://www.scala-lang.org/node/6698, but he can probably say more about
this "diamond problem".
Lukas
René
Email Gateway (Aug 18 2022 at 17:12):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Test.scala
Test.thy
Email Gateway (Aug 18 2022 at 17:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
for a substantial solution I have to ask on the scala mailing list, this
will take some time.
Luckily there is a workaround for that: provide an explicit union of
both classes s.t. the resulting constraint only mentions one class:
class class3 = class1 + class2
lemma [code]:
"(f :: 'a::class3) = elem"
by (simp add: f_def)
Then it works fine.
Note that the preprocessor propagates sort constraints through systems
of code equations, so it might be enough to provide a more specialized
code lemma for exactly one operation.
Hope this helps in the first place,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Btw. the relevant paper for implementing type classes by implicits is
http://infoscience.epfl.ch/record/150280
Florian
signature.asc
Email Gateway (Aug 18 2022 at 17:13):From: bnord <bnord01@googlemail.com>
The problem seems to be that the code generator doesn't generate the
necessary "val ... = " parts for values that are not used anywhere and
the resulting anonymous function isn't a valid statement on it's own.
A simpler example might be:
theory Test
imports Main
begin
definition myfun :: "bool"
where "myfun \<equiv> let x = \<lambda> l::bool. True
in True"
export_code myfun in Scala file "Test.scala"
end
which produces:
object Test {
def myfun: Boolean = {
(_: Boolean) => true;
true
}
} /* object Test */
Email Gateway (Aug 18 2022 at 17:14):From: Lars Hupel <hupel@in.tum.de>
The problem there is actually precedence. The following version works as
expected, and the Scala compiler should be able to remove that piece of
dead code.
object Test {
def myfun: Boolean = {
{(_: Boolean) => true;}
true
}
} /* object Test */
smime.p7s
Email Gateway (Aug 18 2022 at 17:17):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I tried almost the same example and found that the reason for the error
is that a definition
def myfun: Boolean = {
(_: Boolean) => true;
true
}
is parsed as
def myfun: Boolean = {
(_: Boolean) => { true; true };
}
by the scala compiler. I'm not sure whether this is intended from the
Scala side. However, a (hopefully) easy workaround in the Isabelle setup
is to provide additional parentheses around function literals.
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC