Re: [isabelle] Scala generator



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

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







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