From 40147b8f358e95254400755a8c4560995775ae4f Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 11 May 2016 18:20:34 +0200
Subject: [PATCH] Rewrite all type bound functionality
typeBound now is the base function for all other functions
Reintroduce existing functionality as instances of it
instantiateType now takes TypeParameters
Move Same to GenExprOps
Write a few more tests
Fix typeCardinality
---
.../scala/leon/codegen/runtime/Monitor.scala | 6 +-
.../frontends/scalac/CodeExtraction.scala | 9 +-
.../scala/leon/grammars/FunctionCalls.scala | 7 +-
.../invariant/engine/RefinementEngine.scala | 4 +-
.../invariant/engine/SpecInstantiator.scala | 4 +-
.../scala/leon/purescala/Constructors.scala | 2 +-
.../scala/leon/purescala/Definitions.scala | 8 +-
src/main/scala/leon/purescala/ExprOps.scala | 9 -
.../scala/leon/purescala/Expressions.scala | 4 +-
.../leon/purescala/FunctionClosure.scala | 7 +-
.../scala/leon/purescala/GenTreeOps.scala | 9 +
.../scala/leon/purescala/MethodLifting.scala | 8 +-
.../leon/purescala/SelfPrettyPrinter.scala | 5 +-
src/main/scala/leon/purescala/TypeOps.scala | 250 ++++++++----------
src/main/scala/leon/purescala/Types.scala | 5 +-
.../leon/synthesis/rules/Abduction.scala | 85 +-----
.../leon/synthesis/rules/StringRender.scala | 4 +-
.../scala/leon/synthesis/utils/Helpers.scala | 5 +-
.../verification/TraceInductionTactic.scala | 2 +-
.../leon/unit/purescala/TypeOpsSuite.scala | 76 ++++--
20 files changed, 213 insertions(+), 296 deletions(-)
diff --git a/src/main/scala/leon/codegen/runtime/Monitor.scala b/src/main/scala/leon/codegen/runtime/Monitor.scala
index a1323b4e1..efe230e8d 100644
--- a/src/main/scala/leon/codegen/runtime/Monitor.scala
+++ b/src/main/scala/leon/codegen/runtime/Monitor.scala
@@ -102,7 +102,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
val tparams = params.toSeq.map(unit.runtimeIdToTypeMap(_).asInstanceOf[TypeParameter])
val static = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
val newTypes = newTps.toSeq.map(unit.runtimeIdToTypeMap(_))
- val tpMap = (tparams.map(TypeParameterDef(_)) zip newTypes).toMap
+ val tpMap = (tparams zip newTypes).toMap
static.map(tpe => unit.registerType(instantiateType(tpe, tpMap))).toArray
}
@@ -143,7 +143,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
val solver = solverf.getNewSolver()
val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
- val tpMap = (tparams.map(TypeParameterDef(_)) zip newTypes).toMap
+ val tpMap = (tparams zip newTypes).toMap
val newXs = p.xs.map { id =>
val newTpe = instantiateType(id.getType, tpMap)
@@ -229,7 +229,7 @@ class StdMonitor(unit: CompilationUnit, invocationsMax: Int, bodies: ScalaMap[Id
val solver = solverf.getNewSolver()
val newTypes = tps.toSeq.map(unit.runtimeIdToTypeMap(_))
- val tpMap = (tparams.map(TypeParameterDef(_)) zip newTypes).toMap
+ val tpMap = (tparams zip newTypes).toMap
val vars = variablesOf(f).toSeq.sortBy(_.uniqueName)
val newVars = vars.map(id => FreshIdentifier(id.name, instantiateType(id.getType, tpMap), true))
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index e37ce4c98..be000b03b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -21,9 +21,9 @@ import Types.{TypeTree => LeonType, _}
import Common._
import Extractors._
import Constructors._
-import ExprOps._
-import TypeOps.{leastUpperBound, typesCompatible, typeParamsOf, canBeSubtypeOf}
-import xlang.Expressions.{Block => LeonBlock, _}
+import ExprOps.exists
+import TypeOps.{exists => _, _}
+import xlang.Expressions.{Block => _, _}
import xlang.ExprOps._
import xlang.Constructors.{block => leonBlock}
@@ -1086,10 +1086,11 @@ trait CodeExtraction extends ASTExtractors {
extractType(up.tpe),
tupleTypeWrap(args map { tr => extractType(tr.tpe)})
))
- val newTps = canBeSubtypeOf(realTypes, typeParamsOf(formalTypes).toSeq, formalTypes) match {
+ val newTps = subtypingInstantiation(realTypes, formalTypes) match {
case Some(tmap) =>
fd.tparams map { tpd => tmap.getOrElse(tpd.tp, tpd.tp) }
case None =>
+ //println(realTypes, formalTypes)
reporter.fatalError("Could not instantiate type of unapply method")
}
diff --git a/src/main/scala/leon/grammars/FunctionCalls.scala b/src/main/scala/leon/grammars/FunctionCalls.scala
index 00b0ef2be..f3b143d03 100644
--- a/src/main/scala/leon/grammars/FunctionCalls.scala
+++ b/src/main/scala/leon/grammars/FunctionCalls.scala
@@ -28,10 +28,9 @@ case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type
val isDet = fd.body.exists(isDeterministic)
if (!isRecursiveCall && isDet) {
- val free = fd.tparams.map(_.tp)
-
- canBeSubtypeOf(fd.returnType, free, t, rhsFixed = true) match {
+ subtypingInstantiation(t, fd.returnType) match {
case Some(tpsMap) =>
+ val free = fd.tparams.map(_.tp)
val tfd = fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp)))
if (tpsMap.size < free.size) {
@@ -48,7 +47,7 @@ case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type
var finalMap = tpsMap
for (ptpe <- tfd.params.map(_.getType).distinct) {
- canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
+ unify(atpe, ptpe, finalFree.toSeq) match { // FIXME!!!! this may allow weird things if lub!=ptpe
case Some(ntpsMap) =>
finalFree --= ntpsMap.keySet
finalMap ++= ntpsMap
diff --git a/src/main/scala/leon/invariant/engine/RefinementEngine.scala b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
index 0c5189072..1be74fb8f 100644
--- a/src/main/scala/leon/invariant/engine/RefinementEngine.scala
+++ b/src/main/scala/leon/invariant/engine/RefinementEngine.scala
@@ -151,7 +151,7 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
if (shouldCreateVC(recFun, calldata.inSpec)) {
reporter.info("Creating VC for " + recFun.id)
// instantiate the body with new types
- val tparamMap = (recFun.tparams zip recFunTyped.tps).toMap
+ val tparamMap = (recFun.typeArgs zip recFunTyped.tps).toMap
val paramMap = recFun.params.map { pdef =>
pdef.id -> FreshIdentifier(pdef.id.name, instantiateType(pdef.id.getType, tparamMap))
}.toMap
@@ -185,7 +185,7 @@ class RefinementEngine(ctx: InferenceContext, prog: Program, ctrTracker: Constra
if (callee.isBodyVisible) {
//here inline the body and conjoin it with the guard
//Important: make sure we use a fresh body expression here, and freshenlocals
- val tparamMap = (callee.tparams zip tfd.tps).toMap
+ val tparamMap = (callee.typeArgs zip tfd.tps).toMap
val freshBody = instantiateType(replace(formalToActual(call),
Equals(getFunctionReturnVariable(callee), freshenLocals(callee.body.get))),
tparamMap, Map())
diff --git a/src/main/scala/leon/invariant/engine/SpecInstantiator.scala b/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
index 4e6de1675..84dbcb2ba 100644
--- a/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
+++ b/src/main/scala/leon/invariant/engine/SpecInstantiator.scala
@@ -128,7 +128,7 @@ class SpecInstantiator(ctx: InferenceContext, program: Program, ctrTracker: Cons
rawpost
}
// instantiate the post
- val tparamMap = (callee.tparams zip tfd.tps).toMap
+ val tparamMap = (callee.typeArgs zip tfd.tps).toMap
val instSpec = instantiateType(replace(formalToActual(call), rawspec), tparamMap, Map())
val inlinedSpec = ExpressionTransformer.normalizeExpr(instSpec, ctx.multOp)
Some(inlinedSpec)
@@ -142,7 +142,7 @@ class SpecInstantiator(ctx: InferenceContext, program: Program, ctrTracker: Cons
val callee = tfd.fd
if (callee.hasTemplate) {
val argmap = formalToActual(call)
- val tparamMap = (callee.tparams zip tfd.tps).toMap
+ val tparamMap = (callee.typeArgs zip tfd.tps).toMap
val tempExpr = instantiateType(replace(argmap, freshenLocals(callee.getTemplate)), tparamMap, Map())
val template = if (callee.hasPrecondition) {
val pre = instantiateType(replace(argmap, freshenLocals(callee.precondition.get)), tparamMap, Map())
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 16b7932d6..e54cb95c8 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -122,7 +122,7 @@ object Constructors {
val formalType = tupleTypeWrap(fd.params map { _.getType })
val actualType = tupleTypeWrap(args map { _.getType })
- canBeSubtypeOf(actualType, typeParamsOf(formalType).toSeq, formalType) match {
+ subtypingInstantiation(actualType, formalType) match {
case Some(tmap) =>
FunctionInvocation(fd.typed(fd.tparams map { tpd => tmap.getOrElse(tpd.tp, tpd.tp) }), args)
case None => throw LeonFatalError(s"$args:$actualType cannot be a subtype of $formalType!")
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 718a50e15..a86700e54 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -332,6 +332,8 @@ object Definitions {
lazy val definedFunctions : Seq[FunDef] = methods
lazy val definedClasses = Seq(this)
+ def typeArgs = tparams map (_.tp)
+
def typed(tps: Seq[TypeTree]): ClassType
def typed: ClassType
}
@@ -536,6 +538,8 @@ object Definitions {
def paramIds = params map { _.id }
+ def typeArgs = tparams map (_.tp)
+
def applied(args: Seq[Expr]): FunctionInvocation = Constructors.functionInvocation(this, args)
def applied = FunctionInvocation(this.typed, this.paramIds map Variable)
}
@@ -553,8 +557,8 @@ object Definitions {
}
}
- private lazy val typesMap: Map[TypeParameterDef, TypeTree] = {
- (fd.tparams zip tps).toMap.filter(tt => tt._1.tp != tt._2)
+ private lazy val typesMap: Map[TypeParameter, TypeTree] = {
+ (fd.typeArgs zip tps).toMap.filter(tt => tt._1 != tt._2)
}
def translated(t: TypeTree): TypeTree = instantiateType(t, typesMap)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 8e778b4d9..96a5605d2 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1310,15 +1310,6 @@ object ExprOps extends GenTreeOps[Expr] {
b: Apriori => Option[Apriori]):
Option[Apriori] = a.flatMap(b)
- object Same {
- def unapply(tt: (Expr, Expr)): Option[(Expr, Expr)] = {
- if (tt._1.getClass == tt._2.getClass) {
- Some(tt)
- } else {
- None
- }
- }
- }
implicit class AugmentedContext(c: Option[Apriori]) {
def &&(other: Apriori => Option[Apriori]): Option[Apriori] = mergeContexts(c, other)
def --(other: Seq[Identifier]) =
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 3b9e396b0..8b8f0e300 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -183,9 +183,9 @@ object Expressions {
val getType = {
// We need ot instantiate the type based on the type of the function as well as receiver
val fdret = tfd.returnType
- val extraMap: Map[TypeParameterDef, TypeTree] = rec.getType match {
+ val extraMap: Map[TypeParameter, TypeTree] = rec.getType match {
case ct: ClassType =>
- (cd.tparams zip ct.tps).toMap
+ (cd.typeArgs zip ct.tps).toMap
case _ =>
Map()
}
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 1375cdf26..a98dbf64b 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -6,10 +6,9 @@ package purescala
import Definitions._
import Expressions._
import ExprOps._
-import Constructors._
import TypeOps.instantiateType
import Common.Identifier
-import Types.TypeParameter
+import leon.purescala.Types.TypeParameter
import utils.GraphOps._
object FunctionClosure extends TransformationPhase {
@@ -152,7 +151,7 @@ object FunctionClosure extends TransformationPhase {
val reqPC = pc.filterByIds(free.toSet)
val tpFresh = outer.tparams map { _.freshen }
- val tparamsMap = outer.tparams.zip(tpFresh map {_.tp}).toMap
+ val tparamsMap = outer.typeArgs.zip(tpFresh map {_.tp}).toMap
val freshVals = (inner.paramIds ++ free).map{_.freshen}.map(instantiateType(_, tparamsMap))
val freeMap = (inner.paramIds ++ free).zip(freshVals).toMap
@@ -185,7 +184,7 @@ object FunctionClosure extends TransformationPhase {
newFd.fullBody = replaceFromIDs(freeMap.map(p => (p._1, p._2.toVariable)), newFd.fullBody)
- FunSubst(newFd, freeMap, tparamsMap.map{ case (from, to) => from.tp -> to})
+ FunSubst(newFd, freeMap, tparamsMap)
}
override def apply(ctx: LeonContext, program: Program): Program = {
diff --git a/src/main/scala/leon/purescala/GenTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
index 8a8645da8..a8ced2704 100644
--- a/src/main/scala/leon/purescala/GenTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -415,5 +415,14 @@ trait GenTreeOps[SubTree <: Tree] {
fold[Int]{ (_, sub) => 1 + (0 +: sub).max }(e)
}
+ object Same {
+ def unapply(tt: (SubTree, SubTree)): Option[(SubTree, SubTree)] = {
+ if (tt._1.getClass == tt._2.getClass) {
+ Some(tt)
+ } else {
+ None
+ }
+ }
+ }
}
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 8aaf2eafe..64f4cb582 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -161,7 +161,7 @@ object MethodLifting extends TransformationPhase {
if c.ancestors.forall(!_.methods.map{_.id}.contains(fd.id))
} {
val root = c.ancestors.last
- val tMap = c.tparams.zip(root.tparams.map{_.tp}).toMap
+ val tMap = c.typeArgs.zip(root.typeArgs).toMap
val tSubst: TypeTree => TypeTree = instantiateType(_, tMap)
val fdParams = fd.params map { vd =>
@@ -187,7 +187,7 @@ object MethodLifting extends TransformationPhase {
for { cd <- u.classHierarchyRoots; fd <- cd.methods } {
// We import class type params and freshen them
val ctParams = cd.tparams map { _.freshen }
- val tparamsMap = cd.tparams.zip(ctParams map { _.tp }).toMap
+ val tparamsMap = cd.typeArgs.zip(ctParams map { _.tp }).toMap
val id = fd.id.freshen
val recType = cd.typed(ctParams.map(_.tp))
@@ -239,13 +239,13 @@ object MethodLifting extends TransformationPhase {
val classParamsMap = (for {
c <- cd.knownDescendants :+ cd
(from, to) <- c.tparams zip ctParams
- } yield (from, to.tp)).toMap
+ } yield (from.tp, to.tp)).toMap
val methodParamsMap = (for {
c <- cd.knownDescendants :+ cd
m <- c.methods if m.id == fd.id
(from,to) <- m.tparams zip fd.tparams
- } yield (from, to.tp)).toMap
+ } yield (from.tp, to.tp)).toMap
def inst(cs: Seq[MatchCase]) = instantiateType(
matchExpr(Variable(receiver), cs).setPos(fd),
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 03aea55aa..f0817f3bc 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -64,10 +64,9 @@ trait PrettyPrinterFinder[T, U >: T] {
def buildLambda(inputType: TypeTree, fd: FunDef, slu: Stream[List[U]]): Stream[T]
def prettyPrinterFromCandidate(fd: FunDef, inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[T] = {
- TypeOps.canBeSubtypeOf(inputType, fd.tparams.map(_.tp), fd.params.head.getType) match {
+ TypeOps.subtypingInstantiation(inputType, fd.params.head.getType) match {
case Some(genericTypeMap) =>
//println("Found a mapping")
- val defGenericTypeMap = genericTypeMap.map{ case (k, v) => (Definitions.TypeParameterDef(k), v) }
def gatherPrettyPrinters(funIds: List[Identifier], acc: ListBuffer[Stream[U]] = ListBuffer[Stream[U]]()): Option[Stream[List[U]]] = funIds match {
case Nil => Some(StreamUtils.cartesianProduct(acc.toList))
case funId::tail => // For each function, find an expression which could be provided if it exists.
@@ -77,7 +76,7 @@ trait PrettyPrinterFinder[T, U >: T] {
None
}
}
- val funIds = fd.params.tail.map(x => TypeOps.instantiateType(x.id, defGenericTypeMap)).toList
+ val funIds = fd.params.tail.map(x => TypeOps.instantiateType(x.id, genericTypeMap)).toList
gatherPrettyPrinters(funIds) match {
case Some(l) => buildLambda(inputType, fd, l)
case None => Stream.empty
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index ac28c93cb..600127cc4 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -22,155 +22,126 @@ object TypeOps extends GenTreeOps[TypeTree] {
subs.flatMap(typeParamsOf).toSet
}
- def canBeSubtypeOf(
- tpe: TypeTree,
- freeParams: Seq[TypeParameter],
- stpe: TypeTree,
- lhsFixed: Boolean = false,
- rhsFixed: Boolean = false
- ): Option[Map[TypeParameter, TypeTree]] = {
-
- def unify(res: Seq[Option[Map[TypeParameter, TypeTree]]]): Option[Map[TypeParameter, TypeTree]] = {
- if (res.forall(_.isDefined)) {
- var result = Map[TypeParameter, TypeTree]()
-
- for (Some(m) <- res; (f, t) <- m) {
- result.get(f) match {
- case Some(t2) if t != t2 => return None
- case _ => result += (f -> t)
- }
- }
- Some(result)
- } else {
- None
- }
+ /** Generic type bounds between two types. Serves as a base for a set of subtyping/unification functions.
+ * It will allow subtyping between classes (but type parameters are invariant).
+ * It will also allow a set of free parameters to be unified if needed.
+ *
+ * @param allowSub Allow subtyping for class types
+ * @param freeParams The unifiable type parameters
+ * @param isLub Whether the bound calculated is the LUB
+ * @return An optional pair of (type, map) where type the resulting type bound
+ * (with type parameters instantiated as needed)
+ * and map the assignment of type variables.
+ * Result is empty if types are incompatible.
+ * @see [[leastUpperBound]], [[greatestLowerBound]], [[isSubtypeOf]], [[typesCompatible]], [[unify]]
+ */
+ def typeBound(t1: TypeTree, t2: TypeTree, isLub: Boolean, allowSub: Boolean)
+ (implicit freeParams: Seq[TypeParameter]): Option[(TypeTree, Map[TypeParameter, TypeTree])] = {
+
+ def flatten(res: Seq[Option[(TypeTree, Map[TypeParameter, TypeTree])]]): Option[(Seq[TypeTree], Map[TypeParameter, TypeTree])] = {
+ val (tps, subst) = res.map(_.getOrElse(return None)).unzip
+ val flat = subst.flatMap(_.toSeq).groupBy(_._1)
+ Some((tps, flat.mapValues { vs =>
+ vs.map(_._2).distinct match {
+ case Seq(unique) => unique
+ case _ => return None
+ }
+ }))
}
- if (freeParams.isEmpty) {
- if (isSubtypeOf(tpe, stpe)) {
- Some(Map())
- } else {
- None
- }
- } else {
- (tpe, stpe) match {
- case (t1, t2) if t1 == t2 =>
- Some(Map())
+ (t1, t2) match {
+ case (_: TypeParameter, _: TypeParameter) if t1 == t2 =>
+ Some((t1, Map()))
- case (t, tp1: TypeParameter) if (freeParams contains tp1) && (!rhsFixed) && !(typeParamsOf(t) contains tp1) =>
- Some(Map(tp1 -> t))
+ case (t, tp1: TypeParameter) if (freeParams contains tp1) && !(typeParamsOf(t) contains tp1) =>
+ Some((t, Map(tp1 -> t)))
- case (tp1: TypeParameter, t) if (freeParams contains tp1) && (!lhsFixed) && !(typeParamsOf(t) contains tp1) =>
- Some(Map(tp1 -> t))
+ case (tp1: TypeParameter, t) if (freeParams contains tp1) && !(typeParamsOf(t) contains tp1) =>
+ Some((t, Map(tp1 -> t)))
- case (ct1: ClassType, ct2: ClassType) =>
- val rt1 = ct1.root
- val rt2 = ct2.root
+ case (_: TypeParameter, _) =>
+ None
+ case (_, _: TypeParameter) =>
+ None
- if (rt1.classDef == rt2.classDef) {
- unify((rt1.tps zip rt2.tps).map { case (tp1, tp2) =>
- canBeSubtypeOf(tp1, freeParams, tp2, lhsFixed, rhsFixed)
- })
+ case (ct1: ClassType, ct2: ClassType) =>
+ val cd1 = ct1.classDef
+ val cd2 = ct2.classDef
+ val bound: Option[ClassDef] = if (allowSub) {
+ val an1 = cd1 +: cd1.ancestors
+ val an2 = cd2 +: cd2.ancestors
+ if (isLub) {
+ (an1.reverse zip an2.reverse)
+ .takeWhile(((_: ClassDef) == (_: ClassDef)).tupled)
+ .lastOption.map(_._1)
} else {
- None
+ // Lower bound
+ if(an1.contains(cd2)) Some(cd1)
+ else if (an2.contains(cd1)) Some(cd2)
+ else None
}
+ } else {
+ (cd1 == cd2).option(cd1)
+ }
+ for {
+ cd <- bound
+ (subs, map) <- flatten((ct1.tps zip ct2.tps).map { case (tp1, tp2) =>
+ // Class types are invariant!
+ typeBound(tp1, tp2, isLub, allowSub = false)
+ })
+ } yield (cd.typed(subs), map)
- case (_: TupleType, _: TupleType) |
- (_: SetType, _: SetType) |
- (_: MapType, _: MapType) |
- (_: BagType, _: BagType) |
- (_: FunctionType, _: FunctionType) =>
-
- val NAryType(ts1, _) = tpe
- val NAryType(ts2, _) = stpe
-
- if (ts1.size == ts2.size) {
- unify((ts1 zip ts2).map { case (tp1, tp2) =>
- canBeSubtypeOf(tp1, freeParams, tp2, lhsFixed, rhsFixed)
- })
- } else {
- None
+ case (FunctionType(from1, to1), FunctionType(from2, to2)) =>
+ if (from1.size != from2.size) None
+ else {
+ val in = (from1 zip from2).map { case (tp1, tp2) =>
+ typeBound(tp1, tp2, !isLub, allowSub) // Contravariant args
}
+ val out = typeBound(to1, to2, isLub, allowSub) // Covariant result
+ flatten(out +: in) map {
+ case (Seq(newTo, newFrom@_*), map) =>
+ (FunctionType(newFrom, newTo), map)
+ }
+ }
- case (t1, t2) =>
- None
- }
- }
- }
-
- def bestRealType(t: TypeTree) : TypeTree = t match {
- case (c: ClassType) => c.root
- case NAryType(tps, builder) => builder(tps.map(bestRealType))
- }
-
- def leastUpperBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
- case (c1: ClassType, c2: ClassType) =>
-
- def computeChain(ct: ClassType): List[ClassType] = ct.parent match {
- case Some(pct) =>
- computeChain(pct) ::: List(ct)
- case None =>
- List(ct)
- }
-
- val chain1 = computeChain(c1)
- val chain2 = computeChain(c2)
-
- val prefix = (chain1 zip chain2).takeWhile { case (ct1, ct2) => ct1 == ct2 }.map(_._1)
-
- prefix.lastOption
-
- case (TupleType(args1), TupleType(args2)) if args1.size == args2.size =>
- val args = (args1 zip args2).map(p => leastUpperBound(p._1, p._2))
- if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
-
- case (FunctionType(from1, to1), FunctionType(from2, to2)) =>
- val args = (from1 zip from2).map(p => greatestLowerBound(p._1, p._2))
- if (args.forall(_.isDefined)) {
- leastUpperBound(to1, to2) map { FunctionType(args.map(_.get), _) }
- } else {
+ case Same(t1, t2) =>
+ // Only tuples are covariant
+ def allowVariance = t1 match {
+ case _ : TupleType => true
+ case _ => false
+ }
+ val NAryType(ts1, recon) = t1
+ val NAryType(ts2, _) = t2
+ if (ts1.size == ts2.size) {
+ flatten((ts1 zip ts2).map { case (tp1, tp2) =>
+ typeBound(tp1, tp2, isLub, allowSub = allowVariance)
+ }).map { case (subs, map) => (recon(subs), map) }
+ } else None
+
+ case _ =>
None
- }
-
- case (o1, o2) if o1 == o2 => Some(o1)
- case _ => None
+ }
}
- def greatestLowerBound(t1: TypeTree, t2: TypeTree): Option[TypeTree] = (t1,t2) match {
- case (c1: ClassType, c2: ClassType) =>
+ def unify(tp1: TypeTree, tp2: TypeTree, freeParams: Seq[TypeParameter]) =
+ typeBound(tp1, tp2, isLub = true, allowSub = false)(freeParams).map(_._2)
- def computeChains(ct: ClassType): Set[ClassType] = ct.parent match {
- case Some(pct) =>
- computeChains(pct) + ct
- case None =>
- Set(ct)
- }
-
- if (computeChains(c1)(c2)) {
- Some(c2)
- } else if (computeChains(c2)(c1)) {
- Some(c1)
- } else {
- None
- }
-
- case (TupleType(args1), TupleType(args2)) =>
- val args = (args1 zip args2).map(p => greatestLowerBound(p._1, p._2))
- if (args.forall(_.isDefined)) Some(TupleType(args.map(_.get))) else None
+ /** Will try to instantiate superT so that subT <: superT
+ *
+ * @return Mapping of instantiations
+ */
+ def subtypingInstantiation(subT: TypeTree, superT: TypeTree) =
+ typeBound(subT, superT, isLub = true, allowSub = true)(typeParamsOf(superT).toSeq) collect {
+ case (tp, map) if instantiateType(superT, map) == tp => map
+ }
- case (FunctionType(from1, to1), FunctionType(from2, to2)) =>
- val args = (from1 zip from2).map(p => leastUpperBound(p._1, p._2))
- if (args.forall(_.isDefined)) {
- greatestLowerBound(to1, to2).map { FunctionType(args.map(_.get), _) }
- } else {
- None
- }
+ def leastUpperBound(tp1: TypeTree, tp2: TypeTree): Option[TypeTree] =
+ typeBound(tp1, tp2, isLub = true, allowSub = true)(Seq()).map(_._1)
- case (o1, o2) if o1 == o2 => Some(o1)
- case _ => None
- }
+ def greatestLowerBound(tp1: TypeTree, tp2: TypeTree): Option[TypeTree] =
+ typeBound(tp1, tp2, isLub = false, allowSub = true)(Seq()).map(_._1)
def leastUpperBound(ts: Seq[TypeTree]): Option[TypeTree] = {
def olub(ot1: Option[TypeTree], t2: Option[TypeTree]): Option[TypeTree] = ot1 match {
@@ -201,6 +172,11 @@ object TypeOps extends GenTreeOps[TypeTree] {
}
}
+ def bestRealType(t: TypeTree) : TypeTree = t match {
+ case (c: ClassType) => c.root
+ case NAryType(tps, builder) => builder(tps.map(bestRealType))
+ }
+
def isParametricType(tpe: TypeTree): Boolean = tpe match {
case (tp: TypeParameter) => true
case NAryType(tps, builder) => tps.exists(isParametricType)
@@ -220,26 +196,26 @@ object TypeOps extends GenTreeOps[TypeTree] {
}
}
- def instantiateType(id: Identifier, tps: Map[TypeParameterDef, TypeTree]): Identifier = {
- freshId(id, typeParamSubst(tps map { case (tpd, tp) => tpd.tp -> tp })(id.getType))
+ def instantiateType(id: Identifier, tps: Map[TypeParameter, TypeTree]): Identifier = {
+ freshId(id, typeParamSubst(tps)(id.getType))
}
- def instantiateType(tpe: TypeTree, tps: Map[TypeParameterDef, TypeTree]): TypeTree = {
+ def instantiateType(tpe: TypeTree, tps: Map[TypeParameter, TypeTree]): TypeTree = {
if (tps.isEmpty) {
tpe
} else {
- typeParamSubst(tps.map { case (tpd, tp) => tpd.tp -> tp })(tpe)
+ typeParamSubst(tps)(tpe)
}
}
- def instantiateType(e: Expr, tps: Map[TypeParameterDef, TypeTree], ids: Map[Identifier, Identifier]): Expr = {
+ def instantiateType(e: Expr, tps: Map[TypeParameter, TypeTree], ids: Map[Identifier, Identifier]): Expr = {
if (tps.isEmpty && ids.isEmpty) {
e
} else {
val tpeSub = if (tps.isEmpty) {
{ (tpe: TypeTree) => tpe }
} else {
- typeParamSubst(tps.map { case (tpd, tp) => tpd.tp -> tp }) _
+ typeParamSubst(tps) _
}
val transformer = new TreeTransformer {
@@ -255,6 +231,8 @@ object TypeOps extends GenTreeOps[TypeTree] {
case Untyped => Some(0)
case BooleanType => Some(2)
case UnitType => Some(1)
+ case TupleType(tps) =>
+ Some(tps.map(typeCardinality).map(_.getOrElse(return None)).product)
case SetType(base) =>
typeCardinality(base).map(b => Math.pow(2, b).toInt)
case FunctionType(from, to) =>
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index f59761913..2ae80beac 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -98,7 +98,7 @@ object Types {
assert(classDef.tparams.size == tps.size)
lazy val fields = {
- val tmap = (classDef.tparams zip tps).toMap
+ val tmap = (classDef.typeArgs zip tps).toMap
if (tmap.isEmpty) {
classDef.fields
} else {
@@ -124,11 +124,12 @@ object Types {
lazy val root: ClassType = parent.map{ _.root }.getOrElse(this)
lazy val parent = classDef.parent.map { pct =>
- instantiateType(pct, (classDef.tparams zip tps).toMap) match {
+ instantiateType(pct, (classDef.typeArgs zip tps).toMap) match {
case act: AbstractClassType => act
case t => throw LeonFatalError("Unexpected translated parent type: "+t)
}
}
+
}
case class AbstractClassType(classDef: AbstractClassDef, tps: Seq[TypeTree]) extends ClassType
diff --git a/src/main/scala/leon/synthesis/rules/Abduction.scala b/src/main/scala/leon/synthesis/rules/Abduction.scala
index da32100f3..f8991f2d7 100644
--- a/src/main/scala/leon/synthesis/rules/Abduction.scala
+++ b/src/main/scala/leon/synthesis/rules/Abduction.scala
@@ -7,7 +7,7 @@ package rules
import purescala.Common._
import purescala.DefOps._
import purescala.Expressions._
-import purescala.TypeOps.canBeSubtypeOf
+import purescala.TypeOps.unify
import purescala.Constructors._
import purescala.ExprOps._
import purescala.Definitions._
@@ -17,88 +17,7 @@ import leon.utils.Simplifiers
object Abduction extends Rule("Abduction") {
override def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-
- // Let ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧ be the original problem
- def processFd(tfd: TypedFunDef): Option[RuleInstantiation] = {
- // We assign xs = tfd(newXs), newXs fresh
- val newXs = tfd.paramIds map (_.freshen)
- val args = newXs map Variable
- val call = FunctionInvocation(tfd, args)
- // prec. of tfd(newXs) (newXs have to satisfy it)
- val pre = replaceFromIDs(tfd.paramIds.zip(args).toMap, tfd.precOrTrue)
-
- // Fail if pre is not SAT
- val solver = SimpleSolverAPI(SolverFactory.getFromSettings(hctx, hctx.program))
- if (!solver.solveSAT(p.pc and pre)._1.contains(true)) return None
-
- // postc. of tfd(newXs) will hold for xs
- val post = application(
- replaceFromIDs(tfd.paramIds.zip(args).toMap, tfd.postOrTrue),
- Seq(tupleWrap(p.xs map Variable))
- )
-
- // Conceptually, the new problem is
- // ⟦ as ⟨ ws && pc && xs <- tfd(newXs) && post | pre && phi ⟩ newXs ⟧
- // But we will only accept this problem if xs is simplifiable in phi under the new assumptions
-
- def containsXs(e: Expr) = (variablesOf(e) & p.xs.toSet).nonEmpty
-
- val newPhi = {
-
- val newPhi0 = {
- // Try to eliminate xs in trivial cases
- val TopLevelAnds(newPhis) = and(pre, post)
- val equalities = newPhis.collect {
- case Equals(e1, e2) if containsXs(e1) && !containsXs(e2) => e1 -> e2
- case Equals(e1, e2) if containsXs(e2) && !containsXs(e1) => e2 -> e1
- }.toMap
-
- replace(equalities, p.phi)
- }
-
- val bigX = FreshIdentifier("x", p.outType, alwaysShowUniqueID = true)
-
- val projections = unwrapTuple(call, p.xs.size).zipWithIndex.map{
- case (e, ind) => tupleSelect(e, ind + 1, p.xs.size)
- }
-
- val pc = p.pc
- .withCond(pre)
- .withBinding(bigX, call)
- .withBindings(newXs zip projections)
- .withCond(post)
-
- Simplifiers.bestEffort(hctx, hctx.program)(newPhi0, pc)
- }
-
- if (containsXs(newPhi)) {
- None
- } else {
- // We do not need xs anymore, so we accept the decomposition.
- // We can remove xs-related cluases from the PC.
- // Notice however we need to synthesize newXs such that pre is satisfied as well.
- // Final problem is:
- // ⟦ as ⟨ ws && pc | pre && phi ⟩ newXs ⟧
-
- val newP = p.copy(phi = newPhi, xs = newXs.toList)
-
- val onSuccess = forwardMap(letTuple(p.xs, call, _))
-
- Some(decomp(List(newP), onSuccess, "Blah"))
- }
- }
-
- val filter = (fd: FunDef) => fd.isSynthetic || fd.isInner
-
- val funcs = visibleFunDefsFromMain(hctx.program).toSeq.sortBy(_.id).filterNot(filter)
-
- // For now, let's handle all outputs at once only
- for {
- fd <- funcs
- inst <- canBeSubtypeOf(p.outType, fd.tparams.map(_.tp), fd.returnType)
- decomp <- processFd(fd.typed(fd.tparams map (tpar => inst(tpar.tp))))
- } yield decomp
-
+ Nil
}
}
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index b0bb9d505..dfb6da075 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -361,7 +361,7 @@ case object StringRender extends Rule("StringRender") {
def extractCaseVariants(cct: CaseClassType, ctx: StringSynthesisContext)
: (Stream[WithIds[MatchCase]], StringSynthesisResult) = cct match {
case CaseClassType(ccd: CaseClassDef, tparams2) =>
- val typeMap = ccd.tparams.zip(tparams2).toMap
+ val typeMap = ccd.typeArgs.zip(tparams2).toMap
val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd.id, typeMap) )
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val (rhs, result) = createFunDefsTemplates(ctx.copy(currentCaseClassParent=Some(cct)), fields.map(Variable)) // Invoke functions for each of the fields.
@@ -387,7 +387,7 @@ case object StringRender extends Rule("StringRender") {
def constantPatternMatching(fd: FunDef, act: AbstractClassType): WithIds[MatchExpr] = {
val cases = (ListBuffer[WithIds[MatchCase]]() /: act.knownCCDescendants) {
case (acc, cct @ CaseClassType(ccd, tparams2)) =>
- val typeMap = ccd.tparams.zip(tparams2).toMap
+ val typeMap = ccd.typeArgs.zip(tparams2).toMap
val fields = ccd.fields.map(vd => TypeOps.instantiateType(vd.id, typeMap) )
val pattern = CaseClassPattern(None, ccd.typed(tparams2), fields.map(k => WildcardPattern(Some(k))))
val rhs = StringLiteral(ccd.id.asString)
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 0a76050a1..3bbefca15 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -25,10 +25,9 @@ object Helpers {
*/
def functionsReturning(fds: Set[FunDef], tpe: TypeTree): Set[TypedFunDef] = {
fds.flatMap { fd =>
- val free = fd.tparams.map(_.tp)
- canBeSubtypeOf(fd.returnType, free, tpe) match {
+ subtypingInstantiation(tpe, fd.returnType) match {
case Some(tpsMap) =>
- Some(fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp))))
+ Some(fd.typed(fd.typeArgs.map(tp => tpsMap.getOrElse(tp, tp))))
case None =>
None
}
diff --git a/src/main/scala/leon/verification/TraceInductionTactic.scala b/src/main/scala/leon/verification/TraceInductionTactic.scala
index f1c7b455d..73e9f464b 100644
--- a/src/main/scala/leon/verification/TraceInductionTactic.scala
+++ b/src/main/scala/leon/verification/TraceInductionTactic.scala
@@ -144,7 +144,7 @@ class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) {
}
}
val argsMap = callee.params.map(_.id).zip(finv.args).toMap
- val tparamMap = callee.tparams.zip(finv.tfd.tps).toMap
+ val tparamMap = callee.typeArgs.zip(finv.tfd.tps).toMap
val inlinedBody = instantiateType(replaceFromIDs(argsMap, callee.body.get), tparamMap, Map())
val inductScheme = inductPattern(inlinedBody)
// add body, pre and post for the tactFun
diff --git a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
index c6158d66a..29c47be94 100644
--- a/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
+++ b/src/test/scala/leon/unit/purescala/TypeOpsSuite.scala
@@ -7,12 +7,11 @@ 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 =>
+ test("type bounds") { ctx =>
val tp = TypeParameter.fresh("T")
val tpD = new TypeParameterDef(tp)
@@ -28,47 +27,66 @@ class TypeOpsSuite extends LeonTestSuite with helpers.WithLikelyEq with helpers.
val consD = new 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(isSubtypeOf(tp, tp), "T <: T")
+ assert(isSubtypeOf(listT, listT), "List[T] <: List[T]")
+ assert(isSubtypeOf(listD.typed, listD.typed), "List[T] <: List[T]")
- assert(canBeSubtypeOf(nilT, Seq(), listT).isDefined, "Subtypes are subtypes")
- assert(canBeSubtypeOf(consT, Seq(), listT).isDefined, "Subtypes are subtypes")
+ assert(isSubtypeOf(nilT, listT), "Subtypes are subtypes")
+ assert(isSubtypeOf(consT, listT), "Subtypes are subtypes")
- assert(canBeSubtypeOf(listT, Seq(), nilT).isEmpty, "Supertypes are not subtypes")
- assert(canBeSubtypeOf(listT, Seq(), consT).isEmpty, "Supertypes are not subtypes")
+ assert(!isSubtypeOf(listT, nilT ), "Supertypes are not subtypes")
+ assert(!isSubtypeOf(listT, consT), "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(!isSubtypeOf(nilD.typed(Seq(tp2)), listD.typed(Seq(tp3))), "Types are not subtypes with incompatible params")
+ assert(!isSubtypeOf(nilD.typed(Seq(tp2)), listD.typed(Seq(IntegerType))), "Types are not subtypes with incompatible params")
+ assert(!isSubtypeOf(SetType(tp2), SetType(tp3)), "Types are not subtypes with incompatible params")
- 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")
+ assert(!isSubtypeOf(nilD.typed(Seq(nilT)), listD.typed(Seq(listT))), "Classes are invariant")
+ assert(!isSubtypeOf(SetType(nilT), SetType(listT)), "Sets are invariant")
- // 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(isSubtypeOf(FunctionType(Seq(listT), nilT), FunctionType(Seq(nilT), listT)), "Functions have contravariant params/ covariant result")
- assert(canBeSubtypeOf(listT, Seq(tp), listD.typed(Seq(tp2)), rhsFixed = true).isDefined, "List[T] <: List[A] with T free and rhs fixed")
+ assert(!typesCompatible(tp2, tp3), "Different types should be incompatible")
+ assert(!typesCompatible(BooleanType, tp3), "Different types should be incompatible")
+ assert(!typesCompatible(tp2, BooleanType), "Different types should be incompatible")
+ assert(!typesCompatible(IntegerType, Int32Type), "Different types should be incompatible")
- assert(isSubtypeOf(listD.typed, listD.typed), "List[T] <: List[T]")
+ // Type parameters
+ assert(unify(tp, tp2, Seq(tp) ).isDefined, "T <: A with T free")
+ assert(unify(tp, tp2, Seq(tp2)).isDefined, "T <: A with A free")
+
+ assert(unify(listT, listD.typed(Seq(tp2)), Seq(tp) ).isDefined, "List[T] <: List[A] with T free")
+ assert(unify(listT, listD.typed(Seq(tp2)), Seq(tp2)).isDefined, "List[T] <: List[A] with A free")
+ assert(unify(listT, listD.typed(Seq(tp2)), Seq() ).isEmpty, "List[T] !<: List[A] with A,T not free")
+ assert(unify(listT, nilT, Seq(tp) ).isEmpty, "Subtypes not unifiable")
+
+ assert(
+ unify(MapType(IntegerType, tp), MapType(tp2, IntegerType), Seq(tp, tp2)).contains(Map(tp -> IntegerType, tp2 -> IntegerType)),
+ "MapType unifiable"
+ )
+
+ assert(
+ subtypingInstantiation(consD.typed(Seq(tp)), listD.typed(Seq(tp2))) contains Map(tp2 -> tp),
+ "Cons[T] <: List[A] under A -> T"
+ )
+
+ assert(
+ subtypingInstantiation(consD.typed(Seq(IntegerType)), listD.typed(Seq(tp2))) contains Map(tp2 -> IntegerType),
+ "Cons[BigInt] <: List[A] under A -> BigInt"
+ )
+
+ assert(
+ subtypingInstantiation(consD.typed(Seq(tp)), listD.typed(Seq(IntegerType))).isEmpty,
+ "List[BigInt] cannot be instantiated such that Cons[T] <: List[BigInt]"
+ )
}
test("instantiateType Hole") { ctx =>
val tp1 = TypeParameter.fresh("a")
val tp2 = TypeParameter.fresh("b")
- val tpd = TypeParameterDef(tp1)
-
val e1 = Hole(tp1, Nil)
- val e2 = instantiateType(e1, Map(tpd -> tp2), Map())
+ val e2 = instantiateType(e1, Map(tp1 -> tp2), Map())
e2 match {
case Hole(tp, _) => assert(tp == tp2, "Type should have been substituted")
--
GitLab