From 71db39f01b204e9ad9cf98511db2265d286e253f Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 17 Mar 2016 12:30:39 +0100
Subject: [PATCH] fix some positions propagation in ops
---
src/main/scala/leon/purescala/DefOps.scala | 8 ++--
src/main/scala/leon/purescala/ExprOps.scala | 48 +++++++++----------
.../scala/leon/purescala/Extractors.scala | 4 +-
src/main/scala/leon/utils/TypingPhase.scala | 26 +++++-----
.../scala/leon/xlang/AntiAliasingPhase.scala | 4 +-
5 files changed, 45 insertions(+), 45 deletions(-)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index f713cab8f..c79282c53 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -371,12 +371,12 @@ object DefOps {
def replaceFunCalls(e: Expr, fdMapF: FunDef => FunDef, fiMapF: (FunctionInvocation, FunDef) => Option[Expr] = defaultFiMap): Expr = {
preMap {
- case MatchExpr(scrut, cases) =>
+ case me@MatchExpr(scrut, cases) =>
Some(MatchExpr(scrut, cases.map(matchcase => matchcase match {
- case MatchCase(pattern, guard, rhs) => MatchCase(replaceFunCalls(pattern, fdMapF), guard, rhs)
- })))
+ case mc@MatchCase(pattern, guard, rhs) => MatchCase(replaceFunCalls(pattern, fdMapF), guard, rhs).copiedFrom(mc)
+ })).copiedFrom(me))
case fi @ FunctionInvocation(TypedFunDef(fd, tps), args) =>
- fiMapF(fi, fdMapF(fd)).map(_.setPos(fi))
+ fiMapF(fi, fdMapF(fd)).map(_.copiedFrom(fi))
case _ =>
None
}(e)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 058e3a0ea..801bc8c7c 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -43,33 +43,33 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
def preTransformWithBinders(f: (Expr, Set[Identifier]) => Expr, initBinders: Set[Identifier] = Set())(e: Expr) = {
import xlang.Expressions.LetVar
- def rec(binders: Set[Identifier], e: Expr): Expr = (f(e, binders) match {
- case LetDef(fds, bd) =>
+ def rec(binders: Set[Identifier], e: Expr): Expr = f(e, binders) match {
+ case ld@LetDef(fds, bd) =>
fds.foreach(fd => {
fd.fullBody = rec(binders ++ fd.paramIds, fd.fullBody)
})
- LetDef(fds, rec(binders, bd))
- case Let(i, v, b) =>
- Let(i, rec(binders + i, v), rec(binders + i, b))
- case LetVar(i, v, b) =>
- LetVar(i, rec(binders + i, v), rec(binders + i, b))
- case MatchExpr(scrut, cses) =>
- MatchExpr(rec(binders, scrut), cses map { case MatchCase(pat, og, rhs) =>
+ LetDef(fds, rec(binders, bd)).copiedFrom(ld)
+ case l@Let(i, v, b) =>
+ Let(i, rec(binders + i, v), rec(binders + i, b)).copiedFrom(l)
+ case lv@LetVar(i, v, b) =>
+ LetVar(i, rec(binders + i, v), rec(binders + i, b)).copiedFrom(lv)
+ case m@MatchExpr(scrut, cses) =>
+ MatchExpr(rec(binders, scrut), cses map { case mc@MatchCase(pat, og, rhs) =>
val newBs = binders ++ pat.binders
- MatchCase(pat, og map (rec(newBs, _)), rec(newBs, rhs))
- })
- case Passes(in, out, cses) =>
- Passes(rec(binders, in), rec(binders, out), cses map { case MatchCase(pat, og, rhs) =>
+ MatchCase(pat, og map (rec(newBs, _)), rec(newBs, rhs)).copiedFrom(mc)
+ }).copiedFrom(m)
+ case p@Passes(in, out, cses) =>
+ Passes(rec(binders, in), rec(binders, out), cses map { case mc@MatchCase(pat, og, rhs) =>
val newBs = binders ++ pat.binders
- MatchCase(pat, og map (rec(newBs, _)), rec(newBs, rhs))
- })
- case Lambda(args, bd) =>
- Lambda(args, rec(binders ++ args.map(_.id), bd))
- case Forall(args, bd) =>
- Forall(args, rec(binders ++ args.map(_.id), bd))
- case Deconstructor(subs, builder) =>
- builder(subs map (rec(binders, _)))
- }).copiedFrom(e)
+ MatchCase(pat, og map (rec(newBs, _)), rec(newBs, rhs)).copiedFrom(mc)
+ }).copiedFrom(p)
+ case l@Lambda(args, bd) =>
+ Lambda(args, rec(binders ++ args.map(_.id), bd)).copiedFrom(l)
+ case f@Forall(args, bd) =>
+ Forall(args, rec(binders ++ args.map(_.id), bd)).copiedFrom(f)
+ case d@Deconstructor(subs, builder) =>
+ builder(subs map (rec(binders, _))).copiedFrom(d)
+ }
rec(initBinders, e)
}
@@ -287,9 +287,9 @@ object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
case Lambda(args, body) => Some(Lambda(args.map(vd => vd.copy(id = subst(vd.id))), body))
case Forall(args, body) => Some(Forall(args.map(vd => vd.copy(id = subst(vd.id))), body))
case Let(i, e, b) => Some(Let(subst(i), e, b))
- case MatchExpr(scrut, cses) => Some(MatchExpr(scrut, cses.map { cse =>
+ case m@MatchExpr(scrut, cses) => Some(MatchExpr(scrut, cses.map { cse =>
cse.copy(pattern = replacePatternBinders(cse.pattern, subst))
- }))
+ }).copiedFrom(m))
case Passes(in, out, cses) => Some(Passes(in, out, cses.map { cse =>
cse.copy(pattern = replacePatternBinders(cse.pattern, subst))
}))
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 49e6afd3a..d0cbbbf17 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -210,7 +210,7 @@ object Extractors {
Seq(cond, thenn, elze),
{ case Seq(c, t, e) => IfExpr(c, t, e) }
))
- case MatchExpr(scrut, cases) => Some((
+ case m@MatchExpr(scrut, cases) => Some((
scrut +: cases.flatMap { _.expressions },
(es: Seq[Expr]) => {
var i = 1
@@ -219,7 +219,7 @@ object Extractors {
case GuardedCase(b, _, _) => i += 2; GuardedCase(b, es(i - 2), es(i - 1))
}
- matchExpr(es.head, newcases)
+ matchExpr(es.head, newcases).copiedFrom(m)
}
))
case Passes(in, out, cases) => Some((
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 08b415c6b..203c81e12 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -32,19 +32,19 @@ object TypingPhase extends SimpleLeonPhase[Program, Program] {
pgm.definedFunctions.foreach(fd => {
// Part (1)
- fd.precondition = {
- val argTypesPreconditions = fd.params.flatMap(arg => arg.getType match {
- case cct: ClassType if cct.parent.isDefined =>
- Seq(IsInstanceOf(arg.id.toVariable, cct))
- case at: ArrayType =>
- Seq(GreaterEquals(ArrayLength(arg.id.toVariable), IntLiteral(0)))
- case _ =>
- Seq()
- })
- argTypesPreconditions match {
- case Nil => fd.precondition
- case xs => fd.precondition match {
- case Some(p) => Some(andJoin(xs :+ p))
+ val argTypesPreconditions = fd.params.flatMap(arg => arg.getType match {
+ case cct: ClassType if cct.parent.isDefined =>
+ Seq(IsInstanceOf(arg.id.toVariable, cct))
+ case at: ArrayType =>
+ Seq(GreaterEquals(ArrayLength(arg.id.toVariable), IntLiteral(0)))
+ case _ =>
+ Seq()
+ })
+ argTypesPreconditions match {
+ case Nil => ()
+ case xs => fd.precondition = {
+ fd.precondition match {
+ case Some(p) => Some(andJoin(xs :+ p).copiedFrom(p))
case None => Some(andJoin(xs))
}
}
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 7eb391088..4d1e903fd 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -181,7 +181,7 @@ object AntiAliasingPhase extends TransformationPhase {
//so we need to ignore the second times by checking if updatedFunDefs
//contains a mapping or not
val nfds = fds.map(fd => updatedFunDefs.get(fd).getOrElse(fd))
- (Some(LetDef(nfds, body)), bindings)
+ (Some(LetDef(nfds, body).copiedFrom(l)), bindings)
}
case fi@FunctionInvocation(fd, args) => {
@@ -196,7 +196,7 @@ object AntiAliasingPhase extends TransformationPhase {
updatedFunDefs.get(fd.fd) match {
case None => (None, bindings)
case Some(nfd) => {
- val nfi = FunctionInvocation(nfd.typed(fd.tps), args).setPos(fi)
+ val nfi = FunctionInvocation(nfd.typed(fd.tps), args).copiedFrom(fi)
val fiEffects = effects.getOrElse(fd.fd, Set())
if(fiEffects.nonEmpty) {
val modifiedArgs: Seq[Variable] =
--
GitLab