diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index defcdb45380a151c7ecd1268f3857541a708b2ce..b41389fc2040b4d3785098830d4328c0d7d6d5d2 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -172,7 +172,7 @@ trait ASTExtractors {
* objects of case classes (or any synthetic class). */
def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
- Some((if (name.toString == "package") cd.symbol.owner.name.toString else name.toString, impl))
+ Some((name.toString, impl))
}
case _ => None
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index ceaac05a72e988d33ace2e7a88f3473543c51cb7..4d08236a73ddff5e8d71409229cfd55114c1900d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -23,8 +23,7 @@ import purescala.Common._
import purescala.Extractors.IsTyped
import purescala.TreeOps._
import purescala.TypeTreeOps._
-import purescala.DefOps.inPackage
-
+import purescala.DefOps.{inPackage, inUnit}
import xlang.Trees.{Block => LeonBlock, _}
import xlang.TreeOps._
@@ -114,7 +113,7 @@ 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])
+ case class TempModule(name : Identifier, trees : List[Tree], isStandalone : Boolean)
case class TempUnit(
name : String,
pack : PackageRef,
@@ -190,57 +189,73 @@ trait CodeExtraction extends ASTExtractors {
def isExtern(s: Symbol) = {
annotationsOf(s) contains "extern"
}
-
+
def extractUnits: List[UnitDef] = {
try {
def isLib(u : CompilationUnit) = Build.libFiles contains u.source.file.absolute.path
val templates: List[TempUnit] = units.reverse.map { u => u.body match {
- case pd @ PackageDef(refTree, lst) =>
-
- var standaloneDefs = List[Tree]()
-
- val modules = lst.flatMap { _ match {
-
- case t if isIgnored(t.symbol) =>
- None
+ // 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)
+ )
- case PackageDef(_, List(ExObjectDef(n, templ))) =>
- Some(TempModule(FreshIdentifier(n), templ.body))
-
- case ExObjectDef(n, templ) =>
- Some(TempModule(FreshIdentifier(n), templ.body))
-
- case d @ ExAbstractClass(_, _, _) =>
- standaloneDefs ::= d
- None
-
- case d @ ExCaseClass(_, _, _, _) =>
- standaloneDefs ::= d
- None
-
- case d @ ExCaseClassSyntheticJunk() =>
- None
-
- case other =>
- outOfSubsetError(other, "Expected: top-level object/class.")
- None
- }}
-
- // File name without extension
- val unitName = u.source.file.name.replaceFirst("[.][^.]+$", "")
+
+ case pd @ PackageDef(refTree, lst) =>
+
+ var standaloneDefs = List[Tree]()
+
+ val modules = lst.flatMap { _ match {
- TempUnit(unitName,
- extractPackageRef(refTree),
- if (standaloneDefs.isEmpty) modules
- else ( TempModule(FreshIdentifier(unitName+ "$standalone"), standaloneDefs) ) :: modules,
- imports.getOrElse(refTree, Nil),
- !isLib(u)
- )
+ case t if isIgnored(t.symbol) =>
+ None
+
+ case po@ExObjectDef(n, templ) if n == "package" =>
+ outOfSubsetError(po, "No other definitions are allowed in a file with a package object.")
+
+ case ExObjectDef(n, templ) if n != "package" =>
+ Some(TempModule(FreshIdentifier(n), templ.body, false))
- }
- }
+ case d @ ExAbstractClass(_, _, _) =>
+ standaloneDefs ::= d
+ None
+
+ case d @ ExCaseClass(_, _, _, _) =>
+ standaloneDefs ::= d
+ None
+
+ case d @ ExCaseClassSyntheticJunk() =>
+ None
+
+ case other =>
+ outOfSubsetError(other, "Expected: top-level object/class.")
+ None
+ }}
+
+ // 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
+ }
+
+ TempUnit(unitName,
+ extractPackageRef(refTree),
+ finalModules,
+ imports.getOrElse(refTree, Nil),
+ !isLib(u)
+ )
+ }}
// Phase 1, we detect objects/classes/types
for (temp <- templates; mod <- temp.modules) collectClassSymbols(mod.trees)
@@ -258,22 +273,35 @@ trait CodeExtraction extends ASTExtractors {
for (temp <- templates; mod <- temp.modules) extractFunDefs(mod.trees)
// Phase 6, we create modules and extract bodies
- for (temp <- templates; mod <- temp.modules) extractObjectDef(mod.name, mod.trees)
+ 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),
+ for( TempModule(nm,_,_) <- mods) yield objects2Objects(nm),
pack, Nil, isPrintable
)
, imps
)
}
+ // With the aid of formed units, we extract the correct imports
+ val objPerPack = objects2Objects map { _._2 } groupBy { inPackage(_)}
withoutImports map { case (u, imps) =>
- u.copy(imports = imps flatMap { extractImport(_, u,withoutImports map { _._1}) }
- )}
+ 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
+ })
+ }
} catch {
case icee: ImpureCodeEncounteredException =>
@@ -342,14 +370,24 @@ trait CodeExtraction extends ASTExtractors {
def isWildcard (l : List[String]) = l.length == 1 && l.head == "_"
if (isWildcard(objectPart)) Some(PackageImport(packagePart))
else {
-
+ // FIXME this is terribly inefficient
def fromName(pack : PackageRef, name : String) : Option[ Definition ] = {
- objects2Objects find { case (_,v) =>
+ val cand1 = objects2Objects find { case (_,v) =>
val id = v.id.toString
val pack_ = inPackage(v)
- id == objectPart.head &&
- pack_ == pack
+ id == objectPart.head && pack_ == pack
} map { _._2 }
+
+ if (cand1.isDefined) cand1 else {
+ // Search in standalone objects
+ objects2Objects.collect {
+ case (_, LeonModuleDef(_,subDefs, true)) => subDefs
+ }.flatten.find { v =>
+ val id = v.id.toString
+ val pack_ = inPackage(v)
+ id == objectPart.head && pack_ == pack
+ }
+ }
}
// Finds the correct Definition from a RefPath, starting in df
@@ -755,7 +793,7 @@ trait CodeExtraction extends ASTExtractors {
var objects2Objects = Map[Identifier, LeonModuleDef]()
- private def extractObjectDef(id : Identifier, defs: List[Tree]) {
+ private def extractObjectDef(id : Identifier, defs: List[Tree], isStandalone : Boolean) {
val newDefs = defs.flatMap{ t => t match {
case t if isIgnored(t.symbol) =>
@@ -795,7 +833,7 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
}
- objects2Objects += id -> LeonModuleDef(id, newDefs, id.toString contains "$standalone")
+ objects2Objects += id -> LeonModuleDef(id, newDefs, isStandalone)
}
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index b986ea6774740bcfb2f2dd6856f63da210314e59..c5e192e34301e6e00a0e162488109bdcce9b7f91 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -25,7 +25,7 @@ object DefOps {
case other => inProgram(other.owner.get)
}
}
-
+
def pathFromRoot (df : Definition): List[Definition] ={
def rec(df : Definition) : List[Definition] = df.owner match {
case Some(owner) => df :: rec(owner)
@@ -52,7 +52,7 @@ object DefOps {
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) = {
val visiblePacks =
inPackage(df) +: (inUnit(df).toSeq.flatMap(_.imports) collect { case PackageImport(pack) => pack })
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 20cdf8b5eb79cef04916e8d42f3d28e251675790..61b8c53a6c5ae143149b695ae167b781651c89b0 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -71,7 +71,8 @@ object Definitions {
def classHierarchyRoots = units.flatMap(_.classHierarchyRoots)
def algebraicDataTypes = units.flatMap(_.algebraicDataTypes).toMap
def singleCaseClasses = units.flatMap(_.singleCaseClasses)
-
+ def modules = units.flatMap(_.modules)
+
lazy val callGraph = new CallGraph(this)
def caseClassDef(name: String) = definedClasses.collect {
@@ -106,6 +107,7 @@ object Definitions {
setSubDefOwners()
}
+ /** A package as a path of names */
type PackageRef = List[String]
abstract class Import extends Definition {
@@ -114,15 +116,14 @@ object Definitions {
lazy val importedDefs = this match {
case PackageImport(pack) => {
import DefOps._
- // Ignore standalone objects, assume there are extra imports for them
+ // Ignore standalone modules, assume there are extra imports for them
unitsInPackage(inProgram(this),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 "."))
@@ -176,7 +177,7 @@ object Definitions {
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
- case class ModuleDef(id: Identifier, defs : Seq[Definition], isStandalone : Boolean = false) extends Definition {
+ case class ModuleDef(id: Identifier, defs : Seq[Definition], val isStandalone : Boolean) extends Definition {
def subDefinitions = defs
@@ -201,7 +202,7 @@ object Definitions {
case cd : ClassDef => cd.duplicate
case other => other // FIXME: huh?
}})
-
+
setSubDefOwners()
}
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 225070f6f834f99a8bd357f28108aa8b3e892216..7d9066f895fb9bcc841b2ad005127aac29d97188 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -38,7 +38,7 @@ object FunctionClosure extends TransformationPhase {
fd.body = fd.body.map(b => functionClosure(b, fd.params.map(_.id).toSet, Map(), Map()))
})
- ModuleDef(m.id, m.defs ++ topLevelFuns)
+ ModuleDef(m.id, m.defs ++ topLevelFuns, m.isStandalone )
})}
val res = Program(program.id, newUnits)
res
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index abac76b18f7049e5286988c00f081e9d40770343..3ab73e549b25eb7ff3be969fe8fa98ca0a4b6255 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -98,7 +98,7 @@ object MethodLifting extends TransformationPhase {
case _ =>
}
- ModuleDef(m.id, newDefs)
+ ModuleDef(m.id, newDefs, m.isStandalone )
})}
Program(program.id, newUnits)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index d048771eb35fe3ce8cb9ab29c3cda3e2105bc6fd..938960f506c1ceb8d50a0ee3fa69c41afdb12786 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -113,7 +113,7 @@ class Synthesizer(val context : LeonContext,
val newDefs = sol.defs + fd
val npr = program.copy(units = program.units map { u =>
- u.copy(modules = ModuleDef(FreshIdentifier("synthesis"), newDefs.toSeq) +: u.modules )
+ u.copy(modules = ModuleDef(FreshIdentifier("synthesis"), newDefs.toSeq, false) +: u.modules )
})
(npr, newDefs)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 23edc4de565d83411cc4ed3a1a522d8648b1194a..9d9311ef49f6bd81da54e3914c5d15082aaa0d7e 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -40,7 +40,7 @@ trait Solvable extends Processor {
val structDefs = checker.defs
val program : Program = checker.program
val context : LeonContext = checker.context
- val sizeModule : ModuleDef = ModuleDef(FreshIdentifier("$size", false), checker.defs.toSeq)
+ val sizeModule : ModuleDef = ModuleDef(FreshIdentifier("$size", false), checker.defs.toSeq, false)
val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size", false),Seq(sizeModule))
val newProgram : Program = program.copy( units = sizeUnit :: program.units)
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 0bd55feb3b29d29f686896730ea82d13207f0bf8..5cdbdc3d582919924f2aa2081f868cffca6ac7b1 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -44,7 +44,7 @@ object UnitElimination extends TransformationPhase {
Seq(newFd)
})
- ModuleDef(m.id, m.definedClasses ++ newFuns)
+ ModuleDef(m.id, m.definedClasses ++ newFuns, m.isStandalone )
})}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index b646893d3b4de1ce3032b022a7a276bf04430a31..bde8cc42346edb8b5c2e53821f9a153e6e94c264 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -46,7 +46,7 @@ class FairZ3SolverTests extends LeonTestSuite {
FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
- List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef))
+ 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 663a9038a6dca67284004defff6953601890910c..685bea19be921c205f0a427f3269b2b36e21cfb8 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -54,7 +54,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
- List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef))
+ 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 561a107dc3f9d85b5104b9401a6337cddad6a404..b56d3e0bad214d4e92a1b79a97a94d88d2df65c6 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -51,7 +51,7 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
FreshIdentifier("Minimal"),
List(UnitDef(
FreshIdentifier("Minimal"),
- List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef))
+ List(ModuleDef(FreshIdentifier("Minimal"), Seq(fDef), false)
)))
)