leon.collection set operations

library/collection/package.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+import leon.annotation._
+import leon.collection.List
+import leon.lang.synthesis.choose
+
+package object collection {
+
+  @library
+  def setToList[A](set: Set[A]): List[A] = choose { 
+    (x: List[A]) => x.content == set
+  }
+
+  @library
+  def setForall[A](set: Set[A], p: A => Boolean): Boolean = 
+    setToList(set).forall(p)
+
+  @library
+  def setExists[A](set: Set[A], p: A => Boolean): Boolean =
+    setToList(set).exists(p)
+
+}

src/main/scala/leon/codegen/CodeGeneration.scala

@@ -396,6 +396,59 @@ trait CodeGeneration {
           case _ =>
         }
         
+      case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
+
+        val ObjectClass = "java/lang/Object"
+        val IteratorClass = "java/util/Iterator"
+        val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
+        val cons = program.library.Cons.get
+        val (consName, ccApplySig) = leonClassToJVMInfo(cons).getOrElse {
+          throw CompilationException("Unknown class : " + cons)
+        }
+        
+        mkExpr(nil, ch)
+        mkExpr(set, ch)
+        //if (params.requireMonitor) {
+        //  ch << ALoad(locals.monitorIndex)
+        //}
+
+        // No dynamic dispatching/overriding in Leon, 
+        // so no need to take care of own vs. "super" methods
+        ch << InvokeVirtual(SetClass, "getElements", s"()L$IteratorClass;")
+        
+        val loop = ch.getFreshLabel("loop")
+        val out = ch.getFreshLabel("out")
+        ch << Label(loop)
+        // list, it
+        ch << DUP
+        // list, it, it
+        ch << InvokeInterface(IteratorClass, "hasNext", "()Z")
+        // list, it, hasNext
+        ch << IfEq(out)
+        // list, it
+        ch << DUP2
+        // list, it, list, it
+        ch << InvokeInterface(IteratorClass, "next", s"()L$ObjectClass;") << SWAP
+        // list, it, elem, list
+        ch << New(consName) << DUP << DUP2_X2
+        // list, it, cons, cons, elem, list, cons, cons
+        ch << POP << POP
+        // list, it, cons, cons, elem, list
+        
+        if (params.requireMonitor) {
+          ch << ALoad(locals.monitorIndex) << DUP_X2 << POP
+        }
+        ch << InvokeSpecial(consName, constructorName, ccApplySig)
+        // list, it, newList
+        ch << DUP_X2 << POP << SWAP << POP
+        // newList, it
+        ch << Goto(loop)
+        
+        ch << Label(out)
+        // list, it
+        ch << POP
+        // list
+      
       // Static lazy fields/ functions
       case FunctionInvocation(tfd, as) =>
         val (cn, mn, ms) = leonFunDefToJVMInfo(tfd.fd).getOrElse {

src/main/scala/leon/datagen/VanuatooDataGen.scala

@@ -66,6 +66,15 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
         cs
       })
 
+    case st @ SetType(sub) =>
+      constructors.getOrElse(st, {
+        val cs = for (size <- List(0, 1, 2, 5)) yield {
+          Constructor[Expr, TypeTree]((1 to size).map(i => sub).toList, st, s => FiniteSet(s.toSet).setType(st), st.toString+"@"+size)
+        }
+        constructors += st -> cs
+        cs
+      })
+    
     case tt @ TupleType(parts) =>
       constructors.getOrElse(tt, {
         val cs = List(Constructor[Expr, TypeTree](parts, tt, s => Tuple(s), tt.toString))

src/main/scala/leon/evaluators/RecursiveEvaluator.scala

@@ -130,6 +130,16 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         case _ => throw EvalError(typeErrorMsg(first, BooleanType))
       }
 
+    case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
+      val els = e(set) match {
+        case FiniteSet(els) => els
+        case _ => throw EvalError(typeErrorMsg(set, SetType(tp)))
+      }
+      val cons = program.library.Cons.get
+      val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
+      def mkCons(h: Expr, t: Expr) = CaseClass(CaseClassType(cons, Seq(tp)), Seq(h,t))
+      els.foldRight(nil)(mkCons)
+      
     case FunctionInvocation(tfd, args) =>
       if (gctx.stepsLeft < 0) {
         throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")

src/main/scala/leon/frontends/scalac/CodeExtraction.scala

@@ -1607,7 +1607,6 @@ trait CodeExtraction extends ASTExtractors {
             case (IsTyped(a1, SetType(b1)), "contains", List(a2)) =>
               ElementOfSet(a2, a1)
 
-
             // Multiset methods
             case (IsTyped(a1, MultisetType(b1)), "++", List(IsTyped(a2, MultisetType(b2))))  if b1 == b2 =>
               MultisetUnion(a1, a2)

src/main/scala/leon/utils/Library.scala

@@ -12,6 +12,8 @@ case class Library(pgm: Program) {
   lazy val Nil  = lookup("leon.collection.Nil") collect { case ccd : CaseClassDef => ccd }
 
   lazy val String = lookup("leon.lang.string.String") collect { case ccd : CaseClassDef => ccd }
+
+  lazy val setToList = lookup("leon.collection.setToList") collect { case fd : FunDef => fd }
   
   def lookup(name: String): Option[Definition] = {
     searchByFullName(name, pgm)

src/test/scala/leon/test/codegen/CodeGenTests.scala

@@ -420,7 +420,20 @@ class CodeGenTests extends test.LeonTestSuite {
         def test =  sum(l)
       }""",
       IntLiteral(1 + 2 + 3)
+    ),
+    
+    TestCase("SetToList", """
+      import leon.collection._
+      object SetToList {
+        def test = {
+          val s = Set(1, 2, 3, 4, 5)
+          val s2 = setToList(s).content
+          s == s2
+        }
+      }""",
+      BooleanLiteral(true)
     )
+    
   )