From b8da1b1481081bcdc1571ea69ce4321caaf3d0e3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 19 Aug 2015 16:03:07 +0200
Subject: [PATCH] Fix canBeSubtypeOf
---
src/main/scala/leon/purescala/TypeOps.scala | 33 +++-------
.../leon/test/purescala/TypeOpsSuite.scala | 63 +++++++++++++++++++
2 files changed, 73 insertions(+), 23 deletions(-)
create mode 100644 src/test/scala/leon/test/purescala/TypeOpsSuite.scala
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 05317ca8f..0eac83d63 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -24,9 +24,9 @@ object TypeOps {
def canBeSubtypeOf(
tpe: TypeTree,
- freeParams: Seq[TypeParameter],
+ freeParams: Seq[TypeParameter],
stpe: TypeTree,
- lhsFixed: Boolean = false,
+ lhsFixed: Boolean = false,
rhsFixed: Boolean = false
): Option[Map[TypeParameter, TypeTree]] = {
@@ -55,23 +55,14 @@ object TypeOps {
}
} else {
(tpe, stpe) match {
- case (t, tp1: TypeParameter) =>
- if ((freeParams contains tp1) && (!rhsFixed) && !(typeParamsOf(t) contains tp1)) {
- Some(Map(tp1 -> t))
- } else if (tp1 == t) {
- Some(Map())
- } else {
- None
- }
+ case (t1, t2) if t1 == t2 =>
+ Some(Map())
- case (tp1: TypeParameter, t) =>
- if ((freeParams contains tp1) && (!lhsFixed) && !(typeParamsOf(t) contains tp1)) {
- Some(Map(tp1 -> t))
- } else if (tp1 == t) {
- Some(Map())
- } else {
- None
- }
+ case (t, tp1: TypeParameter) if (freeParams contains tp1) && (!rhsFixed) && !(typeParamsOf(t) contains tp1) =>
+ Some(Map(tp1 -> t))
+
+ case (tp1: TypeParameter, t) if (freeParams contains tp1) && (!lhsFixed) && !(typeParamsOf(t) contains tp1) =>
+ Some(Map(tp1 -> t))
case (ct1: ClassType, ct2: ClassType) =>
val rt1 = ct1.root
@@ -103,11 +94,7 @@ object TypeOps {
}
case (t1, t2) =>
- if (t1 == t2) {
- Some(Map())
- } else {
- None
- }
+ None
}
}
}
diff --git a/src/test/scala/leon/test/purescala/TypeOpsSuite.scala b/src/test/scala/leon/test/purescala/TypeOpsSuite.scala
new file mode 100644
index 000000000..af9edfec0
--- /dev/null
+++ b/src/test/scala/leon/test/purescala/TypeOpsSuite.scala
@@ -0,0 +1,63 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+import leon.purescala.Common._
+import leon.purescala.Expressions._
+import leon.purescala.Definitions._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
+import leon.purescala.TypeOps._
+
+class TypeOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.ExpressionsDSL {
+
+ test("canBeSubtypeOf 1") { ctx =>
+ val tp = TypeParameter.fresh("T")
+ val tpD = new TypeParameterDef(tp)
+
+ 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
+
+ val nilD = CaseClassDef(FreshIdentifier("Nil"), Seq(tpD), Some(listT), false)
+ val nilT = nilD.typed
+
+ val consD = CaseClassDef(FreshIdentifier("Cons"), Seq(tpD), Some(listT), false)
+ val consT = consD.typed
+
+ // Simple tests for fixed types
+ assert(canBeSubtypeOf(tp, Seq(), tp).isDefined, "Same types can be subtypes")
+ assert(canBeSubtypeOf(listT, Seq(), listT).isDefined, "Different types are not subtypes")
+
+ assert(canBeSubtypeOf(tp2, Seq(), tp3).isEmpty, "Different types are not subtypes")
+ assert(canBeSubtypeOf(BooleanType, Seq(), tp3).isEmpty, "Different types are not subtypes")
+ assert(canBeSubtypeOf(tp2, Seq(), BooleanType).isEmpty, "Different types are not subtypes")
+ assert(canBeSubtypeOf(IntegerType, Seq(), Int32Type).isEmpty, "Different types are not subtypes")
+
+ assert(canBeSubtypeOf(nilT, Seq(), listT).isDefined, "Subtypes are subtypes")
+ assert(canBeSubtypeOf(consT, Seq(), listT).isDefined, "Subtypes are subtypes")
+
+ assert(canBeSubtypeOf(listT, Seq(), nilT).isEmpty, "Supertypes are not subtypes")
+ assert(canBeSubtypeOf(listT, Seq(), consT).isEmpty, "Supertypes are not subtypes")
+
+ // Type parameters
+ assert(canBeSubtypeOf(tp, Seq(tp), tp2).isDefined, "T <: A with T free")
+ assert(canBeSubtypeOf(tp, Seq(tp2), tp2).isDefined, "T <: A with A free")
+
+ assert(canBeSubtypeOf(listT, Seq(tp), listD.typed(Seq(tp2))).isDefined, "List[T] <: List[A] with T free")
+ assert(canBeSubtypeOf(listT, Seq(tp2), listD.typed(Seq(tp2))).isDefined, "List[T] <: List[A] with A free")
+
+ // Type parameters with fixed sides
+ assert(canBeSubtypeOf(tp, Seq(tp), tp2, lhsFixed = true).isEmpty, "T </: A with T free when lhs is fixed")
+ assert(canBeSubtypeOf(tp, Seq(tp), tp2, rhsFixed = true).isDefined, "T <: A with T free but rhs is fixed")
+ assert(canBeSubtypeOf(tp, Seq(tp2), tp2, lhsFixed = true).isDefined, "T <: A with A free when lhs is fixed")
+ 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")
+ }
+
+}
--
GitLab