More fixes in lambda normalization

src/main/scala/inox/ast/SymbolOps.scala

@@ -116,7 +116,7 @@ trait SymbolOps { self: TypeOps =>
     val remainingIds: MutableMap[Type, List[Identifier]] = MutableMap.empty ++ typedIds.toMap
 
     def getId(e: Expr): Identifier = {
-      val tpe = bestRealType(e.getType)
+      val tpe = e.getType
       val newId = remainingIds.get(tpe) match {
         case Some(x :: xs) =>
           remainingIds += tpe -> xs

src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala

@@ -55,7 +55,6 @@ trait LambdaTemplates { self: Templates =>
       ids: (Variable, Encoded),
       pathVar: (Variable, Encoded),
       arguments: Seq[(Variable, Encoded)],
-      closures: Seq[(Variable, Encoded)],
       condVars: Map[Variable, Encoded],
       exprVars: Map[Variable, Encoded],
       condTree: Map[Variable, Set[Variable]],
@@ -72,14 +71,14 @@ trait LambdaTemplates { self: Templates =>
       val tpe = ids._1.getType.asInstanceOf[FunctionType]
       val (clauses, blockers, applications, matchers, templateString) =
         Template.encode(pathVar, arguments, condVars, exprVars, guardedExprs, equations,
-          lambdas, quantifications, substMap = baseSubstMap + ids ++ closures, optApp = Some(id -> tpe))
+          lambdas, quantifications, substMap = baseSubstMap + ids, optApp = Some(id -> tpe))
 
       val lambdaString : () => String = () => {
         "Template for lambda " + ids._1 + ": " + lambda + " is :\n" + templateString()
       }
 
       new LambdaTemplate(
-        ids, pathVar, arguments, closures,
+        ids, pathVar, arguments,
         condVars, exprVars, condTree,
         clauses, blockers, applications, matchers,
         lambdas, quantifications,
@@ -201,7 +200,6 @@ trait LambdaTemplates { self: Templates =>
     val ids: (Variable, Encoded),
     val pathVar: (Variable, Encoded),
     val arguments: Seq[(Variable, Encoded)],
-    val closures: Seq[(Variable, Encoded)],
     val condVars: Map[Variable, Encoded],
     val exprVars: Map[Variable, Encoded],
     val condTree: Map[Variable, Set[Variable]],
@@ -222,7 +220,7 @@ trait LambdaTemplates { self: Templates =>
     def substitute(substituter: Encoded => Encoded, msubst: Map[Encoded, Matcher]): LambdaTemplate = new LambdaTemplate(
       ids._1 -> substituter(ids._2),
       pathVar._1 -> substituter(pathVar._2),
-      arguments, closures, condVars, exprVars, condTree,
+      arguments, condVars, exprVars, condTree,
       clauses.map(substituter),
       blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, msubst)) },
       applications.map { case (b, apps) => substituter(b) -> apps.map(_.substitute(substituter, msubst)) },
@@ -235,10 +233,10 @@ trait LambdaTemplates { self: Templates =>
     /** This must be called right before returning the clauses in [[structure.instantiation]]! */
     def concretize(idT: Encoded): LambdaTemplate = {
       assert(!isConcrete, "Can't concretize concrete lambda template")
-      val substituter = mkSubstituter(Map(ids._2 -> idT) ++ (closures.map(_._2) zip structure.locals.map(_._2)))
+      val substituter = mkSubstituter(Map(ids._2 -> idT))
       new LambdaTemplate(
         ids._1 -> idT,
-        pathVar, arguments, closures, condVars, exprVars, condTree,
+        pathVar, arguments, condVars, exprVars, condTree,
         clauses map substituter,
         blockers.map { case (b, fis) => b -> fis.map(_.substitute(substituter, Map.empty)) },
         applications.map { case (b, apps) => b -> apps.map(_.substitute(substituter, Map.empty)) },

src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala

@@ -278,21 +278,16 @@ trait TemplateGenerator { self: Templates =>
 
         val (struct, deps) = normalizeStructure(l)
         val sortedDeps = deps.toSeq.sortBy(_._1.id.uniqueName)
-        val idDeps = sortedDeps.map(_._1)
-        val trDeps = idDeps.map(id => encodeSymbol(id))
 
-        val lid = Variable(FreshIdentifier("lambda", true), bestRealType(l.getType))
-        val clauses = liftedEquals(lid, struct, idArgs, inlineFirst = true)
+        val depsByScope: Seq[(Variable, Expr)] = {
+          def rec(v: Variable): Seq[Variable] =
+            (exprOps.variablesOf(deps(v)) & deps.keySet).toSeq.flatMap(rec) :+ v
+          deps.keys.toSeq.flatMap(rec).distinct.map(v => v -> deps(v))
+        }
 
         val localSubst: Map[Variable, Encoded] = substMap ++ condVars ++ exprVars ++ lambdaVars
-        val clauseSubst: Map[Variable, Encoded] = localSubst ++ (idArgs zip trArgs) ++ (idDeps zip trDeps)
-        val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants) =
-          clauses.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(pathVar, cls, clauseSubst))
-
-        val ids: (Variable, Encoded) = lid -> storeLambda(lid)
-
         val (depSubst, (depConds, depExprs, depTree, depGuarded, depEqs, depLambdas, depQuants)) =
-          sortedDeps.foldLeft[(Map[Variable, Encoded], TemplateClauses)](localSubst -> emptyClauses) {
+          depsByScope.foldLeft[(Map[Variable, Encoded], TemplateClauses)](localSubst -> emptyClauses) {
             case ((depSubst, clsSet), (v, expr)) =>
               if (!exprOps.isSimple(expr)) {
                 val (e, cls @ (_, _, _, _, _, lmbds, quants)) = mkExprClauses(pathVar, expr, depSubst)
@@ -322,8 +317,36 @@ trait TemplateGenerator { self: Templates =>
           struct, dependencies, pathVar -> encodedCond(pathVar), depClosures,
           depConds, depExprs, depTree, depClauses, depCalls, depApps, depMatchers, depLambdas, depQuants)
 
+        val isNormalForm: Boolean = {
+          def extractBody(e: Expr): (Seq[ValDef], Expr) = e match {
+            case Lambda(args, body) =>
+              val (nextArgs, nextBody) = extractBody(body)
+              (args ++ nextArgs, nextBody)
+            case _ => (Seq.empty, e)
+          }
+
+          extractBody(struct) match {
+            case (params, ApplicationExtractor(caller: Variable, args)) =>
+              (params.map(_.toVariable) == args) && (deps.get(caller) match {
+                case Some(_: Application | _: FunctionInvocation) => true
+                case _ => false
+              })
+            case _ => false
+          }
+        }
+
+        val realLambda = if (isNormalForm) l else struct
+        val lid = Variable(FreshIdentifier("lambda", true), bestRealType(l.getType))
+        val clauses = liftedEquals(lid, realLambda, idArgs, inlineFirst = true)
+
+        val clauseSubst: Map[Variable, Encoded] = depSubst ++ (idArgs zip trArgs)
+        val (lambdaConds, lambdaExprs, lambdaTree, lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants) =
+          clauses.foldLeft(emptyClauses)((clsSet, cls) => clsSet ++ mkClauses(pathVar, cls, clauseSubst))
+
+        val ids: (Variable, Encoded) = lid -> storeLambda(lid)
+
         val template = LambdaTemplate(ids, pathVar -> encodedCond(pathVar),
-          idArgs zip trArgs, idDeps zip trDeps, lambdaConds, lambdaExprs, lambdaTree,
+          idArgs zip trArgs, lambdaConds, lambdaExprs, lambdaTree,
           lambdaGuarded, lambdaEqs, lambdaTemplates, lambdaQuants, structure, depSubst, l)
         registerLambda(template)
         lid