diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala index e03ac549e7da56a3b510e9c5dc6a5b13977f93d7..d15c78c951fe3f3990c16ee51422dc53b8223806 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 b8c0dbd8a4e8338643d33d133b56444aff9ad4d4..fe548c1b013e3cbef8e5a7024286c1e9e8781e0f 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) } }