From eeb0f67398df04c79db8785c181f2c09fb708676 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Fri, 5 Sep 2014 14:54:36 +0200
Subject: [PATCH] Support for looking up Definitions

---
 src/main/scala/leon/purescala/DefOps.scala | 141 +++++++++++++++++++++
 1 file changed, 141 insertions(+)

diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index c5e192e34..d42162ce3 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -48,6 +48,30 @@ object DefOps {
     .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] = {
+    var toRet = Map[String,Definition]()
+    val asList = 
+      (pathFromRoot(df).reverse flatMap { _.subDefinitions })  ++
+      (unitsInPackage(inProgram(df), inPackage(df)) flatMap { _.subDefinitions } ) ++
+      Seq(inProgram(df)) ++
+      ( for ( u <- inUnit(df).toSeq;
+              imp <- u.imports;
+              impDf <- imp.importedDefs
+            ) yield impDf 
+      )
+    for ( 
+      df <- asList;
+      name = df.id.toString
+    ) {
+      if (!(toRet contains name)) toRet += name -> df
+    }
+    toRet.values.toSet
+  }
+
   /** Returns true for strict superpackage */ 
   def isSuperPackageOf(p1:PackageRef, p2 : PackageRef) = 
     (p2.length > p1.length) && 
@@ -83,6 +107,123 @@ object DefOps {
     (pack, finalPath)
   }
 
+
+  def searchByFullName (
+    fullName : String,
+    p : Program,
+    reliableVisibility : Boolean = true, // Unset this if imports have not yet been set correctly
+    exploreStandalones : Boolean = true  // Unset this if your path already includes standalone object names
+  ) = searchByFullNameRelative(fullName, p, reliableVisibility,exploreStandalones)
+  
+  
+  def searchByFullNameRelative(
+    fullName : String,    
+    base : Definition,
+    reliableVisibility : Boolean = true, // Unset this if imports have not yet been set correctly
+    exploreStandalones : Boolean = true  // Unset this if your path already includes standalone object names
+  ) : Option[Definition] = {
+  
+    val fullNameList = fullName.split("\\.").toList map scala.reflect.NameTransformer.encode
+    require(!fullNameList.isEmpty)
+    
+    def onCondition[A](cond:Boolean)(body : => Option[A]) : Option[A] = {
+      if (cond) body else None
+    }
+    
+    // Find a definition by full name, starting from an another definition
+    def descendDefs (df : Definition, path : List[String]) : Option[Definition] = { 
+      path match {
+        case Nil => Some(df)
+        case hd :: tl =>
+          // ignore UnitDefs
+          val subs = df match {
+            case p : Program => p.modules
+            case _ => df.subDefinitions
+          }          
+          for (
+            nested <- subs find {_.id.toString == hd}; 
+            df <- descendDefs(nested, tl) 
+          ) yield df
+      }
+    }
+    
+    // First, try to find your way from the visible packages from this def
+    // ignoring package nonsense.
+    // Skip if unreliable visibility.
+    ( for ( 
+      startingPoint <- {
+        onCondition (reliableVisibility) {
+          val visible = visibleDefsFrom(base).toList
+          val defs : List[Definition] = 
+            if(exploreStandalones) 
+              visible ++ (visible.collect{ case ModuleDef(_,subs,true) => subs }.flatten)
+            else visible
+          defs find { _.id.toString == fullNameList.head }
+        }
+      };
+      path = fullNameList.tail;
+      df <- descendDefs(startingPoint,path) 
+    ) yield df ) orElse {
+      
+      // Now starts the package nonsense
+      def isPrefixOf[A](pre : List[A],l : List[A]) : Boolean = (pre,l) match {
+        case (Nil, _) => true
+        case (hp :: tp, hl :: tl) if hp == hl => isPrefixOf(tp,tl)
+        case _ => false
+      }
+
+      val program = inProgram(base)
+      val currentPack = inPackage(base)
+      val knownPacks = program.units map { _.pack }
+      // The correct package has the maximum identifiers
+    
+      // First try to find a correct subpackage of this package
+      val subPacks = knownPacks collect { 
+        case p if isSuperPackageOf(currentPack, p) =>
+          p drop currentPack.length
+      }
+      
+      import scala.util.Try
+      val (packagePart, objectPart) = Try {
+        // Find the longest match, then re-attach the current package.
+        val pack = subPacks filter { isPrefixOf(_,fullNameList) } maxBy(_.length)
+        ( currentPack ++ pack, fullNameList drop pack.length )
+      } orElse { Try {
+        // In this case, try to find a package that fits beginning from the root package
+        val pack = knownPacks filter { isPrefixOf(_,fullNameList) } maxBy(_.length)
+        (pack, fullNameList drop pack.length)
+      }} getOrElse {
+        // No package matches
+        (Nil, fullNameList)
+      }
+      
+      assert(!objectPart.isEmpty)     
+      
+      val point = program.modules find { mod => 
+        mod.id.toString == objectPart.head && 
+        inPackage(mod)  == packagePart
+      } orElse {
+        onCondition (exploreStandalones) {
+          // Search in standalone objects
+          program.modules.collect {
+            case ModuleDef(_,subDefs,true) => subDefs 
+          }.flatten.find { df =>
+            df.id.toString == objectPart.head && 
+            inPackage(df)  == packagePart 
+          }
+        }
+      }
+  
+      for (
+        startingPoint <- point;
+        path = objectPart.tail;
+        df <- descendDefs(startingPoint,path) 
+      ) yield df
+    }
+    
+  }
+  
+  
   
   import Trees.Expr
   import TreeOps.{preMap, postMap}
-- 
GitLab