diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 23562e7740363a7c79d76e7ee0ccb575332d3d73..66c7d98444a0b23476098bd98c5c6bd72cb390b3 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -17,7 +17,25 @@ trait CodeExtraction extends Extractors {
import ExpressionExtractors._
private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
- private lazy val multisetTraitSym = definitions.getClass("scala.collection.immutable.Multiset")
+ private lazy val multisetTraitSym = try {
+ definitions.getClass("scala.collection.immutable.Multiset")
+ } catch {
+ case _ => null
+ }
+ private lazy val optionClassSym = definitions.getClass("scala.Option")
+ private lazy val someClassSym = definitions.getClass("scala.Some")
+
+ def isSetTraitSym(sym : Symbol) : Boolean = {
+ sym == setTraitSym || sym.tpe.toString.startsWith("scala.Predef.Set")
+ }
+
+ def isMultisetTraitSym(sym : Symbol) : Boolean = {
+ sym == multisetTraitSym
+ }
+
+ def isOptionClassSym(sym : Symbol) : Boolean = {
+ sym == optionClassSym || sym == someClassSym
+ }
private val varSubsts: scala.collection.mutable.Map[Symbol,Function0[Expr]] =
scala.collection.mutable.Map.empty[Symbol,Function0[Expr]]
@@ -346,6 +364,11 @@ trait CodeExtraction extends Extractors {
throw ImpureCodeEncounteredException(tr)
}
}
+ case ExSomeConstruction(tpe, arg) => {
+ println("Got Some !" + tpe + ":" + arg)
+ val underlying = scalaType2PureScala(unit, silent)(tpe)
+ OptionSome(rec(arg)).setType(OptionType(underlying))
+ }
case ExCaseClassConstruction(tpt, args) => {
val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
if(!cctype.isInstanceOf[CaseClassType]) {
@@ -562,13 +585,15 @@ trait CodeExtraction extends Extractors {
def rec(tr: Type): purescala.TypeTrees.TypeTree = tr match {
case tpe if tpe == IntClass.tpe => Int32Type
case tpe if tpe == BooleanClass.tpe => BooleanType
- case TypeRef(_, sym, btt :: Nil) if sym == setTraitSym => SetType(rec(btt))
- case TypeRef(_, sym, btt :: Nil) if sym == multisetTraitSym => MultisetType(rec(btt))
+ case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
+ 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, Nil) if classesToClasses.keySet.contains(sym) => classDefToClassType(classesToClasses(sym))
case _ => {
if(!silent) {
unit.error(NoPosition, "Could not extract type as PureScala. [" + tr + "]")
+ throw new Exception("aouch")
}
throw ImpureCodeEncounteredException(null)
}
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 3b540a735526dd6a752f3dfe2642b4c64a822540..f833efd3b4af95476862e2eaeb210b0b6b5adf48 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -12,6 +12,7 @@ trait Extractors {
private lazy val setTraitSym = definitions.getClass("scala.collection.immutable.Set")
private lazy val multisetTraitSym = definitions.getClass("scala.collection.immutable.Multiset")
+ private lazy val optionClassSym = definitions.getClass("scala.Option")
object StructuralExtractors {
object ScalaPredef {
@@ -172,6 +173,16 @@ trait Extractors {
}
}
+ object ExSomeConstruction {
+ def unapply(tree: Apply) : Option[(Type,Tree)] = tree match {
+ case Apply(s @ Select(New(tpt), n), arg) if (arg.size == 1 && n == nme.CONSTRUCTOR && tpt.symbol.name.toString == "Some") => tpt.tpe match {
+ case TypeRef(_, sym, tpe :: Nil) => Some((tpe, arg(0)))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
object ExCaseClassConstruction {
def unapply(tree: Apply): Option[(Tree,Seq[Tree])] = tree match {
case Apply(s @ Select(New(tpt), n), args) if (n == nme.CONSTRUCTOR) => {
@@ -345,6 +356,7 @@ trait Extractors {
emptyName), theTypeTree :: Nil) if (
collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && emptyName.toString == "empty"
) => Some(theTypeTree)
+ case TypeApply(Select(Select(Select(This(scalaName), predefName), setname), applyName), theTypeTree :: Nil) if ("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString) && "empty".equals(applyName.toString)) => Some(theTypeTree)
case _ => None
}
}
@@ -367,17 +379,8 @@ 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 Apply(TypeApply(Select(Select(Select(Select(Ident(s), collectionName), immutableName), setName), applyName), theTypeTree :: Nil), args) if (collectionName.toString == "collection" && immutableName.toString == "immutable" && setName.toString == "Set" && applyName.toString == "apply") => Some((theTypeTree, args))
+ case Apply(TypeApply(Select(Select(Select(This(scalaName), predefName), setname), applyName), theTypeTree :: Nil), args) if ("scala".equals(scalaName.toString) && "Predef".equals(predefName.toString) && "apply".equals(applyName.toString)) => Some((theTypeTree, args))
case _ => None
}
}
diff --git a/src/funcheck/Main.scala b/src/funcheck/Main.scala
index 2796bcf8540d7c010a7d91c51b9456bbd3dfcf09..7ec91a61841ef71c9b5bbeb3e02ba18b927bdc9f 100644
--- a/src/funcheck/Main.scala
+++ b/src/funcheck/Main.scala
@@ -48,7 +48,7 @@ object Main {
} else {
val runner = new PluginRunner(settings, printerFunction, actionOnProgram)
runner.funcheckPlugin.processOptions(funcheckOptions.map(_.substring(2)), Console.err.println(_))
- runner.funcheckPlugin.stopAfterExtraction = false
+ //runner.funcheckPlugin.stopAfterExtraction = false
runner.funcheckPlugin.stopAfterAnalysis = false
val run = new runner.Run
run.compile(command.files)
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index e76b8e270abed6f8707529fbe9fd8980ca1a5bde..5cdfe7b6801e44d3a2c6d5431ee1b40666c38e71 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -80,6 +80,17 @@ object PrettyPrinter {
case IntLiteral(v) => sb.append(v)
case BooleanLiteral(v) => sb.append(v)
case StringLiteral(s) => sb.append("\"" + s + "\"")
+
+ case OptionSome(a) => {
+ var nsb = sb
+ nsb.append("Some(")
+ nsb = pp(a, nsb, lvl)
+ nsb.append(")")
+ nsb
+ }
+
+ case OptionNone(_) => sb.append("None")
+
case CaseClass(cd, args) => {
var nsb = sb
nsb.append(cd.id)
@@ -222,6 +233,7 @@ object PrettyPrinter {
case BooleanType => sb.append("Boolean")
case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
+ case OptionType(bt) => pp(bt, sb.append("Option["), lvl).append("]")
case c: ClassType => sb.append(c.classDef.id)
case _ => sb.append("Type?")
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 8be09ed17e197c91419e87602a8929606fa5fc46..7b00d7d87f658adb7a704df39290208bee281149 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -272,8 +272,10 @@ object Trees {
}
/* Option expressions */
- // case class OptionSome(value: Expr) extends Expr
- // case class OptionNone(baseType: TypeTree) extends Expr with Terminal
+ @serializable case class OptionSome(value: Expr) extends Expr
+ @serializable case class OptionNone(baseType: TypeTree) extends Expr with Terminal with FixedType {
+ val fixedType = OptionType(baseType)
+ }
/* Set expressions */
@serializable case class EmptySet(baseType: TypeTree) extends Expr with Terminal
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index 6f65972d3343aac47fd55098cf928695d30b7b48..33234900b2e39d563df618b8d930b3ffdba67706 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -78,8 +78,8 @@ object TypeTrees {
}
case (o1, o2) if (o1 == o2) => o1
- case (o1,NoType) => o1
- case (NoType,o2) => o2
+ case (o1,BottomType) => o1
+ case (BottomType,o2) => o2
case (o1,AnyType) => AnyType
case (AnyType,o2) => AnyType
@@ -94,7 +94,7 @@ object TypeTrees {
def domainSize(typeTree: TypeTree) : TypeSize = typeTree match {
case Untyped => FiniteSize(0)
case AnyType => InfiniteSize
- case NoType => FiniteSize(0)
+ case BottomType => FiniteSize(0)
case BooleanType => FiniteSize(2)
case Int32Type => InfiniteSize
case ListType(_) => InfiniteSize
@@ -124,7 +124,7 @@ object TypeTrees {
@serializable case object Untyped extends TypeTree
@serializable case object AnyType extends TypeTree
- @serializable case object NoType extends TypeTree // This is the type of errors (ie. subtype of anything)
+ @serializable case object BottomType extends TypeTree // This type is useful when we need an underlying type for None, Set.empty, etc. It should always be removed after parsing, though.
@serializable case object BooleanType extends TypeTree
@serializable case object Int32Type extends TypeTree