diff --git a/library/collection/List.scala b/library/collection/List.scala
index baf9622fe27a5bfeb8bcb16131d38cd0532c580e..c7a38dc6388be2db68adbf2d4a54fb5d42b1bc24 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -493,8 +493,8 @@ sealed abstract class List[T] {
}
-@ignore
object List {
+ @ignore
def apply[T](elems: T*): List[T] = {
var l: List[T] = Nil[T]()
for (e <- elems) {
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 8f79149b9eb3290209ede19c6b7afb11410af3f0..f42ce69b468dbd960bb0786b01220448e96a1165 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -402,20 +402,23 @@ class CompilationUnit(val ctx: LeonContext,
/** Traverses the program to find all definitions, and stores those in global variables */
def init() {
// First define all classes/ methods/ functions
- for (u <- program.units; m <- u.modules) {
- val (parents, children) = m.algebraicDataTypes.toSeq.unzip
- for ( cls <- parents ++ children.flatten ++ m.singleCaseClasses) {
+ for (u <- program.units) {
+
+ val (parents, children) = u.algebraicDataTypes.toSeq.unzip
+
+ for ( cls <- parents ++ children.flatten ++ u.singleCaseClasses) {
defineClass(cls)
for (meth <- cls.methods) {
defToModuleOrClass += meth -> cls
}
}
- defineClass(m)
- for(funDef <- m.definedFunctions) {
- defToModuleOrClass += funDef -> m
+ for (m <- u.modules) {
+ defineClass(m)
+ for(funDef <- m.definedFunctions) {
+ defToModuleOrClass += funDef -> m
+ }
}
-
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index cc27bbc3b6c43418f40a065cdcba6ecfc984d374..abe7d0ac0351bb9d2c81208e73daadde207fbfa9 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -15,6 +15,7 @@ import purescala.Definitions.{
Import => LeonImport,
_
}
+
import purescala.Expressions.{Expr => LeonExpr, This => LeonThis, _}
import purescala.Types.{TypeTree => LeonType, _}
import purescala.Common._
@@ -85,7 +86,7 @@ trait CodeExtraction extends ASTExtractors {
sealed class ImpureCodeEncounteredException(pos: Position, msg: String, ot: Option[Tree]) extends Exception(msg) {
def emit() {
val debugInfo = if (ctx.findOptionOrDefault(SharedOptions.optDebug) contains utils.DebugSectionTrees) {
- ot.map { t =>
+ ot.map { t =>
val strWr = new java.io.StringWriter()
new global.TreePrinter(new java.io.PrintWriter(strWr)).printTree(t)
" (Tree: "+strWr.toString+" ; Class: "+t.getClass+")"
@@ -111,52 +112,20 @@ trait CodeExtraction extends ASTExtractors {
}
// Simple case classes to capture the representation of units/modules after discovering them.
- case class TempModule(name : Identifier, trees : List[Tree], isStandalone : Boolean)
- case class TempUnit(
- name : String,
- pack : PackageRef,
- modules : List[TempModule],
+ case class ScalaUnit(
+ name : String,
+ pack : PackageRef,
imports : List[Import],
+ defs : List[Tree],
isPrintable : Boolean
- )
-
- class Extraction(units: List[CompilationUnit]) {
-
- private var currentFunDef: FunDef = null
-
- //This is a bit misleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
- //that it can have any owner
- private var owners: Map[Identifier, Option[FunDef]] = Map()
-
-
-
- def toPureScala(tree: Tree)(implicit dctx: DefContext): Option[LeonExpr] = {
- try {
- Some(extractTree(tree))
- } catch {
- case e: ImpureCodeEncounteredException =>
- e.emit()
- None
- }
- }
+ )
- // This one never fails, on error, it returns Untyped
- def toPureScalaType(tpt: Type)(implicit dctx: DefContext, pos: Position): LeonType = {
- try {
- extractType(tpt)
- } catch {
- case e: ImpureCodeEncounteredException =>
- e.emit()
- Untyped
- }
- }
+ class Extraction(units: List[CompilationUnit]) {
- case class DefContext(
- tparams: Map[Symbol, TypeParameter] = Map(),
- vars: Map[Symbol, () => LeonExpr] = Map(),
- mutableVars: Map[Symbol, () => LeonExpr] = Map(),
- isExtern: Boolean = false
- ) {
+ case class DefContext(tparams: Map[Symbol, TypeParameter] = Map(),
+ vars: Map[Symbol, () => LeonExpr] = Map(),
+ mutableVars: Map[Symbol, () => LeonExpr] = Map(),
+ isExtern: Boolean = false){
def union(that: DefContext) = {
copy(this.tparams ++ that.tparams,
@@ -180,176 +149,242 @@ trait CodeExtraction extends ASTExtractors {
}
}
- def isIgnored(s: Symbol) = {
+ private var currentFunDef: FunDef = null
+
+ //This is a bit misleading, if an expr is not mapped then it has no owner, if it is mapped to None it means
+ //that it can have any owner
+ private var owners: Map[Identifier, Option[FunDef]] = Map()
+
+ // This one never fails, on error, it returns Untyped
+ def leonType(tpt: Type)(implicit dctx: DefContext, pos: Position): LeonType = {
+ try {
+ extractType(tpt)
+ } catch {
+ case e: ImpureCodeEncounteredException =>
+ e.emit()
+ Untyped
+ }
+ }
+
+ private def isIgnored(s: Symbol) = {
(annotationsOf(s) contains "ignore") || s.fullName.toString.endsWith(".main")
}
-
- def extractUnits: List[UnitDef] = {
+
+ private def isLibrary(u: CompilationUnit) = Build.libFiles contains u.source.file.absolute.path
+
+ def extractProgram: Option[Program] = {
try {
- def isLib(u : CompilationUnit) = Build.libFiles contains u.source.file.absolute.path
-
- val templates: List[TempUnit] = units.reverseMap { u => u.body match {
-
- // Unit with a single package object
- case PackageDef(refTree, List(PackageDef(inner, List(ExObjectDef(n, templ))))) if n == "package" =>
- // File name without extension
- val unitName = extractPackageRef(inner).mkString("$") + "$package"
- val id = FreshIdentifier(unitName + "$standalone")
- TempUnit(unitName,
- extractPackageRef(refTree) ++ extractPackageRef(inner),
- List(TempModule(id, templ.body, true)),
- imports.getOrElse(refTree, Nil),
- !isLib(u)
- )
+ val scalaUnits = units.map { u => u.body match {
+ // package object
+ case PackageDef(refTree, List(PackageDef(inner, body))) =>
+ val name = extractPackageRef(inner).mkString("$")
+ val pack = extractPackageRef(refTree) ++ extractPackageRef(inner)
+ val imps = imports.getOrElse(refTree, Nil)
+ ScalaUnit(name, pack, imps, body, !isLibrary(u))
+
+ // normal package
case pd@PackageDef(refTree, lst) =>
+ val name = u.source.file.name.replaceFirst("[.][^.]+$", "")
+ val pack = extractPackageRef(refTree)
+ val imps = imports.getOrElse(refTree, Nil)
- var standaloneDefs = List[Tree]()
+ ScalaUnit(name, pack, imps, lst, !isLibrary(u))
- val modules = lst.flatMap {
+ case _ =>
+ outOfSubsetError(u.body, "Unnexpected Unit body")
+ }}
- case t if isIgnored(t.symbol) =>
- None
+ // Phase 1, we discover and define objects/classes/types
+ for (unit <- scalaUnits) collectClassSymbols(unit.defs)
- case po@ExObjectDef(n, templ) if n == "package" =>
- outOfSubsetError(po, "No other definitions are allowed in a file with a package object.")
+ // Phase 2, build scafolding program with empty bodies
+ val leonUnits = scalaUnits.map { createLeonUnit }
- case ExObjectDef(n, templ) if n != "package" =>
- Some(TempModule(FreshIdentifier(n), templ.body, false))
+ // Phase 3, define bodies of all functions/methods
+ for (unit <- scalaUnits) fillLeonUnit(unit)
- /*
- case d @ ExCompanionObjectSynthetic(_, sym, templ) =>
- // Find default param. implementations
- templ.body foreach {
- case ExDefaultValueFunction(sym, _, _, _, owner, index, _) =>
- val namePieces = sym.toString.reverse.split("\\$", 3).reverse map { _.reverse }
- assert(namePieces.length == 3 && namePieces(0)== "$lessinit$greater" && namePieces(1) == "default") // FIXME : maybe $lessinit$greater?
- val index = namePieces(2).toInt
- val theParam = sym.companionClass.paramss.head(index - 1)
- paramsToDefaultValues += theParam -> body
- case _ =>
- }
- None
- */
+ val pgm0 = Program(leonUnits)
- case d@ExAbstractClass(_, _, _) =>
- standaloneDefs ::= d
- None
+ // Phase 4, resolve imports
+ val leonUnits1 = for ((sunit, lunit) <- scalaUnits zip leonUnits) yield {
+ val imports = sunit.imports.flatMap(i => extractImport(i, lunit)(pgm0))
+ lunit.copy(imports = imports)
+ }
- case d@ExCaseClass(_, _, _, _) =>
- standaloneDefs ::= d
- None
+ val pgm1 = Program(leonUnits1)
- case d@ExCaseClassSyntheticJunk() =>
- None
+ Some(pgm1)
+ } catch {
+ case icee: ImpureCodeEncounteredException =>
+ icee.emit()
+ None
+ }
+ }
- case cd: ClassDef =>
- outOfSubsetError(cd, "Found class that is not an abstract class nor a case class")
- None
+ private def collectClassSymbols(defs: List[Tree]) {
+ // We collect all defined classes
+ for (t <- defs) t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
- case other =>
- outOfSubsetError(other, "Expected: top-level object/class.")
- None
- }
+ case ExAbstractClass(o2, sym, tmpl) =>
+ seenClasses += sym -> ((Nil, tmpl))
- // File name without extension
- val unitName = u.source.file.name.replaceFirst("[.][^.]+$", "")
- val finalModules =
- if (standaloneDefs.isEmpty) modules
- else {
- val id = FreshIdentifier(unitName + "$standalone")
- TempModule(id, standaloneDefs, true) :: modules
- }
+ case ExCaseClass(o2, sym, args, tmpl) =>
+ seenClasses += sym -> ((args, tmpl))
- TempUnit(unitName,
- extractPackageRef(refTree),
- finalModules,
- imports.getOrElse(refTree, Nil),
- !isLib(u)
- )
- }}
+ case ExObjectDef(n, templ) =>
+ for (t <- templ.body) t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
- // Phase 1, we detect objects/classes/types
- for (temp <- templates; mod <- temp.modules) collectClassSymbols(mod.trees)
-
- // Phase 2, we collect functions signatures
- for (temp <- templates; mod <- temp.modules) collectFunSigs(mod.trees)
+ case ExAbstractClass(_, sym, tmpl) =>
+ seenClasses += sym -> ((Nil, tmpl))
- // Phase 3, we collect classes/types' definitions
- for (temp <- templates; mod <- temp.modules) extractClassDefs(mod.trees)
+ case ExCaseClass(_, sym, args, tmpl) =>
+ seenClasses += sym -> ((args, tmpl))
- // Phase 4, we collect methods' definitions
- for (temp <- templates; mod <- temp.modules) extractMethodDefs(mod.trees)
+ case _ =>
+ }
- // Phase 5, we collect function definitions
- for (temp <- templates; mod <- temp.modules) extractFunDefs(mod.trees)
+ case _ =>
+ }
+ }
- // Phase 6, we create modules and extract bodies
- for (temp <- templates; mod <- temp.modules) extractObjectDef(mod.name, mod.trees, mod.isStandalone)
-
- // Phase 7, we wrap modules in units
- // We first form the units without valid imports
- val withoutImports = for (TempUnit(name,pack,mods,imps,isPrintable) <- templates) yield {
- ( UnitDef(
- FreshIdentifier(name),
- for( TempModule(nm,_,_) <- mods) yield objects2Objects(nm),
- pack, Nil, isPrintable
- )
- , imps
- )
- }
-
- // Just doing this so everything is in the same program and searches work properly
- val _ = Program(FreshIdentifier("__program"), withoutImports map { _._1 })
-
- // With the aid of formed units, we extract the correct imports
- val objPerPack = objects2Objects map { _._2 } groupBy { packageOf(_)}
- withoutImports map { case (u, imps) =>
- u.copy(imports = {
- // Extract imports from source
- val extracted = imps flatMap { extractImport(_, u,withoutImports map { _._1}) }
- // Add extra imports for contents of standalone objects
- val packs = u.pack :: extracted. collect { case PackageImport(pack) => pack }
- val additional = objPerPack. collect {
- case (p,obs) if packs contains p =>
- obs filter { _.isStandalone} map WildcardImport
- }.flatten
- extracted ++ additional
- })
- }
+ private def createLeonUnit(u: ScalaUnit): UnitDef = {
+ val ScalaUnit(name, pack, imports, defs, isPrintable) = u
- } catch {
- case icee: ImpureCodeEncounteredException =>
- icee.emit()
- Nil
- }
+ val leonDefs = defs flatMap { t => t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+ None
+
+ case ExAbstractClass(o2, sym, _) =>
+ Some(getClassDef(sym, t.pos))
+
+ case ExCaseClass(o2, sym, args, _) =>
+ Some(getClassDef(sym, t.pos))
+
+ case ExObjectDef(n, templ) =>
+ // Module
+ val id = FreshIdentifier(n)
+ val leonDefs = templ.body.flatMap { t => t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+ None
+
+ case ExAbstractClass(_, sym, _) =>
+ Some(getClassDef(sym, t.pos))
+
+ case ExCaseClass(_, sym, _, _) =>
+ Some(getClassDef(sym, t.pos))
+
+ // Functions
+ case ExFunctionDef(sym, _, _, _, _) =>
+ Some(defineFunDef(sym)(DefContext()))
+
+ // Default value functions
+ case ExDefaultValueFunction(sym, _, _, _ ,_ , _, _) =>
+ val fd = defineFunDef(sym)(DefContext())
+ fd.addAnnotation("synthetic")
+
+ Some(fd)
+
+ // Lazy vals
+ case ExLazyAccessorFunction(sym, _, _) =>
+ Some(defineFieldFunDef(sym, true)(DefContext()))
+
+ // Normal vals
+ case ExFieldDef(sym, _, _) =>
+ Some(defineFieldFunDef(sym, false)(DefContext()))
+
+ case ExCaseClassSyntheticJunk() => None
+ case ExConstructorDef() => None
+ case ExLazyFieldDef() => None
+ case ExFieldAccessorFunction() => None
+ case d if (d.symbol.isImplicit && d.symbol.isSynthetic) => None
+ case tree =>
+ println(tree)
+ outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
+ }}
+ Some(LeonModuleDef(id, leonDefs, id.name == "package"))
+
+ case ExCaseClassSyntheticJunk() => None
+ case ExConstructorDef() => None
+ case d if (d.symbol.isImplicit && d.symbol.isSynthetic) => None
+ case tree =>
+ println(tree)
+ outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
+ }}
+
+ // we only resolve imports once we have the full program
+ UnitDef(FreshIdentifier(name), pack, Nil, leonDefs, isPrintable)
}
-
-
-
- private def getSelectChain(e : Tree) : List[String] = {
- def rec (e : Tree) : List[Name] = e match {
+
+ private def fillLeonUnit(u: ScalaUnit): Unit = {
+ for (t <- u.defs) t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+
+ case ExAbstractClass(_, sym, tpl) =>
+ for (t <- tpl.body) {
+ extractFunOrMethodBody(Some(sym), t)
+ }
+
+ case ExCaseClass(_, sym, _, tpl) =>
+ for (t <- tpl.body) {
+ extractFunOrMethodBody(Some(sym), t)
+ }
+
+ case ExObjectDef(n, templ) =>
+ for (t <- templ.body) t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+ None
+
+ case ExAbstractClass(_, sym, tpl) =>
+ for (t <- tpl.body) {
+ extractFunOrMethodBody(Some(sym), t)
+ }
+
+ case ExCaseClass(_, sym, _, tpl) =>
+ for (t <- tpl.body) {
+ extractFunOrMethodBody(Some(sym), t)
+ }
+
+ case t =>
+ extractFunOrMethodBody(None, t)
+
+ }
+ case _ =>
+ }
+ }
+
+ private def getSelectChain(e: Tree): List[String] = {
+ def rec(e: Tree): List[Name] = e match {
case Select(q, name) => name :: rec(q)
case Ident(name) => List(name)
case EmptyTree => List()
- case _ => ctx.reporter.internalError("getSelectChain: unexpected Tree:\n" + e.toString)
- }
+ case _ =>
+ ctx.reporter.internalError("getSelectChain: unexpected Tree:\n" + e.toString)
+ }
rec(e).reverseMap(_.toString)
}
-
- private def extractPackageRef(refPath : RefTree) : PackageRef =
- (getSelectChain(refPath.qualifier) :+ refPath.name.toString) match {
- // Make sure to drop "<empty>" package
- case List("<empty>") => List()
- case other => other
- }
-
- private def extractImport(i : Import, current : UnitDef, units : List[UnitDef]) : Seq[ LeonImport ] = i match { case Import(expr, sels) =>
+
+ private def extractPackageRef(refPath: RefTree): PackageRef = {
+ (getSelectChain(refPath.qualifier) :+ refPath.name.toString).filter(_ != "<empty>")
+ }
+
+ private def extractImport(i: Import, current: UnitDef)(implicit pgm: Program): Seq[LeonImport] = {
+ val Import(expr, sels) = i
import DefOps._
-
- val prefix = getSelectChain(expr)
+
+ val prefix = getSelectChain(expr)
+
val allSels = sels map { prefix :+ _.name.toString }
+
// Make a different import for each selector at the end of the chain
allSels flatMap { selectors =>
assert(selectors.nonEmpty)
@@ -357,14 +392,14 @@ trait CodeExtraction extends ASTExtractors {
case "_" => (selectors.dropRight(1), true)
case _ => (selectors, false)
}
-
- val theDef = searchByFullNameRelative(thePath mkString ".", current, reliableVisibility = false)
-
+
+ val theDef = searchRelative(thePath.mkString("."), current).headOption
+
(isWild, theDef) match {
- case (true, Some(df)) => Some(WildcardImport(df))
- case (false,Some(df)) => Some(SingleImport(df))
- case (true, None) => Some(PackageImport(thePath))
- case (false,None) => None // import comes from a Scala library or something...
+ case (true, Some(df)) => Some(WildcardImport(df))
+ case (false, Some(df)) => Some(SingleImport(df))
+ case (true, None) => Some(PackageImport(thePath))
+ case (false, None) => None // import comes from a Scala library or something...
}
}
}
@@ -396,40 +431,10 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(pos, "Class "+className+" is not a case class")
}
}
-
- private var paramsToDefaultValues = Map[Symbol,FunDef]()
- private def collectClassSymbols(defs: List[Tree]) {
- // We collect all defined classes
- for (t <- defs) t match {
- case t if isIgnored(t.symbol) =>
- // ignore
-
- case ExAbstractClass(o2, sym, tmpl) =>
- seenClasses += sym -> ((Nil, tmpl))
-
- case ExCaseClass(o2, sym, args, tmpl) =>
- seenClasses += sym -> ((args, tmpl))
- case _ =>
- }
- }
-
- private def extractClassDefs(defs: List[Tree]) {
- // We collect all defined classes
- for (t <- defs) t match {
- case t if isIgnored(t.symbol) =>
- // ignore
-
- case ExAbstractClass(o2, sym, _) =>
- getClassDef(sym, t.pos)
-
- case ExCaseClass(o2, sym, args, _) =>
- getClassDef(sym, t.pos)
+ private var paramsToDefaultValues = Map[Symbol,FunDef]()
- case _ =>
- }
- }
def getClassDef(sym: Symbol, pos: Position): LeonClassDef = {
classesToClasses.get(sym) match {
@@ -440,9 +445,6 @@ trait CodeExtraction extends ASTExtractors {
extractClassDef(sym, args, tmpl)
} else {
- if (sym.name.toString == "synthesis") {
- new Exception().printStackTrace()
- }
outOfSubsetError(pos, "Class "+sym.fullName+" not defined?")
}
}
@@ -471,7 +473,7 @@ trait CodeExtraction extends ASTExtractors {
) {
// Search tmpl to find the function that includes this parameter
val paramOwner = defs.collectFirst(matcher).get
-
+
// assumes single argument list
if(paramOwner.paramss.length != 1) {
outOfSubsetError(paramOwner.pos, "Multiple argument lists for a function are not allowed")
@@ -479,8 +481,7 @@ trait CodeExtraction extends ASTExtractors {
val theParam = paramOwner.paramss.head(index)
paramsToDefaultValues += (theParam -> fd)
}
-
-
+
def extractClassDef(sym: Symbol, args: Seq[(Symbol, ValDef)], tmpl: Template): LeonClassDef = {
val id = FreshIdentifier(sym.name.toString).setPos(sym.pos)
@@ -527,7 +528,7 @@ trait CodeExtraction extends ASTExtractors {
val fields = args.map { case (symbol, t) =>
val tpt = t.tpt
- val tpe = toPureScalaType(tpt.tpe)(defCtx, sym.pos)
+ val tpe = leonType(tpt.tpe)(defCtx, sym.pos)
LeonValDef(FreshIdentifier(symbol.name.toString, tpe).setPos(t.pos)).setPos(t.pos)
}
@@ -577,45 +578,47 @@ trait CodeExtraction extends ASTExtractors {
cd.registerMethod(fd)
// Default values for parameters
- case t@ ExDefaultValueFunction(fsym, _, _, _, owner, index, _) =>
+ case t@ ExDefaultValueFunction(fsym, _, _, _, owner, index, _) =>
val fd = defineFunDef(fsym)(defCtx)
fd.addAnnotation("synthetic")
-
+
isMethod += fsym
methodToClass += fd -> cd
- cd.registerMethod(fd)
- val matcher : PartialFunction[Tree, Symbol] = {
+ cd.registerMethod(fd)
+ val matcher: PartialFunction[Tree, Symbol] = {
case ExFunctionDef(ownerSym, _ ,_ ,_, _) if ownerSym.name.toString == owner => ownerSym
- }
+ }
registerDefaultMethod(tmpl.body, matcher, index, fd )
-
-
+
// Lazy fields
case t @ ExLazyAccessorFunction(fsym, _, _) =>
if (parent.isDefined) {
- outOfSubsetError(t, "Only hierarchy roots can define lazy fields")
+ outOfSubsetError(t, "Only hierarchy roots can define lazy fields")
}
+
val fd = defineFieldFunDef(fsym, true)(defCtx)
isMethod += fsym
methodToClass += fd -> cd
cd.registerMethod(fd)
-
+
// normal fields
case t @ ExFieldDef(fsym, _, _) =>
- // we will be using the accessor method of this field everywhere
- val fsymAsMethod = fsym
if (parent.isDefined) {
outOfSubsetError(t, "Only hierarchy roots can define fields")
}
+
+ // we will be using the accessor method of this field everywhere
+ val fsymAsMethod = fsym
val fd = defineFieldFunDef(fsymAsMethod, false)(defCtx)
isMethod += fsymAsMethod
methodToClass += fd -> cd
cd.registerMethod(fd)
+
case _ =>
}
@@ -631,7 +634,7 @@ trait CodeExtraction extends ASTExtractors {
val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap)
val newParams = sym.info.paramss.flatten.map{ sym =>
- val ptpe = toPureScalaType(sym.tpe)(nctx, sym.pos)
+ val ptpe = leonType(sym.tpe)(nctx, sym.pos)
val newID = FreshIdentifier(sym.name.toString, ptpe).setPos(sym.pos)
owners += (newID -> None)
LeonValDef(newID).setPos(sym.pos)
@@ -639,7 +642,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
- val returnType = toPureScalaType(sym.info.finalResultType)(nctx, sym.pos)
+ val returnType = leonType(sym.info.finalResultType)(nctx, sym.pos)
val name = sym.name.toString
@@ -658,160 +661,83 @@ trait CodeExtraction extends ASTExtractors {
val nctx = dctx.copy(tparams = dctx.tparams)
- val returnType = toPureScalaType(sym.info.finalResultType)(nctx, sym.pos)
+ val returnType = leonType(sym.info.finalResultType)(nctx, sym.pos)
val name = sym.name.toString
val fieldType = if (isLazy) DefType.LazyFieldDef else DefType.StrictFieldDef
-
+
val fd = new FunDef(FreshIdentifier(name).setPos(sym.pos), Seq(), returnType, Seq(), fieldType)
fd.setPos(sym.pos)
fd.addAnnotation(annotationsOf(sym).toSeq : _*)
-
+
defsToDefs += sym -> fd
fd
}
-
-
-
- private def collectFunSigs(defs: List[Tree]) = {
- // We collect defined function bodies
- for (d <- defs) d match {
- case t if isIgnored(t.symbol) =>
- //ignore
- case ExFunctionDef(sym, _, _, _, _) =>
- defineFunDef(sym)(DefContext())
-
- case t @ ExDefaultValueFunction(sym, _, _, _, owner, index, _) => {
-
- val fd = defineFunDef(sym)(DefContext())
- fd.addAnnotation("synthetic")
- val matcher : PartialFunction[Tree, Symbol] = {
- case ExFunctionDef(ownerSym, _ ,_ ,_, _) if ownerSym.name.toString == owner => ownerSym
- }
- registerDefaultMethod(defs, matcher, index, fd)
-
- }
- case ExLazyAccessorFunction(sym, _, _) =>
- defineFieldFunDef(sym,true)(DefContext())
-
- case ExFieldDef(sym, _, _) =>
- defineFieldFunDef(sym, false)(DefContext())
-
- case _ =>
- }
- }
+ private def extractFunOrMethodBody(ocsym: Option[Symbol], t: Tree) {
- private def extractMethodDefs(defs: List[Tree]) = {
- // We collect defined function bodies
- def extractFromClass(csym: Symbol, tmpl: Template) {
- val cd = classesToClasses(csym)
+ val ctparamsMap = ocsym match {
+ case Some(csym) =>
+ val cd = classesToClasses(csym)
- val ctparams = csym.tpe match {
- case TypeRef(_, _, tps) =>
- extractTypeParams(tps).map(_._1)
- case _ =>
- Nil
- }
-
- val ctparamsMap = ctparams zip cd.tparams.map(_.tp)
-
- for (d <- tmpl.body) d match {
- case t if isIgnored(t.symbol) =>
- //ignore
-
- case ExFunctionDef(sym, tparams, params, _, body) =>
- val fd = defsToDefs(sym)
-
- val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
-
- if(body != EmptyTree) {
- extractFunBody(fd, params, body)(DefContext(tparamsMap))
- }
-
- // Default value functions
- case ExDefaultValueFunction(sym, tparams, params, _, _, _, body) =>
- val fd = defsToDefs(sym)
-
- val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
-
- if(body != EmptyTree) {
- extractFunBody(fd, params, body)(DefContext(tparamsMap))
- }
-
- // Lazy fields
- case t @ ExLazyAccessorFunction(sym, _, body) =>
- val fd = defsToDefs(sym)
- val tparamsMap = ctparamsMap
-
- if(body != EmptyTree) {
- extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
- }
-
- // normal fields
- case t @ ExFieldDef(sym, _, body) => // if !sym.isSynthetic && !sym.isAccessor =>
- val fd = defsToDefs(sym)
- val tparamsMap = ctparamsMap
-
- if(body != EmptyTree) {
- extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
- }
-
- case _ =>
-
- }
- }
- for (d <- defs) d match {
- case t if isIgnored(t.symbol) =>
- // ignore
-
- case ExAbstractClass(_, csym, tmpl) =>
- extractFromClass(csym, tmpl)
+ val ctparams = csym.tpe match {
+ case TypeRef(_, _, tps) =>
+ extractTypeParams(tps).map(_._1)
+ case _ =>
+ Nil
+ }
- case ExCaseClass(_, csym, _, tmpl) =>
- extractFromClass(csym, tmpl)
+ ctparams zip cd.tparams.map(_.tp)
- case _ =>
+ case None =>
+ Map[Symbol, TypeParameter]()
}
- }
- private def extractFunDefs(defs: List[Tree]) = {
- // We collect defined function bodies
- for (d <- defs) d match {
+ t match {
case t if isIgnored(t.symbol) =>
- // ignore
+ //ignore
-
case ExFunctionDef(sym, tparams, params, _, body) =>
- // Methods
val fd = defsToDefs(sym)
- val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
+ val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
- extractFunBody(fd, params, body)(DefContext(tparamsMap))
+ if(body != EmptyTree) {
+ extractFunBody(fd, params, body)(DefContext(tparamsMap))
+ }
- case ExDefaultValueFunction(sym, tparams, params, _ ,_ , _, body) =>
- // Default value functions
+ // Default value functions
+ case ExDefaultValueFunction(sym, tparams, params, _, _, _, body) =>
val fd = defsToDefs(sym)
- val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
+ val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap ++ ctparamsMap
- extractFunBody(fd, params, body)(DefContext(tparamsMap))
-
- case ExLazyAccessorFunction(sym, _, body) =>
- // Lazy vals
+ if(body != EmptyTree) {
+ extractFunBody(fd, params, body)(DefContext(tparamsMap))
+ }
+
+ // Lazy fields
+ case t @ ExLazyAccessorFunction(sym, _, body) =>
val fd = defsToDefs(sym)
- extractFunBody(fd, Seq(), body)(DefContext())
+ val tparamsMap = ctparamsMap
- case ExFieldDef(sym, tpe, body) =>
- // Normal vals
+ if(body != EmptyTree) {
+ extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
+ }
+
+ // normal fields
+ case t @ ExFieldDef(sym, _, body) => // if !sym.isSynthetic && !sym.isAccessor =>
val fd = defsToDefs(sym)
- extractFunBody(fd, Seq(), body)(DefContext())
-
+ val tparamsMap = ctparamsMap
+
+ if(body != EmptyTree) {
+ extractFunBody(fd, Seq(), body)(DefContext(tparamsMap.toMap))
+ }
+
case _ =>
}
}
@@ -826,71 +752,22 @@ trait CodeExtraction extends ASTExtractors {
}
}
- var objects2Objects = Map[Identifier, LeonModuleDef]()
-
- private def extractObjectDef(id : Identifier, defs: List[Tree], isStandalone : Boolean) {
-
- val newDefs = defs.flatMap {
- case t if isIgnored(t.symbol) =>
- None
-
- case ExAbstractClass(o2, sym, _) =>
- Some(classesToClasses(sym))
-
- case ExCaseClass(o2, sym, args, _) =>
- Some(classesToClasses(sym))
-
- // Taking accessor functions will duplicate work for strict fields, but we need them in case of lazy fields
- case ExFunctionDef(sym, tparams, params, _, body) =>
- Some(defsToDefs(sym))
- case ExDefaultValueFunction(sym, _, _, _, _, _, _) =>
- Some(defsToDefs(sym))
- case ExLazyAccessorFunction(sym, _, _) =>
- Some(defsToDefs(sym))
- case ExFieldDef(sym, _, _) =>
- Some(defsToDefs(sym))
-
- case _ =>
- None
- }
-
- // We check nothing else is polluting the object
- for (t <- defs) t match {
- case ExCaseClassSyntheticJunk() =>
- case ExAbstractClass(_,_,_) =>
- case ExCaseClass(_,_,_,_) =>
- case ExConstructorDef() =>
- case ExFunctionDef(_, _, _, _, _) =>
- case ExLazyAccessorFunction(_, _, _) =>
- case ExDefaultValueFunction(_, _, _, _, _, _, _ ) =>
- case ExFieldDef(_,_,_) =>
- case ExLazyFieldDef() =>
- case ExFieldAccessorFunction() =>
- case d if isIgnored(d.symbol) || (d.symbol.isImplicit && d.symbol.isSynthetic) =>
- case tree =>
- println(tree)
- outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
- }
-
- objects2Objects += id -> LeonModuleDef(id, newDefs, isStandalone)
- }
-
+ //var objects2Objects = Map[Identifier, LeonModuleDef]()
private def extractFunBody(funDef: FunDef, params: Seq[ValDef], body0 : Tree)(dctx: DefContext): FunDef = {
currentFunDef = funDef
-
+
// Find defining function for params with default value
for ((s,vd) <- params zip funDef.params) {
vd.defaultValue = paramsToDefaultValues.get(s.symbol)
}
-
+
val newVars = for ((s, vd) <- params zip funDef.params) yield {
s.symbol -> (() => Variable(vd.id))
}
val fctx = dctx.withNewVars(newVars).copy(isExtern = funDef.annotations("extern"))
-
// If this is a lazy field definition, drop the assignment/ accessing
val body =
if (funDef.defType == DefType.LazyFieldDef) { body0 match {
@@ -928,7 +805,7 @@ trait CodeExtraction extends ASTExtractors {
NoTree(funDef.returnType)
}
- funDef.fullBody = finalBody
+ funDef.fullBody = finalBody
// Post-extraction sanity checks
@@ -951,12 +828,12 @@ trait CodeExtraction extends ASTExtractors {
private def extractPattern(p: Tree, binder: Option[Identifier] = None)(implicit dctx: DefContext): (Pattern, DefContext) = p match {
case b @ Bind(name, t @ Typed(pat, tpt)) =>
- val newID = FreshIdentifier(name.toString, extractType(tpt)).setPos(b.pos).setOwner(currentFunDef)
+ val newID = FreshIdentifier(name.toString, extractType(tpt)).setPos(b.pos)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(t, Some(newID))(pctx)
case b @ Bind(name, pat) =>
- val newID = FreshIdentifier(name.toString, extractType(b)).setPos(b.pos).setOwner(currentFunDef)
+ val newID = FreshIdentifier(name.toString, extractType(b)).setPos(b.pos)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(pat, Some(newID))(pctx)
@@ -1077,7 +954,7 @@ trait CodeExtraction extends ASTExtractors {
val closure = post.getType match {
case BooleanType =>
- val resId = FreshIdentifier("res", b.getType).setPos(post).setOwner(currentFunDef)
+ val resId = FreshIdentifier("res", b.getType).setPos(post)
Lambda(Seq(LeonValDef(resId)), post).setPos(post)
case _ => post
}
@@ -1085,7 +962,7 @@ trait CodeExtraction extends ASTExtractors {
Ensuring(b, closure)
case t @ ExHoldsExpression(body) =>
- val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos).setOwner(currentFunDef)
+ val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos)
val post = Lambda(Seq(LeonValDef(resId)), Variable(resId)).setPos(current.pos)
val b = extractTreeOrNoTree(body)
@@ -1158,7 +1035,7 @@ trait CodeExtraction extends ASTExtractors {
case ExValDef(vs, tpt, bdy) =>
val binderTpe = extractType(tpt)
- val newID = FreshIdentifier(vs.name.toString, binderTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(vs.name.toString, binderTpe)
val valTree = extractTree(bdy)
if(valTree.getType.isInstanceOf[ArrayType]) {
@@ -1193,7 +1070,7 @@ trait CodeExtraction extends ASTExtractors {
val oldCurrentFunDef = currentFunDef
- val funDefWithBody = extractFunBody(fd, params, b)(newDctx.copy(mutableVars = Map())).setOwner(oldCurrentFunDef)
+ val funDefWithBody = extractFunBody(fd, params, b)(newDctx.copy(mutableVars = Map()))
currentFunDef = oldCurrentFunDef
@@ -1212,7 +1089,7 @@ trait CodeExtraction extends ASTExtractors {
case ExVarDef(vs, tpt, bdy) => {
val binderTpe = extractType(tpt)
- val newID = FreshIdentifier(vs.name.toString, binderTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(vs.name.toString, binderTpe)
val valTree = extractTree(bdy)
if(valTree.getType.isInstanceOf[ArrayType]) {
@@ -1349,7 +1226,7 @@ trait CodeExtraction extends ASTExtractors {
val newOracles = oracles map { case (tpt, sym) =>
val aTpe = extractType(tpt)
val oTpe = oracleType(ops.pos, aTpe)
- val newID = FreshIdentifier(sym.name.toString, oTpe).setOwner(currentFunDef)
+ val newID = FreshIdentifier(sym.name.toString, oTpe)
owners += (newID -> None)
newID
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index c4131034a5c215890de58a4042f9dff945f969ec..461f145019edf1c136e896065d8402174052099b 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -69,8 +69,13 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
compiler.leonExtraction.setImports(compiler.saveImports.imports )
- val pgm = Program(FreshIdentifier("__program"), compiler.leonExtraction.compiledUnits)
- pgm
+ compiler.leonExtraction.compiledProgram match {
+ case Some(pgm) =>
+ pgm
+
+ case None =>
+ ctx.reporter.fatalError("Failed to extract Leon program.")
+ }
} else {
ctx.reporter.fatalError("No input program.")
}
diff --git a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
index fbb0f598058a5286666b80176ffbd0e975ea84ee..1de899e28f9e0e8a755bc48d3047a87ec947fcda 100644
--- a/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/LeonExtraction.scala
@@ -20,8 +20,8 @@ trait LeonExtraction extends SubComponent with CodeExtraction {
this.imports = imports
}
- def compiledUnits = {
- new Extraction(units).extractUnits
+ def compiledProgram = {
+ new Extraction(units).extractProgram
}
def newPhase(prev: scala.tools.nsc.Phase): StdPhase = new Phase(prev)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index a9796942b62f452c3eb02a742279075bf66210c6..7817438dfd039b751d09aef633f5aa6b0bc62634 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -8,75 +8,77 @@ import ExprOps.{preMap, postMap, functionCallsOf}
object DefOps {
- def packageOf(df: Definition): PackageRef = {
+ def packageOf(df: Definition)(implicit pgm: Program): PackageRef = {
df match {
case _ : Program => List()
- case u : UnitDef => u.pack
- case _ => df.owner map packageOf getOrElse List()
+ case u : UnitDef => u.pack
+ case _ => unitOf(df).map(_.pack).getOrElse(List())
}
}
- def unitOf(df: Definition): Option[UnitDef] = df match {
+ def unitOf(df: Definition)(implicit pgm: Program): Option[UnitDef] = df match {
case p : Program => None
case u : UnitDef => Some(u)
- case other => other.owner flatMap unitOf
+ case other => pgm.units.find(_.containsDef(df))
}
- def moduleOf(df: Definition): Option[ModuleDef] = df match {
+ def moduleOf(df: Definition)(implicit pgm: Program): Option[ModuleDef] = df match {
case p : Program => None
case m : ModuleDef => Some(m)
- case other => other.owner flatMap moduleOf
- }
-
- def programOf(df: Definition): Option[Program] = {
- df match {
- case p : Program => Some(p)
- case other => other.owner flatMap programOf
+ case other => unitOf(df).flatMap { u =>
+ u.modules.find(_.containsDef(df))
}
}
- def pathFromRoot(df: Definition): List[Definition] ={
- def rec(df : Definition) : List[Definition] = df.owner match {
- case Some(owner) => df :: rec(owner)
- case None => List(df)
- }
- rec(df).reverse
+ def pathFromRoot(df: Definition)(implicit pgm: Program): List[Definition] ={
+ def rec(from: Definition): List[Definition] = {
+ from :: (if (from == df) {
+ Nil
+ } else {
+ from.subDefinitions.find { sd => (sd eq df) || sd.containsDef(df) } match {
+ case Some(sd) =>
+ rec(sd)
+ case None =>
+ Nil
+ }
+ })
+ }
+ rec(pgm)
}
- def unitsInPackage(p: Program, pack : PackageRef) = p.units filter { _.pack == pack }
+ def unitsInPackage(p: Program, pack: PackageRef) = p.units filter { _.pack == pack }
- def isImportedBy(df : Definition, i : Import) : Boolean =
- i.importedDefs contains df
+ //def isImportedBy(df: Definition, i: Import) : Boolean = {
+ // i.importedDefs contains df
+ //}
- def isImportedBy(df : Definition, is: Seq[Import]) : Boolean =
- is exists {isImportedBy(df,_)}
+ //def isImportedBy(df : Definition, is: Seq[Import]) : Boolean = {
+ // is exists {isImportedBy(df,_)}
+ //}
- def leastCommonAncestor(df1 : Definition, df2 : Definition) : Definition = {
- (pathFromRoot(df1) zip pathFromRoot(df2))
- .takeWhile{case (df1,df2) => df1 eq df2}
- .last._1
+ def leastCommonAncestor(df1: Definition, df2: Definition)(implicit pgm: Program): Definition = {
+ (pathFromRoot(df1) zip pathFromRoot(df2)).takeWhile {
+ case (df1, df2) => df1 eq df2
+ }.last._1
}
/** Returns the set of definitions directly visible from the current definition
* Definitions that are shadowed by others are not returned.
*/
- def visibleDefsFrom(df : Definition) : Set[Definition] = {
+ def visibleDefsFrom(df: Definition)(implicit pgm: Program): Set[Definition] = {
var toRet = Map[String,Definition]()
val asList =
(pathFromRoot(df).reverse flatMap { _.subDefinitions }) ++ {
- programOf(df) match {
- case None => List()
- case Some(p) => unitsInPackage(p, packageOf(df)) flatMap { _.subDefinitions }
- }
+ unitsInPackage(pgm, packageOf(df)) flatMap { _.subDefinitions }
} ++
- programOf(df).toList ++
+ List(pgm) ++
( for ( u <- unitOf(df).toSeq;
imp <- u.imports;
impDf <- imp.importedDefs
- ) yield impDf
+ ) yield impDf
)
- for (
+ for (
df <- asList;
name = df.id.toString
) {
@@ -85,30 +87,31 @@ object DefOps {
toRet.values.toSet
}
- def visibleFunDefsFrom(df: Definition): Set[FunDef] = {
+ def visibleFunDefsFrom(df: Definition)(implicit pgm: Program): Set[FunDef] = {
visibleDefsFrom(df).collect {
case fd: FunDef => fd
}
}
- def funDefsFromMain(p: Program): Set[FunDef] = {
- p.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
+ def funDefsFromMain(implicit pgm: Program): Set[FunDef] = {
+ pgm.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
u.definedFunctions
}
}
- def visibleFunDefsFromMain(p: Program): Set[FunDef] = {
+ def visibleFunDefsFromMain(implicit p: Program): Set[FunDef] = {
p.units.filter(_.isMainUnit).toSet.flatMap{ (u: UnitDef) =>
visibleFunDefsFrom(u) ++ u.definedFunctions
}
}
/** Returns true for strict superpackage */
- def isSuperPackageOf(p1:PackageRef, p2 : PackageRef) =
- (p2.length > p1.length) &&
+ def isSuperPackageOf(p1:PackageRef, p2 : PackageRef) = {
+ (p2.length > p1.length) &&
( (p1 zip p2 takeWhile { case (n1,n2) => n1 == n2 }).length == p1.length )
-
- def packageAsVisibleFrom(df : Definition, p : PackageRef) = {
+ }
+
+ def packageAsVisibleFrom(df: Definition, p: PackageRef)(implicit pgm: Program) = {
val visiblePacks =
packageOf(df) +: (unitOf(df).toSeq.flatMap(_.imports) collect { case PackageImport(pack) => pack })
val bestSuper = visiblePacks filter { pack => pack == p || isSuperPackageOf(pack,p)} match {
@@ -118,8 +121,8 @@ object DefOps {
p drop bestSuper.length
}
- // This assumes base and target are in the same program
- def pathAsVisibleFrom(base : Definition, target : Definition) : (PackageRef, List[Definition]) = {
+ /*
+ private def pathAsVisibleFrom(base: Definition, target: Definition)(implicit pgm: Program): (PackageRef, List[Definition]) = {
val rootPath = pathFromRoot(target)
val ancestor = leastCommonAncestor(base, target)
val pth = rootPath dropWhile { _.owner != Some(ancestor) }
@@ -137,20 +140,136 @@ object DefOps {
(pack, finalPath)
}
+ */
+
+ private def pathToString(path: List[Definition]): String = {
+ val expandPack = path.flatMap {
+ case p: Program =>
+ Nil
+ case u: UnitDef =>
+ u.pack
+ case m: ModuleDef if m.isPackageObject =>
+ Nil
+ case d =>
+ List(d.id.name)
+ }
+
+ expandPack.mkString(".")
+ }
+
+ def fullName(df: Definition)(implicit pgm: Program): String = {
+ pathToString(pathFromRoot(df))
+ }
+
+ private def nameToParts(name: String) = {
+ name.split("\\.").toList map scala.reflect.NameTransformer.encode
+ }
+
+ def searchWithin(name: String, within: Definition): Seq[Definition] = {
+ searchWithin(nameToParts(name), within)
+ }
- def fullName(df: Definition, fromProgram: Option[Program] = None): String =
- fromProgram orElse programOf(df) match {
- case None => df.id.name
- case Some(p) =>
- val (pr, ds) = pathAsVisibleFrom(p, df)
-
- (pr ::: ds.flatMap{
- case _: UnitDef => None
- case m: ModuleDef if m.isStandalone => None
- case d => Some(d.id.name)
- }).mkString(".")
+ def searchWithin(ns: List[String], within: Definition): Seq[Definition] = {
+ (ns, within) match {
+ case (ns, p: Program) =>
+ p.units.flatMap { u =>
+ searchWithin(ns, u)
+ }
+
+ case (ns, u: UnitDef) =>
+ if (ns.startsWith(u.pack)) {
+ val rest = ns.drop(u.pack.size)
+
+ u.defs.flatMap {
+ case d: ModuleDef if d.isPackageObject =>
+ searchWithin(rest, d)
+
+ case d =>
+ rest match {
+ case n :: ns =>
+ if (d.id.name == n) {
+ searchWithin(ns, d)
+ } else {
+ Nil
+ }
+ case Nil =>
+ List(u)
+ }
+ }
+ } else {
+ Nil
+ }
+
+ case (Nil, d) => List(d)
+ case (n :: ns, d) =>
+ d.subDefinitions.filter(_.id.name == n).flatMap { sd =>
+ searchWithin(ns, sd)
+ }
}
+ }
+
+ def searchRelative(name: String, from: Definition)(implicit pgm: Program): Seq[Definition] = {
+ val names = nameToParts(name)
+ val path = pathFromRoot(from)
+
+ searchRelative(names, path.reverse)
+ }
+
+ private case class ImportPath(ls: List[String], wild: Boolean)
+
+ private def resolveImports(imports: List[ImportPath], names: List[String]): List[List[String]] = {
+ def resolveImport(i: ImportPath): Option[List[String]] = {
+ if (!i.wild && names.startsWith(i.ls.last)) {
+ Some(i.ls ++ names.tail)
+ } else if (i.wild) {
+ Some(i.ls ++ names)
+ } else {
+ None
+ }
+ }
+
+ imports.flatMap(resolveImport)
+ }
+
+ private def searchRelative(names: List[String], rpath: List[Definition])(implicit pgm: Program): Seq[Definition] = {
+ (names, rpath) match {
+ case (n :: ns, d :: ds) =>
+ (d match {
+ case p: Program =>
+ searchWithin(names, p)
+
+ case u: UnitDef =>
+ val imports = u.imports.map {
+ case PackageImport(ls) => ImportPath(ls, true)
+ case SingleImport(d) => ImportPath(nameToParts(fullName(d)), false)
+ case WildcardImport(d) => ImportPath(nameToParts(fullName(d)), true)
+ }.toList
+ val inModules = d.subDefinitions.filter(_.id.name == n).flatMap { sd =>
+ searchWithin(ns, sd)
+ }
+
+ val namesImported = resolveImports(imports, names)
+ val nameWithPackage = u.pack ++ names
+
+ val allNames = namesImported :+ nameWithPackage
+
+ allNames.foldLeft(inModules) { _ ++ searchRelative(_, ds) }
+
+ case d =>
+ if (n == d.id.name) {
+ searchWithin(ns, d)
+ } else {
+ searchWithin(n :: ns, d)
+ }
+ }) ++ searchRelative(names, ds)
+
+ case _ =>
+ Nil
+ }
+ }
+
+ /*
def searchByFullName (
fullName : String,
p : Program,
@@ -159,7 +278,7 @@ object DefOps {
) = searchByFullNameRelative(fullName, p, reliableVisibility,exploreStandalones)
- def searchByFullNameRelative(
+ private def searchByFullNameRelative(
fullName : String,
base : Definition,
reliableVisibility : Boolean = true, // Unset this if imports have not yet been set correctly
@@ -264,6 +383,7 @@ object DefOps {
}
}
+ */
/*
@@ -319,24 +439,19 @@ object DefOps {
val newP = p.copy(units = for (u <- p.units) yield {
u.copy(
- modules = for (m <- u.modules) yield {
- m.copy(defs = for (df <- m.defs) yield {
- df match {
- case f : FunDef =>
- val newF = fdMap(f)
- newF.fullBody = replaceCalls(newF.fullBody)
- newF
- case c : ClassDef =>
- // val oldMethods = c.methods
- // c.clearMethods()
- // for (m <- oldMethods) {
- // c.registerMethod(functionToFunction.get(m).map{_.to}.getOrElse(m))
- // }
- c
- case d =>
- d
- }
+ defs = u.defs.map {
+ case m : ModuleDef =>
+ m.copy(defs = for (df <- m.defs) yield {
+ df match {
+ case f : FunDef =>
+ val newF = fdMap(f)
+ newF.fullBody = replaceCalls(newF.fullBody)
+ newF
+ case d =>
+ d
+ }
})
+ case d => d
},
imports = u.imports map {
case SingleImport(fd : FunDef) =>
@@ -353,18 +468,20 @@ object DefOps {
var found = false
val res = p.copy(units = for (u <- p.units) yield {
u.copy(
- modules = for (m <- u.modules) yield {
- val newdefs = for (df <- m.defs) yield {
- df match {
- case `after` =>
- found = true
- after +: fds.toSeq
- case d =>
- Seq(d)
+ defs = u.defs.map {
+ case m: ModuleDef =>
+ val newdefs = for (df <- m.defs) yield {
+ df match {
+ case `after` =>
+ found = true
+ after +: fds.toSeq
+ case d =>
+ Seq(d)
+ }
}
- }
- m.copy(defs = newdefs.flatten)
+ m.copy(defs = newdefs.flatten)
+ case d => d
}
)
})
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index c19c7383fa2602171d834db56934d849ee1c8571..280a7ae39d6594290c12154628ffd906ade139a0 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -16,30 +16,30 @@ object Definitions {
val id: Identifier
- def owner = id.owner
- def setOwner(owner : Definition) : this.type = { id.owner = Some(owner); this }
-
var origOwner : Option[Definition] = None // The definition/scope enclosing this definition
def subDefinitions : Seq[Definition] // The enclosed scopes/definitions by this definition
+
+ def containsDef(df: Definition): Boolean = {
+ subDefinitions.exists { sd =>
+ sd == df || sd.containsDef(df)
+ }
+ }
+
override def hashCode : Int = id.hashCode
override def equals(that : Any) : Boolean = that match {
case t : Definition => t.id == this.id
case _ => false
}
- override def copiedFrom(o : Tree) : this.type = {
- super.copiedFrom(o)
- o match {
- case df : Definition if df.owner.isDefined =>
- this.setOwner(df.owner.get)
- case _ =>
- this
- }
-
- }
- def setSubDefOwners() = for (df <- subDefinitions) df.setOwner(this)
-
+ def writeScalaFile(filename: String) {
+ import java.io.FileWriter
+ import java.io.BufferedWriter
+ val fstream = new FileWriter(filename)
+ val out = new BufferedWriter(fstream)
+ out.write(ScalaPrinter(this))
+ out.close()
+ }
}
/**
@@ -59,14 +59,17 @@ object Definitions {
// Warning: the variable will not have the same type as the ValDef, but
// the Identifier type is enough for all use cases in Leon
def toVariable : Variable = Variable(id)
-
- setSubDefOwners()
}
/** A wrapper for a program. For now a program is simply a single object. The
* name is meaningless and we just use the package name as id. */
- case class Program(id: Identifier, units: List[UnitDef]) extends Definition {
+ case class Program(units: List[UnitDef]) extends Definition {
+ val id = FreshIdentifier("program")
+
origOwner = None
+
+ lazy val library = Library(this)
+
def subDefinitions = units
def definedFunctions = units.flatMap(_.definedFunctions)
@@ -74,7 +77,11 @@ object Definitions {
def classHierarchyRoots = units.flatMap(_.classHierarchyRoots)
def algebraicDataTypes = units.flatMap(_.algebraicDataTypes).toMap
def singleCaseClasses = units.flatMap(_.singleCaseClasses)
- def modules = units.flatMap(_.modules)
+ def modules = {
+ units.flatMap(_.defs.collect {
+ case md: ModuleDef => md
+ })
+ }
lazy val callGraph = new CallGraph(this)
@@ -85,32 +92,19 @@ object Definitions {
def duplicate = {
copy(units = units.map{_.duplicate})
}
-
- lazy val library = Library(this)
- def writeScalaFile(filename: String) {
- import java.io.FileWriter
- import java.io.BufferedWriter
- val fstream = new FileWriter(filename)
- val out = new BufferedWriter(fstream)
- out.write(ScalaPrinter(this))
- out.close()
- }
- setSubDefOwners()
+ def lookupAll(name: String) = DefOps.searchWithin(name, this)
+ def lookup(name: String) = lookupAll(name).headOption
}
object Program {
- lazy val empty : Program = Program(
- FreshIdentifier("empty"),
- Nil
- )
+ lazy val empty: Program = Program(Nil)
}
case class TypeParameterDef(tp: TypeParameter) extends Definition {
def subDefinitions = Seq()
def freshen = TypeParameterDef(tp.freshen)
val id = tp.id
- setSubDefOwners()
}
/** A package as a path of names */
@@ -118,18 +112,20 @@ object Definitions {
abstract class Import extends Definition {
def subDefinitions = Nil
-
- def importedDefs = this match {
- case PackageImport(pack) => {
- import DefOps._
+
+ def importedDefs(implicit pgm: Program) = this match {
+ case PackageImport(pack) =>
// Ignore standalone modules, assume there are extra imports for them
- programOf(this) map { unitsInPackage(_,pack) } getOrElse List()
- }
- case SingleImport(imported) => List(imported)
- case WildcardImport(imported) => imported.subDefinitions
+ DefOps.unitsInPackage(pgm, pack)
+
+ case SingleImport(imported) =>
+ List(imported)
+
+ case WildcardImport(imported) =>
+ imported.subDefinitions
}
}
-
+
// import pack._
case class PackageImport(pack : PackageRef) extends Import {
val id = FreshIdentifier("import " + (pack mkString "."))
@@ -143,47 +139,64 @@ object Definitions {
val id = FreshIdentifier(s"import ${df.id.toString}._")
}
-
case class UnitDef(
id: Identifier,
- modules : Seq[ModuleDef],
pack : PackageRef,
imports : Seq[Import],
+ defs : Seq[Definition],
isMainUnit : Boolean // false for libraries/imports
) extends Definition {
- def subDefinitions = modules ++ imports
+ def subDefinitions = defs
- def definedFunctions = modules.flatMap(_.definedFunctions)
- def definedClasses = modules.flatMap(_.definedClasses)
- def classHierarchyRoots = modules.flatMap(_.classHierarchyRoots)
- def algebraicDataTypes = modules.flatMap(_.algebraicDataTypes)
- def singleCaseClasses = modules.flatMap(_.singleCaseClasses)
+ def definedFunctions = defs.flatMap{
+ case m: ModuleDef => m.definedFunctions
+ case _ => Nil
+ }
+
+ def definedClasses = defs.flatMap {
+ case c: ClassDef => List(c)
+ case m: ModuleDef => m.definedClasses
+ case _ => Nil
+ }
+
+ def classHierarchyRoots = {
+ definedClasses.filter(!_.hasParent)
+ }
+
+ def algebraicDataTypes = {
+ definedClasses.collect {
+ case ccd: CaseClassDef if ccd.hasParent => ccd
+ }.groupBy(_.parent.get.classDef)
+ }
+
+ def singleCaseClasses = {
+ definedClasses.collect {
+ case ccd: CaseClassDef if !ccd.hasParent => ccd
+ }
+ }
def duplicate = {
- copy(modules = modules map { _.duplicate } )
+ copy(defs = defs map {
+ case cd: ClassDef => cd.duplicate
+ case m: ModuleDef => m.duplicate
+ case d => d
+ })
}
-
- def writeScalaFile(filename: String) {
- import java.io.FileWriter
- import java.io.BufferedWriter
- val fstream = new FileWriter(filename)
- val out = new BufferedWriter(fstream)
- out.write(ScalaPrinter(this))
- out.close()
+
+ def modules = defs.collect {
+ case md: ModuleDef => md
}
-
- setSubDefOwners()
}
object UnitDef {
def apply(id: Identifier, modules : Seq[ModuleDef]) : UnitDef =
- UnitDef(id,modules, Nil,Nil,true)
+ UnitDef(id,Nil, Nil, modules,true)
}
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
- case class ModuleDef(id: Identifier, defs : Seq[Definition], isStandalone : Boolean) extends Definition {
+ case class ModuleDef(id: Identifier, defs: Seq[Definition], isPackageObject: Boolean) extends Definition {
def subDefinitions = defs
@@ -208,9 +221,6 @@ object Definitions {
case cd: ClassDef => cd.duplicate
case other => other
})
-
- setSubDefOwners()
-
}
/** Useful because case classes and classes are somewhat unified in some
@@ -239,7 +249,6 @@ object Definitions {
def registerMethod(fd: FunDef) = {
_methods = _methods ::: List(fd)
- fd.setOwner(this)
}
def clearMethods() {
@@ -296,7 +305,6 @@ object Definitions {
val isCaseObject = false
lazy val singleCaseClasses : Seq[CaseClassDef] = Nil
- setSubDefOwners()
}
/** Case classes/objects. */
@@ -311,7 +319,6 @@ object Definitions {
def setFields(fields: Seq[ValDef]) {
_fields = fields
- _fields foreach { _.setOwner(this)}
}
@@ -327,7 +334,6 @@ object Definitions {
}
lazy val singleCaseClasses : Seq[CaseClassDef] = if (hasParent) Nil else Seq(this)
- setSubDefOwners()
}
@@ -364,7 +370,6 @@ object Definitions {
def fullBody = fullBody_
def fullBody_= (e : Expr) {
fullBody_ = e
- nestedFuns map {_.setOwner(this)}
}
def body: Option[Expr] = withoutSpec(fullBody)
@@ -439,7 +444,6 @@ object Definitions {
def isRecursive(p: Program) = p.callGraph.transitiveCallees(this) contains this
- setSubDefOwners()
// Deprecated, old API
@deprecated("Use .body instead", "2.3")
def implementation : Option[Expr] = body
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 9f1dfccc44670e2ed5c2378edf2d29bc49cf88d8..b043da9ac1fcdae8271419544e3aea9d3e192688 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1955,19 +1955,17 @@ object ExprOps {
(fds.values.toSet, res2)
}
- def isListLiteral(e: Expr): Option[(TypeTree, List[Expr])] = e match {
+ def isListLiteral(e: Expr)(implicit pgm: Program): Option[(TypeTree, List[Expr])] = e match {
case CaseClass(CaseClassType(classDef, Seq(tp)), Nil) =>
for {
- p <- programOf(classDef)
- leonNil <- p.library.Nil
+ leonNil <- pgm.library.Nil
if classDef == leonNil
} yield {
(tp, Nil)
}
case CaseClass(CaseClassType(classDef, Seq(tp)), Seq(hd, tl)) =>
for {
- p <- programOf(classDef)
- leonCons <- p.library.Cons
+ leonCons <- pgm.library.Cons
if classDef == leonCons
(_, tlElems) <- isListLiteral(tl)
} yield {
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 61bb1650e9a99a1e747b1188e3d16a1f4e359a7f..8b5b3cf240957a1d7cf0aab08a0fa1aad27157b9 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -8,6 +8,7 @@ import Common._
import Types._
import Constructors._
import ExprOps._
+import Definitions.Program
object Extractors {
@@ -179,11 +180,10 @@ object Extractors {
}
object StringLiteral {
- def unapply(e: Expr): Option[String] = e match {
+ def unapply(e: Expr)(implicit pgm: Program): Option[String] = e match {
case CaseClass(cct, args) =>
for {
- p <- DefOps.programOf(cct.classDef)
- libS <- p.library.String
+ libS <- pgm.library.String
if cct.classDef == libS
(_, chars) <- isListLiteral(args.head)
if chars.forall(_.isInstanceOf[CharLiteral])
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 8f77e8812e172a362b7ffa46086fa4045b020cce..1eed1d4842d668231538e47aaf01d263823390a4 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -15,6 +15,7 @@ object FunctionClosure extends TransformationPhase {
val name = "Function Closure"
val description = "Closing function with its scoping variables"
+ // TODO: Rewrite this phase
/* I know, that's a lot of mutable variables */
private var pathConstraints: List[Expr] = Nil
private var enclosingLets: List[(Identifier, Expr)] = Nil
@@ -24,24 +25,25 @@ object FunctionClosure extends TransformationPhase {
def apply(ctx: LeonContext, program: Program): Program = {
- val newUnits = program.units.map { u => u.copy(modules = u.modules map { m =>
- pathConstraints = Nil
- enclosingLets = Nil
- newFunDefs = Map()
- topLevelFuns = Set()
- parent = null
-
- val funDefs = m.definedFunctions
- funDefs.foreach(fd => {
- parent = fd
- pathConstraints = fd.precondition.toList
- fd.body = fd.body.map(b => functionClosure(b, fd.params.map(_.id).toSet, Map(), Map()))
- })
+ val newUnits = program.units.map { u => u.copy(defs = u.defs map {
+ case m: ModuleDef =>
+ pathConstraints = Nil
+ enclosingLets = Nil
+ newFunDefs = Map()
+ topLevelFuns = Set()
+ parent = null
+
+ val funDefs = m.definedFunctions
+ funDefs.foreach(fd => {
+ parent = fd
+ pathConstraints = fd.precondition.toList
+ fd.body = fd.body.map(b => functionClosure(b, fd.params.map(_.id).toSet, Map(), Map()))
+ })
- ModuleDef(m.id, m.defs ++ topLevelFuns, m.isStandalone )
+ ModuleDef(m.id, m.defs ++ topLevelFuns, m.isPackageObject )
+ case cd => cd
})}
- val res = Program(program.id, newUnits)
- res
+ Program(newUnits)
}
private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
@@ -61,8 +63,6 @@ object FunctionClosure extends TransformationPhase {
val newFunDef = new FunDef(newFunId, fd.tparams, fd.returnType, newValDefs, fd.defType).copiedFrom(fd)
topLevelFuns += newFunDef
newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
- newFunDef.setOwner(parent)
- fd .setOwner(parent)
newFunDef.orig = Some(fd)
def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
diff --git a/src/main/scala/leon/purescala/FunctionMapping.scala b/src/main/scala/leon/purescala/FunctionMapping.scala
index 19d16c2b13fb27819f26c7e58f090d47af7dc231..c7a31c61500a144f531dc7963ed87b0c963a400e 100644
--- a/src/main/scala/leon/purescala/FunctionMapping.scala
+++ b/src/main/scala/leon/purescala/FunctionMapping.scala
@@ -33,24 +33,26 @@ abstract class FunctionMapping extends TransformationPhase {
val newP =
program.copy(units = for (u <- program.units) yield {
u.copy(
- modules = for (m <- u.modules) yield {
- m.copy(defs = for (df <- m.defs) yield {
- df match {
- case f : FunDef =>
- val newF = functionToFunction.get(f).map{_.to}.getOrElse(f)
- newF.fullBody = replaceCalls(f.fullBody)
- newF
- case c : ClassDef =>
- // val oldMethods = c.methods
- // c.clearMethods()
- // for (m <- oldMethods) {
- // c.registerMethod(functionToFunction.get(m).map{_.to}.getOrElse(m))
- // }
- c
- case d =>
- d
- }
- })
+ defs = u.defs map {
+ case m: ModuleDef =>
+ m.copy(defs = for (df <- m.defs) yield {
+ df match {
+ case f : FunDef =>
+ val newF = functionToFunction.get(f).map{_.to}.getOrElse(f)
+ newF.fullBody = replaceCalls(f.fullBody)
+ newF
+ case c : ClassDef =>
+ // val oldMethods = c.methods
+ // c.clearMethods()
+ // for (m <- oldMethods) {
+ // c.registerMethod(functionToFunction.get(m).map{_.to}.getOrElse(m))
+ // }
+ c
+ case d =>
+ d
+ }
+ })
+ case d => d
},
imports = u.imports map {
case SingleImport(fd : FunDef) =>
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index c93f8fe9c6396de0b12a1adda037b2ad84049f86..f033681b2937046213aa07ff75f4908870242bf2 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -14,117 +14,79 @@ import TypeOps.instantiateType
object MethodLifting extends TransformationPhase {
val name = "Method Lifting"
- val description = "Translate methods into top-level functions"
+ val description = "Translate methods into functions of the companion object"
def apply(ctx: LeonContext, program: Program): Program = {
+
// First we create the appropriate functions from methods:
- var mdToFds = Map[FunDef, FunDef]()
-
- for {
- cd <- program.classHierarchyRoots
- if cd.methods.nonEmpty
- fd <- cd.methods
- } {
- // We import class type params and freshen them
- val ctParams = cd.tparams map { _.freshen }
- val tparamsMap = cd.tparams.zip(ctParams map { _.tp }).toMap
-
- val id = FreshIdentifier(cd.id.name+"$"+fd.id.name).setPos(fd.id)
- val recType = classDefToClassType(cd, ctParams.map(_.tp))
- 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).setPos(vd.getPos)
+ var mdToFds = Map[FunDef, FunDef]()
+
+ val newUnits = for (u <- program.units) yield {
+ var fdsOf = Map[String, Set[FunDef]]()
+
+ // 1) Create one function for each method
+ for { cd <- u.classHierarchyRoots if cd.methods.nonEmpty; fd <- cd.methods } {
+ // We import class type params and freshen them
+ val ctParams = cd.tparams map { _.freshen }
+ val tparamsMap = cd.tparams.zip(ctParams map { _.tp }).toMap
+
+ val id = fd.id.freshen
+ val recType = classDefToClassType(cd, ctParams.map(_.tp))
+ 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).setPos(vd.getPos)
+ }
+ 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) +: fdParams, fd.defType)
+ nfd.copyContentFrom(fd)
+ nfd.setPos(fd)
+ nfd.fullBody = postMap{
+ case This(ct) if ct.classDef == cd => Some(receiver.toVariable)
+ case _ => None
+ }(instantiateType(nfd.fullBody, tparamsMap, paramsMap))
+
+ mdToFds += fd -> nfd
+ fdsOf += cd.id.name -> (fdsOf.getOrElse(cd.id.name, Set()) + nfd)
}
- 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) +: fdParams, fd.defType)
- nfd.copyContentFrom(fd)
- nfd.setPos(fd)
- nfd.fullBody = instantiateType(nfd.fullBody, tparamsMap, paramsMap)
+ // 2) Place functions in existing companions:
+ val defs = u.defs map {
+ case md: ModuleDef if fdsOf contains md.id.name =>
+ val fds = fdsOf(md.id.name)
+ fdsOf -= md.id.name
+ ModuleDef(md.id, md.defs ++ fds, false)
+ case d => d
+ }
- mdToFds += fd -> nfd
- }
+ // 3) Create missing companions
+ val newCompanions = for ((name, fds) <- fdsOf) yield {
+ ModuleDef(FreshIdentifier(name), fds.toSeq, false)
+ }
- def translateMethod(fd: FunDef) = {
- val (nfd, rec) = mdToFds.get(fd) match {
- case Some(nfd) =>
- (nfd, Some(() => Variable(nfd.params.head.id)))
- case None =>
- (fd, None)
+ // 4) Remove methods in classes
+ for (cd <- u.definedClasses) {
+ cd.clearMethods
}
- nfd.fullBody = removeMethodCalls(rec)(nfd.fullBody)
- nfd
+ u.copy(defs = defs ++ newCompanions)
}
- def removeMethodCalls(rec: Option[() => Expr])(e: Expr): Expr = {
- postMap{
- case th: This =>
- rec match {
- case Some(r) =>
- Some(r().setPos(th))
- case None =>
- ctx.reporter.fatalError("`this` used out of a method context?!?")
- }
- case mi @ MethodInvocation(rec, cd, tfd, args) =>
- rec match {
- case IsTyped(rec, ct: ClassType) =>
- Some(FunctionInvocation(mdToFds(tfd.fd).typed(ct.tps ++ tfd.tps), rec +: args).setPos(mi))
- case _ =>
- ctx.reporter.fatalError("MethodInvocation on a non-class receiver !?!")
- }
+ val pgm = Program(newUnits)
+
+ // 5) Replace method calls with function calls
+ for (fd <- pgm.definedFunctions) {
+ fd.fullBody = postMap{
+ case mi @ MethodInvocation(IsTyped(rec, ct: ClassType), cd, tfd, args) =>
+ Some(FunctionInvocation(mdToFds(tfd.fd).typed(ct.tps ++ tfd.tps), rec +: args).setPos(mi))
case _ => None
- }(e)
+ }(fd.fullBody)
}
- val modsToMods = ( for {
- u <- program.units
- m <- u.modules
- } yield (m, {
- // We remove methods from class definitions and add corresponding functions
- val newDefs = m.defs.flatMap {
- case acd: AbstractClassDef if acd.methods.nonEmpty =>
- acd +: acd.methods.map(translateMethod)
-
- case ccd: CaseClassDef if ccd.methods.nonEmpty =>
- ccd +: ccd.methods.map(translateMethod)
-
- case fd: FunDef =>
- List(translateMethod(fd))
-
- case d =>
- List(d)
- }
-
- // finally, we clear methods from classes
- m.defs.foreach {
- case cd: ClassDef =>
- cd.clearMethods()
- case _ =>
- }
- ModuleDef(m.id, newDefs, m.isStandalone )
- })).toMap
-
- val newUnits = program.units map { u => u.copy(
-
- imports = u.imports flatMap {
- case s@SingleImport(c : ClassDef) =>
- // If a class is imported, also add the "methods" of this class
- s :: ( c.methods map { md => SingleImport(mdToFds(md))})
- // If importing a ModuleDef, update to new ModuleDef
- case SingleImport(m : ModuleDef) => List(SingleImport(modsToMods(m)))
- case WildcardImport(m : ModuleDef) => List(WildcardImport(modsToMods(m)))
- case other => List(other)
- },
-
- modules = u.modules map modsToMods
-
- )}
-
- Program(program.id, newUnits)
+ pgm
}
}
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index ee545d9ab73cbdff03a15f89d86f0ec355799a8b..a21149b594f9da1509b5e3edbc298d7ce31ee1c8 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -132,19 +132,19 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
def printWithPath(df: Definition)(implicit ctx : PrinterContext) {
- ctx.scope match {
- case Some(scope) =>
- try {
- val (pack, defPath) = pathAsVisibleFrom(scope, df)
- val toPrint = pack ++ (defPath collect { case df if !df.isInstanceOf[UnitDef] => df.id})
- p"${nary(toPrint, ".")}"
- } catch {
- // If we did not manage to find the path, just print the id
- case _ : NoSuchElementException => p"${df.id}"
- }
- case None =>
+ //ctx.scope match {
+ // case Some(scope) =>
+ // try {
+ // val (pack, defPath) = pathAsVisibleFrom(scope, df)
+ // val toPrint = pack ++ (defPath collect { case df if !df.isInstanceOf[UnitDef] => df.id})
+ // p"${nary(toPrint, ".")}"
+ // } catch {
+ // // If we did not manage to find the path, just print the id
+ // case _ : NoSuchElementException => p"${df.id}"
+ // }
+ // case None =>
p"${df.id}"
- }
+ //}
}
@@ -233,30 +233,30 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
p"""|?($es)"""
}
case e @ CaseClass(cct, args) =>
- isListLiteral(e) match {
- case Some((tpe, elems)) =>
- val chars = elems.collect{case CharLiteral(ch) => ch}
- if (chars.length == elems.length && tpe == CharType) {
- // String literal
- val str = chars mkString ""
- val q = '"'
- p"$q$str$q"
- } else {
- val elemTps = leastUpperBound(elems.map(_.getType))
- if (elemTps == Some(tpe)) {
- p"List($elems)"
- } else {
- p"List[$tpe]($elems)"
- }
- }
-
- case None =>
+ //isListLiteral(e) match {
+ // case Some((tpe, elems)) =>
+ // val chars = elems.collect{case CharLiteral(ch) => ch}
+ // if (chars.length == elems.length && tpe == CharType) {
+ // // String literal
+ // val str = chars mkString ""
+ // val q = '"'
+ // p"$q$str$q"
+ // } else {
+ // val elemTps = leastUpperBound(elems.map(_.getType))
+ // if (elemTps == Some(tpe)) {
+ // p"List($elems)"
+ // } else {
+ // p"List[$tpe]($elems)"
+ // }
+ // }
+
+ // case None =>
if (cct.classDef.isCaseObject) {
p"$cct"
} else {
p"$cct($args)"
}
- }
+ //}
@@ -539,31 +539,32 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
// Definitions
- case Program(id, units) =>
+ case Program(units) =>
p"""${nary(units filter {_.isMainUnit}, "\n\n")}"""
+ //p"""${nary(units, "\n\n")}"""
- case UnitDef(id,modules,pack,imports,_) =>
+ case UnitDef(id,pack, imports, defs,_) =>
if (pack.nonEmpty){
p"""|package ${pack mkString "."}
|"""
}
p"""|${nary(imports,"\n")}
- |${nary(modules,"\n\n")}
+ |${nary(defs,"\n\n")}
|"""
case PackageImport(pack) =>
- import leon.purescala.DefOps._
- val newPack = ( for (
- scope <- ctx.scope;
- unit <- unitOf(scope);
- currentPack = unit.pack
- ) yield {
- if (isSuperPackageOf(currentPack,pack))
- pack drop currentPack.length
- else
- pack
- }).getOrElse(pack)
- p"import ${nary(newPack,".")}._"
+ //import leon.purescala.DefOps._
+ //val newPack = ( for (
+ // scope <- ctx.scope;
+ // unit <- unitOf(scope);
+ // currentPack = unit.pack
+ //) yield {
+ // if (isSuperPackageOf(currentPack,pack))
+ // pack drop currentPack.length
+ // else
+ // pack
+ //}).getOrElse(pack)
+ p"import ${nary(pack,".")}._"
case SingleImport(df) =>
p"import "; printWithPath(df)
@@ -686,13 +687,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
val fid = tfd.fd.id
- val maybeClassName = fid.name.substring(0, cd.id.name.length)
-
- val fname = if (maybeClassName == cd.id.name) {
- fid.name.substring(cd.id.name.length + 1) // +1 to also remove $
- } else {
- fid.name
- }
+ val fname = fid.name
val decoded = scala.reflect.NameTransformer.decode(fname)
@@ -793,12 +788,12 @@ abstract class PrettyPrinterFactory {
def apply(tree: Tree, opts: PrinterOptions = PrinterOptions(), scope : Option[Definition] = None): String = {
val printer = create(opts)
- val scope_ = (tree, scope) match {
- // Try to find a scope, if we are given none.
- case (df : Definition, None) => df.owner
- case _ => None
- }
- val ctx = PrinterContext(tree, None, scope_, opts.baseIndent, printer)
+// val scope_ = (tree, scope) match {
+// // Try to find a scope, if we are given none.
+// case (df : Definition, None) => df.owner
+// case _ => None
+// }
+ val ctx = PrinterContext(tree, None, scope, opts.baseIndent, printer)
printer.pp(tree)(ctx)
printer.toString
}
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index 87bd92e6428022c32025a6734dd41e77a2df41d7..61c85d389c0805e0ba7937f8f1af9767f69b0c31 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -20,6 +20,8 @@ object RestoreMethods extends TransformationPhase {
* New functions are returned, whereas classes are mutated
*/
def apply(ctx : LeonContext, p : Program) = {
+ p
+ /*
var fd2Md = Map[FunDef, FunDef]()
var whoseMethods = Map[ClassDef, Seq[FunDef]]()
@@ -57,9 +59,9 @@ object RestoreMethods extends TransformationPhase {
}
}
- /**
+ / **
* Substitute a function in an expression with the respective new method
- */
+ * /
def substituteMethods = preMapOnFunDef ({
case FunctionInvocation(tfd,args) if fd2Md contains tfd.fd => {
val md = fd2Md.get(tfd.fd).get // the method we are substituting
@@ -74,9 +76,9 @@ object RestoreMethods extends TransformationPhase {
case _ => None
}, true) _
- /**
+ / **
* Renew that function map by applying subsituteMethods on its values to obtain correct functions
- */
+ * /
val fd2MdFinal = fd2Md.mapValues(substituteMethods)
val oldFuns = fd2MdFinal.map{ _._1 }.toSet
@@ -136,7 +138,7 @@ object RestoreMethods extends TransformationPhase {
}
)})
-
+ */
}
}
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 920a45b5060cde5508c8acaa4279c8cc14cbf02e..aa9e60f4b95eae7b621238ba01ea94614d253a0b 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -5,23 +5,23 @@ package utils
import purescala.Definitions._
import purescala.Types._
-import purescala.DefOps.searchByFullName
+import purescala.DefOps._
case class Library(pgm: Program) {
- lazy val List = lookup("leon.collection.List") collect { case acd : AbstractClassDef => acd }
- lazy val Cons = lookup("leon.collection.Cons") collect { case ccd : CaseClassDef => ccd }
- lazy val Nil = lookup("leon.collection.Nil") collect { case ccd : CaseClassDef => ccd }
+ lazy val List = lookup("leon.collection.List").collect{ case acd : AbstractClassDef => acd }.headOption
+ lazy val Cons = lookup("leon.collection.Cons").collect { case ccd : CaseClassDef => ccd }.headOption
+ lazy val Nil = lookup("leon.collection.Nil").collect { case ccd : CaseClassDef => ccd }.headOption
- lazy val Option = lookup("leon.lang.Option") collect { case acd : AbstractClassDef => acd }
- lazy val Some = lookup("leon.lang.Some") collect { case ccd : CaseClassDef => ccd }
- lazy val None = lookup("leon.lang.None") collect { case ccd : CaseClassDef => ccd }
+ lazy val Option = lookup("leon.lang.Option").collect { case acd : AbstractClassDef => acd }.headOption
+ lazy val Some = lookup("leon.lang.Some").collect { case ccd : CaseClassDef => ccd }.headOption
+ lazy val None = lookup("leon.lang.None").collect { case ccd : CaseClassDef => ccd }.headOption
- lazy val String = lookup("leon.lang.string.String") collect { case ccd : CaseClassDef => ccd }
+ lazy val String = lookup("leon.lang.string.String").collect { case ccd : CaseClassDef => ccd }.headOption
- lazy val setToList = lookup("leon.collection.setToList") collect { case fd : FunDef => fd }
-
- def lookup(name: String): Option[Definition] = {
- searchByFullName(name, pgm)
+ lazy val setToList = lookup("leon.collection.setToList").collect { case fd : FunDef => fd }.headOption
+
+ def lookup(name: String): Seq[Definition] = {
+ pgm.lookupAll(name)
}
def optionType(tp: TypeTree) = AbstractClassType(Option.get, Seq(tp))
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index a8728346c71fecafadda56c760e12c7173a5cde8..0af3318395d518743208ce3c7777c3c774354bea 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -19,32 +19,35 @@ object UnitElimination extends TransformationPhase {
private var id2FreshId: Map[Identifier, Identifier] = Map()
def apply(ctx: LeonContext, pgm: Program): Program = {
- val newUnits = pgm.units map { u => u.copy(modules = u.modules.map { m =>
- fun2FreshFun = Map()
- val allFuns = m.definedFunctions
- //first introduce new signatures without Unit parameters
- allFuns.foreach(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.addAnnotation(fd.annotations.toSeq:_*)
- fun2FreshFun += (fd -> freshFunDef)
- } else {
- fun2FreshFun += (fd -> fd) //this will make the next step simpler
- }
- })
+ val newUnits = pgm.units map { u => u.copy(defs = u.defs.map {
+ case m: ModuleDef =>
+ fun2FreshFun = Map()
+ val allFuns = m.definedFunctions
+ //first introduce new signatures without Unit parameters
+ allFuns.foreach(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.addAnnotation(fd.annotations.toSeq:_*)
+ fun2FreshFun += (fd -> freshFunDef)
+ } else {
+ fun2FreshFun += (fd -> fd) //this will make the next step simpler
+ }
+ })
- //then apply recursively to the bodies
- val newFuns = allFuns.collect{ case fd if fd.returnType != UnitType =>
- val newFd = fun2FreshFun(fd)
- newFd.fullBody = removeUnit(fd.fullBody)
- newFd
- }
+ //then apply recursively to the bodies
+ val newFuns = allFuns.collect{ case fd if fd.returnType != UnitType =>
+ val newFd = fun2FreshFun(fd)
+ newFd.fullBody = removeUnit(fd.fullBody)
+ newFd
+ }
- ModuleDef(m.id, m.definedClasses ++ newFuns, m.isStandalone )
+ ModuleDef(m.id, m.definedClasses ++ newFuns, m.isPackageObject )
+ case d =>
+ d
})}
- Program(pgm.id, newUnits)
+ Program(newUnits)
}
private def simplifyType(tpe: TypeTree): TypeTree = tpe match {
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 28ff7349b5d586b2156537d1b31e4e8179b067e6..2828a220fbcee0c6ffd470cbc3d1431513c45c1c 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -37,11 +37,11 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
var subFunctionsOf = Map[FunDef, Set[FunDef]]().withDefaultValue(Set())
- pgm2.definedFunctions.foreach { fd => fd.owner match {
- case Some(p : FunDef) =>
- subFunctionsOf += p -> (subFunctionsOf(p) + fd)
- case _ =>
- }}
+ //pgm2.definedFunctions.foreach { fd => fd.owner match {
+ // case Some(p : FunDef) =>
+ // subFunctionsOf += p -> (subFunctionsOf(p) + fd)
+ // case _ =>
+ //}}
val newOptions = ctx.options map {
@@ -78,10 +78,11 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val newResults = for ((vc, ovr) <- vr.results) yield {
if(functionWasLoop(vc.fd)) {
val nvc = VC(vc.condition,
- vc.fd.owner match {
- case Some(fd: FunDef) => fd
- case _ => vc.fd
- },
+ vc.fd,
+ //vc.fd.owner match {
+ // case Some(fd: FunDef) => fd
+ // case _ => vc.fd
+ //},
vc.kind.underlying match {
case VCKinds.Postcondition => VCXLangKinds.InvariantPost
case VCKinds.Precondition => VCXLangKinds.InvariantInd
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index f34d82dee639a7052cfcb9adc314b0bf7f4c4a63..1f00e411f8864613f38903512334388c898b2fea 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -40,7 +40,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
private def mkCall(name : String, args : Expr*)(implicit p : Program) = {
val fn = s"Program.$name"
- searchByFullName(fn, p) match {
+ p.lookup(fn) match {
case Some(fd: FunDef) =>
FunctionInvocation(fd.typed, args.toSeq)
case _ =>
@@ -49,7 +49,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
}
private def mkCaseClass(name : String, args : Expr*)(implicit p : Program) = {
- searchByFullName("Program."+name, p) match {
+ p.lookup("Program."+name) match {
case Some(ccd: CaseClassDef) =>
CaseClass(CaseClassType(ccd, Nil), args.toSeq)
case _ =>
diff --git a/src/test/scala/leon/test/purescala/DefOpsTests.scala b/src/test/scala/leon/test/purescala/DefOpsTests.scala
index 0f6d2465cb4b7531e3465d7c73d8b8368e050bd3..ece376ccab14563e71d984514fca1b14f5076c3d 100644
--- a/src/test/scala/leon/test/purescala/DefOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/DefOpsTests.scala
@@ -66,36 +66,38 @@ private [purescala] object DefOpsHelper extends LeonTestSuite {
""" object InEmpty { def arrayLookup(a : Array[Int], i : Int) = a(i) } """
)
- val program = parseStrings(test1)
- val fooC = searchByFullName("foo.bar.baz.Foo.fooC",program)
+ implicit val program = parseStrings(test1)
+ lazy val fooC = program.lookup("foo.bar.baz.Foo.fooC")
}
class DefOpsTests extends LeonTestSuite {
import DefOpsHelper._
- test("Find base definition"){assert(fooC.isDefined)}
+ test("Find base definition"){
+ assert(fooC.isDefined)
+ }
test("Least common ancestor"){
- val x = searchByFullName("foo.bar.baz.x",program)
+ val x = program.lookup("foo.bar.baz.x")
assert(x.isDefined)
- assert(leastCommonAncestor(x.get,fooC.get) == program)
- val fooClass = searchByFullName("foo.bar.baz.Foo.FooC",program)
+ assert(leastCommonAncestor(x.get, fooC.get) == program)
+ val fooClass = program.lookup("foo.bar.baz.Foo.FooC")
assert (fooClass.isDefined)
assert(leastCommonAncestor(fooC.get, fooClass.get).id.name == "Foo")
}
test("In empty package") {
val name = "InEmpty.arrayLookup"
- val df = searchByFullName(name,program)
+ val df = program.lookup(name)
assert(df.isDefined)
assert{fullName(df.get) == name }
}
// Search by full name
- def mustFind(name : String, msg : String) = test(msg) {assert(searchByFullNameRelative(name,fooC.get).isDefined) }
- def mustFail(name : String, msg : String) = test(msg) {assert(searchByFullNameRelative(name,fooC.get).isEmpty) }
+ def mustFind(name: String, msg: String) = test(msg) {assert(searchRelative(name, fooC.get).nonEmpty) }
+ def mustFail(name: String, msg: String) = test(msg) {assert(searchRelative(name, fooC.get).isEmpty) }
mustFind("fooC", "Find yourself")
mustFind("FooC", "Find a definition in the same scope 1")
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index 17fb42fa16cf5b72a3ff068869849b1eede57cdb..121101041a2fc6cfde07820341998f116b0b24f4 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -23,7 +23,6 @@ class UnrollingSolverTests extends LeonTestSuite {
fDef.postcondition = Some(Lambda(Seq(ValDef(fres)), GreaterThan(Variable(fres), InfiniteIntegerLiteral(0))))
private val program = Program(
- FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false))
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index cab248d9b342186dc3b286ba386c94fedf04ec92..544d9cd4ae663bfcd5e102ef3464d26c49e37d26 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -42,7 +42,6 @@ class FairZ3SolverTests extends LeonTestSuite {
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
- FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false)
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 58d88cbdf8fa41226bf7345792ce518b3d04af2f..a6ae287369fdc5b7d1c540ec289c46dfa2b062db 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -51,7 +51,6 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
- FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false)
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index cb78580356700e05b0350289cefd819f31cb027d..b59e7437a89ef0a0befdf75a181cc50511c6ee49 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -48,7 +48,6 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
gDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
- FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false)
diff --git a/src/test/scala/leon/test/verification/VerificationRegression.scala b/src/test/scala/leon/test/verification/VerificationRegression.scala
index 5b559d5b54d2ea9e976982587deca6d2f22787d1..55030f8713ca386c79b0359345f6db9cc84561ba 100644
--- a/src/test/scala/leon/test/verification/VerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/VerificationRegression.scala
@@ -42,10 +42,10 @@ trait VerificationRegression extends LeonTestSuite {
val ast = extraction.run(ctx)(files)
val programs = {
val (user, lib) = ast.units partition { _.isMainUnit }
- user map { u => Program(u.id.freshen, u :: lib) }
+ user map { u => (u.id, Program(u :: lib)) }
}
- for (p <- programs; options <- optionVariants) {
- test(f"${nextInt()}%3d: ${p.id.name} ${options.mkString(" ")}") {
+ for ((id, p) <- programs; options <- optionVariants) {
+ test(f"${nextInt()}%3d: ${id.name} ${options.mkString(" ")}") {
val ctx = createLeonContext(options: _*)
val report = pipeBack.run(ctx)(p)
block(Output(report, ctx.reporter))