diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index ca52d4592842da60629423e9d0ba3ff52ea2a73c..058e3a0ead6262f367ef5c4441dd075dd9e79be7 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -11,6 +11,7 @@ import Extractors._
import Constructors._
import utils._
import solvers._
+import scala.language.implicitConversions
/** Provides functions to manipulate [[purescala.Expressions]].
*
@@ -1285,20 +1286,18 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
false
}
+ type Apriori = Map[Identifier, Identifier]
+
/** Checks whether two expressions can be homomorphic and returns the corresponding mapping */
def canBeHomomorphic(t1: Expr, t2: Expr): Option[Map[Identifier, Identifier]] = {
val freeT1Variables = ExprOps.variablesOf(t1)
val freeT2Variables = ExprOps.variablesOf(t2)
- def mergeContexts(a: Option[Map[Identifier, Identifier]], b: =>Option[Map[Identifier, Identifier]]) = a match {
- case Some(m) =>
- b match {
- case Some(n) if (m.keySet & n.keySet) forall (key => m(key) == n(key)) =>
- Some(m ++ n)
- case _ =>None
- }
- case _ => None
- }
+ def mergeContexts(
+ a: Option[Apriori],
+ 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) {
@@ -1308,27 +1307,38 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
}
}
}
- implicit class AugmentedContext(c: Option[Map[Identifier, Identifier]]) {
- def &&(other: => Option[Map[Identifier, Identifier]]) = mergeContexts(c, other)
+ implicit class AugmentedContext(c: Option[Apriori]) {
+ def &&(other: Apriori => Option[Apriori]): Option[Apriori] = mergeContexts(c, other)
def --(other: Seq[Identifier]) =
c.map(_ -- other)
}
- implicit class AugmentedBooleant(c: Boolean) {
- def &&(other: => Option[Map[Identifier, Identifier]]) = if(c) other else None
+ implicit class AugmentedBoolean(c: Boolean) {
+ def &&(other: => Option[Apriori]) = if(c) other else None
+ }
+ implicit class AugmentedFilter(c: Apriori => Option[Apriori]) {
+ def &&(other: Apriori => Option[Apriori]):
+ Apriori => Option[Apriori]
+ = (m: Apriori) => c(m).flatMap(mp => other(mp))
}
implicit class AugmentedSeq[T](c: Seq[T]) {
- def mergeall(p: T => Option[Map[Identifier, Identifier]]) =
- (Option(Map[Identifier, Identifier]()) /: c) {
- case (s, c) => s && p(c)
+ def mergeall(p: T => Apriori => Option[Apriori])(apriori: Apriori) =
+ (Option(apriori) /: c) {
+ case (s, c) => s.flatMap(apriori => p(c)(apriori))
}
}
+ implicit def noneToContextTaker(c: None.type) = {
+ (m: Apriori) => None
+ }
- def idHomo(i1: Identifier, i2: Identifier): Option[Map[Identifier, Identifier]] = {
- if(!(freeT1Variables(i1) || freeT2Variables(i2)) || i1 == i2) Some(Map(i1 -> i2)) else None
+ def idHomo(i1: Identifier, i2: Identifier)(apriori: Apriori): Option[Apriori] = {
+ if(!(freeT1Variables(i1) || freeT2Variables(i2)) || i1 == i2 || apriori.get(i1) == Some(i2)) Some(Map(i1 -> i2)) else None
+ }
+ def idOptionHomo(i1: Option[Identifier], i2: Option[Identifier])(apriori: Apriori): Option[Apriori] = {
+ (i1.size == i2.size) && (i1 zip i2).headOption.flatMap(i => idHomo(i._1, i._2)(apriori))
}
- def fdHomo(fd1: FunDef, fd2: FunDef): Option[Map[Identifier, Identifier]] = {
+ def fdHomo(fd1: FunDef, fd2: FunDef)(apriori: Apriori): Option[Apriori] = {
if(fd1.params.size == fd2.params.size) {
val newMap = Map((
(fd1.id -> fd2.id) +:
@@ -1337,114 +1347,113 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
} else None
}
- def isHomo(t1: Expr, t2: Expr): Option[Map[Identifier, Identifier]] = {
- def casesMatch(cs1 : Seq[MatchCase], cs2 : Seq[MatchCase]) : Option[Map[Identifier, Identifier]] = {
- def patternHomo(p1: Pattern, p2: Pattern): (Boolean, Map[Identifier, Identifier]) = (p1, p2) match {
+ def isHomo(t1: Expr, t2: Expr)(apriori: Apriori): Option[Apriori] = {
+ def casesMatch(cs1 : Seq[MatchCase], cs2 : Seq[MatchCase])(apriori: Apriori) : Option[Apriori] = {
+ def patternHomo(p1: Pattern, p2: Pattern)(apriori: Apriori): Option[Apriori] = (p1, p2) match {
case (InstanceOfPattern(ob1, cd1), InstanceOfPattern(ob2, cd2)) =>
- (ob1.size == ob2.size && cd1 == cd2, Map((ob1 zip ob2).toSeq : _*))
+ cd1 == cd2 && idOptionHomo(ob1, ob2)(apriori)
case (WildcardPattern(ob1), WildcardPattern(ob2)) =>
- (ob1.size == ob2.size, Map((ob1 zip ob2).toSeq : _*))
+ idOptionHomo(ob1, ob2)(apriori)
case (CaseClassPattern(ob1, ccd1, subs1), CaseClassPattern(ob2, ccd2, subs2)) =>
- val m = Map[Identifier, Identifier]() ++ (ob1 zip ob2)
+ val m = idOptionHomo(ob1, ob2)(apriori)
- if (ob1.size == ob2.size && ccd1 == ccd2 && subs1.size == subs2.size) {
- (subs1 zip subs2).map { case (p1, p2) => patternHomo(p1, p2) }.foldLeft((true, m)) {
- case ((b1, m1), (b2,m2)) => (b1 && b2, m1 ++ m2)
- }
- } else {
- (false, Map())
- }
+ (ccd1 == ccd2 && subs1.size == subs2.size) && m &&
+ ((subs1 zip subs2) mergeall { case (p1, p2) => patternHomo(p1, p2) })
- case (UnapplyPattern(ob1, fd1, subs1), UnapplyPattern(ob2, fd2, subs2)) =>
- val m = Map[Identifier, Identifier]() ++ (ob1 zip ob2)
+ case (UnapplyPattern(ob1, TypedFunDef(fd1, ts1), subs1), UnapplyPattern(ob2, TypedFunDef(fd2, ts2), subs2)) =>
+ val m = idOptionHomo(ob1, ob2)(apriori)
- if (ob1.size == ob2.size && fd1 == fd2 && subs1.size == subs2.size) {
- (subs1 zip subs2).map { case (p1, p2) => patternHomo(p1, p2) }.foldLeft((true, m)) {
- case ((b1, m1), (b2,m2)) => (b1 && b2, m1 ++ m2)
- }
- } else {
- (false, Map())
- }
+ (subs1.size == subs2.size && ts1 == ts2) && m && fdHomo(fd1, fd2) && (
+ (subs1 zip subs2) mergeall { case (p1, p2) => patternHomo(p1, p2) })
case (TuplePattern(ob1, subs1), TuplePattern(ob2, subs2)) =>
- val m = Map[Identifier, Identifier]() ++ (ob1 zip ob2)
+ val m = idOptionHomo(ob1, ob2)(apriori)
- if (ob1.size == ob2.size && subs1.size == subs2.size) {
- (subs1 zip subs2).map { case (p1, p2) => patternHomo(p1, p2) }.foldLeft((true, m)) {
- case ((b1, m1), (b2,m2)) => (b1 && b2, m1 ++ m2)
- }
- } else {
- (false, Map())
- }
+ (ob1.size == ob2.size && subs1.size == subs2.size) && m && (
+ (subs1 zip subs2) mergeall { case (p1, p2) => patternHomo(p1, p2) })
case (LiteralPattern(ob1, lit1), LiteralPattern(ob2,lit2)) =>
- (ob1.size == ob2.size && lit1 == lit2, (ob1 zip ob2).toMap)
+ lit1 == lit2 && idOptionHomo(ob1, ob2)(apriori)
case _ =>
- (false, Map())
+ None
}
(cs1 zip cs2).mergeall {
case (MatchCase(p1, g1, e1), MatchCase(p2, g2, e2)) =>
- val (h, nm) = patternHomo(p1, p2)
- val g: Option[Map[Identifier, Identifier]] = (g1, g2) match {
- case (Some(g1), Some(g2)) => Some(nm) && isHomo(g1,g2)
- case (None, None) => Some(Map())
+ val h = patternHomo(p1, p2) _
+ val g: Apriori => Option[Apriori] = (g1, g2) match {
+ case (Some(g1), Some(g2)) => isHomo(g1, g2)(_)
+ case (None, None) => (m: Apriori) => Some(m)
case _ => None
}
- val e = Some(nm) && isHomo(e1, e2)
+ val e = isHomo(e1, e2) _
h && g && e
- }
-
+ }(apriori)
}
import synthesis.Witnesses.Terminating
- val res: Option[Map[Identifier, Identifier]] = (t1, t2) match {
+ val res: Option[Apriori] = (t1, t2) match {
case (Variable(i1), Variable(i2)) =>
- idHomo(i1, i2)
+ idHomo(i1, i2)(apriori)
case (Let(id1, v1, e1), Let(id2, v2, e2)) =>
- isHomo(v1, v2) &&
- isHomo(e1, e2) && Some(Map(id1 -> id2))
+
+ isHomo(v1, v2)(apriori + (id1 -> id2)) &&
+ isHomo(e1, e2)
+
+ case (Hole(_, _), Hole(_, _)) =>
+ None
case (LetDef(fds1, e1), LetDef(fds2, e2)) =>
fds1.size == fds2.size &&
{
val zipped = fds1.zip(fds2)
- (zipped mergeall (fds => fdHomo(fds._1, fds._2))) && Some(zipped.map(fds => fds._1.id -> fds._2.id).toMap) &&
+ (zipped mergeall (fds => fdHomo(fds._1, fds._2)))(apriori) &&
isHomo(e1, e2)
}
case (MatchExpr(s1, cs1), MatchExpr(s2, cs2)) =>
- cs1.size == cs2.size && casesMatch(cs1,cs2) && isHomo(s1, s2)
+ cs1.size == cs2.size && casesMatch(cs1,cs2)(apriori) && isHomo(s1, s2)
case (Passes(in1, out1, cs1), Passes(in2, out2, cs2)) =>
- (cs1.size == cs2.size && casesMatch(cs1,cs2)) && isHomo(in1,in2) && isHomo(out1,out2)
+ (cs1.size == cs2.size && casesMatch(cs1,cs2)(apriori)) && isHomo(in1,in2) && isHomo(out1,out2)
case (FunctionInvocation(tfd1, args1), FunctionInvocation(tfd2, args2)) =>
- idHomo(tfd1.fd.id, tfd2.fd.id) && tfd1.tps.zip(tfd2.tps).mergeall{ case (t1, t2) => if(t1 == t2) Option(Map()) else None} &&
+ (if(tfd1 == tfd2) Some(apriori) else (apriori.get(tfd1.fd.id) match {
+ case None =>
+ isHomo(tfd1.fd.fullBody, tfd2.fd.fullBody)(apriori + (tfd1.fd.id -> tfd2.fd.id))
+ case Some(fdid2) =>
+ if(fdid2 == tfd2.fd.id) Some(apriori) else None
+ })) &&
+ tfd1.tps.zip(tfd2.tps).mergeall{
+ case (t1, t2) => if(t1 == t2)
+ (m: Apriori) => Option(m)
+ else (m: Apriori) => None} &&
(args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
case (Terminating(tfd1, args1), Terminating(tfd2, args2)) =>
- idHomo(tfd1.fd.id, tfd2.fd.id) && tfd1.tps.zip(tfd2.tps).mergeall{ case (t1, t2) => if(t1 == t2) Option(Map()) else None} &&
+ idHomo(tfd1.fd.id, tfd2.fd.id)(apriori) && tfd1.tps.zip(tfd2.tps).mergeall{ case (t1, t2) => if(t1 == t2) (m: Apriori) => Option(m) else (m: Apriori) => None} &&
(args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
case (Lambda(defs, body), Lambda(defs2, body2)) =>
// We remove variables introduced by lambdas.
- (isHomo(body, body2) &&
- (defs zip defs2).mergeall{ case (ValDef(a1), ValDef(a2)) => Option(Map(a1 -> a2)) }
+ ((defs zip defs2).mergeall{ case (ValDef(a1), ValDef(a2)) =>
+ (m: Apriori) =>
+ Some(m + (a1 -> a2)) }(apriori)
+ && isHomo(body, body2)
) -- (defs.map(_.id))
case (v1, v2) if isValue(v1) && isValue(v2) =>
- v1 == v2 && Some(Map[Identifier, Identifier]())
+ v1 == v2 && Some(apriori)
case Same(Operator(es1, _), Operator(es2, _)) =>
(es1.size == es2.size) &&
- (es1 zip es2).mergeall{ case (e1, e2) => isHomo(e1, e2) }
+ (es1 zip es2).mergeall{ case (e1, e2) => isHomo(e1, e2) }(apriori)
case _ =>
None
@@ -1453,9 +1462,7 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
res
}
- isHomo(t1,t2)
-
-
+ isHomo(t1,t2)(Map())
} // ensuring (res => res.isEmpty || isHomomorphic(t1, t2)(res.get))
/** Checks whether two trees are homomoprhic modulo an identifier map.
diff --git a/testcases/web/synthesis/24_String_DoubleList.scala b/testcases/web/synthesis/24_String_DoubleList.scala
index 652f5e4b84ed8837dc56cdce10393a480232c1b0..021a11bcef87e883ea01424ed2024ca44bd255cd 100644
--- a/testcases/web/synthesis/24_String_DoubleList.scala
+++ b/testcases/web/synthesis/24_String_DoubleList.scala
@@ -21,14 +21,11 @@ object DoubleListRender {
} holds
def AtoString(a : A): String = {
- ???
- } ensuring {
- (res : String) => (a, res) passes {
- case N() =>
- "[]"
- case B(NN(), N()) =>
- "[()]"
- }
+ ???[String] ask a
+ }
+
+ def AAtoString(a : AA): String = {
+ ???[String] ask a
}
def structurallyEqualA(a: A, b: A): Boolean = (a, b) match {