From 18d49df78990103b0cfe516a978c25733b2a2948 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 22 Jul 2016 19:51:01 +0200
Subject: [PATCH] Fixes in trees
---
src/main/scala/inox/ast/Definitions.scala | 8 ++------
src/main/scala/inox/ast/Expressions.scala | 2 +-
src/main/scala/inox/ast/GenTreeOps.scala | 2 +-
src/main/scala/inox/ast/SymbolOps.scala | 6 +++---
src/main/scala/inox/ast/TypeOps.scala | 6 +++---
.../inox/solvers/SolverUnsupportedError.scala | 15 ---------------
6 files changed, 10 insertions(+), 29 deletions(-)
delete mode 100644 src/main/scala/inox/solvers/SolverUnsupportedError.scala
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index b9b3e2006..47903f24f 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -181,15 +181,12 @@ trait Definitions { self: Trees =>
val flags: Set[ClassFlag]) extends ClassDef {
val isAbstract = true
- def descendants(implicit s: Symbols): Seq[ClassDef] = children
+ def descendants(implicit s: Symbols): Seq[CaseClassDef] = children
.map(id => s.getClass(id) match {
case ccd: CaseClassDef => ccd
case _ => throw NotWellFormedException(id, s)
})
- def ccDescendants(implicit s: Symbols): Seq[CaseClassDef] =
- descendants collect { case ccd: CaseClassDef => ccd }
-
def isInductive(implicit s: Symbols): Boolean = {
def induct(tpe: Type, seen: Set[ClassDef]): Boolean = tpe match {
case ct: ClassType =>
@@ -206,7 +203,7 @@ trait Definitions { self: Trees =>
}
if (this == root && !this.isAbstract) false
- else ccDescendants.exists { ccd =>
+ else descendants.exists { ccd =>
ccd.fields.exists(vd => induct(vd.getType, Set(root)))
}
}
@@ -275,7 +272,6 @@ trait Definitions { self: Trees =>
case class TypedAbstractClassDef(cd: AbstractClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
def descendants: Seq[TypedClassDef] = cd.descendants.map(_.typed(tps))
- def ccDescendants: Seq[TypedCaseClassDef] = cd.ccDescendants.map(_.typed(tps))
}
case class TypedCaseClassDef(cd: CaseClassDef, tps: Seq[Type])(implicit val symbols: Symbols) extends TypedClassDef {
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 472d68a17..b8d259cd1 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -276,7 +276,7 @@ trait Expressions { self: Trees =>
// Hacky, but ok
def optionType(implicit s: Symbols) = s.getFunction(id, tps).returnType.asInstanceOf[ClassType]
def optionChildren(implicit s: Symbols): (ClassType, ClassType) = {
- val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].ccDescendants.sortBy(_.fields.size)
+ val children = optionType.tcd.asInstanceOf[TypedAbstractClassDef].descendants.sortBy(_.fields.size)
val Seq(noneType, someType) = children.map(_.toType)
(noneType, someType)
}
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index c87ea98dc..7e179f003 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -232,7 +232,7 @@ trait GenTreeOps {
val Deconstructor(es, builder) = e
val newEss = es.map(rec)
- val newVs: Seq[SubTree] = leon.utils.SeqUtils.cartesianProduct(newEss).map { newEs =>
+ val newVs: Seq[SubTree] = SeqUtils.cartesianProduct(newEss).map { newEs =>
if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
builder(newEs).copiedFrom(e)
} else {
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 19202719b..889a31a19 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -447,7 +447,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
}
val tcds = tcd match {
- case tacd: TypedAbstractClassDef => tacd.ccDescendants
+ case tacd: TypedAbstractClassDef => tacd.descendants
case tccd: TypedCaseClassDef => Seq(tccd)
}
@@ -476,7 +476,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
val tccd @ TypedCaseClassDef(cd, tps) = tcd match {
case tacd: TypedAbstractClassDef =>
- tacd.ccDescendants.filter(hasInstance(_)).sortBy(_.fields.size).head
+ tacd.descendants.filter(hasInstance(_)).sortBy(_.fields.size).head
case tccd: TypedCaseClassDef => tccd
}
@@ -534,7 +534,7 @@ trait SymbolOps extends TreeOps { self: TypeOps =>
case Some(tccd: TypedCaseClassDef) =>
cartesianProduct(tccd.fieldsTypes map valuesOf) map (CaseClass(ct, _))
case Some(accd: TypedAbstractClassDef) =>
- interleave(accd.ccDescendants.map(tccd => valuesOf(tccd.toType)))
+ interleave(accd.descendants.map(tccd => valuesOf(tccd.toType)))
case None => throw ClassLookupException(ct.id)
}
}
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 5f294f6c7..d02ceb26c 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -245,17 +245,17 @@ trait TypeOps {
Set(tpe) ++ (tpe match {
case ct: ClassType => ct.tcd match {
case tccd: TypedCaseClassDef => tccd.fieldsTypes
- case tacd: TypedAbstractClassDef => (Set(tacd) ++ tacd.ccDescendants).map(_.toType)
+ case tacd: TypedAbstractClassDef => (Set(tacd) ++ tacd.descendants).map(_.toType)
}
case _ => Set.empty
})
)
- })(accd.ccDescendants.map(_.toType).toSet)
+ })(accd.descendants.map(_.toType).toSet)
if (possibleChildTypes(accd.toType)) {
None
} else {
- cards(accd.ccDescendants.map(_.toType)).map(_.sum)
+ cards(accd.descendants.map(_.toType)).map(_.sum)
}
}
case _ => None
diff --git a/src/main/scala/inox/solvers/SolverUnsupportedError.scala b/src/main/scala/inox/solvers/SolverUnsupportedError.scala
deleted file mode 100644
index 48acc71f4..000000000
--- a/src/main/scala/inox/solvers/SolverUnsupportedError.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Common.Tree
-
-object SolverUnsupportedError {
- def msg(t: Tree, s: Solver, reason: Option[String]) = {
- s"(of ${t.getClass}) is unsupported by solver ${s.name}" + reason.map(":\n " + _ ).getOrElse("")
- }
-}
-
-case class SolverUnsupportedError(t: Tree, s: Solver, reason: Option[String] = None)
- extends Unsupported(t, SolverUnsupportedError.msg(t,s,reason))(s.context)
--
GitLab