From f40b49c77dda7783aa4a3ea72515dca780eb8e6f Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Wed, 19 Mar 2014 18:33:05 +0100
Subject: [PATCH] Extract all standalone defs into one module

---
 .../frontends/scalac/CodeExtraction.scala     | 80 ++++++++++---------
 1 file changed, 42 insertions(+), 38 deletions(-)

diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index e34b95c9b..149e91bd4 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -173,44 +173,48 @@ trait CodeExtraction extends ASTExtractors {
 
     def extractModules: List[LeonModuleDef] = {
       try {
-        val templates: List[(String, List[Tree])] = units.reverse.flatMap { u => u.body match {
-          case PackageDef(name, lst) =>
-            var standaloneDefs = List[Tree]()
-
-            val modules: List[(String, List[Tree])] = lst.flatMap { _ match {
-              case t if isIgnored(t.symbol) =>
-                None
-
-              case PackageDef(_, List(ExObjectDef(n, templ))) =>
-                Some((n.toString, templ.body))
-
-              case ExObjectDef(n, templ) =>
-                Some((n.toString, 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
-            }}.toList
-
-            val extraModules: List[(String, List[Tree])] = if (standaloneDefs.isEmpty) {
-              Nil
-            } else {
-              List(("standalone", standaloneDefs.reverse))
-            }
-
-            modules ++ extraModules
-        }}
+        val templates: List[(String, List[Tree])] = {
+          
+          var standaloneDefs = List[Tree]()
+          
+          val modules = units.reverse.flatMap { u => u.body match {
+        
+            case PackageDef(name, lst) =>
+  
+              lst.flatMap { _ match {
+                
+                case t if isIgnored(t.symbol) =>
+                  None
+   
+                case PackageDef(_, List(ExObjectDef(n, templ))) =>
+                  Some((n.toString, templ.body))
+
+                case ExObjectDef(n, templ) =>
+                  Some((n.toString, 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
+              }}.toList
+  
+          }}
+          
+          
+          // Combine all standalone definitions into one module
+          if (standaloneDefs.isEmpty) modules
+          else modules :+  ("standalone$", standaloneDefs.reverse) 
+        }
 
         // Phase 1, we detect classes/types
         templates.foreach{ case (name, templ) => collectClassSymbols(templ) }
-- 
GitLab