From af6c55b1d98c747fd6ada8d04e39828e1e965563 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 16 Apr 2012 22:32:27 +0000
Subject: [PATCH] Keeping position of Match expression and call to nested
function
---
src/main/scala/leon/FunctionClosure.scala | 8 ++------
src/main/scala/leon/FunctionHoisting.scala | 2 +-
src/main/scala/leon/ImperativeCodeElimination.scala | 2 +-
src/main/scala/leon/UnitElimination.scala | 2 +-
4 files changed, 5 insertions(+), 9 deletions(-)
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 47c0be139..f21f1ad9f 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -58,7 +58,7 @@ object FunctionClosure extends Pass {
newFunDef.postcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
- case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)))
+ case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ extraVarDecls.map(_.id.toVariable)).setPosInfo(fi))
case _ => None
}
val freshBody = replace(freshVarsExpr, funBody)
@@ -70,17 +70,13 @@ object FunctionClosure extends Pass {
newFunDef.body = Some(recBody2)
def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
- case FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)))
+ case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
case _ => None
}
val recRest = functionClosure(rest, bindedVars)
val recRest2 = searchAndReplaceDFS(substFunInvocInRest)(recRest)
LetDef(newFunDef, recRest2).setType(l.getType)
}
-
- //case fi @ FunctionInvocation(fd, args) => {
-
- //}
case l @ Let(i,e,b) => {
val re = functionClosure(e, bindedVars)
pathConstraints ::= Equals(Variable(i), re)
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
index ec02d4336..1cfdffdc3 100644
--- a/src/main/scala/leon/FunctionHoisting.scala
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -65,7 +65,7 @@ object FunctionHoisting extends Pass {
(GuardedCase(pat, guard, r), s)
}
}.unzip
- (MatchExpr(scrutRes, csesRes).setType(m.getType), csesSets.toSet.flatten ++ scrutSet)
+ (MatchExpr(scrutRes, csesRes).setType(m.getType).setPosInfo(m), csesSets.toSet.flatten ++ scrutSet)
}
case t if t.isInstanceOf[Terminal] => (t, Set())
case unhandled => scala.sys.error("Non-terminal case should be handled in searchAndReplace: " + unhandled)
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index c60dd94b2..9c21a5d2a 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -107,7 +107,7 @@ object ImperativeCodeElimination extends Pass {
val matchExpr = MatchExpr(scrutRes, cses.zip(newRhs).map{
case (SimpleCase(pat, _), newRhs) => SimpleCase(pat, newRhs)
case (GuardedCase(pat, guard, _), newRhs) => GuardedCase(pat, replaceNames(scrutFun, guard), newRhs)
- }).setType(matchType)
+ }).setType(matchType).setPosInfo(m)
val scope = ((body: Expr) => {
val tupleId = FreshIdentifier("t").setType(matchType)
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 005544d9b..b52561750 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -135,7 +135,7 @@ object UnitElimination extends Pass {
case GuardedCase(pat, guard, rhs) => GuardedCase(pat, removeUnit(guard), removeUnit(rhs))
}
val tpe = csesRec.head.rhs.getType
- MatchExpr(scrutRec, csesRec).setType(tpe)
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
}
case _ => sys.error("not supported: " + expr)
}
--
GitLab