# [isabelle] Integration of Scala code generated from Isabelle theories

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] Integration of Scala code generated from Isabelle theories
• From: Thomas Genet <Thomas.Genet at irisa.fr>
• Date: Mon, 20 Jun 2011 16:26:06 +0200
• User-agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; fr; rv:1.9.2.17) Gecko/20110414 Thunderbird/3.1.10

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

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 = equal[A](a, b)

} /* 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.eq[A](x, y)) true else member[A](x, yr))
}

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

--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44   E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet

```

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