[isabelle] Integration of Scala code generated from Isabelle theories




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