diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala index 5bfdf62aa325ba046a33c771a6a1573c644e6ea4..c5ab883453778d8de950fbe19c078ab1d2e296eb 100644 --- a/src/main/scala/inox/ast/ExprOps.scala +++ b/src/main/scala/inox/ast/ExprOps.scala @@ -38,10 +38,17 @@ trait ExprOps extends GenTreeOps { lazy val Deconstructor = Operator /** Replaces bottom-up variables by looking up for them in a map */ - def replaceFromSymbols[V <: VariableSymbol](substs: Map[V, Expr], expr: Expr)(implicit ev: VariableConverter[V]): Expr = { + def replaceFromSymbols[V <: VariableSymbol]( + substs: Map[V, Expr], + expr: Expr, + copyPositions: Boolean = false + )(implicit ev: VariableConverter[V]): Expr = { new SelfTreeTransformer { override def transform(expr: Expr): Expr = expr match { - case v: Variable => substs.getOrElse(v.to[V], super.transform(v)) + case v: Variable => + val res = substs.getOrElse(v.to[V], super.transform(v)) + if (copyPositions) res.copiedFrom(v) + else res case _ => super.transform(expr) } }.transform(expr) diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala index 6da2fb57a9ac50641b8183dcfbec3a8fc6d2bd59..d5905fca2b605cc1bc34880e1669fa3fc0598969 100644 --- a/src/main/scala/inox/ast/Types.scala +++ b/src/main/scala/inox/ast/Types.scala @@ -336,11 +336,15 @@ trait Types { self: Trees => case NAryType(tps, builder) => tps.exists(isParametricType) } - def replaceFromSymbols[V <: VariableSymbol](subst: Map[V, Expr], tpe: Type) - (implicit ev: VariableConverter[V]): Type = { + def replaceFromSymbols[V <: VariableSymbol] + (subst: Map[V, Expr], tpe: Type, copyPositions: Boolean = false) + (implicit ev: VariableConverter[V]): Type = { new SelfTreeTransformer { override def transform(expr: Expr): Expr = expr match { - case v: Variable => subst.getOrElse(v.to[V], v) + case v: Variable => + val res = subst.getOrElse(v.to[V], v) + if (copyPositions) res.copiedFrom(v) + else res case _ => super.transform(expr) } }.transform(tpe)