handles extraction of finite sets

src/funcheck/CodeExtraction.scala

@@ -342,7 +342,10 @@ trait CodeExtraction extends Extractors {
       case ExGreaterEqThan(l, r) => GreaterEquals(rec(l), rec(r)).setType(BooleanType)
       case ExLessThan(l, r) => LessThan(rec(l), rec(r)).setType(BooleanType)
       case ExLessEqThan(l, r) => LessEquals(rec(l), rec(r)).setType(BooleanType)
-
+      case ExFiniteSet(tt, args) => {
+        val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+          FiniteSet(args.map(rec(_))).setType(SetType(underlying))
+      }
       case ExEmptySet(tt) => {
         val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
         EmptySet(underlying).setType(SetType(underlying))          

src/funcheck/Extractors.scala

@@ -305,6 +305,23 @@ trait Extractors {
       }
     }
 
+    object ExFiniteSet {
+      def unapply(tree: Apply): Option[(Tree,List[Tree])] = tree match {
+        case Apply(
+          TypeApply(
+            Select(
+              Select(
+                Select(
+                  Select(Ident(s), collectionName),
+                  immutableName),
+                setName),
+              emptyName),  theTypeTree :: Nil), args) if (
+              collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && emptyName.toString == "apply"
+            )=> Some(theTypeTree, args)
+        case _ => None
+      }
+    }
+
     object ExUnion {
       def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
         case Apply(Select(lhs, n), List(rhs)) if (n == nme.PLUSPLUS) => Some((lhs,rhs))

src/purescala/PrettyPrinter.scala

@@ -99,6 +99,7 @@ object PrettyPrinter {
     case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
     case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl)      // \leq
     case GreaterEquals(l,r) => ppBinary(sb, l, r, " \u2265 ", lvl)   // \geq
+    case FiniteSet(rs) => ppNary(sb.append("{ "), rs, ", ", lvl).append(" }")
     case EmptySet(_) => sb.append("\u2205")                          // Ø
     case SetUnion(l,r) => ppBinary(sb, l, r, " \u222A ", lvl)        // \cup
     case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)       

testcases/BinarySearchTree.scala

@@ -7,12 +7,12 @@ object BinarySearchTree {
 
     def emptySet() : Tree = Leaf()
 
-    def insert(tree: Tree, value: Int) : Tree = (tree match {
+    def insert(tree: Tree, value: Int) : Node = (tree match {
         case Leaf() => Node(Leaf(), value, Leaf())
         case n @ Node(_, v, _) if v == value => n
         case Node(l, v, r) if v < value => Node(l, v, insert(r, value))
         case Node(l, v, r) if v > value => Node(insert(l, value), v, r)
-    }) ensuring(_ != Leaf())
+    }) ensuring(result => contents(result) != Set.empty[Int])
 
     def contains(tree: Tree, value: Int) : Boolean = tree match {
         case Leaf() => false
@@ -23,7 +23,7 @@ object BinarySearchTree {
 
     def contents(tree: Tree) : Set[Int] = tree match {
         case Leaf() => Set.empty[Int]
-        case Node(l, v, r) => contents(l) /*++ Set(v)*/ ++ contents(r)
+        case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
     }
 }