support for some set operations.

src/funcheck/CodeExtraction.scala

@@ -307,8 +307,8 @@ trait CodeExtraction extends Extractors {
     }
 
     def rec(tr: Tree): Expr = tr match {
-      case ExInt32Literal(v) => IntLiteral(v)
-      case ExBooleanLiteral(v) => BooleanLiteral(v)
+      case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
+      case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
       case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
         case Some(fun) => fun()
         case None => {
@@ -337,10 +337,31 @@ trait CodeExtraction extends Extractors {
       case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
       case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
       case ExEquals(l, r) => Equals(rec(l), rec(r)).setType(BooleanType)
+      case ExNotEquals(l, r) => Not(Equals(rec(l), rec(r)).setType(BooleanType)).setType(BooleanType)
       case ExGreaterThan(l, r) => GreaterThan(rec(l), rec(r)).setType(BooleanType)
       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 ExEmptySet(tt) => {
+        val underlying = scalaType2PureScala(unit, silent)(tt.tpe)
+        EmptySet(underlying).setType(SetType(underlying))          
+      }
+      case ExUnion(t1,t2) => {
+        val rl = rec(t1)
+        val rr = rec(t2)
+        SetUnion(rl, rr).setType(rl.getType) // this is not entirely correct: should be a setype of LUB of underlying types of left and right.
+      }
+      case ExIntersection(t1,t2) => {
+        val rl = rec(t1)
+        val rr = rec(t2)
+        SetIntersection(rl, rr).setType(rl.getType) // same as union
+      } 
+      case ExSetMinus(t1,t2) => {
+        val rl = rec(t1)
+        val rr = rec(t2)
+        SetDifference(rl, rr).setType(rl.getType) // same as union
+      } 
       case ExIfThenElse(t1,t2,t3) => {
         val r1 = rec(t1)
         val r2 = rec(t2)

src/funcheck/Extractors.scala

@@ -10,6 +10,8 @@ trait Extractors {
   import global._
   import global.definitions._
 
+  private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
+
   object StructuralExtractors {
     object ScalaPredef {
       /** Extracts method calls from scala.Predef. */
@@ -286,5 +288,43 @@ trait Extractors {
       def unapply(tree: Match): Option[(Tree,List[CaseDef])] =
         if(tree != null) Some((tree.selector, tree.cases)) else None
     }
+
+    object ExEmptySet {
+      def unapply(tree: TypeApply): Option[Tree] = tree match {
+        case TypeApply(
+          Select(
+            Select(
+              Select(
+                Select(Ident(s), collectionName),
+                immutableName),
+              setName),
+            emptyName),  theTypeTree :: Nil) if (
+            collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && emptyName.toString == "empty"
+          ) => Some(theTypeTree)
+        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))
+        case _ => None
+      }
+    }
+  
+    object ExIntersection {
+      def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+        case Apply(Select(lhs, n), List(rhs)) if (n == encode("**")) => Some((lhs,rhs))
+        case _ => None
+      }
+    }
+  
+    object ExSetMinus {
+      def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+        case Apply(Select(lhs, n), List(rhs)) if (n == encode("--")) => Some((lhs,rhs))
+        case _ => None
+      }
+    }
+    
   }
 }

src/purescala/PrettyPrinter.scala

@@ -98,6 +98,10 @@ 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 EmptySet(_) => sb.append("Ø")
+    case SetUnion(l,r) => ppBinary(sb, l, r, " U ", lvl)
+    case SetDifference(l,r) => ppBinary(sb, l, r, " \\ ", lvl)
+    case SetIntersection(l,r) => ppBinary(sb, l, r, " INT ", lvl)
     
     case IfExpr(c, t, e) => {
       var nsb = sb
@@ -162,6 +166,7 @@ object PrettyPrinter {
 
     case ResultVariable() => sb.append("#res")
 
+
     case _ => sb.append("Expr?")
   }