xlang does not work with mutually recursive functions

src/main/scala/leon/xlang/ImperativeCodeElimination.scala

@@ -28,9 +28,9 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
     }
   }
 
-  /** varsInScope refers to variable declared in the same level scope.
-    * Typically, when entering a nested function body, the scope should be
-    * reset to empty */
+  /* varsInScope refers to variable declared in the same level scope.
+     Typically, when entering a nested function body, the scope should be
+     reset to empty */
   private case class State(
     parent: FunDef, 
     varsInScope: Set[Identifier],
@@ -39,14 +39,12 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
     def withVar(i: Identifier) = copy(varsInScope = varsInScope + i)
     def withFunDef(fd: FunDef, nfd: FunDef, ids: List[Identifier]) = 
       copy(funDefsMapping = funDefsMapping + (fd -> (nfd, ids)))
-    def withFunDefs(fdNfd: Seq[(FunDef, (FunDef, List[Identifier]))]) = 
-      copy(funDefsMapping = funDefsMapping ++ fdNfd)
   }
 
-  /** Returns a "scope" consisting of purely functional code that defines potentially needed 
-    * new variables (val, not var) and a mapping for each modified variable (var, not val :) )
-    * to their new name defined in the scope. The first returned valued is the value of the expression
-    * that should be introduced as such in the returned scope (the val already refers to the new names) */
+  //return a "scope" consisting of purely functional code that defines potentially needed 
+  //new variables (val, not var) and a mapping for each modified variable (var, not val :) )
+  //to their new name defined in the scope. The first returned valued is the value of the expression
+  //that should be introduced as such in the returned scope (the val already refers to the new names)
   private def toFunction(expr: Expr)(implicit state: State): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
     import state._
     expr match {
@@ -145,7 +143,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
           ).setPos(wh)
         )
 
-        val newExpr = LetDef(List(whileFunDef), FunctionInvocation(whileFunDef.typed, Seq()).setPos(wh)).setPos(wh)
+        val newExpr = LetDef(Seq(whileFunDef), FunctionInvocation(whileFunDef.typed, Seq()).setPos(wh)).setPos(wh)
         toFunction(newExpr)
 
       case Block(Seq(), expr) =>
@@ -219,95 +217,67 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
 
 
       case LetDef(fds, b) =>
