From da408410c654eb2f9e64cd57ccdc7efad458ca01 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 17 Mar 2014 13:53:39 +0100
Subject: [PATCH] Improve types, support ???[T] as all-seeing choose
- Holes become chooses
- Unhandled types are removed, Untyped is now checked for and
a warning is issued if an untyped expression is found.
---
library/lang/package.scala | 2 +
src/main/scala/leon/Main.scala | 7 +-
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../leon/frontends/scalac/ASTExtractors.scala | 8 ++
.../frontends/scalac/CodeExtraction.scala | 6 +-
src/main/scala/leon/purescala/Common.scala | 4 -
.../scala/leon/purescala/PrettyPrinter.scala | 8 +-
src/main/scala/leon/purescala/TreeOps.scala | 2 +-
src/main/scala/leon/purescala/Trees.scala | 17 ++-
.../scala/leon/purescala/TypeTreeOps.scala | 5 -
src/main/scala/leon/purescala/TypeTrees.scala | 4 -
.../scala/leon/synthesis/ConvertHoles.scala | 101 ++++++++++++++++++
.../insynth/leon/DomainTypeTransformer.scala | 7 +-
.../insynth/leon/TypeTransformer.scala | 7 +-
src/main/scala/leon/utils/Positions.scala | 4 +
...SubtypingPhase.scala => TypingPhase.scala} | 30 +++++-
src/main/scala/leon/xlang/Trees.scala | 1 -
.../test/purescala/TransformationTests.scala | 2 +-
.../synthesis/SynthesisRegressionSuite.scala | 2 +-
.../termination/TerminationRegression.scala | 2 +-
.../LibraryVerificationRegression.scala | 2 +-
.../PureScalaVerificationRegression.scala | 2 +-
.../XLangVerificationRegression.scala | 2 +-
23 files changed, 175 insertions(+), 52 deletions(-)
create mode 100644 src/main/scala/leon/synthesis/ConvertHoles.scala
rename src/main/scala/leon/utils/{SubtypingPhase.scala => TypingPhase.scala} (58%)
diff --git a/library/lang/package.scala b/library/lang/package.scala
index 358cf40f2..8cb68e7a1 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 959607856..7a30d6530 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 a9c1231fb..ecad71452 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 aceb624af..d5aec11a0 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 7451ba0a6..250b96211 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 d6fe41299..ba8b05cc2 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 6c73e1e63..b04aa62fc 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 233d9913b..5a8eb3913 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 877bc6a62..a7a46e3c6 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 2068c5fa6..6bdb5fa24 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 ecab7fc07..7e13555d0 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 000000000..686c5e4b1
--- /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 b1e48f05b..bf353c58a 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 eb9251609..afc51eb5e 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 a18d721c1..1068863b5 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 35729c85b..1dc7b5616 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 98bd2011d..3532030ae 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 f79ea2438..e358e1436 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 03d8b1170..38971a80b 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 0037901e8..6fa590904 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 119a31764..bf54de007 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 594a0cb34..18d39fa76 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 9af2b1498..89eaaca64 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()
--
GitLab