code extraction complete

src/main/scala/leon/plugin/CodeExtraction.scala

@@ -28,6 +28,8 @@ trait CodeExtraction extends Extractors {
   private lazy val someClassSym       = definitions.getClass("scala.Some")
   private lazy val function1TraitSym  = definitions.getClass("scala.Function1")
 
+  def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
+
   def isSetTraitSym(sym : Symbol) : Boolean = {
     sym == setTraitSym || sym.tpe.toString.startsWith("scala.Predef.Set")
   }
@@ -357,6 +359,20 @@ trait CodeExtraction extends Extractors {
     }
 
     def rec(tr: Tree): Expr = tr match {
+      case ExTuple(tpes, exprs) => {
+        println("getting ExTuple with " + tpes + " and " + exprs)
+        val tupleType = TupleType(tpes.map(tpe => scalaType2PureScala(unit, silent)(tpe)))
+        val tupleExprs = exprs.map(e => rec(e))
+        Tuple(tupleExprs).setType(tupleType)
+      }
+      case ExTupleExtract(tuple, index) => {
+        val tupleExpr = rec(tuple)
+        val TupleType(tpes) = tupleExpr.getType
+        if(tpes.size < index)
+          throw ImpureCodeEncounteredException(tree)
+        else
+          TupleSelect(tupleExpr, index).setType(tpes(index-1))
+      }
       case ExValDef(vs, tpt, bdy, rst) => {
         val binderTpe = scalaType2PureScala(unit, silent)(tpt.tpe)
         val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
@@ -650,6 +666,7 @@ trait CodeExtraction extends Extractors {
       case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
       case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
       case TypeRef(_, sym, List(ftt,ttt)) if isMapTraitSym(sym) => MapType(rec(ftt),rec(ttt))
+      case TypeRef(_, sym, List(ftt,ttt)) if isTuple2(sym) => TupleType(Seq(rec(ftt),rec(ttt)))
       case TypeRef(_, sym, ftt :: ttt :: Nil) if isFunction1TraitSym(sym) => FunctionType(List(rec(ftt)), rec(ttt))
       case TypeRef(_, sym, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
       case _ => {

src/main/scala/leon/plugin/Extractors.scala

@@ -11,6 +11,7 @@ trait Extractors {
   import global._
   import global.definitions._
 
+  protected lazy val tuple2Sym: Symbol = definitions.getClass("scala.Tuple2")
   private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
   private lazy val mapTraitSym = definitions.getClass("scala.collection.immutable.Map")
   private lazy val multisetTraitSym = definitions.getClass("scala.collection.immutable.Multiset")
@@ -27,6 +28,19 @@ trait Extractors {
       }
     }
 
+    object ExTuple {
+      def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
+        case Apply(
+          Select(New(tupleType), _),
+          List(e1, e2)
+        ) if tupleType.symbol == tuple2Sym => tupleType.tpe match {
+            case TypeRef(_, sym, List(t1, t2)) => Some((Seq(t1, t2), Seq(e1, e2)))
+            case _ => None
+          }
+        case _ => None
+      }
+    }
+
     object ExEnsuredExpression {
       /** Extracts the 'ensuring' contract from an expression. */
       def unapply(tree: Apply): Option[(Tree,Symbol,Tree)] = tree match {
@@ -44,6 +58,26 @@ trait Extractors {
       }
     }
 
+    object ExTupleExtract {
+      def unapply(tree: Select) : Option[(Tree,Int)] = tree match {
+        case Select(lhs, n) => {
+          val methodName = n.toString
+          if(methodName.head == '_') {
+            val indexString = methodName.tail
+            try {
+              val index = indexString.toInt
+              if(index > 0) {
+                Some((lhs, index)) 
+              } else None
+            } catch {
+              case _ => None
+            }
+          } else None
+        }
+        case _ => None
+      }
+    }
+
     object ExHoldsExpression {
       def unapply(tree: Select) : Option[Tree] = tree match {
         case Select(Apply(Select(Select(leonIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (