From eb87ecf0e1f33ba4e5b0ba0826d774f0106b6b96 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Sat, 29 Jun 2019 22:27:35 +0200 Subject: [PATCH 1/2] Move implicit debug section higher --- src/main/scala/inox/solvers/unrolling/Templates.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala index 6232c71b1..4e6ac73da 100644 --- a/src/main/scala/inox/solvers/unrolling/Templates.scala +++ b/src/main/scala/inox/solvers/unrolling/Templates.scala @@ -26,6 +26,8 @@ trait Templates import program.trees._ import program.symbols._ + implicit val debugSection = DebugSectionSolver + type Encoded def asString(e: Encoded): String @@ -206,8 +208,6 @@ trait Templates promoted } - implicit val debugSection = DebugSectionSolver - type Arg = Either[Encoded, Matcher] implicit class ArgWrapper(arg: Arg) { From ce17562d370a9a68cd27762452800500f30c4b03 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Mon, 2 Sep 2019 13:18:15 +0200 Subject: [PATCH 2/2] 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)