Temporarily add replaceKeepPositions function to use Inox release

epfl-lara · Sep 17, 2019 · a2f2600 · a2f2600
1 parent 9f3380a
commit a2f2600
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 6 deletions.
diff --git a/core/src/main/scala/stainless/ast/ExprOps.scala b/core/src/main/scala/stainless/ast/ExprOps.scala
@@ -307,4 +307,13 @@ trait ExprOps extends inox.ast.ExprOps {
         other
     }
   }
+
+  def replaceKeepPositions(subst: Map[Variable, Expr], expr: Expr): Expr = {
+    new SelfTreeTransformer {
+      override def transform(expr: Expr): Expr = expr match {
+        case v: Variable => subst.getOrElse(v, v).copiedFrom(v)
+        case _ => super.transform(expr)
+      }
+    }.transform(expr)
+  }
 }
diff --git a/core/src/main/scala/stainless/ast/TypeOps.scala b/core/src/main/scala/stainless/ast/TypeOps.scala
@@ -68,4 +68,13 @@ trait TypeOps extends inox.ast.TypeOps {
           }
       }
   }
+
+  def replaceKeepPositions(subst: Map[Variable, Expr], tpe: Type): Type = {
+    new SelfTreeTransformer {
+      override def transform(expr: Expr): Expr = expr match {
+        case v: Variable => subst.getOrElse(v, v).copiedFrom(v)
+        case _ => super.transform(expr)
+      }
+    }.transform(tpe)
+  }
 }
diff --git a/core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala b/core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala
@@ -24,6 +24,7 @@ trait ImperativeCodeElimination
   override protected def extractFunction(symbols: s.Symbols, fd: s.FunDef): t.FunDef = {
     import symbols._
     import exprOps._
+    import exprOps.{ replaceKeepPositions => replace }
 
     /* varsInScope refers to variable declared in the same level scope.
      * Typically, when entering a nested function body, the scope should be
@@ -104,7 +105,7 @@ trait ImperativeCodeElimination
           }
 
           val newRhs = csesVals.zip(csesScope).map {
-            case (cVal, cScope) => replaceFromSymbols(scrutFun, cScope(cVal), true)
+            case (cVal, cScope) => replace(scrutFun, cScope(cVal))
           }
 
           val matchE = MatchExpr(scrutRes, cses.zip(newRhs).map {

diff --git a/core/src/main/scala/stainless/extraction/methods/Sealing.scala b/core/src/main/scala/stainless/extraction/methods/Sealing.scala
@@ -46,16 +46,16 @@ trait Sealing extends oo.CachingPhase
         .toMap
 
       val (paramSubst, params) = fd.params
-        .foldLeft((Map.empty[ValDef, Expr], Seq.empty[ValDef])) { case ((paramSubst, params), vd) =>
-          val ntpe = typeOps.replaceFromSymbols(paramSubst, vd.tpe, true)
+        .foldLeft((Map.empty[Variable, Expr], Seq.empty[ValDef])) { case ((paramSubst, params), vd) =>
+          val ntpe = symbols.replaceKeepPositions(paramSubst, vd.tpe)
           val nvd = pureParams.getOrElse(vd.id, vd).copy(tpe = ntpe).copiedFrom(vd)
-          (paramSubst + (vd -> nvd.toVariable), params :+ nvd)
+          (paramSubst + (vd.toVariable -> nvd.toVariable), params :+ nvd)
         }
 
       fd.copy(
         params = params,
-        returnType = typeOps.replaceFromSymbols(paramSubst, fd.returnType, true),
-        fullBody = exprOps.replaceFromSymbols(paramSubst, fd.fullBody, true)
+        returnType = symbols.replaceKeepPositions(paramSubst, fd.returnType),
+        fullBody = exprOps.replaceKeepPositions(paramSubst, fd.fullBody)
       ).copiedFrom(fd)
     }