From 0f51db75093fa83a410ac7c31ef86fe07cec8582 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 17 Mar 2014 20:18:00 +0100
Subject: [PATCH] Scope information in Definition
---
src/main/scala/leon/Main.scala | 1 +
.../scala/leon/purescala/Definitions.scala | 24 +++++++++++++++++++
.../scala/leon/utils/PreprocessingPhase.scala | 1 +
src/main/scala/leon/utils/ScopingPhase.scala | 24 +++++++++++++++++++
4 files changed, 50 insertions(+)
create mode 100644 src/main/scala/leon/utils/ScopingPhase.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 325ba92de..77772b1cf 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -11,6 +11,7 @@ object Main {
frontends.scalac.ExtractionPhase,
utils.TypingPhase,
FileOutputPhase,
+ ScopingPhase,
xlang.ArrayTransformation,
xlang.EpsilonElimination,
xlang.ImperativeCodeElimination,
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index e3ad66bef..e2d22bbb0 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -15,11 +15,22 @@ object Definitions {
sealed abstract class Definition extends Tree {
val id: Identifier
+ var enclosing : Option[Definition] = None // The definition/scope enclosing this definition
+ def subDefinitions : Seq[Definition] // The enclosed scopes/definitions by this definition
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 => enclosing = df.enclosing
+ case _ => // FIXME should this ever happen?
+ }
+ this
+ }
+
}
/** A ValDef declares a new identifier to be of a certain type. */
@@ -28,6 +39,7 @@ object Definitions {
val fixedType = tpe
+ def subDefinitions = Seq()
override def hashCode : Int = id.hashCode
override def equals(that : Any) : Boolean = that match {
case t : ValDef => t.id == this.id
@@ -40,6 +52,9 @@ object Definitions {
/** 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, modules: List[ModuleDef]) extends Definition {
+ enclosing = None
+ def subDefinitions = modules
+
def definedFunctions = modules.flatMap(_.definedFunctions)
def definedClasses = modules.flatMap(_.definedClasses)
def classHierarchyRoots = modules.flatMap(_.classHierarchyRoots)
@@ -77,12 +92,16 @@ object Definitions {
}
case class TypeParameterDef(tp: TypeParameter) extends Definition {
+ def subDefinitions = Seq()
val id = tp.id
}
/** Objects work as containers for class definitions, functions (def's) and
* val's. */
case class ModuleDef(id: Identifier, defs : Seq[Definition]) extends Definition {
+
+ def subDefinitions = defs
+
lazy val definedFunctions : Seq[FunDef] = defs.collect { case fd: FunDef => fd }
lazy val definedClasses : Seq[ClassDef] = defs.collect { case ctd: ClassDef => ctd }
@@ -106,6 +125,8 @@ object Definitions {
sealed trait ClassDef extends Definition {
self =>
+ def subDefinitions = methods
+
val id: Identifier
val tparams: Seq[TypeParameterDef]
def fields: Seq[ValDef]
@@ -206,6 +227,8 @@ object Definitions {
fullBody = withPostcondition(fullBody, op)
}
+ def subDefinitions = Seq()
+
// Metadata kept here after transformations
var parent: Option[FunDef] = None
var orig: Option[FunDef] = None
@@ -220,6 +243,7 @@ object Definitions {
this.fullBody = from.fullBody
this.parent = from.parent
this.orig = from.orig
+ this.enclosing = from.enclosing
this.addAnnotation(from.annotations.toSeq : _*)
}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 9d1c277e9..9a27ea1c5 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -16,6 +16,7 @@ object PreprocessingPhase extends TransformationPhase {
def apply(ctx: LeonContext, p: Program): Program = {
val phases =
+ ScopingPhase andThen
MethodLifting andThen
TypingPhase andThen
ConvertWithOracle andThen
diff --git a/src/main/scala/leon/utils/ScopingPhase.scala b/src/main/scala/leon/utils/ScopingPhase.scala
new file mode 100644
index 000000000..deb2e8a13
--- /dev/null
+++ b/src/main/scala/leon/utils/ScopingPhase.scala
@@ -0,0 +1,24 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon.utils
+
+import leon._
+import purescala.Definitions._
+
+object ScopingPhase extends UnitPhase[Program] {
+
+ val name = "Scoping phase"
+ val description = "Insert scoping information to all definitions in the program"
+
+ def apply(ctx: LeonContext, p: Program) {
+ insertScopingInformation(p, None)
+ }
+
+ private def insertScopingInformation(df : Definition , parent : Option[Definition]) {
+ df.enclosing = parent
+ for (sub <- df.subDefinitions){
+ insertScopingInformation(sub, Some(df))
+ }
+ }
+
+}
\ No newline at end of file
--
GitLab