From ce17562d370a9a68cd27762452800500f30c4b03 Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Mon, 2 Sep 2019 13:18:15 +0200
Subject: [PATCH] Add an option to copy positions from old tree when doing
substitutions
---
src/main/scala/inox/ast/ExprOps.scala | 11 +++++++++--
src/main/scala/inox/ast/Types.scala | 10 +++++++---
2 files changed, 16 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 5bfdf62aa..c5ab88345 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 6da2fb57a..d5905fca2 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)
--
GitLab