From 1b1592a8673c6164caaea2206f2f3c6e398fe50f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 21 Mar 2012 23:57:52 +0000
Subject: [PATCH] code extraction complete
---
.../scala/leon/plugin/CodeExtraction.scala | 17 ++++++++++
src/main/scala/leon/plugin/Extractors.scala | 34 +++++++++++++++++++
2 files changed, 51 insertions(+)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index f1cfeb44c..3bd31a2e3 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/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 _ => {
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 6985e9b8f..e58d67a88 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/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 (
--
GitLab