diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 8b72eb86c5706c7870acfb44a643ee74b86a1500..9e4939dd47ee7498a605c6f746f9862568197cb9 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -296,10 +296,10 @@ trait CodeExtraction extends ASTExtractors {
val tparams = extractTypeParams(tps.map(_.tpe))
- val dctx = DefContext(tparams.toMap)
+ val newDctx = DefContext(dctx.tparams ++ tparams.toMap)
val newParams = params.map{ vd =>
- val ptpe = toPureScalaType(vd.tpt.tpe)(dctx)
+ val ptpe = toPureScalaType(vd.tpt.tpe)(newDctx)
val newID = FreshIdentifier(vd.symbol.name.toString).setType(ptpe).setPos(vd.pos)
owners += (newID -> None)
varSubsts += vd.symbol -> (() => Variable(newID))
@@ -308,7 +308,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
- new FunDef(FreshIdentifier(sym.name.toString), tparamsDef, toPureScalaType(ret)(dctx), newParams)
+ new FunDef(FreshIdentifier(sym.name.toString), tparamsDef, toPureScalaType(ret)(newDctx), newParams)
}
private def extractFunDef(funDef: FunDef, body: Tree)(implicit dctx: DefContext): FunDef = {
@@ -556,9 +556,6 @@ trait CodeExtraction extends ASTExtractors {
rest = None
Let(newID, valTree, restTree)
- /**
- * XLang Extractors
- */
case ExFunctionDef(symbol, tparams, params, ret, b) =>
val funDef = extractFunSig(symbol, tparams, params, ret)
@@ -566,7 +563,11 @@ trait CodeExtraction extends ASTExtractors {
val oldMutableVarSubst = mutableVarSubsts.toMap //take an immutable snapshot of the map
val oldCurrentFunDef = currentFunDef
mutableVarSubsts.clear //reseting the visible mutable vars, we do not handle mutable variable closure in nested functions
- val funDefWithBody = extractFunDef(funDef, b)
+
+ val tparamsMap = (tparams zip funDef.tparams.map(_.tp)).toMap
+ val newDctx = DefContext(dctx.tparams ++ tparamsMap)
+
+ val funDefWithBody = extractFunDef(funDef, b)(newDctx)
mutableVarSubsts ++= oldMutableVarSubst
currentFunDef = oldCurrentFunDef
val restTree = rest match {
@@ -577,6 +578,10 @@ trait CodeExtraction extends ASTExtractors {
rest = None
LetDef(funDefWithBody, restTree)
+ /**
+ * XLang Extractors
+ */
+
case ExVarDef(vs, tpt, bdy) => {
val binderTpe = extractType(tpt.tpe)
val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index e8838bee75a1ef7f0474cdc3c83221f8f5483b43..89fc30674d9155d5949e0c3714edce32e52c2c50 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -50,7 +50,7 @@ object Common {
def markAsLetBinder : Identifier = { _islb = true; this }
def isLetBinder : Boolean = _islb
- def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).setType(getType)
+ def freshen: Identifier = FreshIdentifier(name, alwaysShowUniqueID).copiedFrom(this)
}
private object UniqueCounter {
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index a02055b7457556ccab7afd560481e9156cb0e910..832c514ab423726968479a9ec0cf774f264dc9d3 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -22,11 +22,10 @@ object Definitions {
}
/** A VarDecl declares a new identifier to be of a certain type. */
- case class VarDecl(id: Identifier, tpe: TypeTree) extends Definition with Typed {
+ case class VarDecl(id: Identifier, tpe: TypeTree) extends Definition with FixedType {
self: Serializable =>
- override def getType = tpe
- override def setType(tt: TypeTree) = scala.sys.error("Can't set type of VarDecl.")
+ val fixedType = tpe
override def hashCode : Int = id.hashCode
override def equals(that : Any) : Boolean = that match {
@@ -316,7 +315,7 @@ object Definitions {
}
private lazy val typesMap = {
- (fd.tparams zip tps).toMap
+ (fd.tparams zip tps).toMap.filter(tt => tt._1 != tt._2)
}
def translated(t: TypeTree): TypeTree = instantiateType(t, typesMap)
@@ -324,7 +323,7 @@ object Definitions {
def translated(e: Expr): Expr = instantiateType(e, typesMap, argsMap)
lazy val (args: Seq[VarDecl], argsMap: Map[Identifier, Identifier]) = {
- if (tps.isEmpty) {
+ if (typesMap.isEmpty) {
(fd.args, Map())
} else {
val newArgs = fd.args.map {
@@ -365,7 +364,7 @@ object Definitions {
}
def postcondition = fd.postcondition.map {
- case (id, post) if tps.nonEmpty =>
+ case (id, post) if typesMap.nonEmpty =>
postCache.getOrElse((id, post), {
val nId = FreshIdentifier(id.name).setType(translated(id.getType)).copiedFrom(id)
val res = nId -> instantiateType(post, typesMap, argsMap + (id -> nId))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 63d302ad2dad607089fceaf2ae106aa9d099e404..a5962a428b3497730f6c475d12e83d9b0efaf474 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -14,7 +14,7 @@ import java.lang.StringBuffer
/** This pretty-printer uses Unicode for some operators, to make sure we
* distinguish PureScala from "real" Scala (and also because it's cute). */
-class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
+class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffer) {
override def toString = sb.toString
def append(str: String) {
@@ -57,20 +57,16 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
sb.append(post)
}
- def idToString(id: Identifier): String = {
- if (opts.printUniqueIds) {
- id.uniqueName
- } else {
- id.toString
- }
- }
-
def pp(tree: Tree, parent: Option[Tree])(implicit lvl: Int): Unit = {
implicit val p = Some(tree)
tree match {
case id: Identifier =>
- sb.append(idToString(id))
+ if (opts.printUniqueIds) {
+ sb.append(id.uniqueName)
+ } else {
+ sb.append(id.toString)
+ }
case Variable(id) =>
//sb.append("(")
@@ -80,7 +76,8 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
//sb.append(")")
case LetTuple(bs,d,e) =>
- sb.append("(let (" + bs.map(idToString _).mkString(",") + " := ");
+ sb.append("(let ")
+ ppNary(bs, "(", ",", " :=");
pp(d, p)
sb.append(") in")
nl(lvl+1)
@@ -88,7 +85,9 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
sb.append(")")
case Let(b,d,e) =>
- sb.append("(let (" + idToString(b) + " := ");
+ sb.append("(let (")
+ pp(b, p)
+ sb.append(" := ");
pp(d, p)
sb.append(") in")
nl(lvl+1)
@@ -124,7 +123,9 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
sb.append("._" + i)
case c@Choose(vars, pred) =>
- sb.append("choose("+vars.map(idToString _).mkString(", ")+" => ")
+ sb.append("choose(")
+ ppNary(vars, "", ", ", "")
+ sb.append(" => ")
pp(pred, p)
sb.append(")")
@@ -144,10 +145,11 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
case CaseClassSelector(_, cc, id) =>
pp(cc, p)
- sb.append("." + idToString(id))
+ sb.append(".")
+ pp(id, p)
case FunctionInvocation(tfd, args) =>
- sb.append(idToString(tfd.id))
+ pp(tfd.id, p)
if (tfd.tps.nonEmpty) {
ppNary(tfd.tps, "[", ",", "]")
@@ -307,7 +309,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
sb.append(")")
case WildcardPattern(None) => sb.append("_")
- case WildcardPattern(Some(id)) => sb.append(idToString(id))
+ case WildcardPattern(Some(id)) => pp(id, p)
case InstanceOfPattern(bndr, cct) =>
bndr.foreach(b => sb.append(b + " : "))
pp(cct, p)
@@ -325,6 +327,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
// Types
case Untyped => sb.append("???")
+ case BottomType => sb.append("Nothing")
case UnitType => sb.append("Unit")
case Int32Type => sb.append("Int")
case BooleanType => sb.append("Boolean")
@@ -357,7 +360,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
pp(tt, p)
case c: ClassType =>
- sb.append(idToString(c.classDef.id))
+ pp(c.classDef.id, p)
if (c.tps.nonEmpty) {
ppNary(c.tps, "[", ",", "]")
}
@@ -367,7 +370,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
case Program(id, mainObj) =>
assert(lvl == 0)
sb.append("package ")
- sb.append(idToString(id))
+ pp(id, p)
sb.append(" {\n")
pp(mainObj, p)(lvl+1)
sb.append("}\n")
@@ -375,7 +378,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
case ModuleDef(id, defs, invs) =>
nl
sb.append("object ")
- sb.append(idToString(id))
+ pp(id, p)
sb.append(" {")
var c = 0
@@ -395,8 +398,11 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
case AbstractClassDef(id, tparams, parent) =>
nl
sb.append("sealed abstract class ")
- sb.append(idToString(id))
- parent.foreach(p => sb.append(" extends " + idToString(p.id)))
+ pp(id, p)
+ parent.foreach{ par =>
+ sb.append(" extends ")
+ pp(par.id, p)
+ }
case ccd @ CaseClassDef(id, tparams, parent, isObj) =>
nl
@@ -406,7 +412,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
sb.append("case class ")
}
- sb.append(idToString(id))
+ pp(id, p)
if (tparams.nonEmpty) {
ppNary(tparams, "[", ", ", "]")
@@ -416,7 +422,10 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
ppNary(ccd.fields, "(", ", ", ")")
}
- parent.foreach(p => sb.append(" extends " + idToString(p.id)))
+ parent.foreach{ par =>
+ sb.append(" extends ")
+ pp(par.id, p)
+ }
case fd: FunDef =>
for(a <- fd.annotations) {
@@ -434,14 +443,15 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
fd.postcondition.foreach{ case (id, postc) => {
ind
sb.append("@post: ")
- sb.append(idToString(id)+" => ")
+ pp(id, p)
+ sb.append(" => ")
pp(postc, p)(lvl)
sb.append("\n")
}}
ind
sb.append("def ")
- sb.append(idToString(fd.id))
+ pp(fd.id, p)
sb.append("(")
val sz = fd.args.size
@@ -473,7 +483,7 @@ class PrettyPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) {
pp(tp, p)
case TypeParameter(id) =>
- pp(id, p)
+ sb.append(id.uniqueName)
case _ => sb.append("Tree? (" + tree.getClass + ")")
}
@@ -498,7 +508,15 @@ trait PrettyPrintable {
}
class EquivalencePrettyPrinter(opts: PrinterOptions) extends PrettyPrinter(opts) {
- override def idToString(id: Identifier) = id.name
+ override def pp(tree: Tree, parent: Option[Tree])(implicit lvl: Int): Unit = {
+ tree match {
+ case id: Identifier =>
+ sb.append(id.name)
+
+ case _ =>
+ super.pp(tree, parent)
+ }
+ }
}
abstract class PrettyPrinterFactory {
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 3bbfc02603a94dd60e4cd6d8ae1faef17dbc5e47..843e0905bb99472eaca61192cf281d4986cdf890 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -53,12 +53,15 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
var printPos = opts.printPositions
tree match {
- case Variable(id) => sb.append(idToString(id))
+ case Variable(id) =>
+ pp(id, p)
+
case LetTuple(ids,d,e) =>
optBraces { implicit lvl =>
sb.append("val (" )
for (((id, tpe), i) <- ids.map(id => (id, id.getType)).zipWithIndex) {
- sb.append(idToString(id)+": ")
+ pp(id, p)
+ sb.append(": ")
pp(tpe, p)
if (i != ids.size-1) {
sb.append(", ")
@@ -111,8 +114,13 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
pp(t, p)
sb.append("._" + i)
- case FunctionInvocation(fd, args) =>
- sb.append(idToString(fd.id))
+ case FunctionInvocation(tfd, args) =>
+ pp(tfd.id, p)
+
+ if (tfd.tps.nonEmpty) {
+ ppNary(tfd.tps, "[", ", ", "]")
+ }
+
ppNary(args, "(", ", ", ")")
case Plus(l,r) => optParentheses { ppBinary(l, r, " + ") }
@@ -226,7 +234,8 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
optParentheses {
sb.append("choose { (")
for (((id, tpe), i) <- ids.map(id => (id, id.getType)).zipWithIndex) {
- sb.append(idToString(id)+": ")
+ pp(id, p)
+ sb.append(": ")
pp(tpe, p)
if (i != ids.size-1) {
sb.append(", ")
@@ -273,7 +282,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case ModuleDef(id, defs, invs) =>
sb.append("object ")
- sb.append(idToString(id))
+ pp(id, p)
sb.append(" {\n")
var c = 0
@@ -294,13 +303,16 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case AbstractClassDef(id, tparams, parent) =>
sb.append("sealed abstract class ")
- sb.append(idToString(id))
+ pp(id, p)
if (tparams.nonEmpty) {
ppNary(tparams, "[", ",", "]")
}
- parent.foreach(p => sb.append(" extends " + idToString(p.id)))
+ parent.foreach{ par =>
+ sb.append(" extends ")
+ pp(par.id, p)
+ }
case ccd @ CaseClassDef(id, tparams, parent, isObj) =>
if (isObj) {
@@ -309,7 +321,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
sb.append("case class ")
}
- sb.append(idToString(id))
+ pp(id, p)
if (tparams.nonEmpty) {
ppNary(tparams, "[", ", ", "]")
@@ -319,7 +331,10 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
ppNary(ccd.fields, "(", ", ", ")")
}
- parent.foreach(p => sb.append(" extends " + idToString(p.id)))
+ parent.foreach{ par =>
+ sb.append(" extends ")
+ pp(par.id, p)
+ }
case vd: VarDecl =>
pp(vd.id, p)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 59d0ba02c27e326c5993f2e9ad8de7105cf548da..0bd6546bda2ff4f2e47be0f1285aa37c0cb32c9c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -292,6 +292,7 @@ object TreeOps {
e match {
case Variable(i) => subvs + i
+ case LetDef(fd,_) => subvs -- fd.args.map(_.id) -- fd.postcondition.map(_._1)
case Let(i,_,_) => subvs - i
case Choose(is,_) => subvs -- is
case MatchExpr(_, cses) => subvs -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9344224129106a0b849a5b0834e60182ec07b2d2..a9e7904f3591e60a287b63d54a149f3af65665c4 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -454,6 +454,7 @@ trait AbstractZ3Solver
}
protected[leon] def toZ3Formula(expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
+
class CantTranslateException extends Exception
val varsInformula: Set[Identifier] = variablesOf(expr)