diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 24dadb7240a72bcf92388ddcdb9ecfb52fbb9ba4..d3fd0df76e0af16176dae96724d9c4da64f494e9 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -140,7 +140,7 @@ trait CodeGeneration {
val cf = classes(owner)
val (_,mn,_) = leonFunDefToJVMInfo(funDef).get
- val paramsTypes = funDef.params.map(a => typeToJVM(a.tpe))
+ val paramsTypes = funDef.params.map(a => typeToJVM(a.getType))
val realParams = if (params.requireMonitor) {
("L" + MonitorClass + ";") +: paramsTypes
@@ -255,7 +255,7 @@ trait CodeGeneration {
if (params.requireMonitor)
ch << ALoad(locals.monitorIndex)
for((a, vd) <- as zip cct.classDef.fields) {
- vd.tpe match {
+ vd.getType match {
case TypeParameter(_) =>
mkBoxedExpr(a, ch)
case _ =>
@@ -461,7 +461,7 @@ trait CodeGeneration {
}
for((a, vd) <- as zip tfd.fd.params) {
- vd.tpe match {
+ vd.getType match {
case TypeParameter(_) =>
mkBoxedExpr(a, ch)
case _ =>
@@ -515,7 +515,7 @@ trait CodeGeneration {
}
for((a, vd) <- as zip tfd.fd.params) {
- vd.tpe match {
+ vd.getType match {
case TypeParameter(_) =>
mkBoxedExpr(a, ch)
case _ =>
@@ -591,7 +591,7 @@ trait CodeGeneration {
}
locally {
- val argTypes = args.map(arg => typeToJVM(arg.tpe))
+ val argTypes = args.map(arg => typeToJVM(arg.getType))
val apm = cf.addMethod("Ljava/lang/Object;", "apply", "[Ljava/lang/Object;")
@@ -1290,7 +1290,7 @@ trait CodeGeneration {
val ccd = cct.classDef
ccd.fields.zipWithIndex.find(_._1.id == id) match {
case Some((f, i)) =>
- val expType = cct.fields(i).tpe
+ val expType = cct.fields(i).getType
val cName = defToJVMName(ccd)
if (params.doInstrument) {
@@ -1302,9 +1302,9 @@ trait CodeGeneration {
ch << IOR
ch << PutField(cName, instrumentedField, "I")
}
- ch << GetField(cName, f.id.name, typeToJVM(f.tpe))
+ ch << GetField(cName, f.id.name, typeToJVM(f.getType))
- f.tpe match {
+ f.getType match {
case TypeParameter(_) =>
mkUnbox(expType, ch)
case _ =>
@@ -1356,7 +1356,7 @@ trait CodeGeneration {
}
// Case class parameters
- val namesTypes = ccd.fields.map { vd => (vd.id.name, typeToJVM(vd.tpe)) }
+ val namesTypes = ccd.fields.map { vd => (vd.id.name, typeToJVM(vd.getType)) }
// definition of the constructor
if(!params.doInstrument && !params.requireMonitor && ccd.fields.isEmpty && ccd.methods.filter{ _.canBeField }.isEmpty) {
@@ -1474,7 +1474,7 @@ trait CodeGeneration {
// We are saved because it is not used anywhere,
// but beware if you decide to add any mkExpr and the like.
instrumentedGetField(pech, cct, f.id)(NoLocals(false))
- mkBox(f.tpe, pech)(NoLocals(false))
+ mkBox(f.getType, pech)(NoLocals(false))
pech << AASTORE
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 0e15bc6db719cfc6db98a7d318556ff96d149a3a..5b01232c47ac3a663ea3564f85386425539f881d 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -60,7 +60,7 @@ class CompilationUnit(val ctx: LeonContext,
classes.get(cd) match {
case Some(cf) =>
val monitorType = if (params.requireMonitor) "L"+MonitorClass+";" else ""
- val sig = "(" + monitorType + cd.fields.map(f => typeToJVM(f.tpe)).mkString("") + ")V"
+ val sig = "(" + monitorType + cd.fields.map(f => typeToJVM(f.getType)).mkString("") + ")V"
Some((cf.className, sig))
case _ => None
}
@@ -80,7 +80,7 @@ class CompilationUnit(val ctx: LeonContext,
funDefInfo.get(fd).orElse {
val monitorType = if (params.requireMonitor) "L"+MonitorClass+";" else ""
- val sig = "(" + monitorType + fd.params.map(a => typeToJVM(a.tpe)).mkString("") + ")" + typeToJVM(fd.returnType)
+ val sig = "(" + monitorType + fd.params.map(a => typeToJVM(a.getType)).mkString("") + ")" + typeToJVM(fd.returnType)
defToModuleOrClass.get(fd).flatMap(m => classes.get(m)) match {
case Some(cf) =>
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 3b29ef4ac086abb187b908493c1da05711ffa363..d1fd76888b47e3dd0db830bf72cfd114150f7b96 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -115,7 +115,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val body = grouped.init.foldRight(grouped.last.last) { case (t, elze) =>
IfExpr(Equals(argsTuple, tupleWrap(t.init)), t.last, elze)
}
- Lambda(args.map(id => ValDef(id, id.getType)), body)
+ Lambda(args.map(id => ValDef(id)), body)
}, ft.toString + "@" + size)
}
constructors += ft -> cs
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9a7255eb0dd5e36af397d02ca2e77ac155860b51..056acc8a6367bc3595a4709080496203964a7da7 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -496,7 +496,7 @@ trait CodeExtraction extends ASTExtractors {
val fields = args.map { case (symbol, t) =>
val tpt = t.tpt
val tpe = toPureScalaType(tpt.tpe)(defCtx, sym.pos)
- LeonValDef(FreshIdentifier(symbol.name.toString, tpe).setPos(t.pos), tpe).setPos(t.pos)
+ LeonValDef(FreshIdentifier(symbol.name.toString, tpe).setPos(t.pos)).setPos(t.pos)
}
ccd.setFields(fields)
@@ -587,7 +587,7 @@ trait CodeExtraction extends ASTExtractors {
val ptpe = toPureScalaType(sym.tpe)(nctx, sym.pos)
val newID = FreshIdentifier(sym.name.toString, ptpe).setPos(sym.pos)
owners += (newID -> None)
- LeonValDef(newID, ptpe).setPos(sym.pos)
+ LeonValDef(newID).setPos(sym.pos)
}
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
@@ -1297,7 +1297,7 @@ trait CodeExtraction extends ASTExtractors {
val aTpe = extractType(vd.tpt)
val newID = FreshIdentifier(vd.symbol.name.toString, aTpe)
owners += (newID -> None)
- LeonValDef(newID, aTpe)
+ LeonValDef(newID)
}
val newVars = (args zip vds).map { case (vd, lvd) =>
@@ -1313,7 +1313,7 @@ trait CodeExtraction extends ASTExtractors {
val aTpe = extractType(tpt)
val newID = FreshIdentifier(sym.name.toString, aTpe)
owners += (newID -> None)
- LeonValDef(newID, aTpe)
+ LeonValDef(newID)
}
val newVars = (args zip vds) map { case ((_, sym), vd) =>
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index f82ea8a6d0e928144cc803d7f9667f5680ab6610..02eae14fa5b5b91b16e2964f41f16ee1fdb0abe9 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -219,7 +219,7 @@ object Constructors {
def finiteLambda(default: Expr, els: Seq[(Expr, Expr)], inputTypes: Seq[TypeTree]): Lambda = {
val UnwrapTupleType(argTypes) = els.headOption.map{_._1.getType}.getOrElse(tupleTypeWrap(inputTypes))
- val args = argTypes map { argType => ValDef(FreshIdentifier("x", argType, true), argType) }
+ val args = argTypes map { argType => ValDef(FreshIdentifier("x", argType, true)) }
if (els.isEmpty) {
Lambda(args, default)
} else {
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index d01290bbf15ab1f31eb903d3cb2dc07857d9772e..eee37aa029fe6ad62ca5bf8b6566616d6739e574 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -47,16 +47,17 @@ object Definitions {
/**
* A ValDef declares a new identifier to be of a certain type.
- * When creating a new FunDef, its parameters should obey (id.getType == tp)
+ * The optional tpe, if present, overrides the type of the underlying Identifier id
+ * This is useful to instantiate argument types of polymorphic functions
*/
- case class ValDef(id: Identifier, tpe: TypeTree) extends Definition with Typed {
+ case class ValDef(id: Identifier, tpe: Option[TypeTree] = None) extends Definition with Typed {
self: Serializable =>
- val getType = tpe
+ val getType = tpe getOrElse id.getType
def subDefinitions = Seq()
- def toVariable : Variable = Variable(id, Some(tpe))
+ def toVariable : Variable = Variable(id, tpe)
setSubDefOwners()
}
@@ -473,11 +474,10 @@ object Definitions {
(fd.params, Map())
} else {
val newParams = fd.params.map {
- case vd @ ValDef(id, tpe) =>
- val newTpe = translated(tpe)
+ case vd @ ValDef(id, _) =>
+ val newTpe = translated(vd.getType)
val newId = FreshIdentifier(id.name, newTpe, true).copiedFrom(id)
-
- ValDef(newId, newTpe).setPos(vd)
+ ValDef(newId).setPos(vd)
}
val paramsMap: Map[Identifier, Identifier] = (fd.params zip newParams).map { case (vd1, vd2) => vd1.id -> vd2.id }.toMap
@@ -486,7 +486,7 @@ object Definitions {
}
}
- lazy val functionType = FunctionType(params.map(_.tpe).toList, returnType)
+ lazy val functionType = FunctionType(params.map(_.getType).toList, returnType)
lazy val returnType: TypeTree = translated(fd.returnType)
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index a70de453aa7cb8b7ead42646ed463a97c9f7f04d..10a30c416c6f43d71a52b989282f497d623dee0b 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -55,7 +55,7 @@ object FunctionClosure extends TransformationPhase {
val extraValDefOldIds: Seq[Identifier] = capturedVars.toSeq
val extraValDefFreshIds: Seq[Identifier] = extraValDefOldIds.map(freshIds(_))
- val extraValDefs: Seq[ValDef] = extraValDefFreshIds.map{id => ValDef(id, id.getType)}
+ val extraValDefs: Seq[ValDef] = extraValDefFreshIds.map(ValDef(_))
val newValDefs: Seq[ValDef] = fd.params ++ extraValDefs
val newBindedVars: Set[Identifier] = bindedVars ++ fd.params.map(_.id)
val newFunId = FreshIdentifier(fd.id.uniqueName) //since we hoist this at the top level, we need to make it a unique name
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index b7c766def0b52a81c2b26e3acb5a5dd660f15b0e..4c82c31d71d3e7769c22f88300d3e6b2b92202b2 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -31,13 +31,13 @@ object MethodLifting extends TransformationPhase {
val retType = instantiateType(fd.returnType, tparamsMap)
val fdParams = fd.params map { vd =>
val newId = FreshIdentifier(vd.id.name, instantiateType(vd.id.getType, tparamsMap))
- ValDef(newId, newId.getType)
+ ValDef(newId)
}
val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
val receiver = FreshIdentifier("$this", recType).setPos(cd.id)
- val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver, recType) +: fdParams, fd.defType)
+ val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams, fd.defType)
nfd.copyContentFrom(fd)
nfd.setPos(fd)
nfd.fullBody = instantiateType(nfd.fullBody, tparamsMap, paramsMap)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index e8849a54951b11c58fbd171e998edf916faaddc9..6e0195fc0add618728d93c79f8f20dbc836177ba 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -408,7 +408,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
case Not(expr) => p"\u00AC$expr"
- case ValDef(id, tpe) => p"${typed(id)}"
+ case vd@ValDef(id, _) => p"$id : ${vd.getType}"
case This(_) => p"this"
case (tfd: TypedFunDef) => p"typed def ${tfd.id}[${tfd.tps}]"
case TypeParameterDef(tp) => p"$tp"
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 95bb91aa50ebac17a764077605f4cd6f0d7422c1..a87805871840bed4bca0e6ca497246bb49c110e7 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1033,7 +1033,7 @@ object TreeOps {
GenericValue(tp, 0)
case FunctionType(from, to) =>
- val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true), tpe))
+ val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true)))
Lambda(args, simplestValue(to))
case _ => throw new Exception("I can't choose simplest value for type " + tpe)
@@ -1395,7 +1395,7 @@ object TreeOps {
val isType = CaseClassInstanceOf(cct, Variable(on))
val recSelectors = cct.fields.collect {
- case vd if vd.tpe == on.getType => vd.id
+ case vd if vd.getType == on.getType => vd.id
}
if (recSelectors.isEmpty) {
@@ -1667,7 +1667,7 @@ object TreeOps {
}
subChecks.forall { case (ccd, subs) =>
- val tpes = ccd.fields.map(_.tpe)
+ val tpes = ccd.fields.map(_.getType)
if (subs.isEmpty) {
false
@@ -1901,7 +1901,7 @@ object TreeOps {
case _ : Lambda => expr
case _ : Variable => expr
case e =>
- val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true), tpe))
+ val args = from.map(tpe => ValDef(FreshIdentifier("x", tpe, true)))
val application = apply(expr, args.map(_.toVariable))
Lambda(args, lift(application))
}
@@ -2050,7 +2050,7 @@ object TreeOps {
case a : AbstractClassType => None
case cct : CaseClassType =>
// This is really just one big assertion. We don't rewrite class defs.
- val fieldTypes = cct.fields.map(_.tpe)
+ val fieldTypes = cct.fields.map(_.getType)
if(fieldTypes.exists(t => t match {
case TupleType(ts) if ts.size <= 1 => true
case _ => false
@@ -2068,7 +2068,7 @@ object TreeOps {
def fd2fd(funDef : FunDef) : FunDef = funDefMap.get(funDef) match {
case Some(fd) => fd
case None =>
- if(funDef.params.map(vd => mapType(vd.tpe)).exists(_.isDefined)) {
+ if(funDef.params.map(vd => mapType(vd.getType)).exists(_.isDefined)) {
scala.sys.error("Cannot rewrite function def that takes degenerate tuple arguments,")
}
val newFD = mapType(funDef.returnType) match {
@@ -2245,7 +2245,7 @@ object TreeOps {
if (conditions contains fieldSel) {
computePatternFor(conditions(fieldSel), fieldSel)
} else {
- val b = FreshIdentifier(f.id.name, f.tpe, true)
+ val b = FreshIdentifier(f.id.name, f.getType, true)
substMap += fieldSel -> Variable(b)
WildcardPattern(Some(b))
}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 5b650a5541cf3f47a3b4881d9067bf40398f8a9b..2792539aa51fc12eb6f2b7b09a6c120686085c97 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -99,7 +99,7 @@ object Trees {
}
case class Lambda(args: Seq[ValDef], body: Expr) extends Expr {
- val getType = FunctionType(args.map(_.tpe), body.getType).unveilUntyped
+ val getType = FunctionType(args.map(_.getType), body.getType).unveilUntyped
}
case class Forall(args: Seq[ValDef], body: Expr) extends Expr {
@@ -241,7 +241,7 @@ object Trees {
val getType = BooleanType
}
- // tpe overrides the type of the identifier.
+ // tpe, if present, overrides the type of the underlying Identifier id.
// This is useful for variables that represent class fields with instantiated types.
// E.g. list.head when list: List[Int]
// @mk: TODO: This breaks symmetry with the rest of the trees and is ugly-ish.
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index f43465b521f1ae14842c661c3d0499ea91b4cf75..b61136cf0664ab5e12a23b2e1c8a467dd2bb7952 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -285,8 +285,8 @@ object TypeTreeOps {
case l @ Lambda(args, body) =>
val newArgs = args.map { arg =>
- val tpe = tpeSub(arg.tpe)
- ValDef(freshId(arg.id, tpe), tpe)
+ val tpe = tpeSub(arg.getType)
+ ValDef(freshId(arg.id, tpe))
}
val mapping = args.map(_.id) zip newArgs.map(_.id)
Lambda(newArgs, rec(idsMap ++ mapping)(body)).copiedFrom(l)
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 2c1e0a9e9049782b7127b323840252e0ac8b0f50..4ca362592b7aab3478c4c9014a72843340cd1c8c 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -91,7 +91,8 @@ object TypeTrees {
// !! WARNING !!
// vd.id.getType will NOT match vd.tpe, but we kind of need this for selectorID2Index...
// See with Etienne about changing this!
- classDef.fields.map(vd => ValDef(vd.id, instantiateType(vd.tpe, tmap)))
+ // @mk Fixed this
+ classDef.fields.map(vd => ValDef(vd.id, Some(instantiateType(vd.getType, tmap))))
}
}
@@ -99,7 +100,7 @@ object TypeTrees {
def knownCCDescendents = classDef.knownCCDescendents.map(CaseClassType(_, tps))
- lazy val fieldsTypes = fields.map(_.tpe)
+ lazy val fieldsTypes = fields.map(_.getType)
lazy val root = parent.getOrElse(this)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index d13a366e88d402cdffc4bae6a3b01da992eb24a0..93ce2f342e3d6e6b42216d5358beda94a15160c7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -199,14 +199,14 @@ trait SMTLIBTarget {
val sym = freshSym(ct.id)
val conss = sub.map { case cct =>
- Constructor(freshSym(cct.id), cct, cct.fields.map(vd => (freshSym(vd.id), vd.tpe)))
+ Constructor(freshSym(cct.id), cct, cct.fields.map(vd => (freshSym(vd.id), vd.getType)))
}
var cdts = dts + (root -> DataType(sym, conss))
// look for dependencies
for (ct <- root +: sub; f <- ct.fields) {
- cdts ++= findDependencies(f.tpe, cdts)
+ cdts ++= findDependencies(f.getType, cdts)
}
cdts
@@ -316,7 +316,7 @@ trait SMTLIBTarget {
FreshIdentifier(tfd.id.name)
}
val s = id2sym(id)
- sendCommand(DeclareFun(s, tfd.params.map(p => declareSort(p.tpe)), declareSort(tfd.returnType)))
+ sendCommand(DeclareFun(s, tfd.params.map(p => declareSort(p.getType)), declareSort(tfd.returnType)))
s
}
}
@@ -545,7 +545,7 @@ trait SMTLIBTarget {
case (FunctionApplication(SimpleSymbol(s), args), tpe) if constructors.containsB(s) =>
constructors.toA(s) match {
case cct: CaseClassType =>
- val rargs = args.zip(cct.fields.map(_.tpe)).map(fromSMT)
+ val rargs = args.zip(cct.fields.map(_.getType)).map(fromSMT)
CaseClass(cct, rargs)
case tt: TupleType =>
val rargs = args.zip(tt.bases).map(fromSMT)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 6c31bb28dba39c28a95c8fbcd4e870a74b8aad2e..4a13379f31581bf539656222a13a4a9a3e1c7014 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -29,7 +29,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T]) {
val fakeFunDef = new FunDef(FreshIdentifier("fake", alwaysShowUniqueID = true),
Nil,
body.getType,
- variablesOf(body).toSeq.map(id => ValDef(id, id.getType)),
+ variablesOf(body).toSeq.map(ValDef(_)),
DefType.MethodDef)
fakeFunDef.body = Some(body)
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index ebc955599cef9500aade12fee48aef5fd5920810..4d6716c6b8a337461de95a797f7b1a9af4951fa0 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -221,7 +221,7 @@ object FunctionTemplate {
val funString : () => String = () => {
"Template for def " + tfd.signature +
- "(" + tfd.params.map(a => a.id + " : " + a.tpe).mkString(", ") + ") : " +
+ "(" + tfd.params.map(a => a.id + " : " + a.getType).mkString(", ") + ") : " +
tfd.returnType + " is :\n" + templateString()
}
@@ -263,7 +263,7 @@ class FunctionTemplate[T] private(
override def toString : String = str
override def instantiate(aVar: T, args: Seq[T]): (Seq[T], Map[T, Set[TemplateCallInfo[T]]], Map[(T, App[T]), Set[TemplateAppInfo[T]]]) = {
- if (!isRealFunDef) lambdaManager.registerFree(tfd.params.map(_.tpe) zip args)
+ if (!isRealFunDef) lambdaManager.registerFree(tfd.params.map(_.getType) zip args)
super.instantiate(aVar, args)
}
}
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index c6f9035feaa83c050468852adbced71d9b5c428b..4fad725d9a914f6abd80c0eda8d887bdb50f3984 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -175,8 +175,8 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
val trArgs = template.tfd.params.map(vd => bindings(Variable(vd.id)))
- for (vd <- template.tfd.params if vd.tpe.isInstanceOf[FunctionType]) {
- functionVars += vd.tpe -> (functionVars(vd.tpe) + bindings(vd.toVariable))
+ for (vd <- template.tfd.params if vd.getType.isInstanceOf[FunctionType]) {
+ functionVars += vd.getType -> (functionVars(vd.getType) + bindings(vd.toVariable))
}
// ...now this template defines clauses that are all guarded
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index a91cfb3fe318f59ce686754c2c7ba87a87956d12..1ef7d00d9a4edff5c6cbea09485ea52cf0be2c4e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -74,7 +74,7 @@ trait AbstractZ3Solver
def functionDefToDecl(tfd: TypedFunDef): Z3FuncDecl = {
functions.toZ3OrCompute(tfd) {
- val sortSeq = tfd.params.map(vd => typeToSort(vd.tpe))
+ val sortSeq = tfd.params.map(vd => typeToSort(vd.getType))
val returnSort = typeToSort(tfd.returnType)
z3.mkFreshFuncDecl(tfd.id.uniqueName, sortSeq, returnSort)
@@ -282,7 +282,7 @@ trait AbstractZ3Solver
newHierarchiesMap += root -> sub
// look for dependencies
- for (ct <- root +: sub; f <- ct.fields) f.tpe match {
+ for (ct <- root +: sub; f <- ct.fields) f.getType match {
case fct: ClassType =>
findDependencies(fct)
case _ =>
@@ -319,7 +319,7 @@ trait AbstractZ3Solver
(
root.toString,
childrenList.map(ccd => ccd.id.uniqueName),
- childrenList.map(ccd => ccd.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe))))
+ childrenList.map(ccd => ccd.fields.map(f => (f.id.uniqueName, typeToSortRef(f.getType))))
)
}
(defs, newHierarchies)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 8bc9ee6209922dbacf7d67fe023c47a500ca0804..85c534e3f80ceb5871e4aaf57d4758a1d621de9b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -116,7 +116,7 @@ class Synthesizer(val context : LeonContext,
}.toMap
}
- val fd = new FunDef(FreshIdentifier(ci.fd.id.name+"_final", alwaysShowUniqueID = true), Nil, ret, problem.as.map(id => ValDef(id, id.getType)), DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier(ci.fd.id.name+"_final", alwaysShowUniqueID = true), Nil, ret, problem.as.map(ValDef(_)), DefType.MethodDef)
fd.precondition = Some(and(problem.pc, sol.pre))
fd.postcondition = Some((res.id, replace(mapPost, problem.phi)))
fd.body = Some(sol.term)
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 21d93cb01ef28c63fa0027ad14f6d4277b99e51f..a84797242f531dd3f5fc485fb07a4095ea4a6da6 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -28,10 +28,10 @@ case object ADTInduction extends Rule("ADT Induction") {
val inductOn = FreshIdentifier(origId.name, origId.getType, true)
val residualArgs = oas.map(id => FreshIdentifier(id.name, id.getType, true))
val residualMap = (oas zip residualArgs).map{ case (id, id2) => id -> Variable(id2) }.toMap
- val residualArgDefs = residualArgs.map(a => ValDef(a, a.getType))
+ val residualArgDefs = residualArgs.map(ValDef(_))
def isAlternativeRecursive(ct: CaseClassType): Boolean = {
- ct.fields.exists(_.tpe == origId.getType)
+ ct.fields.exists(_.getType == origId.getType)
}
val isRecursive = ct.knownCCDescendents.exists(isAlternativeRecursive)
@@ -49,7 +49,7 @@ case object ADTInduction extends Rule("ADT Induction") {
var recCalls = Map[List[Identifier], List[Expr]]()
var postFs = List[Expr]()
- val newIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.tpe, true)).toList
+ val newIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType, true)).toList
val inputs = (for (id <- newIds) yield {
if (id.getType == origId.getType) {
@@ -80,7 +80,7 @@ case object ADTInduction extends Rule("ADT Induction") {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs, DefType.MethodDef)
val cases = for ((sol, (problem, pre, cct, ids, calls)) <- (sols zip subProblemsInfo)) yield {
globalPre ::= and(pre, sol.pre)
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 75e4a4ff40bbbd97a5adf955e3a1448f4b39f692..7fe22426fd3462ef16deea69a20c7b8764eec11b 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -29,10 +29,10 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
val inductOn = FreshIdentifier(origId.name, origId.getType, true)
val residualArgs = oas.map(id => FreshIdentifier(id.name, id.getType, true))
val residualMap = (oas zip residualArgs).map{ case (id, id2) => id -> Variable(id2) }.toMap
- val residualArgDefs = residualArgs.map(a => ValDef(a, a.getType))
+ val residualArgDefs = residualArgs.map(ValDef(_))
def isAlternativeRecursive(ct: CaseClassType): Boolean = {
- ct.fields.exists(_.tpe == origId.getType)
+ ct.fields.exists(_.getType == origId.getType)
}
val isRecursive = ct.knownCCDescendents.exists(isAlternativeRecursive)
@@ -68,7 +68,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
(for (id <- ids if isRec(id)) yield {
for (cct <- ct.knownCCDescendents) yield {
- val subIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.tpe, true)).toList
+ val subIds = cct.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType, true)).toList
val newIds = ids.filterNot(_ == id) ++ subIds
val newCalls = if (!subIds.isEmpty) {
@@ -130,7 +130,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") {
case sols =>
var globalPre = List[Expr]()
- val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn, inductOn.getType) +: residualArgDefs, DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, resType, ValDef(inductOn) +: residualArgDefs, DefType.MethodDef)
val cases = for ((sol, (problem, pat, calls, pc)) <- (sols zip subProblemsInfo)) yield {
globalPre ::= and(pc, sol.pre)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 411cf29f67b7e3ff6d79d71d8f00670830b48601..d88016265df5c2312acb7410238e3b2fc5896cfa 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -55,7 +55,7 @@ case object ADTSplit extends Rule("ADT Split.") {
val subInfo = for(ccd <- cases) yield {
val cct = CaseClassType(ccd, act.tps)
- val args = cct.fields.map { vd => FreshIdentifier(vd.id.name, vd.tpe, true) }.toList
+ val args = cct.fields.map { vd => FreshIdentifier(vd.id.name, vd.getType, true) }.toList
val subPhi = subst(id -> CaseClass(cct, args.map(Variable(_))), p.phi)
val subPC = subst(id -> CaseClass(cct, args.map(Variable(_))), p.pc)
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index f3174b8d36b3c4b83972fc648b72c90ca3dd9346..6eeb98f8f89e3bab7919a2e8bde73b3657ee5c22 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -247,14 +247,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
private var cTreeFd = new FunDef(FreshIdentifier("cTree", alwaysShowUniqueID = true),
Seq(),
p.outType,
- p.as.map(id => ValDef(id, id.getType)),
+ p.as.map(id => ValDef(id)),
DefType.MethodDef
)
private var phiFd = new FunDef(FreshIdentifier("phiFd", alwaysShowUniqueID = true),
Seq(),
BooleanType,
- p.as.map(id => ValDef(id, id.getType)),
+ p.as.map(id => ValDef(id)),
DefType.MethodDef
)
@@ -291,7 +291,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val nfd = new FunDef(fd.id.freshen,
fd.tparams,
fd.returnType,
- fd.params :+ ValDef(bArrayId, bArrayId.getType),
+ fd.params :+ ValDef(bArrayId),
fd.defType)
nfd.copyContentFrom(fd)
nfd.copiedFrom(fd)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 4b7eac6044b02e68e4221c8048cb418b9764d3ae..be9f77b61c6e6b821fed2cd16e539b2a3b24ba1c 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -23,7 +23,7 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr]) = id.getType match {
case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
- val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.tpe, true) }
+ val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
val map = (ccd.fields zip newIds).map{ case (vd, nid) => nid -> CaseClassSelector(cct, Variable(id), vd.id) }.toMap
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index fc7d4c8c175e67ebc2f7e5f5a67fab828deadd46..4cb86162496913c8b69fb7e8b9925c9ed4626436 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -27,7 +27,7 @@ case object DetupleOutput extends Rule("Detuple Out") {
if (isDecomposable(x)) {
val ct @ CaseClassType(ccd @ CaseClassDef(name, _, _, _), tpes) = x.getType
- val newIds = ct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.tpe, true) }
+ val newIds = ct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
val newCC = CaseClass(ct, newIds.map(Variable(_)))
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index 150686b81f58fbc7f28327f3ad87479eb29b92e2..3f139099ba2460d3c97725aca403b11787b14352 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -46,7 +46,7 @@ case object IntInduction extends Rule("Int Induction") {
and(LessThan(Variable(inductOn), InfiniteIntegerLiteral(0)), lt.pre))
val preOut = subst(inductOn -> Variable(origId), preIn)
- val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, tpe, Seq(ValDef(inductOn, inductOn.getType)),DefType.MethodDef)
+ val newFun = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, tpe, Seq(ValDef(inductOn)),DefType.MethodDef)
val idPost = FreshIdentifier("res", tpe)
newFun.precondition = Some(preIn)
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 68cd02b9264ad0ad7ce69d2b791bbd19c77ac382..b043d069b108cfd00d7357f3b808d27cf8c37ea2 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -94,7 +94,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
//define max function
- val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b", Int32Type), Int32Type))
+ val maxValDefs: Seq[ValDef] = lowerBounds.map(_ => ValDef(FreshIdentifier("b", Int32Type)))
val maxFun = new FunDef(FreshIdentifier("max"), Nil, Int32Type, maxValDefs, DefType.MethodDef)
def maxRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
@@ -108,7 +108,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
maxFun.body = Some(maxRec(maxValDefs.map(vd => Variable(vd.id)).toList))
def max(xs: Seq[Expr]): Expr = FunctionInvocation(maxFun.typed, xs)
//define min function
- val minValDefs: Seq[ValDef] = upperBounds.map(_ => ValDef(FreshIdentifier("b"), Int32Type))
+ val minValDefs: Seq[ValDef] = upperBounds.map(_ => ValDef(FreshIdentifier("b", Int32Type)))
val minFun = new FunDef(FreshIdentifier("min"), Nil, Int32Type, minValDefs,DefType.MethodDef)
def minRec(bounds: List[Expr]): Expr = bounds match {
case (x1 :: x2 :: xs) => {
@@ -122,12 +122,12 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
minFun.body = Some(minRec(minValDefs.map(vd => Variable(vd.id)).toList))
def min(xs: Seq[Expr]): Expr = FunctionInvocation(minFun.typed, xs)
val floorFun = new FunDef(FreshIdentifier("floorDiv"), Nil, Int32Type, Seq(
- ValDef(FreshIdentifier("x"), Int32Type),
- ValDef(FreshIdentifier("x"), Int32Type)),
+ ValDef(FreshIdentifier("x", Int32Type)),
+ ValDef(FreshIdentifier("x", Int32Type))),
DefType.MethodDef)
val ceilingFun = new FunDef(FreshIdentifier("ceilingDiv"), Nil, Int32Type, Seq(
- ValDef(FreshIdentifier("x"), Int32Type),
- ValDef(FreshIdentifier("x"), Int32Type)),
+ ValDef(FreshIdentifier("x", Int32Type)),
+ ValDef(FreshIdentifier("x", Int32Type))),
DefType.MethodDef)
ceilingFun.body = Some(IntLiteral(0))
def floorDiv(x: Expr, y: Expr): Expr = FunctionInvocation(floorFun.typed, Seq(x, y))
@@ -194,7 +194,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
val concretePre = replace(Map(Variable(k) -> loopCounter), pre)
val concreteTerm = replace(Map(Variable(k) -> loopCounter), term)
val returnType = tupleTypeWrap(problem.xs.map(_.getType))
- val funDef = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, returnType, Seq(ValDef(loopCounter.id, Int32Type)),DefType.MethodDef)
+ val funDef = new FunDef(FreshIdentifier("rec", alwaysShowUniqueID = true), Nil, returnType, Seq(ValDef(loopCounter.id)),DefType.MethodDef)
val funBody = expandAndSimplifyArithmetic(IfExpr(
LessThan(loopCounter, IntLiteral(0)),
Error(returnType, "No solution exists"),
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index a0a73caf45dc12024be4bf05065e6146aeaa3685..23cd164dd1b8ccbf2be8c7280ac6a197fd1b0210 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -373,7 +373,7 @@ object ExpressionGrammars {
var finalFree = free.toSet -- tpsMap.keySet
var finalMap = tpsMap
- for (ptpe <- tfd.params.map(_.tpe).distinct) {
+ for (ptpe <- tfd.params.map(_.getType).distinct) {
canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
case Some(ntpsMap) =>
finalFree --= ntpsMap.keySet
@@ -404,7 +404,7 @@ object ExpressionGrammars {
val funcs = functionsAvailable(prog).toSeq.flatMap(getCandidates).filterNot( tfd => exclude contains tfd.fd)
funcs.map{ tfd =>
- Generator[TypeTree, Expr](tfd.params.map(_.tpe), { sub => FunctionInvocation(tfd, sub) })
+ Generator[TypeTree, Expr](tfd.params.map(_.getType), { sub => FunctionInvocation(tfd, sub) })
}
}
}
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index f80977ae61664b743165848dcb83789becb1fe5f..88b154c5b9543661f4f3b0b5983f6b08061a6199 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -69,9 +69,9 @@ object Helpers {
val res = gs.flatMap {
case Terminating(tfd, args) if isSubtypeOf(tfd.returnType, tpe) =>
- val ids = tfd.params.map(vd => FreshIdentifier("<hole>", vd.tpe, true)).toList
+ val ids = tfd.params.map(vd => FreshIdentifier("<hole>", vd.getType, true)).toList
- for (((a, i), tpe) <- args.zipWithIndex zip tfd.params.map(_.tpe);
+ for (((a, i), tpe) <- args.zipWithIndex zip tfd.params.map(_.getType);
smaller <- argsSmaller(a, tpe)) yield {
val args = ids.map(_.toVariable).updated(i, smaller)
(FunctionInvocation(tfd, args), ids.toSet - ids(i))
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index 1f84bd921ca3f7a70cbbbe2772a87223a02be5af..c5e99812590222f259ac73decfc61a1c59e1c30d 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -68,7 +68,7 @@ final case class Chain(relations: List[Relation]) {
}
case xs =>
val params = tfd.params.map(_.id)
- val freshParams = tfd.params.map(arg => FreshIdentifier(arg.id.name, arg.tpe, true))
+ val freshParams = tfd.params.map(arg => FreshIdentifier(arg.id.name, arg.getType, true))
val bindings = (freshParams.map(_.toVariable) zip newArgs).map(p => Equals(p._1, p._2))
bindings ++ rec(xs, tfd, (params zip freshParams).toMap)
})
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 3b1a6aaeefbc9b919084710c5d34bf85c84d041c..e53716e38dadadf04aa3f37bbd3278ce368dae1f 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -16,9 +16,9 @@ trait ChainComparator { self : StructuralSize with TerminationChecker =>
private object ContainerType {
def unapply(c: ClassType): Option[(CaseClassType, Seq[(Identifier, TypeTree)])] = c match {
case cct @ CaseClassType(ccd, _) =>
- if (cct.fields.exists(arg => isSubtypeOf(arg.tpe, cct.parent.getOrElse(c)))) None
+ if (cct.fields.exists(arg => isSubtypeOf(arg.getType, cct.parent.getOrElse(c)))) None
else if (ccd.hasParent && ccd.parent.get.knownDescendents.size > 1) None
- else Some((cct, cct.fields.map(arg => arg.id -> arg.tpe)))
+ else Some((cct, cct.fields.map(arg => arg.id -> arg.getType)))
case _ => None
}
}
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index 4ff739a063dee0b1c97103d111b98a586d9b2955..ec6bb2b89e4da31b58c6d6939e2a6ed6799cf457 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -29,7 +29,7 @@ class LoopProcessor(val checker: TerminationChecker with ChainBuilder with Stren
reporter.debug("-+> Iteration #" + index)
for (chain <- cs if !nonTerminating.isDefinedAt(chain.funDef) &&
(chain.funDef.params zip chain.finalParams).forall(p => p._1.getType == p._2.getType)) {
- val freshParams = chain.funDef.params.map(arg => FreshIdentifier(arg.id.name, arg.tpe, true))
+ val freshParams = chain.funDef.params.map(arg => FreshIdentifier(arg.id.name, arg.getType, true))
val finalBindings = (chain.funDef.params.map(_.id) zip freshParams).toMap
val path = chain.loop(finalSubst = finalBindings)
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index 0e910e99feef946aa4c3335945f4b923118e00e1..801db775abcd52df2d55940e30182f6f6e562ac3 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -21,7 +21,7 @@ trait RelationBuilder { self: TerminationChecker with Strengthener =>
protected def funDefRelationSignature(fd: FunDef): RelationSignature = {
val strengthenedCallees = self.program.callGraph.callees(fd).map(fd => fd -> strengthened(fd))
- (fd, fd.precondition, fd.body, fd.postcondition.map(_._2), self.terminates(fd).isGuaranteed, strengthenedCallees)
+ (fd, fd.precondition, fd.body, fd.postcondition map {_._2}, self.terminates(fd).isGuaranteed, strengthenedCallees)
}
private val relationCache : MutableMap[FunDef, (Set[Relation], RelationSignature)] = MutableMap.empty
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index be6e98ae3656ec41ac8053ff430e997e6d07d1ad..47bf1f19833c930d39b2e3a36ee56a0c48114ba3 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -95,7 +95,7 @@ class SimpleTerminationChecker(context: LeonContext, program: Program) extends T
} getOrElse Set.empty[FunctionInvocation]
}
- val callsToAnalyze = callsOfInterest(funDef.body) ++ callsOfInterest(funDef.precondition) ++ callsOfInterest(funDef.postcondition.map(_._2))
+ val callsToAnalyze = callsOfInterest(funDef.body) ++ callsOfInterest(funDef.precondition) ++ callsOfInterest(funDef.postcondition map { _._2 })
val funDefArgsIDs = funDef.params.map(_.id).toSet
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 6191aa7492d70820b2096aa76bf1a894aebf4947..eae1f53d0a559fd1e35700fc4d7b501b7976075f 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -32,7 +32,7 @@ trait StructuralSize {
sizeCache.get(argumentType) match {
case Some(fd) => fd
case None =>
- val argument = ValDef(FreshIdentifier("x", argumentType, true), argumentType)
+ val argument = ValDef(FreshIdentifier("x", argumentType, true))
val formalTParams = typeParams.map(TypeParameterDef(_))
val fd = new FunDef(FreshIdentifier("size", alwaysShowUniqueID = true), formalTParams, IntegerType, Seq(argument), DefType.MethodDef)
sizeCache(argumentType) = fd
@@ -49,7 +49,7 @@ trait StructuralSize {
def caseClassType2MatchCase(_c: ClassType): MatchCase = {
val c = _c.asInstanceOf[CaseClassType] // required by leon framework
- val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name, vd.tpe))
+ val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType))
val argumentPatterns = arguments.map(id => WildcardPattern(Some(id)))
val sizes = arguments.map(id => size(Variable(id)))
val result = sizes.foldLeft[Expr](InfiniteIntegerLiteral(1))(Plus(_,_))
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index f4c8fb7474f39c142e4af65480497bc0f07d03bd..b889f0fe490450264c281a7990d3f71167f294db 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -33,7 +33,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
// Part (1)
fd.precondition = {
- val argTypesPreconditions = fd.params.flatMap(arg => arg.tpe match {
+ val argTypesPreconditions = fd.params.flatMap(arg => arg.getType match {
case cct : CaseClassType if cct.parent.isDefined => Seq(CaseClassInstanceOf(cct, arg.id.toVariable))
case (at : ArrayType) => Seq(GreaterEquals(ArrayLength(arg.id.toVariable), IntLiteral(0)))
case _ => Seq()
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index a855055676605c7650d5a893184cf4f5de05b306..e47339018ed7c9737345bbc36dc460a940a18529 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -26,8 +26,8 @@ object UnitElimination extends TransformationPhase {
//first introduce new signatures without Unit parameters
allFuns.foreach(fd => {
- if(fd.returnType != UnitType && fd.params.exists(vd => vd.tpe == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.tpe == UnitType), fd.defType).setPos(fd)
+ if(fd.returnType != UnitType && fd.params.exists(vd => vd.getType == UnitType)) {
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType), fd.defType).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:_*)
@@ -100,8 +100,8 @@ object UnitElimination extends TransformationPhase {
if(fd.returnType == UnitType)
removeUnit(b)
else {
- val (newFd, rest) = if(fd.params.exists(vd => vd.tpe == UnitType)) {
- val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.tpe == UnitType), fd.defType).setPos(fd)
+ val (newFd, rest) = if(fd.params.exists(vd => vd.getType == UnitType)) {
+ val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType), fd.defType).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..
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 6fd90151d8e46bd931373961d95de83196716283..7137f6215f1b9e1036ad0d0a369789b8a61a42f2 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -23,7 +23,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
private def selectorsOfParentType(parentType: ClassType, cct: CaseClassType, expr: Expr): Seq[Expr] = {
- val childrenOfSameType = cct.fields.filter(_.tpe == parentType)
+ val childrenOfSameType = cct.fields.filter(_.getType == parentType)
for (field <- childrenOfSameType) yield {
CaseClassSelector(cct, expr, field.id)
}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index ad34c5f487fe0e2e6182ab9856d6c411254c19b8..12cb3552c4f340263ca0c76755d27769e7f5da7a 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -154,7 +154,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
else {
val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name, id.getType))
val modifiedVars2WhileFunVars = modifiedVars.zip(whileFunVars).toMap
- val whileFunValDefs = whileFunVars.map(id => ValDef(id, id.getType))
+ val whileFunValDefs = whileFunVars.map(ValDef(_))
val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else tupleTypeWrap(whileFunVars.map(_.getType))
val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs,DefType.MethodDef).setPos(wh)
wasLoop += whileFunDef
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index a7f9a4c9d1ae9f2826f014757aa8a4deb2be604b..d451a4cdc02edfcd0cef9a666162d65187460210 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -14,7 +14,7 @@ class UnrollingSolverTests extends LeonTestSuite {
private val fx : Identifier = FreshIdentifier("x", IntegerType)
private val fres : Identifier = FreshIdentifier("res", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
fDef.body = Some(IfExpr(GreaterThan(Variable(fx), InfiniteIntegerLiteral(0)),
Plus(Variable(fx), FunctionInvocation(fDef.typed, Seq(Minus(Variable(fx), InfiniteIntegerLiteral(1))))),
InfiniteIntegerLiteral(1)
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 5025f2fbd6305320400497eb5d1ce5d2088b5227..901d1e05b6c93f0fd830e46b4b6c5751257b9969 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -39,7 +39,7 @@ class FairZ3SolverTests extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 8eae0d8609a7831f0f2e6f243cd7170e77b913f0..54740f920a651ddf2c07b7bad0f5325bb480295a 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -47,7 +47,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index fad21b759e693a51f49e2a9305cc77936f375742..cab51ede7c3184e2e98a68e66cc309ee6aadea9b 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -40,11 +40,11 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
// def f(fx : Int) : Int = fx + 1
private val fx : Identifier = FreshIdentifier("x", IntegerType)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
// g is a function that is not in the program (on purpose)
- private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, IntegerType, ValDef(fx) :: Nil, DefType.MethodDef)
gDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(