diff --git a/src/main/scala/leon/SubtypingPhase.scala b/src/main/scala/leon/SubtypingPhase.scala
index 8a63663b4080bde72176297814a27ec44ab4bce8..350c7ddac18d333505d2654275a98f962720e318 100644
--- a/src/main/scala/leon/SubtypingPhase.scala
+++ b/src/main/scala/leon/SubtypingPhase.scala
@@ -2,6 +2,7 @@
package leon
+import purescala.Common._
import purescala.TypeTrees._
import purescala.Trees._
import purescala.Definitions._
@@ -32,10 +33,15 @@ object SubtypingPhase extends LeonPhase[Program, Program] {
fd.postcondition = fd.returnType match {
case cct@CaseClassType(cd) => {
- val subtypingConstraint = CaseClassInstanceOf(cd, ResultVariable())
+
fd.postcondition match {
- case Some(p) => Some(And(subtypingConstraint, p))
- case None => Some(subtypingConstraint)
+ case Some((id, p)) =>
+ Some((id, And(CaseClassInstanceOf(cd, Variable(id)), p)))
+
+ case None =>
+ val resId = FreshIdentifier("res").setType(cct)
+
+ Some((resId, CaseClassInstanceOf(cd, Variable(resId))))
}
}
case _ => fd.postcondition
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
deleted file mode 100644
index 2733b8781ecbd3abc66fdb6496ee77b55994deb8..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/TypeChecking.scala
+++ /dev/null
@@ -1,119 +0,0 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
-
-package leon
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TypeTrees._
-
-object TypeChecking extends UnitPhase[Program] {
-
- val name = "Type Checking"
- val description = "Type check the AST"
-
- def apply(ctx: LeonContext, pgm: Program): Unit = {
- val allFuns = pgm.definedFunctions
-
- allFuns.foreach(fd => {
- fd.precondition.foreach(typeCheck)
- fd.postcondition.foreach(typeCheck)
- fd.body.foreach(typeCheck)
- })
- }
-
- private def typeCheck(expr: Expr): Unit = { //expr match {
- //quick hack
- //searchAndReplaceDFS(e => {
- // if(e.getType == Untyped) {
- // println("Expression is untyped: " + e)
- // }
- // None
- //})(expr)
-
- //case l@Let(i, v, b) => {
- // if(l.getType == Untyp
- // val vr = transform(v)
- // v.getType match {
- // case ArrayType(_) => {
- // val freshIdentifier = FreshIdentifier("t").setType(vr.getType)
- // id2id += (i -> freshIdentifier)
- // val br = transform(b)
- // LetVar(freshIdentifier, vr, br)
- // }
- // case _ => {
- // val br = transform(b)
- // Let(i, vr, br)
- // }
- // }
- //}
- //case LetVar(id, e, b) => {
- // val er = transform(e)
- // val br = transform(b)
- // LetVar(id, er, br)
- //}
- //case wh@While(c, e) => {
- // val newWh = While(transform(c), transform(e))
- // newWh.invariant = wh.invariant.map(i => transform(i))
- // newWh.setPosInfo(wh)
- //}
-
- //case ite@IfExpr(c, t, e) => {
- // val rc = transform(c)
- // val rt = transform(t)
- // val re = transform(e)
- // IfExpr(rc, rt, re).setType(rt.getType)
- //}
-
- //case m @ MatchExpr(scrut, cses) => {
- // val scrutRec = transform(scrut)
- // val csesRec = cses.map{
- // case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
- // case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
- // }
- // val tpe = csesRec.head.rhs.getType
- // MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
- //}
- //case LetDef(fd, b) => {
- // val newFd = if(fd.hasImplementation) {
- // val body = fd.body.get
- // val args = fd.args
- // val newFd =
- // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
- // val newArgs = args.map(vd => {
- // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
- // id2id += (vd.id -> freshId)
- // val newTpe = transform(vd.tpe)
- // VarDecl(freshId, newTpe)
- // })
- // val freshFunName = FreshIdentifier(fd.id.name)
- // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
- // fd2fd += (fd -> freshFunDef)
- // freshFunDef.precondition = fd.precondition.map(transform)
- // freshFunDef.postcondition = fd.postcondition.map(transform)
- // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
- // freshFunDef
- // } else fd
- // val newBody = transform(body)
- // newFd.body = Some(newBody)
- // newFd
- // } else fd
- // val rb = transform(b)
- // LetDef(newFd, rb)
- //}
- //case FunctionInvocation(fd, args) => {
- // val rargs = args.map(transform)
- // val rfd = fd2fd.get(fd).getOrElse(fd)
- // FunctionInvocation(rfd, rargs)
- //}
-
- //case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
- //case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
- //case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
-
- //case v @ Variable(id) => if(id2id.isDefinedAt(id)) Variable(id2id(id)) else v
- //case (t: Terminal) => t
- //case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
- }
-
-}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index b98224402ed252b9801b11d846f4aa4dea039fd6..727c6ab2b5a311a6b2b9d614c45fb207cc45f587 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -68,9 +68,8 @@ object CodeGeneration {
}
val bodyWithPost = if(funDef.hasPostcondition && env.compileContracts) {
- val freshResID = FreshIdentifier("result").setType(funDef.returnType)
- val post = purescala.TreeOps.replace(Map(ResultVariable() -> Variable(freshResID)), funDef.postcondition.get)
- Let(freshResID, bodyWithPre, IfExpr(post, Variable(freshResID), Error("Postcondition failed")) )
+ val Some((id, post)) = funDef.postcondition
+ Let(id, bodyWithPre, IfExpr(post, Variable(id), Error("Postcondition failed")) )
} else {
bodyWithPre
}
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index b10f23bef57e1904185c429c35c1092fd1dc22fd..dd55f2b5d65c333b575a54605d685ba0eda596f4 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -87,8 +87,10 @@ class DefaultEvaluator(ctx : LeonContext, prog : Program) extends Evaluator(ctx,
val callResult = rec(frame, matchToIfThenElse(body))
if(fd.hasPostcondition) {
+ val (id, post) = fd.postcondition.get
+
val freshResID = FreshIdentifier("result").setType(fd.returnType)
- val postBody = replace(Map(ResultVariable() -> Variable(freshResID)), matchToIfThenElse(fd.postcondition.get))
+ val postBody = replace(Map(Variable(id) -> Variable(freshResID)), matchToIfThenElse(post))
rec(frame + ((freshResID -> callResult)), postBody) match {
case BooleanLiteral(true) => ;
case BooleanLiteral(false) => throw RuntimeError("Postcondition violation for " + fd.id.name + " reached in evaluation.")
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index bd07bf48b594a144b27ab9d48b16e5ba451eacc5..6f9c3101defff497d48fe92493544501f35928f5 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -239,11 +239,13 @@ trait CodeExtraction extends Extractors {
val (body2, ensuring) = body match {
case ExEnsuredExpression(body2, resSym, contract) =>
- varSubsts(resSym) = (() => ResultVariable().setType(funDef.returnType))
- (body2, toPureScala(contract))
+ val resId = FreshIdentifier(resSym.name.toString).setType(funDef.returnType)
+ varSubsts(resSym) = (() => Variable(resId))
+ (body2, toPureScala(contract).map(r => (resId, r)))
case ExHoldsExpression(body2) =>
- (body2, Some(ResultVariable().setType(BooleanType)))
+ val resId = FreshIdentifier("res").setType(BooleanType)
+ (body2, Some((resId, Variable(resId))))
case _ =>
(body, None)
@@ -288,7 +290,7 @@ trait CodeExtraction extends Extractors {
}
}
- val finalEnsuring = ensuring.filter{ e =>
+ val finalEnsuring = ensuring.filter{ case (id, e) =>
if(containsLetDef(e)) {
reporter.error(body3.pos, "Function postcondition should not contain nested function definition")
false
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index f1f3311becb8249fa2b5180569f3d9c22e9e3099..b62992618575b17cbd0cc6f923d1e44a6939b1d0 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -18,7 +18,6 @@ object Definitions {
case t : Definition => t.id == this.id
case _ => false
}
- def allIdentifiers : Set[Identifier]
}
/** A VarDecl declares a new identifier to be of a certain type. */
@@ -58,8 +57,6 @@ object Definitions {
def isRecursive(f1: FunDef) = mainObject.isRecursive(f1)
def isCatamorphism(f1: FunDef) = mainObject.isCatamorphism(f1)
def caseClassDef(name: String) = mainObject.caseClassDef(name)
- def allIdentifiers : Set[Identifier] = mainObject.allIdentifiers + id
- //def isPure: Boolean = definedFunctions.forall(fd => fd.body.forall(TreeOps.isPure) && fd.precondition.forall(TreeOps.isPure) && fd.postcondition.forall(TreeOps.isPure))
def writeScalaFile(filename: String) {
import java.io.FileWriter
@@ -92,11 +89,6 @@ object Definitions {
def caseClassDef(caseClassName : String) : CaseClassDef =
definedClasses.find(ctd => ctd.id.name == caseClassName).getOrElse(scala.sys.error("Asking for non-existent case class def: " + caseClassName)).asInstanceOf[CaseClassDef]
- def allIdentifiers : Set[Identifier] = {
- (defs map (_.allIdentifiers)).foldLeft(Set[Identifier]())((a, b) => a ++ b) ++
- (invariants map (TreeOps.allIdentifiers(_))).foldLeft(Set[Identifier]())((a, b) => a ++ b) + id
- }
-
lazy val classHierarchyRoots : Seq[ClassTypeDef] = defs.filter(_.isInstanceOf[ClassTypeDef]).map(_.asInstanceOf[ClassTypeDef]).filter(!_.hasParent)
lazy val algebraicDataTypes : Map[AbstractClassDef,Seq[CaseClassDef]] = (defs.collect {
@@ -120,7 +112,7 @@ object Definitions {
val resSet: CallGraph = (for(funDef <- definedFunctions) yield {
funDef.precondition.map(treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, _)).getOrElse(Set.empty) ++
funDef.body.map(treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, _)).getOrElse(Set.empty) ++
- funDef.postcondition.map(treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, _)).getOrElse(Set.empty)
+ funDef.postcondition.map( pc => treeCatamorphism[CallGraph](convert, combine, compute(funDef)_, pc._2)).getOrElse(Set.empty)
}).reduceLeft(_ ++ _)
var callers: Map[FunDef,Set[FunDef]] =
@@ -215,10 +207,6 @@ object Definitions {
children = child :: children
}
- def allIdentifiers : Set[Identifier] = {
- fields.map(f => f.id).toSet + id
- }
-
def knownChildren : Seq[ClassTypeDef] = {
children
}
@@ -264,10 +252,6 @@ object Definitions {
}
def parent = parent_
- def allIdentifiers : Set[Identifier] = {
- fields.map(f => f.id).toSet
- }
-
def fieldsIds = fields.map(_.id)
def selectorID2Index(id: Identifier) : Int = {
@@ -289,50 +273,27 @@ object Definitions {
}
}
- /** "Regular" classes */
- //class ClassDef(val id: Identifier, var parent: Option[AbstractClassDef]) extends ClassTypeDef {
- // var fields: VarDecls = Nil
- // val isAbstract = false
- //}
-
/** Values */
case class ValDef(varDecl: VarDecl, value: Expr) extends Definition {
val id: Identifier = varDecl.id
- def allIdentifiers : Set[Identifier] = TreeOps.allIdentifiers(value) + id
}
/** Functions (= 'methods' of objects) */
- object FunDef {
- def unapply(fd: FunDef): Option[(Identifier,TypeTree,VarDecls,Option[Expr],Option[Expr],Option[Expr])] = {
- if(fd != null) {
- Some((fd.id, fd.returnType, fd.args, fd.body, fd.precondition, fd.postcondition))
- } else {
- None
- }
- }
- }
class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition with ScalacPositional {
var body: Option[Expr] = None
def implementation : Option[Expr] = body
var precondition: Option[Expr] = None
- var postcondition: Option[Expr] = None
+ var postcondition: Option[(Identifier, Expr)] = None
// Metadata kept here after transformations
var parent: Option[FunDef] = None
var orig: Option[FunDef] = None
def hasImplementation : Boolean = body.isDefined
- def hasBody = hasImplementation
- def hasPrecondition : Boolean = precondition.isDefined
- def hasPostcondition : Boolean = postcondition.isDefined
-
- def allIdentifiers : Set[Identifier] = {
- args.map(_.id).toSet ++
- body.map(TreeOps.allIdentifiers(_)).getOrElse(Set[Identifier]()) ++
- precondition.map(TreeOps.allIdentifiers(_)).getOrElse(Set[Identifier]()) ++
- postcondition.map(TreeOps.allIdentifiers(_)).getOrElse(Set[Identifier]()) + id
- }
-
+ def hasBody = hasImplementation
+ def hasPrecondition : Boolean = precondition.isDefined
+ def hasPostcondition : Boolean = postcondition.isDefined
+
private var annots: Set[String] = Set.empty[String]
def addAnnotation(as: String*) : FunDef = {
annots = annots ++ as
@@ -342,68 +303,4 @@ object Definitions {
def isPrivate : Boolean = annots.contains("private")
}
-
- object Catamorphism {
- // If a function is a catamorphism, this deconstructs it into the cases. Eg:
- // def size(l : List) : Int = ...
- // should return:
- // List,
- // Seq(
- // (Nil(), 0)
- // (Cons(x, xs), 1 + size(xs)))
- // ...where x and xs are fresh (and could be unused in the expr)
- import scala.collection.mutable.{Map=>MutableMap}
- type CataRepr = (AbstractClassDef,Seq[(CaseClass,Expr)])
- private val unapplyCache : MutableMap[FunDef,CataRepr] = MutableMap.empty
-
- def unapply(funDef : FunDef) : Option[CataRepr] = if(
- funDef == null ||
- funDef.args.size != 1 ||
- funDef.hasPrecondition ||
- !funDef.hasImplementation ||
- (funDef.hasPostcondition && functionCallsOf(funDef.postcondition.get) != Set.empty)
- ) {
- None
- } else if(unapplyCache.isDefinedAt(funDef)) {
- Some(unapplyCache(funDef))
- } else {
- var moreConditions = true
- val argVar = funDef.args(0).toVariable
- val argVarType = argVar.getType
- val body = funDef.body.get
- val iteized = matchToIfThenElse(body)
- val invocations = functionCallsOf(iteized)
- moreConditions = moreConditions && invocations.forall(_ match {
- case FunctionInvocation(fd, Seq(CaseClassSelector(_, e, _))) if fd == funDef && e == argVar => true
- case _ => false
- })
- moreConditions = moreConditions && argVarType.isInstanceOf[AbstractClassType]
- var spmList : Seq[(CaseClassDef,Identifier,Seq[Identifier],Expr)] = Seq.empty
- moreConditions = moreConditions && (body match {
- case SimplePatternMatching(scrut, _, s) if scrut == argVar => spmList = s; true
- case _ => false
- })
-
- val patternSeq : Seq[(CaseClass,Expr)] = if(moreConditions) {
- spmList.map(tuple => {
- val (ccd, id, ids, ex) = tuple
- val ex2 = matchToIfThenElse(ex)
- if(!(variablesOf(ex2) -- ids).isEmpty) {
- moreConditions = false
- }
- (CaseClass(ccd, ids.map(Variable(_))), ex2)
- })
- } else {
- Seq.empty
- }
-
- if(moreConditions) {
- val finalResult = (argVarType.asInstanceOf[AbstractClassType].classDef, patternSeq)
- unapplyCache(funDef) = finalResult
- Some(finalResult)
- } else {
- None
- }
- }
- }
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 02e0e7c2978d8462a8983fd3091ae73471f9a1ba..2047e175597ef4b8791ece32281441378023c39a 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -143,17 +143,17 @@ object Extractors {
fd.precondition = Some(as(2))
LetDef(fd, as(1))
}))
- case (None, Some(post)) =>
+ case (None, Some((pid, post))) =>
Some((Seq(b, body, post), (as: Seq[Expr]) => {
fd.body = Some(as(0))
- fd.postcondition = Some(as(2))
+ fd.postcondition = Some((pid, as(2)))
LetDef(fd, as(1))
}))
- case (Some(pre), Some(post)) =>
+ case (Some(pre), Some((pid, post))) =>
Some((Seq(b, body, pre, post), (as: Seq[Expr]) => {
fd.body = Some(as(0))
fd.precondition = Some(as(2))
- fd.postcondition = Some(as(3))
+ fd.postcondition = Some((pid, as(3)))
LetDef(fd, as(1))
}))
}
@@ -169,15 +169,15 @@ object Extractors {
fd.precondition = Some(as(1))
LetDef(fd, as(0))
}))
- case (None, Some(post)) =>
+ case (None, Some((pid, post))) =>
Some((Seq(body, post), (as: Seq[Expr]) => {
- fd.postcondition = Some(as(1))
+ fd.postcondition = Some((pid, as(1)))
LetDef(fd, as(0))
}))
- case (Some(pre), Some(post)) =>
+ case (Some(pre), Some((pid, post))) =>
Some((Seq(body, pre, post), (as: Seq[Expr]) => {
fd.precondition = Some(as(1))
- fd.postcondition = Some(as(2))
+ fd.postcondition = Some((pid, as(2)))
LetDef(fd, as(0))
}))
}
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index e4d006e2ec25d07b7b0af8c47af345506772d7f4..5b0b7aaaf6b694eef91648f425f099d75000ef6e 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -77,7 +77,7 @@ object FunctionClosure extends TransformationPhase {
val newPrecondition = simplifyLets(introduceLets(And((capturedConstraints ++ fd.precondition).toSeq), fd2FreshFd))
newFunDef.precondition = if(newPrecondition == BooleanLiteral(true)) None else Some(newPrecondition)
- val freshPostcondition = fd.postcondition.map(post => introduceLets(post, fd2FreshFd))
+ val freshPostcondition = fd.postcondition.map{ case (id, post) => (id, introduceLets(post, fd2FreshFd)) }
newFunDef.postcondition = freshPostcondition
pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 147c4635b3e277439c24d1539023bafbf3fc796c..551ea44c0d05e18f1dc004b1df93e4987e0f8746 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -276,7 +276,6 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
sb.append("}")
}
- case ResultVariable() => sb.append("#res")
case Not(expr) => ppUnary(expr, "\u00AC(", ")", lvl) // \neg
case e @ Error(desc) =>
@@ -380,35 +379,36 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
parent.foreach(p => sb.append(" extends " + idToString(p.id)))
}
- case fd @ FunDef(id, rt, args, body, pre, post) => {
+ case fd: FunDef =>
for(a <- fd.annotations) {
ind(lvl)
sb.append("@" + a + "\n")
}
- pre.foreach(prec => {
+ fd.precondition.foreach(prec => {
ind(lvl)
sb.append("@pre : ")
pp(prec, lvl)
sb.append("\n")
})
- post.foreach(postc => {
+ fd.postcondition.foreach{ case (id, postc) => {
ind(lvl)
sb.append("@post: ")
+ sb.append(idToString(id)+" => ")
pp(postc, lvl)
sb.append("\n")
- })
+ }}
ind(lvl)
sb.append("def ")
- sb.append(idToString(id))
+ sb.append(idToString(fd.id))
sb.append("(")
- val sz = args.size
+ val sz = fd.args.size
var c = 0
- args.foreach(arg => {
+ fd.args.foreach(arg => {
sb.append(arg.id)
sb.append(" : ")
pp(arg.tpe, lvl)
@@ -420,13 +420,15 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
})
sb.append(") : ")
- pp(rt, lvl)
+ pp(fd.returnType, lvl)
sb.append(" = ")
- if(body.isDefined)
- pp(body.get, lvl)
- else
- sb.append("[unknown function implementation]")
- }
+ fd.body match {
+ case Some(body) =>
+ pp(body, lvl)
+
+ case None =>
+ sb.append("[unknown function implementation]")
+ }
case _ => sb.append("Defn?")
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index b1d82854d7594bc8c24d8f938bc2f4da4b86d0d2..0c338c4259bbb121ad4b70a6c833fe418767dacc 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -285,7 +285,6 @@ class ScalaPrinter(sb: StringBuffer = new StringBuffer) extends PrettyPrinter(sb
sb.append(")")
}
- case ResultVariable() => sb.append("res")
case Not(expr) => ppUnary(expr, "!(", ")", lvl) // \neg
case e @ Error(desc) => {
@@ -388,22 +387,17 @@ class ScalaPrinter(sb: StringBuffer = new StringBuffer) extends PrettyPrinter(sb
sb.append(")")
parent.foreach(p => sb.append(" extends " + p.id))
- case fd @ FunDef(id, rt, args, body, pre, post) =>
-
- //for(a <- fd.annotations) {
- // ind(lvl)
- // sb.append("@" + a + "\n")
- //}
+ case fd: FunDef =>
ind(lvl)
sb.append("def ")
- sb.append(id)
+ sb.append(fd.id)
sb.append("(")
- val sz = args.size
+ val sz = fd.args.size
var c = 0
- args.foreach(arg => {
+ fd.args.foreach(arg => {
sb.append(arg.id)
sb.append(" : ")
pp(arg.tpe, lvl)
@@ -415,41 +409,35 @@ class ScalaPrinter(sb: StringBuffer = new StringBuffer) extends PrettyPrinter(sb
})
sb.append(") : ")
- pp(rt, lvl)
- sb.append(" = (")
- if(body.isDefined) {
- pre match {
- case None => pp(body.get, lvl)
- case Some(prec) => {
- sb.append("{\n")
- ind(lvl+1)
- sb.append("require(")
- pp(prec, lvl+1)
- sb.append(")\n")
- pp(body.get, lvl)
- sb.append("\n")
- ind(lvl)
- sb.append("}")
- }
- }
- } else
- sb.append("[unknown function implementation]")
+ pp(fd.returnType, lvl)
+ sb.append(" = {")
+
+ fd.precondition match {
+ case None =>
+ case Some(prec) =>
+ ind(lvl+1)
+ sb.append("require(")
+ pp(prec, lvl+1)
+ sb.append(");\n")
+ }
- post match {
- case None => {
- sb.append(")")
- }
- case Some(postc) => {
- val res = Variable(FreshIdentifier("res", true).setType(fd.returnType))
+ fd.body match {
+ case Some(body) =>
+ pp(body, lvl)
+ case None =>
+ sb.append("???")
+ }
- val newPost = TreeOps.replace(Map(ResultVariable() -> res), postc)
+ fd.postcondition match {
+ case None =>
+ sb.append("}")
- sb.append(" ensuring(")
- pp(res, lvl)
- sb.append(" => ") //TODO, not very general solution...
- pp(newPost, lvl)
- sb.append("))")
- }
+ case Some((id, postc)) =>
+ sb.append("} ensuring(")
+ pp(Variable(id), lvl)
+ sb.append(" => ")
+ pp(postc, lvl)
+ sb.append(")")
}
case _ => sb.append("Defn?")
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 45a5ba008d66feb18f4f3db797db3080242ca12f..32e377b4ab08d2ef9590fb2b99295d2d29a409c7 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -433,22 +433,6 @@ object TreeOps {
expr)
}
- def allIdentifiers(expr: Expr) : Set[Identifier] = expr match {
- case l @ Let(binder, e, b) => allIdentifiers(e) ++ allIdentifiers(b) + binder
- //TODO: Cannot have LetVar nor LetDef here, should not be visible at this point
- //case l @ LetVar(binder, e, b) => allIdentifiers(e) ++ allIdentifiers(b) + binder
- //case l @ LetDef(fd, b) => allIdentifiers(fd.getBody) ++ allIdentifiers(b) + fd.id
- case n @ NAryOperator(args, _) =>
- (args map (TreeOps.allIdentifiers(_))).foldLeft(Set[Identifier]())((a, b) => a ++ b)
- case b @ BinaryOperator(a1,a2,_) => allIdentifiers(a1) ++ allIdentifiers(a2)
- case u @ UnaryOperator(a,_) => allIdentifiers(a)
- case i @ IfExpr(a1,a2,a3) => allIdentifiers(a1) ++ allIdentifiers(a2) ++ allIdentifiers(a3)
- case m @ MatchExpr(scrut, cses) =>
- (cses map (_.allIdentifiers)).foldLeft(Set[Identifier]())((a, b) => a ++ b) ++ allIdentifiers(scrut)
- case Variable(id) => Set(id)
- case t: Terminal => Set.empty
- }
-
def allDeBruijnIndices(expr: Expr) : Set[DeBruijnIndex] = {
def convert(t: Expr) : Set[DeBruijnIndex] = t match {
case i @ DeBruijnIndex(idx) => Set(i)
@@ -1456,8 +1440,13 @@ object TreeOps {
newFd.body = fd.body.map(b => rec(b, newScope))
newFd.precondition = fd.precondition.map(pre => rec(pre, newScope))
- newFd.postcondition = fd.postcondition.map(post => rec(post, newScope))
+ newFd.postcondition = fd.postcondition.map {
+ case (id, post) =>
+ val nid = genId(id, newScope)
+ val postScope = newScope.register(id -> nid)
+ (id, rec(post, postScope))
+ }
LetDef(newFd, rec(body, newScope))
@@ -1628,13 +1617,6 @@ object TreeOps {
case l @ LetDef(fd, bdy) =>
LetDef(fd2fd(fd), bdy)
- case r @ ResultVariable() =>
- mapType(r.getType).map { newType =>
- ResultVariable().setType(newType)
- } getOrElse {
- r
- }
-
case FunctionInvocation(fd, args) =>
FunctionInvocation(fd2fd(fd), args)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index f4f18b1b7f3a6f8b6d55cfffbd5f2f244c3986ca..ad833062293a509ded51159a00af7268aea1aba3 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -145,13 +145,6 @@ object Trees {
val theGuard: Option[Expr]
def hasGuard = theGuard.isDefined
def expressions: Seq[Expr]
-
- def allIdentifiers : Set[Identifier] = {
- pattern.allIdentifiers ++
- TreeOps.allIdentifiers(rhs) ++
- theGuard.map(TreeOps.allIdentifiers(_)).getOrElse(Set[Identifier]()) ++
- (expressions map (TreeOps.allIdentifiers(_))).foldLeft(Set[Identifier]())((a, b) => a ++ b)
- }
}
case class SimpleCase(pattern: Pattern, rhs: Expr) extends MatchCase {
@@ -169,11 +162,8 @@ object Trees {
private def subBinders = subPatterns.map(_.binders).foldLeft[Set[Identifier]](Set.empty)(_ ++ _)
def binders: Set[Identifier] = subBinders ++ (if(binder.isDefined) Set(binder.get) else Set.empty)
-
- def allIdentifiers : Set[Identifier] = {
- ((subPatterns map (_.allIdentifiers)).foldLeft(Set[Identifier]())((a, b) => a ++ b)) ++ binders
- }
}
+
case class InstanceOfPattern(binder: Option[Identifier], classTypeDef: ClassTypeDef) extends Pattern { // c: Class
val subPatterns = Seq.empty
}
@@ -389,9 +379,6 @@ object Trees {
case class DeBruijnIndex(index: Int) extends Expr with Terminal
- // represents the result in post-conditions
- case class ResultVariable() extends Expr with Terminal
-
/* Literals */
sealed abstract class Literal[T] extends Expr with Terminal {
val value: T
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 6c5e64b19eeb9df3a063698df21716ce0ab4436e..5a3f2e2f4700dd0f118184377c63fdfa0c3313f0 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -344,8 +344,8 @@ object FunctionTemplate {
// Now the postcondition.
funDef.postcondition match {
- case Some(post) =>
- val newPost : Expr = replace(Map(ResultVariable() -> invocation), matchToIfThenElse(post))
+ case Some((id, post)) =>
+ val newPost : Expr = replace(Map(Variable(id) -> invocation), matchToIfThenElse(post))
val postHolds : Expr =
if(funDef.hasPrecondition) {
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 42546b01abc6328fa3ffb824cfddb1b59f17f741..9c47c9e38ab4eb479e9349551ec555010cca035d 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -155,19 +155,19 @@ class SimpleSearch(synth: Synthesizer,
val map = (p.as.map(Variable(_): Expr) zip freshAs.map(Variable(_): Expr)).toMap
- val res = ResultVariable().setType(ret)
+ val res = Variable(FreshIdentifier("res").setType(ret))
val mapPost: Map[Expr, Expr] = if (p.xs.size > 1) {
p.xs.zipWithIndex.map{ case (id, i) =>
Variable(id) -> TupleSelect(res, i+1)
}.toMap
} else {
- Map(Variable(p.xs.head) -> ResultVariable().setType(ret))
+ Map(Variable(p.xs.head) -> res)
}
val fd = new FunDef(FreshIdentifier("chimp", true), ret, freshAs.map(id => VarDecl(id, id.getType)))
fd.precondition = Some(replace(map, p.pc))
- fd.postcondition = Some(replace(map++mapPost, p.phi))
+ fd.postcondition = Some((res.id, replace(map++mapPost, p.phi)))
fd
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 42032b3e61ca2064a0acc2b3250d8fbaf56ca546..3f53f26abb4beffe434dcdd842c74a621f6f7d5d 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -122,7 +122,7 @@ class Synthesizer(val context : LeonContext,
// Create new fundef for the body
val ret = TupleType(problem.xs.map(_.getType))
- val res = ResultVariable().setType(ret)
+ val res = Variable(FreshIdentifier("res").setType(ret))
val mapPost: Map[Expr, Expr] =
problem.xs.zipWithIndex.map{ case (id, i) =>
@@ -131,7 +131,7 @@ class Synthesizer(val context : LeonContext,
val fd = new FunDef(FreshIdentifier("finalTerm", true), ret, problem.as.map(id => VarDecl(id, id.getType)))
fd.precondition = Some(And(problem.pc, sol.pre))
- fd.postcondition = Some(replace(mapPost, problem.phi))
+ fd.postcondition = Some((res.id, replace(mapPost, problem.phi)))
fd.body = Some(sol.term)
val newDefs = sol.defs + fd
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 2a7b60bd5a4d1e9cf21d60f3fa664337a6e5d101..4b8786987bee1e69f4f3a58f012c66861c2ba6ce 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -103,10 +103,11 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
} else {
val funPre = substAll(substMap, And(p.pc, Or(globalPre)))
val funPost = substAll(substMap, p.phi)
+ val idPost = FreshIdentifier("res").setType(resType)
val outerPre = Or(globalPre)
newFun.precondition = Some(funPre)
- newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(resType), funPost))
+ newFun.postcondition = Some((idPost, LetTuple(p.xs.toSeq, Variable(idPost), funPost)))
newFun.body = Some(MatchExpr(Variable(inductOn), cases))
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index 0437e52e331160bb91e5fa6a371c9062aea8a7f6..db5af8c78876881ce48db86c77312e08c0248b59 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -155,10 +155,11 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
} else {
val funPre = substAll(substMap, And(p.pc, Or(globalPre)))
val funPost = substAll(substMap, p.phi)
+ val idPost = FreshIdentifier("res").setType(resType)
val outerPre = Or(globalPre)
newFun.precondition = Some(funPre)
- newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(resType), funPost))
+ newFun.postcondition = Some((idPost, LetTuple(p.xs.toSeq, Variable(idPost), funPost)))
newFun.body = Some(MatchExpr(Variable(inductOn), cases))
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index 7799a01dee767adf61c1d33848ec00b49bd458bc..1be8dd8eee16e74063a10ef2bbcc3e4c02d68cf0 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -44,8 +44,10 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
val preOut = subst(inductOn -> Variable(origId), preIn)
val newFun = new FunDef(FreshIdentifier("rec", true), tpe, Seq(VarDecl(inductOn, inductOn.getType)))
+ val idPost = FreshIdentifier("res").setType(tpe)
+
newFun.precondition = Some(preIn)
- newFun.postcondition = Some(LetTuple(p.xs.toSeq, ResultVariable().setType(tpe), p.phi))
+ newFun.postcondition = Some((idPost, LetTuple(p.xs.toSeq, Variable(idPost), p.phi)))
newFun.body = Some(
IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index 98303cd74948897246a79157ca0f078350544a9a..058474b2635512a73ff43acb9adfc2b93885dea0 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -87,7 +87,7 @@ class SimpleTerminationChecker(context : LeonContext, program : Program) extends
} getOrElse Set.empty[FunctionInvocation]
}
- val callsToAnalyze = callsOfInterest(funDef.body) ++ callsOfInterest(funDef.precondition) ++ callsOfInterest(funDef.postcondition)
+ val callsToAnalyze = callsOfInterest(funDef.body) ++ callsOfInterest(funDef.precondition) ++ callsOfInterest(funDef.postcondition.map(_._2))
assert(!callsToAnalyze.isEmpty)
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 94f4526f3ce7ea7b4f0af707f3cb774efc41a5a5..44463f11d8755c7219d5c1b1613e3f797688911b 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -28,25 +28,27 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
def generatePostconditions(functionDefinition: FunDef) : Seq[VerificationCondition] = {
assert(functionDefinition.body.isDefined)
val prec = functionDefinition.precondition
- val post = functionDefinition.postcondition
+ val optPost = functionDefinition.postcondition
val body = matchToIfThenElse(functionDefinition.body.get)
- if(post.isEmpty) {
- Seq.empty
- } else {
- val theExpr = {
- val resFresh = FreshIdentifier("result", true).setType(body.getType)
- val bodyAndPost = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(post.get)))
-
- val withPrec = if(prec.isEmpty) {
- bodyAndPost
- } else {
- Implies(matchToIfThenElse(prec.get), bodyAndPost)
- }
+ optPost match {
+ case None =>
+ Seq()
- withPrec
- }
- Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
+ case Some((id, post)) =>
+ val theExpr = {
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPost = Let(resFresh, body, replace(Map(Variable(id) -> Variable(resFresh)), matchToIfThenElse(post)))
+
+ val withPrec = if(prec.isEmpty) {
+ bodyAndPost
+ } else {
+ Implies(matchToIfThenElse(prec.get), bodyAndPost)
+ }
+
+ withPrec
+ }
+ Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
}
}
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 26d9de252f9eed3826a8d4db34f7cbe4e0ac1f4d..2138a02cee212522f8e259057e2b1fea3df2c5e2 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -38,39 +38,41 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
firstAbsClassDef(funDef.args) match {
case Some((classDef, arg)) =>
val prec = funDef.precondition
- val post = funDef.postcondition
+ val optPost = funDef.postcondition
val body = matchToIfThenElse(funDef.body.get)
val argAsVar = arg.toVariable
- if (post.isEmpty) {
- Seq.empty
- } else {
- val children = classDef.knownChildren
- val conditionsForEachChild = (for (child <- classDef.knownChildren) yield (child match {
- case ccd @ CaseClassDef(id, prnt, vds) =>
- val selectors = selectorsOfParentType(classDefToClassType(classDef), ccd, argAsVar)
- // if no subtrees of parent type, assert property for base case
- val resFresh = FreshIdentifier("result", true).setType(body.getType)
- val bodyAndPostForArg = Let(resFresh, body, replace(Map(ResultVariable() -> Variable(resFresh)), matchToIfThenElse(post.get)))
- val withPrec = if (prec.isEmpty) bodyAndPostForArg else Implies(matchToIfThenElse(prec.get), bodyAndPostForArg)
-
- val conditionForChild =
- if (selectors.size == 0)
- withPrec
- else {
- val inductiveHypothesis = (for (sel <- selectors) yield {
- val resFresh = FreshIdentifier("result", true).setType(body.getType)
- val bodyAndPost = Let(resFresh, replace(Map(argAsVar -> sel), body), replace(Map(ResultVariable() -> Variable(resFresh), argAsVar -> sel), matchToIfThenElse(post.get)))
- val withPrec = if (prec.isEmpty) bodyAndPost else Implies(replace(Map(argAsVar -> sel), matchToIfThenElse(prec.get)), bodyAndPost)
+ optPost match {
+ case None =>
+ Seq.empty
+ case Some((pid, post)) =>
+ val children = classDef.knownChildren
+ val conditionsForEachChild = (for (child <- classDef.knownChildren) yield (child match {
+ case ccd @ CaseClassDef(id, prnt, vds) =>
+ val selectors = selectorsOfParentType(classDefToClassType(classDef), ccd, argAsVar)
+ // if no subtrees of parent type, assert property for base case
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPostForArg = Let(resFresh, body, replace(Map(Variable(pid) -> Variable(resFresh)), matchToIfThenElse(post)))
+ val withPrec = if (prec.isEmpty) bodyAndPostForArg else Implies(matchToIfThenElse(prec.get), bodyAndPostForArg)
+
+ val conditionForChild =
+ if (selectors.size == 0)
withPrec
- })
- Implies(And(inductiveHypothesis), withPrec)
- }
- new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this)
- case _ => scala.sys.error("Abstract class has non-case class subtype.")
- }))
- conditionsForEachChild
+ else {
+ val inductiveHypothesis = (for (sel <- selectors) yield {
+ val resFresh = FreshIdentifier("result", true).setType(body.getType)
+ val bodyAndPost = Let(resFresh, replace(Map(argAsVar -> sel), body), replace(Map(Variable(pid) -> Variable(resFresh), argAsVar -> sel), matchToIfThenElse(post)))
+ val withPrec = if (prec.isEmpty) bodyAndPost else Implies(replace(Map(argAsVar -> sel), matchToIfThenElse(prec.get)), bodyAndPost)
+ withPrec
+ })
+ Implies(And(inductiveHypothesis), withPrec)
+ }
+ new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this)
+ case _ => scala.sys.error("Abstract class has non-case class subtype.")
+ }))
+ conditionsForEachChild
}
+
case None =>
reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
defaultPost
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index fb930993103cb6f70cf92b50a10db3999b9eca43..04a75d1037d5aec418d5bbfa7f3b4f184bc50b20 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -26,7 +26,7 @@ object ArrayTransformation extends TransformationPhase {
id2FreshId = Map()
fd.precondition = fd.precondition.map(transform)
fd.body = fd.body.map(transform)
- fd.postcondition = fd.postcondition.map(transform)
+ fd.postcondition = fd.postcondition.map { case (id, post) => (id, transform(post)) }
})
pgm
}
@@ -119,7 +119,7 @@ object ArrayTransformation extends TransformationPhase {
case LetDef(fd, b) => {
fd.precondition = fd.precondition.map(transform)
fd.body = fd.body.map(transform)
- fd.postcondition = fd.postcondition.map(transform)
+ fd.postcondition = fd.postcondition.map { case (id, post) => (id, transform(post)) }
val rb = transform(b)
LetDef(fd, rb)
}
@@ -131,173 +131,4 @@ object ArrayTransformation extends TransformationPhase {
case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
}
- //val newFuns: Seq[FunDef] = allFuns.map(fd => {
- // if(fd.hasImplementation) {
- // val args = fd.args
- // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
- // val newArgs = args.map(vd => {
- // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
- // id2id += (vd.id -> freshId)
- // val newTpe = transform(vd.tpe)
- // VarDecl(freshId, newTpe)
- // })
- // val freshFunName = FreshIdentifier(fd.id.name)
- // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
- // fd2fd += (fd -> freshFunDef)
- // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
- // freshFunDef
- // } else fd
- // } else fd
- //})
-
- //allFuns.zip(newFuns).foreach{ case (ofd, nfd) => ofd.body.map(body => {
- // nfd.precondition = ofd.precondition.map(transform)
- // nfd.postcondition = ofd.postcondition.map(transform)
- // val newBody = transform(body)
- // nfd.body = Some(newBody)
- //})}
-
- //val Program(id, ObjectDef(objId, _, invariants)) = pgm
- //val allClasses: Seq[Definition] = pgm.definedClasses
- //Program(id, ObjectDef(objId, allClasses ++ newFuns, invariants))
-
-
- //private def transform(tpe: TypeTree): TypeTree = tpe match {
- // case ArrayType(base) => TupleType(Seq(ArrayType(transform(base)), Int32Type))
- // case TupleType(tpes) => TupleType(tpes.map(transform))
- // case t => t
- //}
- //private def containsArrayType(tpe: TypeTree): Boolean = tpe match {
- // case ArrayType(base) => true
- // case TupleType(tpes) => tpes.exists(containsArrayType)
- // case t => false
- //}
-
- //private var id2id: Map[Identifier, Identifier] = Map()
- //private var fd2fd: Map[FunDef, FunDef] = Map()
-
- //private def transform(expr: Expr): Expr = expr match {
- // case fill@ArrayFill(length, default) => {
- // var rLength = transform(length)
- // val rDefault = transform(default)
- // val rFill = ArrayMake(rDefault).setType(fill.getType)
- // Tuple(Seq(rFill, rLength)).setType(TupleType(Seq(fill.getType, Int32Type)))
- // }
- // case sel@ArraySelect(a, i) => {
- // val ar = transform(a)
- // val ir = transform(i)
- // val length = TupleSelect(ar, 2).setType(Int32Type)
- // IfExpr(
- // And(GreaterEquals(ir, IntLiteral(0)), LessThan(ir, length)),
- // ArraySelect(TupleSelect(ar, 1).setType(ArrayType(sel.getType)), ir).setType(sel.getType).setPosInfo(sel),
- // Error("Index out of bound").setType(sel.getType).setPosInfo(sel)
- // ).setType(sel.getType)
- // }
- // case up@ArrayUpdate(a, i, v) => {
- // val ar = transform(a)
- // val ir = transform(i)
- // val vr = transform(v)
- // val Variable(id) = ar
- // val length = TupleSelect(ar, 2).setType(Int32Type)
- // val array = TupleSelect(ar, 1).setType(ArrayType(v.getType))
- // IfExpr(
- // And(GreaterEquals(i, IntLiteral(0)), LessThan(i, length)),
- // Assignment(
- // id,
- // Tuple(Seq(
- // ArrayUpdated(array, ir, vr).setType(array.getType).setPosInfo(up),
- // length)
- // ).setType(TupleType(Seq(array.getType, Int32Type)))),
- // Error("Index out of bound").setType(UnitType).setPosInfo(up)
- // ).setType(UnitType)
- // }
- // case ArrayLength(a) => {
- // val ar = transform(a)
- // TupleSelect(ar, 2).setType(Int32Type)
- // }
- // case Let(i, v, b) => {
- // val vr = transform(v)
- // v.getType match {
- // case ArrayType(_) => {
- // val freshIdentifier = FreshIdentifier("t").setType(vr.getType)
- // id2id += (i -> freshIdentifier)
- // val br = transform(b)
- // LetVar(freshIdentifier, vr, br)
- // }
- // case _ => {
- // val br = transform(b)
- // Let(i, vr, br)
- // }
- // }
- // }
- // case LetVar(id, e, b) => {
- // val er = transform(e)
- // val br = transform(b)
- // LetVar(id, er, br)
- // }
- // case wh@While(c, e) => {
- // val newWh = While(transform(c), transform(e))
- // newWh.invariant = wh.invariant.map(i => transform(i))
- // newWh.setPosInfo(wh)
- // }
-
- // case ite@IfExpr(c, t, e) => {
- // val rc = transform(c)
- // val rt = transform(t)
- // val re = transform(e)
- // IfExpr(rc, rt, re).setType(rt.getType)
- // }
-
- // case m @ MatchExpr(scrut, cses) => {
- // val scrutRec = transform(scrut)
- // val csesRec = cses.map{
- // case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
- // case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
- // }
- // val tpe = csesRec.head.rhs.getType
- // MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
- // }
- // case LetDef(fd, b) => {
- // val newFd = if(fd.hasImplementation) {
- // val body = fd.body.get
- // val args = fd.args
- // val newFd =
- // if(args.exists(vd => containsArrayType(vd.tpe)) || containsArrayType(fd.returnType)) {
- // val newArgs = args.map(vd => {
- // val freshId = FreshIdentifier(vd.id.name).setType(transform(vd.tpe))
- // id2id += (vd.id -> freshId)
- // val newTpe = transform(vd.tpe)
- // VarDecl(freshId, newTpe)
- // })
- // val freshFunName = FreshIdentifier(fd.id.name)
- // val freshFunDef = new FunDef(freshFunName, transform(fd.returnType), newArgs)
- // fd2fd += (fd -> freshFunDef)
- // freshFunDef.precondition = fd.precondition.map(transform)
- // freshFunDef.postcondition = fd.postcondition.map(transform)
- // freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
- // freshFunDef
- // } else fd
- // val newBody = transform(body)
- // newFd.body = Some(newBody)
- // newFd
- // } else fd
- // val rb = transform(b)
- // LetDef(newFd, rb)
- // }
- // case FunctionInvocation(fd, args) => {
- // val rargs = args.map(transform)
- // val rfd = fd2fd.get(fd).getOrElse(fd)
- // FunctionInvocation(rfd, rargs)
- // }
-
- // case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)
- // case b @ BinaryOperator(a1, a2, recons) => recons(transform(a1), transform(a2)).setType(b.getType)
- // case u @ UnaryOperator(a, recons) => recons(transform(a)).setType(u.getType)
-
- // case v @ Variable(id) => if(id2id.isDefinedAt(id)) Variable(id2id(id)) else v
- // case (t: Terminal) => t
- // case unhandled => scala.sys.error("Non-terminal case should be handled in ArrayTransformation: " + unhandled)
-
- //}
-
}
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 7a9d3245f59650d53e8b42fe75146e66f2b11198..5e543505ceabcb52fe13b0e4e9efcc44f47d61f2 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -25,9 +25,9 @@ object EpsilonElimination extends TransformationPhase {
val freshName = FreshIdentifier("epsilon")
val newFunDef = new FunDef(freshName, eps.getType, Seq())
val epsilonVar = EpsilonVariable(eps.posIntInfo)
- val resultVar = ResultVariable().setType(eps.getType)
- val postcondition = replace(Map(epsilonVar -> resultVar), pred)
- newFunDef.postcondition = Some(postcondition)
+ val resId = FreshIdentifier("res").setType(eps.getType)
+ val postcondition = replace(Map(epsilonVar -> Variable(resId)), pred)
+ newFunDef.postcondition = Some((resId, postcondition))
Some(LetDef(newFunDef, FunctionInvocation(newFunDef, Seq())))
}
case _ => None
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index a9054aea47ada170e721a268c6b0e7bc5ae0aacd..89a830056f830ac317c088a910c214f32ab29b9a 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -171,7 +171,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
condScope(IfExpr(whileFunCond, whileFunRecursiveCall, whileFunBaseCase).setType(whileFunReturnType)))
whileFunDef.body = Some(whileFunBody)
- val resVar = ResultVariable().setType(whileFunReturnType)
+ val resVar = Variable(FreshIdentifier("res").setType(whileFunReturnType))
val whileFunVars2ResultVars: Map[Expr, Expr] =
if(whileFunVars.size == 1)
Map(whileFunVars.head.toVariable -> resVar)
@@ -188,10 +188,10 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
val invariantPostcondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2ResultVars, expr))
whileFunDef.precondition = invariantPrecondition
whileFunDef.postcondition = trivialPostcondition.map(expr =>
- And(expr, invariantPostcondition match {
+ (resVar.id, And(expr, invariantPostcondition match {
case Some(e) => e
case None => BooleanLiteral(true)
- }))
+ })))
val finalVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
val finalScope = ((body: Expr) => {