From 0dcebb86189dc6b90eddd4a0d36e436bd83e8c32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 2 Feb 2016 16:50:36 +0100
Subject: [PATCH] Added test case about isomorphism of values which should
trigger equality.
---
src/main/scala/leon/purescala/ExprOps.scala | 9 ++++++---
.../scala/leon/integration/purescala/ExprOpsSuite.scala | 3 +++
2 files changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index e03ac549e..d15c78c95 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1685,13 +1685,15 @@ object ExprOps {
fdHomo(tfd1.fd, tfd2.fd) &&
(args1 zip args2).mergeall{ case (a1, a2) => isHomo(a1, a2) }
- // TODO: Seems a lot is missing, like Literals
-
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.map(_.id))
+
+ case (v1, v2) if isValue(v1) && isValue(v2) =>
+ v1 == v2 && Some(Map[Identifier, Identifier]())
+
case Same(Operator(es1, _), Operator(es2, _)) =>
(es1.size == es2.size) &&
(es1 zip es2).mergeall{ case (e1, e2) => isHomo(e1, e2) }
@@ -1837,7 +1839,8 @@ object ExprOps {
fdHomo(tfd1.fd, tfd2.fd) &&
(args1 zip args2).forall{ case (a1, a2) => isHomo(a1, a2) }
- // TODO: Seems a lot is missing, like Literals
+ case (v1, v2) if isValue(v1) && isValue(v2) =>
+ v1 == v2
case Same(Operator(es1, _), Operator(es2, _)) =>
(es1.size == es2.size) &&
diff --git a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
index b8c0dbd8a..fe548c1b0 100644
--- a/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/ExprOpsSuite.scala
@@ -128,6 +128,9 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l2)),
FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l1))).nonEmpty)
+ assert(canBeHomomorphic(
+ StringLiteral("1"),
+ StringLiteral("2")).isEmpty)
}
}
--
GitLab