diff --git a/library/lang/package.scala b/library/lang/package.scala
index 358cf40f287861394a22b9503061699528a25d5a..8cb68e7a183223698cddecfd9e9c862d8e7f1e4b 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -34,5 +34,7 @@ object lang {
def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose
def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose
+ def ???[A]: A = throw new RuntimeException("Implementation not supported")
+
def error[T](reason: String): T = sys.error(reason)
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 9596078569394a576a1ea3ca386d56740f717592..7a30d6530498b123d099334e0449b81fd14e4018 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -9,7 +9,7 @@ object Main {
lazy val allPhases: List[LeonPhase[_, _]] = {
List(
frontends.scalac.ExtractionPhase,
- SubtypingPhase,
+ utils.TypingPhase,
xlang.ArrayTransformation,
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
@@ -191,8 +191,9 @@ object Main {
val pipeBegin : Pipeline[List[String],Program] =
frontends.scalac.ExtractionPhase andThen
purescala.MethodLifting andThen
- utils.SubtypingPhase andThen
- purescala.CompleteAbstractDefinitions
+ utils.TypingPhase andThen
+ purescala.CompleteAbstractDefinitions andThen
+ synthesis.ConvertHoles
val pipeProcess: Pipeline[Program, Any] =
if (settings.synthesis) {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index a9c1231fb032944bed99b432ca7cce18ce3a0eae..ecad714521bde7a8853f143265854933f642dcc7 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -290,7 +290,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
val sr = e(s)
sr match {
case FiniteSet(els) => IntLiteral(els.size)
- case _ => throw EvalError(typeErrorMsg(sr, SetType(AnyType)))
+ case _ => throw EvalError(typeErrorMsg(sr, SetType(Untyped)))
}
case f @ FiniteSet(els) => FiniteSet(els.map(e(_)).distinct).setType(f.getType)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index aceb624af72c3c4f295bf0b1995e44267e5574b3..d5aec11a0703e034931cfc1542d6ee64573ab2a7 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -249,6 +249,14 @@ trait ASTExtractors {
}
}
+ object ExHole {
+ def unapply(tree: TypeApply) : Option[Type] = tree match {
+ case a @ TypeApply(s @ ExSelected("leon", "lang", _), List(tpe)) if s.symbol.name.decoded == "???" =>
+ Some(a.tpe)
+ case _ => None
+ }
+ }
+
object ExChooseExpression {
def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree, Tree)] = tree match {
case a @ Apply(
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 7451ba0a6bcace8f8100d02729d1c0a8b7a14b72..250b96211088026a6216276c5d753f888af5d437 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -896,6 +896,10 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Unidentified variable "+sym+" "+sym.id+".")
}
+ case chs @ ExHole(tpe) =>
+ val cTpe = extractType(tpe)
+ Hole().setType(cTpe)
+
case chs @ ExChooseExpression(args, tpe, body, select) =>
val cTpe = extractType(tpe)
@@ -1195,7 +1199,7 @@ trait CodeExtraction extends ASTExtractors {
UnitType
case tpe if tpe == NothingClass.tpe =>
- BottomType
+ Untyped
case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) =>
SetType(extractType(btt))
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index d6fe412998a0d9279cf7e5fe5dde4c59f0fb8232..ba8b05cc2e4aa48c21dfc63a91ecc69f4d9169f8 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -53,10 +53,6 @@ object Common {
def toVariable : Variable = Variable(this)
- private var _islb: Boolean = false
- def markAsLetBinder : Identifier = { _islb = true; this }
- def isLetBinder : Boolean = _islb
-
def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6c73e1e6313f382659041a91207919cf464eef9f..b04aa62fc43b970a1b00e91042c476aae7045b2e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -126,6 +126,11 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
pp(t, p)
sb.append("._" + i)
+ case h @ Hole() =>
+ sb.append("???[")
+ pp(h.getType, p)
+ sb.append("]")
+
case c@Choose(vars, pred) =>
sb.append("choose(")
ppNary(vars, "", ", ", "")
@@ -341,8 +346,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
// Types
- case Untyped => sb.append("???")
- case BottomType => sb.append("Nothing")
+ case Untyped => sb.append("<untyped>")
case UnitType => sb.append("Unit")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 233d9913b7006d3e39e0b1c5e51863ab6e1a8ff4..5a8eb39130e7af52913da44eb87d43865555a118 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1168,7 +1168,7 @@ object TreeOps {
} else {
None
}
- case Untyped | AnyType | BottomType | BooleanType | Int32Type | UnitType | TypeParameter(_) => None
+ case Untyped | BooleanType | Int32Type | UnitType | TypeParameter(_) => None
}
var idMap = Map[Identifier, Identifier]()
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 877bc6a626e1f96f4b7f3aeae59eef815da81d12..a7a46e3c6e78dd647c33acdf815aa2e253abbbfd 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -26,6 +26,8 @@ object Trees {
* the expected type. */
case class Error(description: String) extends Expr with Terminal
+ case class Hole() extends Expr with Terminal
+
case class Choose(vars: List[Identifier], pred: Expr) extends Expr with FixedType with UnaryExtractable {
assert(!vars.isEmpty)
@@ -39,13 +41,10 @@ object Trees {
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr with FixedType {
- binder.markAsLetBinder
-
val fixedType = body.getType
}
case class LetTuple(binders: Seq[Identifier], value: Expr, body: Expr) extends Expr with FixedType {
- binders.foreach(_.markAsLetBinder)
assert(value.getType.isInstanceOf[TupleType],
"The definition value in LetTuple must be of some tuple type; yet we got [%s]. In expr: \n%s".format(value.getType, this))
@@ -86,7 +85,7 @@ object Trees {
case class IfExpr(cond: Expr, thenn: Expr, elze: Expr) extends Expr with FixedType {
val fixedType = leastUpperBound(thenn.getType, elze.getType).getOrElse{
- AnyType
+ Untyped
}
}
@@ -119,7 +118,7 @@ object Trees {
ts(index - 1)
case _ =>
- AnyType
+ Untyped
}
override def equals(that: Any): Boolean = (that != null) && (that match {
@@ -150,7 +149,7 @@ object Trees {
assert(cases.nonEmpty)
val fixedType = leastUpperBound(cases.map(_.rhs.getType)).getOrElse{
- AnyType
+ Untyped
}
def scrutineeClassType: ClassType = scrutinee.getType.asInstanceOf[ClassType]
@@ -560,7 +559,7 @@ object Trees {
case ArrayType(base) =>
base
case _ =>
- AnyType
+ Untyped
}
}
@@ -571,9 +570,9 @@ object Trees {
val fixedType = array.getType match {
case ArrayType(base) =>
- leastUpperBound(base, newValue.getType).map(ArrayType(_)).getOrElse(AnyType)
+ leastUpperBound(base, newValue.getType).map(ArrayType(_)).getOrElse(Untyped)
case _ =>
- AnyType
+ Untyped
}
}
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 2068c5fa636f7290465ad4d1a59975f15f9b40d5..6bdb5fa2493e8c0148a7fed4f228437569e48b1e 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -60,11 +60,6 @@ object TypeTreeOps {
val args = (args1 zip args2).map(p => leastUpperBound(p._1, p._2))
if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
case (o1, o2) if (o1 == o2) => Some(o1)
- case (o1,BottomType) => Some(o1)
- case (BottomType,o2) => Some(o2)
- case (o1,AnyType) => Some(AnyType)
- case (AnyType,o2) => Some(AnyType)
-
case _ => None
}
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index ecab7fc07515ce87dad1ae57aa462cc1b871d51a..7e13555d0eca8e95e4e8e1a2c7f0832ecc28f432 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -58,8 +58,6 @@ object TypeTrees {
def domainSize(typeTree: TypeTree) : TypeSize = typeTree match {
case Untyped => FiniteSize(0)
- case AnyType => InfiniteSize
- case BottomType => FiniteSize(0)
case BooleanType => FiniteSize(2)
case UnitType => FiniteSize(1)
case Int32Type => InfiniteSize
@@ -97,8 +95,6 @@ object TypeTrees {
}
case object Untyped extends TypeTree
- case object AnyType extends TypeTree
- 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.
case object BooleanType extends TypeTree
case object Int32Type extends TypeTree
case object UnitType extends TypeTree
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
new file mode 100644
index 0000000000000000000000000000000000000000..686c5e4b1c905242d1e6aa9c4e66457520c263df
--- /dev/null
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -0,0 +1,101 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.Definitions._
+
+object ConvertHoles extends LeonPhase[Program, Program] {
+ val name = "Convert Holes to Choose"
+ val description = "Convert holes found in bodies to equivalent Choose"
+
+ /**
+ * This phase converts a body with "holes" into a choose construct:
+ *
+ * def foo(a: T) {
+ * require(..a..)
+ * expr(???, ???)
+ * } ensuring { res =>
+ * pred(res)
+ * }
+ *
+ * gets converted into:
+ *
+ * def foo(a: T) {
+ * require(..a..)
+ * choose { (c1, c2) => {
+ * val res = expr(c1, c2)
+ * pred(res)
+ * }
+ * } ensuring { res =>
+ * pred(res)
+ * }
+ *
+ */
+ def run(ctx: LeonContext)(pgm: Program): Program = {
+ pgm.definedFunctions.foreach(fd => {
+ if (fd.hasPostcondition && fd.hasBody) {
+ var holes = List[Identifier]()
+ val body = preMap {
+ case h @ Hole() =>
+ val id = FreshIdentifier("c", true).copiedFrom(h)
+ holes ::= id
+
+ Some(id.toVariable)
+ case _ => None
+ }(fd.body.get)
+
+ holes = holes.reverse
+
+ if (holes.nonEmpty) {
+ val res = FreshIdentifier("b", true).setType(body.getType)
+ val (pid, pbody) = fd.postcondition.get
+
+ val c = Choose(holes, Let(res, body, replaceFromIDs(Map(pid -> res.toVariable), pbody)))
+
+ if (holes.size > 1) {
+ val newHoles = holes.map(_.freshen)
+ fd.body = Some(LetTuple(newHoles, c, replaceFromIDs((holes zip newHoles.map(_.toVariable)).toMap, body)))
+ } else {
+ fd.body = Some(preMap {
+ case h @ Hole() => Some(c)
+ case _ => None
+ }(fd.body.get))
+ }
+ }
+ } else {
+ // No post-condition: we replace holes with local-chooses without
+ // predicates
+ fd.body = fd.body.map { preMap {
+ case h @ Hole() =>
+ val id = FreshIdentifier("c", true).copiedFrom(h)
+ Some(Choose(List(id), BooleanLiteral(true)).copiedFrom(h))
+ case _ => None
+ } }
+ }
+
+ // Ensure that holes are not found in pre and/or post conditions
+ fd.precondition.foreach {
+ preTraversal{
+ case Hole() =>
+ ctx.reporter.error("Hole expressions are not supported in preconditions. (function "+fd.id.asString(ctx)+")")
+ case _ =>
+ }
+ }
+
+ fd.postcondition.foreach { case (id, post) =>
+ preTraversal{
+ case Hole() =>
+ ctx.reporter.error("Hole expressions are not supported in postconditions. (function "+fd.id.asString(ctx)+")")
+ case _ =>
+ }(post)
+ }
+
+ })
+
+ pgm
+ }
+}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
index b1e48f05b92755c3c2709e37da730b1c06dda663..bf353c58ae4447c23951150a4c746ec56c10117a 100644
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
@@ -4,7 +4,7 @@ package leon.synthesis.condabd.insynth.leon
import insynth.structures._
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, BottomType => LeonBottomType, _ }
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Common.FreshIdentifier
import leon.purescala.Definitions._
@@ -28,11 +28,10 @@ object DomainTypeTransformer extends ( LeonType => DomainType ) {
leonType match {
case Untyped => throw new RuntimeException("Should not happen at this point")
- case AnyType => Atom(Const("Any"))
- case LeonBottomType => Atom(BottomType) //Atom(Const("Bottom"))
case BooleanType => Atom(Const("Boolean"))
case UnitType => Atom(Const("Unit"))
case Int32Type => Atom(Const("Int"))
+ case TypeParameter(id) => Atom(Const(id.name))
case ListType(baseType) => Atom(InSynthTypeTransformer(leonType))
case ArrayType(baseType) => Atom(InSynthTypeTransformer(leonType))
case TupleType(baseTypes) => Atom(InSynthTypeTransformer(leonType))
@@ -49,8 +48,6 @@ object DomainTypeTransformer extends ( LeonType => DomainType ) {
transformFunction(to, params ++ froms)
case Untyped => throw new RuntimeException("Should not happen at this point")
// query will have this
- case LeonBottomType =>
- Function( params map this, this(fun) )
case t =>
Function( params map this, this(t) )
}
diff --git a/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
index eb92516094d408fddbe8665f280926eb06a84a80..afc51eb5e264b750dcf320ff0ab2e0e5ae5261b8 100644
--- a/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
@@ -4,7 +4,7 @@ package leon.synthesis.condabd.insynth.leon
import insynth.structures._
-import leon.purescala.TypeTrees.{ TypeTree => LeonType, BottomType => LeonBottomType, _ }
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Common.FreshIdentifier
import leon.purescala.Definitions._
@@ -28,10 +28,9 @@ object TypeTransformer extends ( LeonType => SuccinctType ) {
leonType match {
case Untyped => throw new RuntimeException("Should not happen at this point")
- case AnyType => Const("Any")
- case LeonBottomType => BottomType //Const("Bottom")
case BooleanType => Const("Boolean")
case UnitType => Const("Unit")
+ case TypeParameter(id) => Const(id.name)
case Int32Type => Const("Int")
case ListType(baseType) => Instance("List", this(baseType) )
case ArrayType(baseType) => Instance("Array", this(baseType) )
@@ -49,8 +48,6 @@ object TypeTransformer extends ( LeonType => SuccinctType ) {
transformFunction(to, params ++ froms)
case Untyped => throw new RuntimeException("Should not happen at this point")
// query will have this
- case LeonBottomType =>
- Arrow( TSet(params map this distinct), this(fun) )
case t =>
Arrow( TSet(params map this distinct), this(t) )
}
diff --git a/src/main/scala/leon/utils/Positions.scala b/src/main/scala/leon/utils/Positions.scala
index a18d721c11683ec1061dadd46ab8629da0ac81c4..1068863b54818c7de77ded37814207246b14da80 100644
--- a/src/main/scala/leon/utils/Positions.scala
+++ b/src/main/scala/leon/utils/Positions.scala
@@ -14,11 +14,14 @@ abstract class Position {
(this.file == that.file) && (this.line < that.line || this.col < that.col)
}
+ def fullString: String
+
def isDefined: Boolean
}
abstract class DefinedPosition extends Position {
override def toString = line+":"+col
+ override def fullString = file.getPath+":"+line+":"+col
override def isDefined = true
def focusBegin: OffsetPosition
@@ -47,6 +50,7 @@ case object NoPosition extends Position {
val file = null
override def toString = "?:?"
+ override def fullString = "?:?:?"
override def isDefined = false
}
diff --git a/src/main/scala/leon/utils/SubtypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
similarity index 58%
rename from src/main/scala/leon/utils/SubtypingPhase.scala
rename to src/main/scala/leon/utils/TypingPhase.scala
index 35729c85bcd9ce123a2269243396716390c01779..1dc7b561609f87aa3ff6c173b02a1d813f492803 100644
--- a/src/main/scala/leon/utils/SubtypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -4,20 +4,31 @@ package leon
package utils
import purescala.Common._
+import purescala.TreeOps.preTraversal
import purescala.TypeTrees._
import purescala.Trees._
import purescala.Definitions._
-object SubtypingPhase extends LeonPhase[Program, Program] {
+object TypingPhase extends LeonPhase[Program, Program] {
- val name = "Subtyping"
- val description = "Protection of function arguments with subtypes"
+ val name = "Typing"
+ val description = "Ensure and enforce certain Leon typing rules"
- //note that this will mutate the existing program functions and
- //not return a new different program
+ /**
+ * This phase does 2 different things:
+ *
+ * 1) Ensure that functions that take and/or return a specific ADT subtype
+ * have this encoded explicitly in pre/postconditions. Solvers such as Z3
+ * unify types, which means that we need to ensure models are consistent
+ * with the original type constraints.
+ *
+ * 2) Report warnings in case parts of the tree are not correctly typed
+ * (Untyped).
+ */
def run(ctx: LeonContext)(pgm: Program): Program = {
pgm.definedFunctions.foreach(fd => {
+ // Part (1)
fd.precondition = {
val argTypesPreconditions = fd.params.flatMap(arg => arg.tpe match {
case cct : CaseClassType => Seq(CaseClassInstanceOf(cct, arg.id.toVariable))
@@ -48,6 +59,15 @@ object SubtypingPhase extends LeonPhase[Program, Program] {
case _ => fd.postcondition
}
+ // Part (2)
+ fd.body.foreach {
+ preTraversal{
+ case t if !t.isTyped =>
+ ctx.reporter.warning("Tree "+t.asString(ctx)+" is not properly typed ("+t.getPos.fullString+")")
+ case _ =>
+ }
+ }
+
})
pgm
}
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 98bd2011daa5314e08eab04ef6f6629fa2f8c413..3532030ae7ab8860157b3d040cfa6187c75225a3 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -111,7 +111,6 @@ object Trees {
//same as let, buf for mutable variable declaration
case class LetVar(binder: Identifier, value: Expr, body: Expr) extends Expr with BinaryExtractable with PrettyPrintable {
- binder.markAsLetBinder
val et = body.getType
if(et != Untyped)
setType(et)
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index f79ea24382ece07e03a0af2a50b7dc5c3a92da3e..e358e14369d58ee192bf7df68fbbc530dc4a45f1 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -16,7 +16,7 @@ import leon.purescala.TypeTrees._
class TransformationTests extends LeonTestSuite {
- val pipeline = ExtractionPhase andThen leon.utils.SubtypingPhase
+ val pipeline = ExtractionPhase andThen leon.utils.TypingPhase
filesInResourceDir("regression/transformations").foreach { file =>
val ctx = testContext.copy(
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 03d8b11707005b3bc61741e67b6bb9b2bd0e97be..38971a80b7369efcc483198c8918f24243e6a91e 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -33,7 +33,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
val opts = SynthesisOptions(searchBound = Some(bound))
- val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase
+ val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase
val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 0037901e8457deac18350b27b786c5f498dc155c..6fa5909049ebcaba9934ceb8fcbd3a0f823c45e0 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -17,7 +17,7 @@ class TerminationRegression extends LeonTestSuite {
private case class Output(report : TerminationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],TerminationReport] =
- leon.frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.termination.TerminationPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase andThen leon.termination.TerminationPhase
private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
index 119a317644a8a87427173e8a1a202e1244275746..bf54de0070f697e845087fa3bdb8de16fc901c2a 100644
--- a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
@@ -10,7 +10,7 @@ class LibraryVerificationRegression extends LeonTestSuite {
test("Verify the library") {
val pipeline = leon.frontends.scalac.ExtractionPhase andThen
leon.purescala.MethodLifting andThen
- leon.utils.SubtypingPhase andThen
+ leon.utils.TypingPhase andThen
leon.purescala.CompleteAbstractDefinitions andThen
leon.verification.AnalysisPhase
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 594a0cb341e9cd8c9ab8ad08769c05585697d848..18d39fa7679e3448e1f62287c1245b59de25764f 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -17,7 +17,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.verification.AnalysisPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase andThen leon.verification.AnalysisPhase
private def mkTest(file : File, leonOptions : Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 9af2b1498331fc887056b857581bc905b80e3d2e..89eaaca6427f1a8a23386fa328cd696989f4184d 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -17,7 +17,7 @@ class XLangVerificationRegression extends LeonTestSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.frontends.scalac.ExtractionPhase andThen leon.utils.SubtypingPhase andThen xlang.XlangAnalysisPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase andThen xlang.XlangAnalysisPhase
private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
val fullName = file.getPath()