Homomorphic to work on lambdas + tests.

Ability to keep abstract term on the RHS of examples without trivially evaluating the choose construct.

src/main/scala/leon/evaluators/RecursiveEvaluator.scala

@@ -28,6 +28,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
   lazy val scalaEv = new ScalacEvaluator(this, ctx, prog)
 
   protected var clpCache = Map[(Choose, Seq[Expr]), Expr]()
+  
+  private var evaluationFailsOnChoose = false
+  /** Sets the flag if when encountering a Choose, it should fail instead of solving it. */
+  def setEvaluationFailOnChoose(b: Boolean) = { this.evaluationFailsOnChoose = b; this }
 
   protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
     case Variable(id) =>
@@ -577,6 +581,9 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       e(p.asConstraint)
 
     case choose: Choose =>
+      if(evaluationFailsOnChoose) {
+        throw EvalError("Evaluator set to not solve choose constructs")
+      }
 
       implicit val debugSection = utils.DebugSectionSynthesis
 

src/main/scala/leon/purescala/ExprOps.scala

@@ -1560,6 +1560,8 @@ object ExprOps {
     }
     implicit class AugmentedContext(c: Option[Map[Identifier, Identifier]]) {
       def &&(other: => Option[Map[Identifier, Identifier]]) = 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
@@ -1685,6 +1687,11 @@ object ExprOps {
 
         // 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 Same(Operator(es1, _), Operator(es2, _)) =>
           (es1.size == es2.size) &&
           (es1 zip es2).mergeall{ case (e1, e2) => isHomo(e1, e2) }

src/main/scala/leon/synthesis/ExamplesFinder.scala

@@ -27,8 +27,11 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
   val reporter = ctx.reporter
   
   private var keepAbstractExamples = false
-  
+  /** If true, will not evaluate examples to check them. */
   def setKeepAbstractExamples(b: Boolean) = { this.keepAbstractExamples = b; this}
+  /** Sets if evalution of the result of tests should stop on choose statements.
+    * Useful for programming by Example */
+  def setEvaluationFailOnChoose(b: Boolean) = { evaluator.setEvaluationFailOnChoose(b); this }
 
   def extractFromFunDef(fd: FunDef, partition: Boolean): ExamplesBank = fd.postcondition match {
     case Some(Lambda(Seq(ValDef(id, _)), post)) =>

src/main/scala/leon/synthesis/rules/StringRender.scala

@@ -176,7 +176,7 @@ case object StringRender extends Rule("StringRender") {
                     case Some(equations) =>
                       gatherEquations(q, acc ++= equations)
                     case None =>
-                      hctx.reporter.info("Could not extract equations from ["+sfget+"] == ["+rhsget+"]")
+                      hctx.reporter.info("Could not extract equations from ["+sfget+"] == ["+rhsget+"]\n coming from ... == " + rhExpr)
                     None
                   }
                 case _ =>
@@ -547,7 +547,9 @@ case object StringRender extends Rule("StringRender") {
       case List(IsTyped(v, StringType)) =>
         val description = "Creates a standard string conversion function"
 
-        val examplesFinder = new ExamplesFinder(hctx.context, hctx.program).setKeepAbstractExamples(true)
+        val examplesFinder = new ExamplesFinder(hctx.context, hctx.program)
+        .setKeepAbstractExamples(true)
+        .setEvaluationFailOnChoose(true)
         val examples = examplesFinder.extractFromProblem(p)
         
         val abstractStringConverters: StringConverters =

src/test/scala/leon/integration/purescala/ExprOpsSuite.scala

@@ -7,6 +7,7 @@ import leon.test._
 import leon.purescala.Constructors._
 import leon.purescala.Expressions._
 import leon.purescala.ExprOps._
+import leon.purescala.Definitions._
 import leon.purescala.Common._
 
 class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
@@ -106,12 +107,27 @@ class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL
     import leon.purescala.ExprOps.canBeHomomorphic
     import leon.purescala.Types._
     import leon.purescala.Definitions._
-    val d = FreshIdentifier("x", IntegerType)
-    val e = FreshIdentifier("y", IntegerType)
-    assert(canBeHomomorphic(Variable(d), Variable(e)).isEmpty)
-    val l1 = Lambda(Seq(ValDef(d)), Variable(d))
-    val l2 = Lambda(Seq(ValDef(e)), Variable(e))
+    val d = FreshIdentifier("d", IntegerType)
+    val x = FreshIdentifier("x", IntegerType)
+    val y = FreshIdentifier("y", IntegerType)
+    assert(canBeHomomorphic(Variable(d), Variable(x)).isEmpty)
+    val l1 = Lambda(Seq(ValDef(x)), Variable(x))
+    val l2 = Lambda(Seq(ValDef(y)), Variable(y))
     assert(canBeHomomorphic(l1, l2).nonEmpty)
+    val fType = FunctionType(Seq(IntegerType), IntegerType)
+    val f = FreshIdentifier("f",
+        FunctionType(Seq(IntegerType, fType, fType), IntegerType))
+    val farg1 = FreshIdentifier("arg1", IntegerType)
+    val farg2 = FreshIdentifier("arg2", fType)
+    val farg3 = FreshIdentifier("arg3", fType)
+    
+    val fdef = new FunDef(f, Seq(), Seq(ValDef(farg1), ValDef(farg2), ValDef(farg3)), IntegerType)
+    
+    // Captured variables should be silent, even if they share the same identifier in two places of the code.
+    assert(canBeHomomorphic(
+        FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l2)),
+        FunctionInvocation(fdef.typed, Seq(Variable(d), l1, l1))).nonEmpty)
+    
   }
 
 }