Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Integration of Scala code generated from Isabe...

Email Gateway (Aug 18 2022 at 17:47):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Isabelle users,

I am trying to use some Scala code generated from an Isabelle theory and
having a problem.
This is a newbie problems (I guess) but, unfortunately, I am a newbie in
Isabelle and Scala!

Since I use the "=" on polymorphic type 'a, the scala generated classes
have to have the HOL.equal trait. I did this using implicit conversion
function. However, I get the same error message with explicit conversions.

Any help is welcome...

Thanks in advance,

Thomas

-------- Here is the Isabelle Theory---------
theory testScala
imports Main
begin

fun member:: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
where
"member x []=False" |
"member x (y#yr) = (if x=y then True else (member x yr))"

export_code member
in Scala
end

-------- Here is the scala generated code----------
object HOL {

trait equal[A] {
val HOL.equal: (A, A) => Boolean
}
def equal[A](a: A, b: A)(implicit A: equal[A]): Boolean =
A.HOL.equal(a, b)

def eq[A: equal](a: A, b: A): Boolean = equalA

} /* object HOL */

object testScala {

def member[A: HOL.equal](x: A, xa1: List[A]): Boolean = (x, xa1) match {
case (x, Nil) => false
case (x, y :: yr) => (if (HOL.eqA) true else memberA)
}

} /* object testScala */

-------- Here is the code trying to call the "member" function-----

object Main {
implicit def wrapString(s:String):StringWrapper = new StringWrapper(s)
implicit def wrapList(l: List[(String,String)]):
List[(StringWrapper,String)]={
l match {
case Nil => Nil
case (x,y) :: xs => ((new StringWrapper(x)),y)::(wrapList(xs))
}
}

class StringWrapper(val s : String) extends HOL.equal[StringWrapper]{
def HOL.equal(s1:StringWrapper, s2:StringWrapper):Boolean = s1==s2
}

val l: List[String]= "John"::"Paul"::"George"::"Ringo"::Nil
val b= testScala.member("John",l)
}

-------- Here is the error message ---------

error: could not find implicit value for evidence parameter of type
member.HOL.equal[String]
val b= testScala.member("John",l)

Email Gateway (Aug 18 2022 at 17:47):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Thomas,

those implicit values must be values (val, def), not classes.

To get an idea how they should look, I recommend to have a look at
generated Scala code which contains implicit value definitions for class
instances, e.g.

definition "foo = distinct [0, Suc 0]"

export_code foo in Scala

As I rule of thumb, I further recommend to avoid plumbing generated and
non-generated code as far as possible and doing as much as possible
within HOL. Note that it is possible to generate Scala strings using
type String.literal with constructor STR:

definition "foo = STR ''foo''"

export_code foo in Scala

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 17:48):

From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear all Isabelle users,

If I understand well the generated code, to match my problem, I should
simply write:

object Main {
implicit def equal_nat: HOL.equal[String] = new HOL.equal[String] {
val HOL.equal = (a: String, b: String) => a==b
}

def main(args: Array[String]): Unit = {
val l: List[String]= "John"::"Paul"::"George"::"Ringo"::Nil
val b= testScala.member("John",l)
}

Instead of all the horrible implicit conversion of classes I wrote first :-)
This solution seems to be OK.
Thanks a lot Florian,

Thomas

Last updated: Apr 23 2024 at 20:15 UTC