Re: [isabelle] Scala generator



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 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.


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
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 */


Thank






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