diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 8e19f10081350fc71359bb1f601d5d53ecf67c0a..0bb34ac382ac4c30127e924e50547fe18a96b09c 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -8,6 +8,7 @@ import scala.tools.nsc.plugins._
import scala.language.implicitConversions
+import purescala._
import purescala.Definitions._
import purescala.Trees.{Expr => LeonExpr, _}
import xlang.Trees.{Block => LeonBlock, _}
@@ -16,6 +17,8 @@ import purescala.TypeTrees.{TypeTree => LeonType, _}
import purescala.Common._
import purescala.TreeOps._
+import utils.{Position => LeonPosition, OffsetPosition => LeonOffsetPosition}
+
trait CodeExtraction extends Extractors {
self: LeonExtraction =>
@@ -25,12 +28,8 @@ trait CodeExtraction extends Extractors {
import ExpressionExtractors._
import ExtractorHelpers._
- class ScalaPos(p: global.Position) extends ScalacPositional {
- setPosInfo(p.line, p.column)
- }
-
- implicit def scalaPosToLeonPos(p: global.Position): ScalacPositional = {
- new ScalaPos(p)
+ implicit def scalaPosToLeonPos(p: global.Position): LeonPosition = {
+ LeonOffsetPosition(p.line, p.column, null)
}
private val mutableVarSubsts: scala.collection.mutable.Map[Symbol,Function0[LeonExpr]] =
@@ -177,7 +176,7 @@ trait CodeExtraction extends Extractors {
// we ignore the main function
case dd @ ExFunctionDef(name, params, tpe, body) =>
- val funDef = extractFunSig(name, params, tpe).setPosInfo(dd.pos)
+ val funDef = extractFunSig(name, params, tpe).setPos(dd.pos)
if (dd.mods.isPrivate) {
funDef.addAnnotation("private")
@@ -474,7 +473,7 @@ trait CodeExtraction extends Extractors {
*/
case dd @ ExFunctionDef(n, p, t, b) =>
- val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
+ val funDef = extractFunSig(n, p, t).setPos(dd.pos)
defsToDefs += (dd.symbol -> funDef)
val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
val oldCurrentFunDef = currentFunDef
@@ -535,21 +534,21 @@ trait CodeExtraction extends Extractors {
case wh @ ExWhile(cond, body) =>
val condTree = extractTree(cond)
val bodyTree = extractTree(body)
- While(condTree, bodyTree).setPosInfo(wh.pos)
+ While(condTree, bodyTree).setPos(wh.pos)
case wh @ ExWhileWithInvariant(cond, body, inv) =>
val condTree = extractTree(cond)
val bodyTree = extractTree(body)
val invTree = extractTree(inv)
- val w = While(condTree, bodyTree).setPosInfo(wh.pos)
+ val w = While(condTree, bodyTree).setPos(wh.pos)
w.invariant = Some(invTree)
w
case epsi @ ExEpsilonExpression(tpe, varSym, predBody) =>
val pstpe = extractType(tpe)
val previousVarSubst: Option[Function0[LeonExpr]] = varSubsts.get(varSym) //save the previous in case of nested epsilon
- varSubsts(varSym) = (() => EpsilonVariable((epsi.pos.line, epsi.pos.column)).setType(pstpe))
+ varSubsts(varSym) = (() => EpsilonVariable(epsi.pos).setType(pstpe))
val c1 = extractTree(predBody)
previousVarSubst match {
case Some(f) => varSubsts(varSym) = f
@@ -558,7 +557,7 @@ trait CodeExtraction extends Extractors {
if(containsEpsilon(c1)) {
unsupported(epsi, "Usage of nested epsilon is not allowed")
}
- Epsilon(c1).setType(pstpe).setPosInfo(epsi.pos.line, epsi.pos.column)
+ Epsilon(c1).setType(pstpe).setPos(epsi.pos)
case ExWaypointExpression(tpe, i, tree) =>
val pstpe = extractType(tpe)
@@ -587,7 +586,7 @@ trait CodeExtraction extends Extractors {
val indexRec = extractTree(index)
val newValueRec = extractTree(newValue)
- ArrayUpdate(lhsRec, indexRec, newValueRec).setPosInfo(update.pos)
+ ArrayUpdate(lhsRec, indexRec, newValueRec).setPos(update.pos)
case ExInt32Literal(v) =>
IntLiteral(v)
@@ -627,7 +626,7 @@ trait CodeExtraction extends Extractors {
val cBody = extractTree(body)
- Choose(vars, cBody).setPosInfo(select.pos)
+ Choose(vars, cBody).setPos(select.pos)
case ExCaseClassConstruction(tpt, args) =>
extractType(tpt.tpe) match {
@@ -834,7 +833,7 @@ trait CodeExtraction extends Extractors {
MapUnion(rm, FiniteMap(Seq((rf, rt))).setType(t)).setType(t)
case t @ ArrayType(bt) =>
- ArrayUpdated(rm, rf, rt).setType(t).setPosInfo(up.pos)
+ ArrayUpdated(rm, rf, rt).setType(t).setPos(up.pos)
case _ =>
unsupported(tr, "updated can only be applied to maps.")
@@ -857,11 +856,11 @@ trait CodeExtraction extends Extractors {
rlhs.getType match {
case MapType(_,tt) =>
assert(rargs.size == 1)
- MapGet(rlhs, rargs.head).setType(tt).setPosInfo(app.pos.line, app.pos.column)
+ MapGet(rlhs, rargs.head).setType(tt).setPos(app.pos)
case ArrayType(bt) =>
assert(rargs.size == 1)
- ArraySelect(rlhs, rargs.head).setType(bt).setPosInfo(app.pos.line, app.pos.column)
+ ArraySelect(rlhs, rargs.head).setType(bt).setPos(app.pos)
case _ =>
unsupported(tr, "apply on unexpected type")
@@ -931,14 +930,14 @@ trait CodeExtraction extends Extractors {
throw ImpureCodeEncounteredException(tr)
}
val fd = defsToDefs(sy)
- FunctionInvocation(fd, ar.map(extractTree(_))).setType(fd.returnType).setPosInfo(lc.pos.line,lc.pos.column)
+ FunctionInvocation(fd, ar.map(extractTree(_))).setType(fd.returnType).setPos(lc.pos)
}
case pm @ ExPatternMatching(sel, cses) =>
val rs = extractTree(sel)
val rc = cses.map(extractMatchCase(_))
val rt: LeonType = rc.map(_.rhs.getType).reduceLeft(leastUpperBound(_,_).get)
- MatchExpr(rs, rc).setType(rt).setPosInfo(pm.pos.line,pm.pos.column)
+ MatchExpr(rs, rc).setType(rt).setPos(pm.pos)
// default behaviour is to complain :)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 149530bb3727742ae6127b663697f671aa599c86..7c3e7271aeab567e4012085cefe8ebdd4ed36397 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -1,13 +1,14 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-
package leon
package purescala
+import utils._
+
object Common {
import Trees.Variable
import TypeTrees.Typed
- abstract class Tree extends Serializable
+ abstract class Tree extends Positioned with Serializable
// the type is left blank (Untyped) for Identifiers that are not variables
class Identifier private[Common](val name: String, private val globalId: Int, val id: Int, alwaysShowUniqueID: Boolean = false) extends Tree with Typed {
@@ -63,32 +64,4 @@ object Common {
}
- trait ScalacPositional {
- self =>
-
- private var prow: Int = -1078
- private var pcol: Int = -1078
-
- def setPosInfo(row: Int, col: Int) : self.type = {
- prow = row
- pcol = col
- this
- }
-
- def setPosInfo(from: ScalacPositional) : self.type = {
- val (or,oc) = from.posIntInfo
- prow = or
- pcol = oc
- this
- }
-
- def posIntInfo : (Int,Int) = (prow,pcol)
-
- def posInfo : String = if(prow != -1078) "(" + prow + "," + pcol + ")" else ""
-
- def <(other: ScalacPositional) : Boolean = {
- val (orow,ocol) = other.posIntInfo
- prow < orow || (prow == orow && pcol < ocol)
- }
- }
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 7bac0be4ca4700ee47e10aab52def1e11a9ed9c6..65b1d70e710b17d34f034bde4b5ba1ac5edbdb21 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -275,7 +275,7 @@ object Definitions {
}
/** Functions (= 'methods' of objects) */
- class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition with ScalacPositional {
+ class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition {
var body: Option[Expr] = None
def implementation : Option[Expr] = body
var precondition: Option[Expr] = None
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index b64ad7ffda8c9ffb6b24e27fb011a26901ef4172..5692aedb52bda00bc45a8c7bdc22fda8249ca796 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -63,7 +63,7 @@ object Extractors {
case MultisetUnion(t1,t2) => Some((t1,t2,MultisetUnion))
case MultisetPlus(t1,t2) => Some((t1,t2,MultisetPlus))
case MultisetDifference(t1,t2) => Some((t1,t2,MultisetDifference))
- case mg@MapGet(t1,t2) => Some((t1,t2, (t1, t2) => MapGet(t1, t2).setPosInfo(mg)))
+ case mg@MapGet(t1,t2) => Some((t1,t2, (t1, t2) => MapGet(t1, t2).setPos(mg)))
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
@@ -84,7 +84,7 @@ object Extractors {
object NAryOperator {
def unapply(expr: Expr) : Option[(Seq[Expr],(Seq[Expr])=>Expr)] = expr match {
- case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPosInfo(fi))))
+ case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPos(fi))))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 5b0b7aaaf6b694eef91648f425f099d75000ef6e..4e1e748022fee54aa6223f90e4317c7bd2931cb2 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -56,7 +56,7 @@ object FunctionClosure extends TransformationPhase {
val newBindedVars: Set[Identifier] = bindedVars ++ fd.args.map(_.id)
val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
- val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPosInfo(fd)
+ val newFunDef = new FunDef(newFunId, fd.returnType, newVarDecls).setPos(fd)
topLevelFuns += newFunDef
newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
newFunDef.parent = Some(parent)
@@ -116,10 +116,10 @@ object FunctionClosure extends TransformationPhase {
IfExpr(rCond, rThen, rElze).setType(i.getType)
}
case fi @ FunctionInvocation(fd, args) => fd2FreshFd.get(fd) match {
- case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPosInfo(fi)
+ case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPos(fi)
case Some((nfd, extraArgs)) =>
FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++
- extraArgs.map(v => replace(id2freshId.map(p => (p._1.toVariable, p._2.toVariable)), v))).setPosInfo(fi)
+ extraArgs.map(v => replace(id2freshId.map(p => (p._1.toVariable, p._2.toVariable)), v))).setPos(fi)
}
case n @ NAryOperator(args, recons) => {
val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd))
@@ -156,7 +156,7 @@ object FunctionClosure extends TransformationPhase {
}
}
val tpe = csesRec.head.rhs.getType
- MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPos(m)
}
case v @ Variable(id) => id2freshId.get(id) match {
case None => v
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 8371b8f0c852db4d9a0a6d2771b2d02eef36c7d6..9d7a569750af2896e5afc4a46485ebee3486ad5d 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -118,7 +118,7 @@ object TreeOps {
else
i
}
- case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType).setPosInfo(m)
+ case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut), cses.map(inCase(_))).setType(m.getType).setPos(m)
case c @ Choose(args, body) =>
val body2 = rec(body)
@@ -236,7 +236,7 @@ object TreeOps {
val rscrut = rec(scrut)
val (newCses,changes) = cses.map(inCase(_)).unzip
applySubst(if(rscrut != scrut || changes.exists(res=>res)) {
- MatchExpr(rscrut, newCses).setType(m.getType).setPosInfo(m)
+ MatchExpr(rscrut, newCses).setType(m.getType).setPos(m)
} else {
m
})
@@ -246,7 +246,7 @@ object TreeOps {
val body2 = rec(body)
applySubst(if (body != body2) {
- Choose(args, body2).setType(c.getType).setPosInfo(c)
+ Choose(args, body2).setType(c.getType).setPos(c)
} else {
c
})
@@ -300,7 +300,7 @@ object TreeOps {
}
def applyToTree(e : Expr) : Option[Expr] = e match {
- case m @ MatchExpr(s, cses) => Some(MatchExpr(s, cses.map(freshenCase(_))).setType(m.getType).setPosInfo(m))
+ case m @ MatchExpr(s, cses) => Some(MatchExpr(s, cses.map(freshenCase(_))).setType(m.getType).setPos(m))
case l @ Let(i,e,b) => {
val newID = FreshIdentifier(i.name, true).setType(i.getType)
Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
@@ -619,7 +619,7 @@ object TreeOps {
case v @ Variable(id) if s.isDefinedAt(id) => rec(s(id), s)
case l @ Let(i,e,b) => rec(b, s + (i -> rec(e, s)))
case i @ IfExpr(t1,t2,t3) => IfExpr(rec(t1, s),rec(t2, s),rec(t3, s)).setType(i.getType)
- case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut, s), cses.map(inCase(_, s))).setType(m.getType).setPosInfo(m)
+ case m @ MatchExpr(scrut,cses) => MatchExpr(rec(scrut, s), cses.map(inCase(_, s))).setType(m.getType).setPos(m)
case n @ NAryOperator(args, recons) => {
var change = false
val rargs = args.map(a => {
@@ -762,7 +762,7 @@ object TreeOps {
(realCond, newRhs)
}
- val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)).setPosInfo(m))((p1, ex) => {
+ val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)).setPos(m))((p1, ex) => {
if(p1._1 == BooleanLiteral(true)) {
p1._2
} else {
@@ -796,7 +796,7 @@ object TreeOps {
def rewriteMapGet(e: Expr) : Option[Expr] = e match {
case mg @ MapGet(m,k) =>
val ida = MapIsDefinedAt(m, k)
- Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType).setPosInfo(mg)).setType(mg.getType))
+ Some(IfExpr(ida, mg, Error("key not found for map access").setType(mg.getType).setPos(mg)).setType(mg.getType))
case _ => None
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 16dda8f063d0d75c96c5b4df726dbee59559a920..e60a31cfa2a3fff0458e18671cde6bdb6e985402 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -3,6 +3,8 @@
package leon
package purescala
+import utils._
+
/** AST definitions for Pure Scala. */
object Trees {
import Common._
@@ -10,8 +12,8 @@ object Trees {
import Definitions._
import Extractors._
- /* EXPRESSIONS */
+ /* EXPRESSIONS */
abstract class Expr extends Tree with Typed with Serializable {
override def toString: String = PrettyPrinter(this)
}
@@ -23,16 +25,16 @@ object Trees {
/* This describes computational errors (unmatched case, taking min of an
* empty set, division by zero, etc.). It should always be typed according to
* the expected type. */
- case class Error(description: String) extends Expr with Terminal with ScalacPositional
+ case class Error(description: String) extends Expr with Terminal
- case class Choose(vars: List[Identifier], pred: Expr) extends Expr with FixedType with ScalacPositional with UnaryExtractable {
+ case class Choose(vars: List[Identifier], pred: Expr) extends Expr with FixedType with UnaryExtractable {
assert(!vars.isEmpty)
val fixedType = if (vars.size > 1) TupleType(vars.map(_.getType)) else vars.head.getType
def extract = {
- Some((pred, (e: Expr) => Choose(vars, e).setPosInfo(this)))
+ Some((pred, (e: Expr) => Choose(vars, e).setPos(this)))
}
}
@@ -60,7 +62,7 @@ object Trees {
/* Control flow */
- case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType with ScalacPositional {
+ case class FunctionInvocation(funDef: FunDef, args: Seq[Expr]) extends Expr with FixedType {
val fixedType = funDef.returnType
funDef.args.zip(args).foreach {
@@ -127,7 +129,7 @@ object Trees {
def unapply(me: MatchExpr) : Option[(Expr,Seq[MatchCase])] = if (me == null) None else Some((me.scrutinee, me.cases))
}
- class MatchExpr(val scrutinee: Expr, val cases: Seq[MatchCase]) extends Expr with ScalacPositional with FixedType {
+ class MatchExpr(val scrutinee: Expr, val cases: Seq[MatchCase]) extends Expr with FixedType {
val fixedType = leastUpperBound(cases.map(_.rhs.getType)).getOrElse(AnyType)
@@ -519,7 +521,7 @@ object Trees {
/* Map operations. */
case class FiniteMap(singletons: Seq[(Expr, Expr)]) extends Expr
- case class MapGet(map: Expr, key: Expr) extends Expr with ScalacPositional
+ case class MapGet(map: Expr, key: Expr) extends Expr
case class MapUnion(map1: Expr, map2: Expr) extends Expr
case class MapDifference(map: Expr, keys: Expr) extends Expr
case class MapIsDefinedAt(map: Expr, key: Expr) extends Expr with FixedType {
@@ -535,7 +537,7 @@ object Trees {
val fixedType = ArrayType(defaultValue.getType)
}
- case class ArraySelect(array: Expr, index: Expr) extends Expr with ScalacPositional with FixedType {
+ case class ArraySelect(array: Expr, index: Expr) extends Expr with FixedType {
assert(array.getType.isInstanceOf[ArrayType],
"The array value in ArraySelect must of of array type; yet we got [%s]. In expr: \n%s".format(array.getType, array))
@@ -548,7 +550,7 @@ object Trees {
}
- case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType {
+ case class ArrayUpdated(array: Expr, index: Expr, newValue: Expr) extends Expr with FixedType {
assert(array.getType.isInstanceOf[ArrayType],
"The array value in ArrayUpdated must of of array type; yet we got [%s]. In expr: \n%s".format(array.getType, array))
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index b97bcc7c7a7fe597e1acdabd37b92e578c7e4352..145b5b132adc2cb318f0d4ccc103b3c28bf6163b 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -5,8 +5,11 @@ package synthesis
import purescala.Trees._
import purescala.Common.Tree
+import purescala.Definitions.FunDef
import purescala.ScalaPrinter
+import leon.utils.Position
+
import java.io.File
class FileInterface(reporter: Reporter) {
@@ -41,10 +44,11 @@ class FileInterface(reporter: Reporter) {
}
}
- case class CodePattern(startWith: String, posIntInfo: (Int, Int), blocks: Int)
+ case class CodePattern(startWith: String, pos: Position, blocks: Int)
object CodePattern {
- def forChoose(ci: ChooseInfo) = CodePattern("choose", ci.ch.posIntInfo, 1)
+ def forChoose(ci: ChooseInfo) = CodePattern("choose", ci.ch.getPos, 1)
+ def forFunDef(fd: FunDef) = CodePattern("def", fd.getPos, 2)
}
def substitute(str: String, pattern: CodePattern, subst: Tree): String = {
@@ -106,7 +110,7 @@ class FileInterface(reporter: Reporter) {
val indent = getLineIndentation(lastFound)
- if (pattern.posIntInfo == (lineno, scalaOffset)) {
+ if (pattern.pos.line == lineno && pattern.pos.col == scalaOffset) {
var lvl = 0;
var i = lastFound + 6;
var continue = true;
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index 7f755e97e6e6304d9ea2035b51479b5d9d81a67d..1d76f388f24faf82dea0cbed50c16630c30f59b9 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -17,7 +17,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
tc.initialize()
- val results = program.definedFunctions.toList.sortWith(_ < _).map { funDef =>
+ val results = program.definedFunctions.toList.sortWith(_.getPos < _.getPos).map { funDef =>
(funDef -> tc.terminates(funDef))
}
val endTime = System.currentTimeMillis
diff --git a/src/main/scala/leon/utils/Positions.scala b/src/main/scala/leon/utils/Positions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b44dc9a36c7924972b114d9b9e4d463b4f59952e
--- /dev/null
+++ b/src/main/scala/leon/utils/Positions.scala
@@ -0,0 +1,54 @@
+package leon
+package utils
+
+import java.io.File
+
+abstract class Position {
+ val line: Int
+ val col: Int
+ val file: File
+
+ def < (that: Position) = {
+ (this.file == that.file) && (this.line < that.line || this.col < that.col)
+ }
+
+ override def toString = line+":"+col
+ def isDefined = true
+}
+
+case class OffsetPosition(line: Int, col: Int, file: File) extends Position
+
+case class RangePosition(lineFrom: Int, colFrom: Int, lineTo: Int, colTo: Int, file: File) extends Position {
+ val line = lineFrom
+ val col = colFrom
+
+ override def toString = lineFrom+":"+colFrom+"->"+lineTo+":"+colTo
+}
+
+case object NoPosition extends Position {
+ val line = -1
+ val col = -1
+ val file = null
+
+ override def toString = "?:?"
+ override def isDefined = false
+}
+
+
+trait Positioned {
+ private[this] var _pos: Position = NoPosition
+
+ def setPos(pos: Position): this.type = {
+ _pos = pos
+ this
+ }
+
+ def setPos(that: Positioned): this.type = {
+ _pos = that.getPos
+ this
+ }
+
+ def getPos = {
+ _pos
+ }
+}
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index c6e9cf4abb3e0a588b09c115e8e323c35db54ac1..dfce1fbfea895ff7e48d164f5c249024a3365d7f 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -25,7 +25,7 @@ object UnitElimination extends TransformationPhase {
//first introduce new signatures without Unit parameters
allFuns.foreach(fd => {
if(fd.returnType != UnitType && fd.args.exists(vd => vd.tpe == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPos(fd)
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
@@ -63,7 +63,7 @@ object UnitElimination extends TransformationPhase {
expr match {
case fi@FunctionInvocation(fd, args) => {
val newArgs = args.filterNot(arg => arg.getType == UnitType)
- FunctionInvocation(fun2FreshFun(fd), newArgs).setPosInfo(fi)
+ FunctionInvocation(fun2FreshFun(fd), newArgs).setPos(fi)
}
case t@Tuple(args) => {
val TupleType(tpes) = t.getType
@@ -101,7 +101,7 @@ object UnitElimination extends TransformationPhase {
removeUnit(b)
else {
val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPos(fd)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
@@ -143,7 +143,7 @@ object UnitElimination extends TransformationPhase {
case GuardedCase(pat, guard, rhs) => GuardedCase(pat, removeUnit(guard), removeUnit(rhs))
}
val tpe = csesRec.head.rhs.getType
- MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPos(m)
}
case _ => sys.error("not supported: " + expr)
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 76a7ea3c2de1c33fc526217cec8110f02e2de2f0..8a162e81ff88efbf989a8e7c82d2f32a8373e08d 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -34,7 +34,9 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
var allVCs = Map[FunDef, List[VerificationCondition]]()
- for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
+ println(purescala.ScalaPrinter(program))
+
+ for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
val tactic: Tactic =
if(funDef.annotations.contains("induct")) {
@@ -66,7 +68,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val interruptManager = vctx.context.interruptManager
- for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1 < b._1); vcInfo <- vcs if !interruptManager.isInterrupted()) {
+ for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1.getPos < b._1.getPos); vcInfo <- vcs if !interruptManager.isInterrupted()) {
val funDef = vcInfo.funDef
val vc = vcInfo.condition
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 44463f11d8755c7219d5c1b1613e3f797688911b..0e258e9aa4d46c852826d6b838c2b524d23bbe6d 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -48,7 +48,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrec
}
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this))
}
}
@@ -88,7 +88,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrecIfDefined(path, newCall),
function,
VCKind.Precondition,
- this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
+ this.asInstanceOf[DefaultTactic]).setPos(fi)
}).toSeq
} else {
Seq.empty
@@ -120,7 +120,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrecIfDefined(pc._1),
function,//if(function.fromLoop) function.parent.get else function,
VCKind.ExhaustiveMatch,
- this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+ this.asInstanceOf[DefaultTactic]).setPos(pc._2)
).toSeq
} else {
Seq.empty
@@ -152,7 +152,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrecIfDefined(pc._1),
function, //if(function.fromLoop) function.parent.get else function,
VCKind.MapAccess,
- this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+ this.asInstanceOf[DefaultTactic]).setPos(pc._2)
).toSeq
} else {
Seq.empty
@@ -181,7 +181,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
withPrecIfDefined(pc._1),
function, //if(function.fromLoop) function.parent.get else function,
VCKind.ArrayAccess,
- this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
+ this.asInstanceOf[DefaultTactic]).setPos(pc._2)
).toSeq
} else {
Seq.empty
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 2138a02cee212522f8e259057e2b1fea3df2c5e2..71d7a31c5568d3ffa8cbdce2c84b5a83bff15689 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -131,7 +131,7 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
})
Implies(And(inductiveHypothesis), toProve)
}
- new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), function, VCKind.Precondition, this).setPosInfo(fi)
+ new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), function, VCKind.Precondition, this).setPos(fi)
}
case _ => scala.sys.error("Abstract class has non-case class subtype")
}))
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index e82d61cf123a9f08f09adce8a2bac57478634c06..660c46309eccd235ba0fa1709486ef25b1f4dee2 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -5,11 +5,12 @@ package leon.verification
import leon.purescala.Trees._
import leon.purescala.Definitions._
import leon.purescala.Common._
+import leon.utils.{Position, Positioned}
import leon.solvers._
/** This is just to hold some history information. */
-class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends ScalacPositional {
+class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends Positioned {
// None = still unknown
// Some(true) = valid
// Some(false) = valid
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 34245e544eeacf48587fe6966364bc1d6d4ba052..a40320ef20a1e92e9549387c1cdfda15df7fa7b4 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -10,7 +10,7 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
(vc1,vc2) =>
val id1 = vc1.funDef.id.name
val id2 = vc2.funDef.id.name
- if(id1 != id2) id1 < id2 else vc1 < vc2
+ if(id1 != id2) id1 < id2 else vc1.getPos < vc2.getPos
}
lazy val totalConditions : Int = conditions.size
@@ -59,7 +59,7 @@ object VerificationReport {
"║ %-25s %-9s %9s %-8s %-10s %-7s %7s ║".format(
fit(vc.funDef.id.toString, 25),
vc.kind,
- vc.posInfo,
+ vc.getPos,
vc.status,
vc.tacticStr,
vc.solverStr,
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 04a75d1037d5aec418d5bbfa7f3b4f184bc50b20..aa259e76c068dc59f2b5c6f96e1bbf5cb7fdd89a 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -39,8 +39,8 @@ object ArrayTransformation extends TransformationPhase {
val length = ArrayLength(ra)
val res = IfExpr(
And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
- ArraySelect(ra, ri).setType(sel.getType).setPosInfo(sel),
- Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
+ ArraySelect(ra, ri).setType(sel.getType).setPos(sel),
+ Error("Index out of bound").setType(sel.getType).setPos(sel)
).setType(sel.getType)
res
}
@@ -52,8 +52,8 @@ object ArrayTransformation extends TransformationPhase {
val length = ArrayLength(ra)
val res = IfExpr(
And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
- Assignment(id, ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up)),
- Error("Index out of bound").setType(UnitType).setPosInfo(up)
+ Assignment(id, ArrayUpdated(ra, ri, rv).setType(ra.getType).setPos(up)),
+ Error("Index out of bound").setType(UnitType).setPos(up)
).setType(UnitType)
res
}
@@ -64,8 +64,8 @@ object ArrayTransformation extends TransformationPhase {
val length = ArrayLength(ra)
val res = IfExpr(
And(LessEquals(IntLiteral(0), ri), LessThan(ri, length)),
- ArrayUpdated(ra, ri, rv).setType(ra.getType).setPosInfo(up),
- Error("Index out of bound").setType(ra.getType).setPosInfo(up)
+ ArrayUpdated(ra, ri, rv).setType(ra.getType).setPos(up),
+ Error("Index out of bound").setType(ra.getType).setPos(up)
).setType(ra.getType)
res
}
@@ -96,7 +96,7 @@ object ArrayTransformation extends TransformationPhase {
case wh@While(c, e) => {
val newWh = While(transform(c), transform(e))
newWh.invariant = wh.invariant.map(i => transform(i))
- newWh.setPosInfo(wh)
+ newWh.setPos(wh)
newWh
}
@@ -114,7 +114,7 @@ object ArrayTransformation extends TransformationPhase {
case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
}
val tpe = csesRec.head.rhs.getType
- MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+ MatchExpr(scrutRec, csesRec).setType(tpe).setPos(m)
}
case LetDef(fd, b) => {
fd.precondition = fd.precondition.map(transform)
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 5e543505ceabcb52fe13b0e4e9efcc44f47d61f2..6e49b70c117ac4164e9c289f4ee7df27f7975aa9 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -24,7 +24,7 @@ object EpsilonElimination extends TransformationPhase {
case eps@Epsilon(pred) => {
val freshName = FreshIdentifier("epsilon")
val newFunDef = new FunDef(freshName, eps.getType, Seq())
- val epsilonVar = EpsilonVariable(eps.posIntInfo)
+ val epsilonVar = EpsilonVariable(eps.getPos)
val resId = FreshIdentifier("res").setType(eps.getType)
val postcondition = replace(Map(epsilonVar -> Variable(resId)), pred)
newFunDef.postcondition = Some((resId, postcondition))
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 89a830056f830ac317c088a910c214f32ab29b9a..94cdd463d110a654db6b7f548684698b6262ed58 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -123,7 +123,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
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).setPosInfo(m)
+ }).setType(matchType).setPos(m)
val scope = ((body: Expr) => {
val tupleId = FreshIdentifier("t").setType(matchType)
@@ -155,12 +155,12 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
val whileFunVarDecls = whileFunVars.map(id => VarDecl(id, id.getType))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
- val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
+ val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), whileFunReturnType, whileFunVarDecls).setPos(wh)
wasLoop += whileFunDef
val whileFunCond = condRes
val whileFunRecursiveCall = replaceNames(condFun,
- bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable)).setPosInfo(wh)))
+ bodyScope(FunctionInvocation(whileFunDef, modifiedVars.map(id => condBodyFun(id).toVariable)).setPos(wh)))
val whileFunBaseCase =
(if(whileFunVars.size == 1)
condFun.get(modifiedVars.head).getOrElse(whileFunVars.head).toVariable
@@ -199,7 +199,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
LetDef(
whileFunDef,
Let(tupleId,
- FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)).setPosInfo(wh),
+ FunctionInvocation(whileFunDef, modifiedVars.map(_.toVariable)).setPos(wh),
if(finalVars.size == 1)
Let(finalVars.head, tupleId.toVariable, body)
else
@@ -252,7 +252,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
case c @ Choose(ids, b) => {
//Recall that Choose cannot mutate variables from the scope
val (bodyRes, bodyScope, bodyFun) = toFunction(b)
- (bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)).setPosInfo(c), bodyFun)
+ (bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)).setPos(c), bodyFun)
}
case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
case n @ NAryOperator(args, recons) => {
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 8595fd3f2805ff822e5869b0a870f59ae8aaa2d1..3b46b29d907dcc37ad8d31b7a74173269ac77792 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -1,14 +1,14 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-
package leon
package xlang
-import leon.purescala.Common._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.Definitions._
-import leon.purescala.Extractors._
-import leon.purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter}
+import purescala.Common._
+import purescala.TypeTrees._
+import purescala.Trees._
+import purescala.Definitions._
+import purescala.Extractors._
+import purescala.{PrettyPrinter, PrettyPrintable, ScalaPrinter}
+import utils._
object Trees {
@@ -53,7 +53,7 @@ object Trees {
}
}
- case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional with BinaryExtractable with PrettyPrintable {
+ case class While(cond: Expr, body: Expr) extends Expr with FixedType with BinaryExtractable with PrettyPrintable {
val fixedType = UnitType
var invariant: Option[Expr] = None
@@ -62,7 +62,7 @@ object Trees {
def setInvariant(inv: Option[Expr]) = { invariant = inv; this }
def extract: Option[(Expr, Expr, (Expr, Expr)=>Expr)] = {
- Some((cond, body, (t1, t2) => While(t1, t2).setInvariant(this.invariant).setPosInfo(this)))
+ Some((cond, body, (t1, t2) => While(t1, t2).setInvariant(this.invariant).setPos(this)))
}
def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
@@ -86,9 +86,9 @@ object Trees {
}
}
- case class Epsilon(pred: Expr) extends Expr with ScalacPositional with UnaryExtractable with PrettyPrintable {
+ case class Epsilon(pred: Expr) extends Expr with UnaryExtractable with PrettyPrintable {
def extract: Option[(Expr, (Expr)=>Expr)] = {
- Some((pred, (expr: Expr) => Epsilon(expr).setType(this.getType).setPosInfo(this)))
+ Some((pred, (expr: Expr) => Epsilon(expr).setType(this.getType).setPos(this)))
}
def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
@@ -97,18 +97,17 @@ object Trees {
sys.error("Not Scala Code")
case _ =>
- printer.append("epsilon(x" + this.posIntInfo._1 + "_" + this.posIntInfo._2 + ". ")
+ printer.append("epsilon(x" + this.getPos.line + "_" + this.getPos.col + ". ")
printer.pp(pred, Some(this))
printer.append(")")
}
}
}
- case class EpsilonVariable(pos: (Int, Int)) extends Expr with Terminal with PrettyPrintable{
+ case class EpsilonVariable(pos: Position) extends Expr with Terminal with PrettyPrintable{
def printWith(printer: PrettyPrinter)(implicit lvl: Int) {
- val (row, col) = pos
- printer.append("x" + row + "_" + col)
+ printer.append("x" + pos.line + "_" + pos.col)
}
}
@@ -171,7 +170,7 @@ object Trees {
//the difference between ArrayUpdate and ArrayUpdated is that the former has a side effect while the latter is the functional version
//ArrayUpdate should be eliminated soon in the analysis while ArrayUpdated is kept all the way to the backend
- case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with ScalacPositional with FixedType with NAryExtractable with PrettyPrintable {
+ case class ArrayUpdate(array: Expr, index: Expr, newValue: Expr) extends Expr with FixedType with NAryExtractable with PrettyPrintable {
val fixedType = UnitType
def extract: Option[(Seq[Expr], (Seq[Expr])=>Expr)] = {
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index 3ec72ee09cea1549a0994ae458052c70496523c2..36f2207879a1191b2aa42464fc26c5a38b8d7ea0 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -72,7 +72,7 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
funDef.parent.getOrElse(funDef),
if(vc.kind == VCKind.Postcondition) VCKind.InvariantPost else if(vc.kind == VCKind.Precondition) VCKind.InvariantInd else vc.kind,
vc.tactic,
- vc.info).setPosInfo(funDef)
+ vc.info).setPos(funDef)
freshVc.value = vc.value
freshVc.solvedWith = vc.solvedWith
freshVc.time = vc.time