-        def fdsWithoutSideEffects =  {
-          for(fd <- fds) {
-            fd.body.foreach { bd =>
-              val (fdRes, fdScope, _) = toFunction(bd)
-              fd.body = Some(fdScope(fdRes))
-            }
+
+        if(fds.size > 1) {
+          sys.error("Xlang does not support mutually recursive functions")
+        }
+
+        val fd = fds.head
+
+        def fdWithoutSideEffects =  {
+          fd.body.foreach { bd =>
+            val (fdRes, fdScope, _) = toFunction(bd)
+            fd.body = Some(fdScope(fdRes))
           }
           val (bodyRes, bodyScope, bodyFun) = toFunction(b)
-          (bodyRes, (b2: Expr) => LetDef(fds, bodyScope(b2)).setPos(fds.head).copiedFrom(expr), bodyFun)
+          (bodyRes, (b2: Expr) => LetDef(Seq(fd), bodyScope(b2)).setPos(fd).copiedFrom(expr), bodyFun)
         }
-        if(fds.forall(_.body.isEmpty)) fdsWithoutSideEffects
-        else {
-          val modified_vars: Seq[(FunDef, List[Identifier])] = for(fd <- fds; bd <- fd.body) yield {
+
+        fd.body match {
+          case Some(bd) => {
+
             val modifiedVars: List[Identifier] =
               collect[Identifier]({
                 case Assignment(v, _) => Set(v)
                 case FunctionInvocation(tfd, _) => state.funDefsMapping.get(tfd.fd).map(p => p._2.toSet).getOrElse(Set())
                 case _ => Set()
               })(bd).intersect(state.varsInScope).toList
-            (fd, modifiedVars)
-          }
-          if(modified_vars.forall(_._2.isEmpty)) fdsWithoutSideEffects else {
-            val freshNames: Seq[(FunDef, Seq[Identifier])] = modified_vars.map(fdmv => (fdmv._1, fdmv._2.map(id => id.freshen)))
-            
-            val newParams: Seq[(FunDef, Seq[ValDef])] = freshNames.map(fdfn => (fdfn._1, fdfn._1.params ++ fdfn._2.map(n => ValDef(n))))
-            
-            val freshVarDecls: Seq[(FunDef, List[Identifier])] = freshNames.map(id => (id._1, id._2.map(_.freshen).toList))
-            
-            val rewritingMap: Map[Identifier, Identifier] =
-                (modified_vars.zip(freshVarDecls).map{
-              case ((fd, md), (_, fv)) => (fd, md.zip(fv).toMap)
-            }).map(_._2).foldLeft(Map[Identifier, Identifier]())(_ ++ _)
-            
-            //TODO:
-            
-            val freshBody: Seq[Option[Expr]] = for(fd <- fds) yield {
-              fd.body.map(bd => 
-              preMap({
-                case Assignment(v, e) => rewritingMap.get(v).map(nv => Assignment(nv, e))
-                case Variable(id) => rewritingMap.get(id).map(nid => Variable(nid))
-                case _ => None
-              })(bd))
-            }
-            
-            val wrappedBody = freshBody.zip(freshNames).zip(freshVarDecls).map{
-              case ((freshBodyOpt, (_, freshNames)), (_, freshVarDecls)) =>
-                freshBodyOpt.map(freshBody => freshNames.zip(freshVarDecls).foldLeft(freshBody)((body, p) => {
-              LetVar(p._2, Variable(p._1), body)
-            }))}
-
-            val newReturnType = for((fd, modifiedVars) <- modified_vars)
-              yield TupleType(fd.returnType :: modifiedVars.map(_.getType))
-
-            val newFds = for(((fd, newParams), newReturnType) <- newParams.zip(newReturnType))
-              yield {
-                val newFd = new FunDef(fd.id.freshen, fd.tparams, newParams, newReturnType).setPos(fd)
-                newFd.addFlags(fd.flags)
-                (fd, newFd)
-              }
-              
-            val mappingToAdd: Seq[(FunDef, (FunDef, List[Identifier]))] =
-              for(((fd, newFd), (_, freshVarDecls)) <- newFds.zip(freshVarDecls)) yield (fd -> ((newFd, freshVarDecls.toList)))
-
-            //Seq[Option[(fdRes, fdScope, fdFun)]] = 
-            val fdsResScopeFun = for(wrappedBodyOpt <- wrappedBody) yield {
-              wrappedBodyOpt.map(wrappedBody => 
+
+            if(modifiedVars.isEmpty) fdWithoutSideEffects else {
+
+              val freshNames: List[Identifier] = modifiedVars.map(id => id.freshen)
+
+              val newParams: Seq[ValDef] = fd.params ++ freshNames.map(n => ValDef(n))
+              val freshVarDecls: List[Identifier] = freshNames.map(id => id.freshen)
+
+              val rewritingMap: Map[Identifier, Identifier] =
+                modifiedVars.zip(freshVarDecls).toMap
+              val freshBody =
+                preMap({
+                  case Assignment(v, e) => rewritingMap.get(v).map(nv => Assignment(nv, e))
+                  case Variable(id) => rewritingMap.get(id).map(nid => Variable(nid))
+                  case _ => None
+                })(bd)
+              val wrappedBody = freshNames.zip(freshVarDecls).foldLeft(freshBody)((body, p) => {
+                LetVar(p._2, Variable(p._1), body)
+              })
+
+              val newReturnType = TupleType(fd.returnType :: modifiedVars.map(_.getType))
+
+              val newFd = new FunDef(fd.id.freshen, fd.tparams, newParams, newReturnType).setPos(fd)
+              newFd.addFlags(fd.flags)
+
+              val (fdRes, fdScope, fdFun) = 
                 toFunction(wrappedBody)(
-                  State(state.parent, Set(), 
-                        state.funDefsMapping.map{
-  case (fd, (nfd, mvs)) =>
-  (fd, (nfd, mvs.map(v => rewritingMap.getOrElse(v, v))))} ++ mappingToAdd)
+                  State(state.parent, 
+                        Set(), 
+                        state.funDefsMapping.map{case (fd, (nfd, mvs)) => (fd, (nfd, mvs.map(v => rewritingMap.getOrElse(v, v))))} + 
+                               (fd -> ((newFd, freshVarDecls))))
                 )
-              )
-            }
-            
-            val newRes= for((optFdsResScopeFun, (_, freshVarDecls)) <- fdsResScopeFun.zip(freshVarDecls)) yield {
-              for((fdRes, fdScope, fdFun) <- optFdsResScopeFun) yield {
-                Tuple(fdRes :: freshVarDecls.map(vd => fdFun(vd).toVariable))
-              }
-            }
-            val newbody = for((optFdsResScopeFun, newRes) <- fdsResScopeFun.zip(newRes)) yield {
-              for(newRes <- newRes;
-                  (fdRes, fdScope, fdFun) <- optFdsResScopeFun) yield {
-                fdScope(newRes)
-              }
-            }
-            val fdForState = for(((((fd, newFd), optNewbody), (_, modifiedVars)), (_, freshNames))
-                <- newFds.zip(newbody).zip(modified_vars).zip(freshNames)) yield {
-              newFd.body = optNewbody
+              val newRes = Tuple(fdRes :: freshVarDecls.map(vd => fdFun(vd).toVariable))
+              val newBody = fdScope(newRes)
+
+              newFd.body = Some(newBody)
               newFd.precondition = fd.precondition.map(prec => {
                 replace(modifiedVars.zip(freshNames).map(p => (p._1.toVariable, p._2.toVariable)).toMap, prec)
               })
@@ -325,11 +295,12 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
                   postBody)
                 Lambda(Seq(newRes), newBody).setPos(post)
               })
-              (fd, (newFd, modifiedVars))
+
+              val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withFunDef(fd, newFd, modifiedVars))
+              (bodyRes, (b2: Expr) => LetDef(Seq(newFd), bodyScope(b2)).copiedFrom(expr), bodyFun)
             }
-            val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withFunDefs(fdForState))
-            (bodyRes, (b2: Expr) => LetDef(newFds.map(_._1), bodyScope(b2)).copiedFrom(expr), bodyFun)
           }
+          case None => fdWithoutSideEffects
         }
 
       case c @ Choose(b) =>