Fix canBeSubtypeOf

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
       }
     }
   }

src/test/scala/leon/test/purescala/TypeOpsSuite.scala

+/* 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")
+  }
+
+}