From 849de6aa80e4c437130bb557f9083cc277f952ee Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 8 Sep 2015 14:58:56 +0200
Subject: [PATCH] Fix MethodLifting and improvements
Make signature of IsInstanceOf consistent with other Expr's
Add isInstOf Constructor
Correctly handle This in instantiateType
Correctly handle This in MethodLifting when it belongs to a subtype
An extra unit test
---
.../scala/leon/codegen/CodeGeneration.scala | 2 +-
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../frontends/scalac/CodeExtraction.scala | 2 +-
.../scala/leon/purescala/Constructors.scala | 10 ++++++++
src/main/scala/leon/purescala/ExprOps.scala | 6 ++---
.../scala/leon/purescala/Expressions.scala | 4 ++--
.../scala/leon/purescala/Extractors.scala | 4 ++--
.../scala/leon/purescala/MethodLifting.scala | 24 +++++++++++--------
.../scala/leon/purescala/PrettyPrinter.scala | 2 +-
src/main/scala/leon/purescala/TypeOps.scala | 7 ++++--
.../leon/solvers/smtlib/SMTLIBSolver.scala | 2 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 8 +++----
.../scala/leon/synthesis/rules/ADTDual.scala | 4 ++--
.../leon/synthesis/rules/ADTInduction.scala | 2 +-
.../synthesis/rules/ADTLongInduction.scala | 2 +-
.../scala/leon/synthesis/rules/ADTSplit.scala | 4 ++--
.../synthesis/rules/EquivalentInputs.scala | 2 +-
.../leon/termination/SelfCallsProcessor.scala | 2 +-
src/main/scala/leon/utils/TypingPhase.scala | 6 ++---
.../leon/verification/InductionTactic.scala | 4 ++--
.../leon/verification/InjectAsserts.scala | 2 +-
.../leon/unit/purescala/TypeOpsSuite.scala | 3 ++-
22 files changed, 61 insertions(+), 43 deletions(-)
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index f4bb00795..1e37626f0 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -279,7 +279,7 @@ trait CodeGeneration {
}
ch << InvokeSpecial(ccName, constructorName, ccApplySig)
- case IsInstanceOf(cct, e) =>
+ case IsInstanceOf(e, cct) =>
val (ccName, _) = leonClassToJVMInfo(cct.classDef).getOrElse {
throw CompilationException("Unknown class : " + cct.id)
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 3f4a67f48..38710837f 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -231,7 +231,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
throw RuntimeError("Cast error: cannot cast "+le.asString+" to "+ct.asString)
}
- case IsInstanceOf(ct, expr) =>
+ case IsInstanceOf(expr, ct) =>
val le = e(expr)
BooleanLiteral(isSubtypeOf(le.getType, ct))
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 2c8325042..0a6633aa4 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1427,7 +1427,7 @@ trait CodeExtraction extends ASTExtractors {
if(rootType != testedExprRootType) {
outOfSubsetError(tr, "isInstanceOf can only be used with compatible classes")
} else {
- IsInstanceOf(ct, ccRec)
+ IsInstanceOf(ccRec, ct)
}
}
case _ =>
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 5f217f229..22697b7df 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -383,8 +383,18 @@ object Constructors {
if (isSubtypeOf(expr.getType, tpe)) {
expr
} else {
+ //println(s"$expr:${expr.getType} is not a subtype of $tpe")
AsInstanceOf(expr, tpe)
}
}
+ def isInstOf(expr: Expr, tpe: ClassType) = {
+ if (isSubtypeOf(expr.getType, tpe)) {
+ BooleanLiteral(true)
+ } else {
+ IsInstanceOf(expr, tpe)
+ }
+
+ }
+
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 69267f7af..91d36d7a9 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -771,7 +771,7 @@ object ExprOps {
if (ct.parent.isEmpty) {
bind(ob, in)
} else {
- and(IsInstanceOf(ct, in), bind(ob, in))
+ and(IsInstanceOf(in, ct), bind(ob, in))
}
case CaseClassPattern(ob, cct, subps) =>
@@ -779,7 +779,7 @@ object ExprOps {
val pairs = cct.fields.map(_.id).toList zip subps.toList
val subTests = pairs.map(p => rec(caseClassSelector(cct, in, p._1), p._2))
val together = and(bind(ob, in) +: subTests :_*)
- and(IsInstanceOf(cct, in), together)
+ and(IsInstanceOf(in, cct), together)
case TuplePattern(ob, subps) =>
val TupleType(tpes) = in.getType
@@ -1326,7 +1326,7 @@ object ExprOps {
case ccd: CaseClassDef =>
val cct = CaseClassType(ccd, tps)
- val isType = IsInstanceOf(cct, Variable(on))
+ val isType = IsInstanceOf(Variable(on), cct)
val recSelectors = cct.fields.collect {
case vd if vd.getType == on.getType => vd.id
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 7882a6269..b44a4b9f8 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -327,7 +327,7 @@ object Expressions {
binder,
FunctionInvocation(unapplyFun, Seq(scrut)),
IfExpr(
- IsInstanceOf(someType, Variable(binder)),
+ IsInstanceOf(Variable(binder), someType),
someCase(CaseClassSelector(someType, Variable(binder), someValue.id)),
noneCase
)
@@ -424,7 +424,7 @@ object Expressions {
}
/** $encodingof `.isInstanceOf[...]` */
- case class IsInstanceOf(classType: ClassType, expr: Expr) extends Expr {
+ case class IsInstanceOf(expr: Expr, classType: ClassType) extends Expr {
val getType = BooleanType
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index c8d54731c..ca6a21fb0 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -31,8 +31,8 @@ object Extractors {
Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
case CaseClassSelector(cd, e, sel) =>
Some((Seq(e), (es: Seq[Expr]) => caseClassSelector(cd, es.head, sel)))
- case IsInstanceOf(ct, e) =>
- Some((Seq(e), (es: Seq[Expr]) => IsInstanceOf(ct, es.head)))
+ case IsInstanceOf(e, ct) =>
+ Some((Seq(e), (es: Seq[Expr]) => IsInstanceOf(es.head, ct)))
case AsInstanceOf(e, ct) =>
Some((Seq(e), (es: Seq[Expr]) => asInstOf(es.head, ct)))
case TupleSelect(t, i) =>
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 277803109..4848bf10e 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -79,8 +79,8 @@ object MethodLifting extends TransformationPhase {
val at = acd.typed
val binder = FreshIdentifier(acd.id.name.toLowerCase, at, true)
def subst(e: Expr): Expr = e match {
- case This(`at`) =>
- Variable(binder)
+ case This(ct) =>
+ asInstOf(Variable(binder), ct)
case e =>
e
}
@@ -125,9 +125,9 @@ object MethodLifting extends TransformationPhase {
newFd.fullBody,
Some(and(
prec,
- IsInstanceOf(
- c.typed(root.tparams.map{ _.tp }),
- This(root.typed)
+ isInstOf(
+ This(root.typed),
+ c.typed(root.tparams.map{ _.tp })
)
))
))
@@ -158,14 +158,18 @@ object MethodLifting extends TransformationPhase {
nfd.addFlag(IsMethod(cd))
if (cd.knownDescendants.forall( cd => (cd.methods ++ cd.fields).forall(_.id != fd.id))) {
- val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
// Don't need to compose methods
- nfd.fullBody = postMap {
- case th@This(ct) if ct.classDef == cd =>
- Some(receiver.toVariable.setPos(th))
+ val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
+ def thisToReceiver(e: Expr): Option[Expr] = e match {
+ case th@This(ct) =>
+ Some(asInstOf(receiver.toVariable, ct).setPos(th))
case _ =>
None
- }(instantiateType(nfd.fullBody, tparamsMap, paramsMap))
+ }
+
+ val insTp: Expr => Expr = instantiateType(_, tparamsMap, paramsMap)
+
+ nfd.fullBody = insTp( postMap(thisToReceiver)(insTp(nfd.fullBody)) )
} else {
// We need to compose methods of subclasses
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c9005ec2d..6d020cc71 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -167,7 +167,7 @@ class PrettyPrinter(opts: PrinterOptions,
case Choose(pred) => p"choose($pred)"
case e @ Error(tpe, err) => p"""error[$tpe]("$err")"""
case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
- case IsInstanceOf(cct, e) =>
+ case IsInstanceOf(e, cct) =>
if (cct.classDef.isCaseObject) {
p"($e == $cct)"
} else {
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 0eac83d63..5c68340e6 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -273,14 +273,17 @@ object TypeOps {
case mi @ MethodInvocation(r, cd, TypedFunDef(fd, tps), args) =>
MethodInvocation(srec(r), cd, TypedFunDef(fd, tps.map(tpeSub)), args.map(srec)).copiedFrom(mi)
+ case th @ This(ct) =>
+ This(tpeSub(ct).asInstanceOf[ClassType]).copiedFrom(th)
+
case cc @ CaseClass(ct, args) =>
CaseClass(tpeSub(ct).asInstanceOf[CaseClassType], args.map(srec)).copiedFrom(cc)
case cc @ CaseClassSelector(ct, e, sel) =>
caseClassSelector(tpeSub(ct).asInstanceOf[CaseClassType], srec(e), sel).copiedFrom(cc)
- case cc @ IsInstanceOf(ct, e) =>
- IsInstanceOf(tpeSub(ct).asInstanceOf[ClassType], srec(e)).copiedFrom(cc)
+ case cc @ IsInstanceOf(e, ct) =>
+ IsInstanceOf(srec(e), tpeSub(ct).asInstanceOf[ClassType]).copiedFrom(cc)
case cc @ AsInstanceOf(e, ct) =>
AsInstanceOf(srec(e), tpeSub(ct).asInstanceOf[ClassType]).copiedFrom(cc)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index aaf65f508..bcf8a5fa1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -333,7 +333,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case AsInstanceOf(expr, cct) =>
toSMT(expr)
- case IsInstanceOf(cct, e) =>
+ case IsInstanceOf(e, cct) =>
declareSort(cct)
val cases = cct match {
case act: AbstractClassType =>
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 07943a8b9..bfa1d9c16 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -426,16 +426,16 @@ trait AbstractZ3Solver extends Solver {
case AsInstanceOf(expr, ct) =>
rec(expr)
- case IsInstanceOf(act: AbstractClassType, e) =>
+ case IsInstanceOf(e, act: AbstractClassType) =>
act.knownCCDescendants match {
case Seq(cct) =>
- rec(IsInstanceOf(cct, e))
+ rec(IsInstanceOf(e, cct))
case more =>
val i = FreshIdentifier("e", act, alwaysShowUniqueID = true)
- rec(Let(i, e, orJoin(more map(IsInstanceOf(_, Variable(i))))))
+ rec(Let(i, e, orJoin(more map(IsInstanceOf(Variable(i), _)))))
}
- case IsInstanceOf(cct: CaseClassType, e) =>
+ case IsInstanceOf(e, cct: CaseClassType) =>
typeToSort(cct) // Making sure the sort is defined
val tester = testers.toB(cct)
tester(rec(e))
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index f8770aafd..392670edf 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -18,10 +18,10 @@ case object ADTDual extends NormalizingRule("ADTDual") {
val (toRemove, toAdd) = exprs.collect {
case eq @ Equals(cc @ CaseClass(ct, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
- (eq, IsInstanceOf(ct, e) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
+ (eq, IsInstanceOf(e, ct) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
case eq @ Equals(e, cc @ CaseClass(ct, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) & xs).nonEmpty =>
- (eq, IsInstanceOf(ct, e) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
+ (eq, IsInstanceOf(e, ct) +: (ct.fields zip args).map{ case (vd, ex) => Equals(ex, caseClassSelector(ct, e, vd.id)) } )
}.unzip
if (toRemove.nonEmpty) {
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 3b6df4524..9f379108f 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -68,7 +68,7 @@ case object ADTInduction extends Rule("ADT Induction") {
val subPC = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable))), innerPC)
val subWS = substAll(Map(inductOn -> CaseClass(cct, newIds.map(Variable))), innerWS)
- val subPre = IsInstanceOf(cct, Variable(origId))
+ val subPre = IsInstanceOf(Variable(origId), cct)
val subProblem = Problem(inputs ::: residualArgs, subWS, andJoin(subPC :: postFs), subPhi, p.xs)
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 093897196..4a5adceed 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -82,7 +82,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
val newMap = trMap.mapValues(v => substAll(Map(id -> CaseClass(cct, subIds.map(Variable))), v))
- InductCase(newIds, newCalls, newPattern, and(pc, IsInstanceOf(cct, Variable(id))), newMap)
+ InductCase(newIds, newCalls, newPattern, and(pc, IsInstanceOf(Variable(id), cct)), newMap)
}
}).flatten
} else {
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 6485d3ffa..294c6e137 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -23,7 +23,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val optCases = for (dcd <- cd.knownDescendants.sortBy(_.id.name)) yield dcd match {
case ccd : CaseClassDef =>
val cct = CaseClassType(ccd, tpes)
- val toSat = and(p.pc, IsInstanceOf(cct, Variable(id)))
+ val toSat = and(p.pc, IsInstanceOf(Variable(id), cct))
val isImplied = solver.solveSAT(toSat) match {
case (Some(false), _) => true
@@ -86,7 +86,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val substs = (for ((field,arg) <- cct.fields zip problem.as ) yield {
(arg, caseClassSelector(cct, id.toVariable, field.id))
}).toMap
- globalPre ::= and(IsInstanceOf(cct, Variable(id)), replaceFromIDs(substs, sol.pre))
+ globalPre ::= and(IsInstanceOf(Variable(id), cct), replaceFromIDs(substs, sol.pre))
} else {
globalPre ::= BooleanLiteral(true)
}
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index c4acb5721..227dd691c 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -22,7 +22,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
val clauses = allClauses.filterNot(instanceOfs.toSet)
- val ccSubsts = for (IsInstanceOf(cct: CaseClassType, s) <- instanceOfs) yield {
+ val ccSubsts = for (IsInstanceOf(s, cct: CaseClassType) <- instanceOfs) yield {
val fieldsVals = (for (f <- cct.fields) yield {
val id = f.id
diff --git a/src/main/scala/leon/termination/SelfCallsProcessor.scala b/src/main/scala/leon/termination/SelfCallsProcessor.scala
index b8fe65f48..157dbce24 100644
--- a/src/main/scala/leon/termination/SelfCallsProcessor.scala
+++ b/src/main/scala/leon/termination/SelfCallsProcessor.scala
@@ -52,7 +52,7 @@ class SelfCallsProcessor(val checker: TerminationChecker) extends Processor {
case Not(expr: Expr) => rec(expr)
case Equals(lhs: Expr, rhs: Expr) => rec(lhs) || rec(rhs)
case CaseClass(ct, args: Seq[Expr]) => args.exists(arg => rec(arg))
- case IsInstanceOf(ct, expr: Expr) => rec(expr)
+ case IsInstanceOf(expr: Expr, ct) => rec(expr)
case AsInstanceOf(expr: Expr, ct) => rec(expr)
case CaseClassSelector(ct, caseClassExpr, selector) => rec(caseClassExpr)
case Plus(lhs: Expr, rhs: Expr) => rec(lhs) || rec(rhs)
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 05648fc9f..cb0f37ab5 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -35,7 +35,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
fd.precondition = {
val argTypesPreconditions = fd.params.flatMap(arg => arg.getType match {
case cct: ClassType if cct.parent.isDefined =>
- Seq(IsInstanceOf(cct, arg.id.toVariable))
+ Seq(IsInstanceOf(arg.id.toVariable, cct))
case at: ArrayType =>
Seq(GreaterEquals(ArrayLength(arg.id.toVariable), IntLiteral(0)))
case _ =>
@@ -57,7 +57,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
case Some(p) =>
Some(Lambda(Seq(ValDef(resId)), and(
application(p, Seq(Variable(resId))),
- IsInstanceOf(ct, Variable(resId))
+ IsInstanceOf(Variable(resId), ct)
).setPos(p)).setPos(p))
case None =>
@@ -65,7 +65,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
case Some(df: DefinedPosition) => df.focusEnd
case _ => NoPosition
}
- Some(Lambda(Seq(ValDef(resId)), IsInstanceOf(ct, Variable(resId))).setPos(pos))
+ Some(Lambda(Seq(ValDef(resId)), IsInstanceOf(Variable(resId), ct)).setPos(pos))
}
}
case _ => fd.postcondition
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 9e06e4abd..74b7b99af 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -40,7 +40,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
val vc = implies(
- and(IsInstanceOf(cct, arg.toVariable), precOrTrue(fd)),
+ and(IsInstanceOf(arg.toVariable, cct), precOrTrue(fd)),
implies(andJoin(subCases), application(post, Seq(body)))
)
@@ -77,7 +77,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
val vc = implies(
- andJoin(Seq(IsInstanceOf(cct, arg.toVariable), precOrTrue(fd), path) ++ subCases),
+ andJoin(Seq(IsInstanceOf(arg.toVariable, cct), precOrTrue(fd), path) ++ subCases),
tfd.withParamSubst(args, pre)
)
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 871662815..8244da31a 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -36,7 +36,7 @@ object InjectAsserts extends LeonPhase[Program, Program] {
Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
case e @ AsInstanceOf(expr, ct) =>
- Some(Assert(IsInstanceOf(ct, expr),
+ Some(Assert(IsInstanceOf(expr, ct),
Some("Cast error"),
e
).setPos(e))
diff --git a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
index 5d8867550..57f37ed34 100644
--- a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
@@ -18,7 +18,6 @@ class TypeOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
val tp2 = TypeParameter.fresh("A")
val tp3 = TypeParameter.fresh("B")
- val tp4 = TypeParameter.fresh("C")
val listD = AbstractClassDef(FreshIdentifier("List"), Seq(tpD), None)
val listT = listD.typed
@@ -58,6 +57,8 @@ class TypeOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
assert(canBeSubtypeOf(tp, Seq(tp2), tp2, rhsFixed = true).isEmpty, "T </: A with A free but lhs is fixed")
assert(canBeSubtypeOf(listT, Seq(tp), listD.typed(Seq(tp2)), rhsFixed = true).isDefined, "List[T] <: List[A] with T free and rhs fixed")
+
+ assert(isSubtypeOf(listD.typed, listD.typed), "List[T] <: List[T]")
}
}
--
GitLab