From 988360c79b349c2f7832c40d249baf4aa65d4c1e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 29 Feb 2016 20:30:14 +0100
Subject: [PATCH] Hot fix: Forgot intermediate descendants.
---
src/main/scala/leon/purescala/DefOps.scala | 20 +++++++++++++-------
1 file changed, 13 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index f81e5f44d..2a20a478b 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -415,13 +415,15 @@ object DefOps {
def duplicateClassDef(cd: ClassDef): ClassDef = {
cdMapCache.get(cd) match {
- case Some(new_cd) => new_cd.get // None would have meant that this class would never be duplicated, which is not possible.
+ case Some(new_cd) =>
+ new_cd.get // None would have meant that this class would never be duplicated, which is not possible.
case None =>
val parent = cd.parent.map(duplicateAbstractClassType)
val new_cd = cdMapF(cd).map(f => f(parent)).getOrElse{
cd match {
case acd:AbstractClassDef => acd.duplicate(parent = parent)
- case ccd:CaseClassDef => ccd.duplicate(parent = parent, fields = ccd.fieldsIds.map(id => ValDef(idMap(id)))) // Should not cycle since fields have to be abstract.
+ case ccd:CaseClassDef =>
+ ccd.duplicate(parent = parent, fields = ccd.fieldsIds.map(id => ValDef(idMap(id)))) // Should not cycle since fields have to be abstract.
}
}
cdMapCache += cd -> Some(new_cd)
@@ -440,10 +442,11 @@ object DefOps {
// If at least one descendants or known case class needs conversion, then all the hierarchy will be converted.
// If something extends List[A] and A is modified, then the first something should be modified.
def dependencies(s: ClassDef): Set[ClassDef] = {
- Set(s) ++ s.parent.toList.flatMap(p => TypeOps.collect[ClassDef]{
- case AbstractClassType(acd, _) => Set(acd:ClassDef) ++ acd.knownCCDescendants
+ leon.utils.fixpoint((s: Set[ClassDef]) => s ++ s.flatMap(_.knownDescendants) ++ s.flatMap(_.parent.toList.flatMap(p => TypeOps.collect[ClassDef]{
+ case AbstractClassType(acd, _) => Set(acd:ClassDef) ++ acd.knownDescendants
case CaseClassType(ccd, _) => Set(ccd:ClassDef)
- }(p))
+ case _ => Set()
+ }(p))))(Set(s))
}
def cdMap(cd: ClassDef): ClassDef = {
@@ -461,7 +464,8 @@ object DefOps {
}
def idMap(id: Identifier): Identifier = {
if (!(idMapCache contains id)) {
- idMapCache += id -> id.duplicate(tpe = tpMap(id.getType))
+ val new_id = id.duplicate(tpe = tpMap(id.getType))
+ idMapCache += id -> new_id
}
idMapCache(id)
}
@@ -474,6 +478,7 @@ object DefOps {
TypeOps.exists{
case AbstractClassType(acd, _) => cdMap(acd) != acd
case CaseClassType(ccd, _) => cdMap(ccd) != ccd
+ case _ => false
}(tp)
}
@@ -588,7 +593,8 @@ object DefOps {
case ci @ CaseClass(ct, args) =>
ciMapF(ci, tpMap(ct)).map(_.setPos(ci))
case CaseClassSelector(cct, expr, identifier) =>
- Some(CaseClassSelector(tpMap(cct), expr, idMap(identifier)))
+ val new_cct = tpMap(cct)
+ Some(CaseClassSelector(new_cct, expr, (if(new_cct != cct) idMap(identifier) else identifier)))
case IsInstanceOf(e, ct) => Some(IsInstanceOf(e, tpMap(ct)))
case AsInstanceOf(e, ct) => Some(AsInstanceOf(e, tpMap(ct)))
case MatchExpr(scrut, cases) =>
--
GitLab