diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 1b07c9f9717a2ff7c67f33048e5b1e949f797507..e50d91ffe95c82b005cd069bd14e0b5aead890de 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -7,7 +7,6 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 import purescala.Common._
-import purescala.Symbols._
 
 trait CodeExtraction extends Extractors {
   self: AnalysisComponent =>
@@ -20,93 +19,85 @@ trait CodeExtraction extends Extractors {
     import scala.collection.mutable.HashMap
 
     // register where the symbols where extracted from
-    val symbolDefMap = new HashMap[Symbol,Tree]
+    val symbolDefMap = new HashMap[purescala.Symbols.Symbol,Tree]
 
     def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
       case Some(ex) => ex
-      case None => stopIfErrors; throw new Error("unreachable")
+      case None => stopIfErrors; throw new Error("unreachable?")
     }
 
-//    def trav(tree: Tree): Unit = tree match {
-//      case t : Tree if t.symbol != null && t.symbol.hasFlag(symtab.Flags.SYNTHETIC) => {
-//        println("Synth! " + t)
-//      }
-//      case d @ DefDef(mods, name, tparams, vparamss, tpt, body) if !(d.symbol.hasFlag(symtab.Flags.SYNTHETIC) || d.symbol.isConstructor) => {
-//        println("In: " + name)
-//        println(d.symbol)
-//        println(d.mods)
-//          
-//        toPureScala(unit)(body) match {
-//          case Some(t) => println("  the body was extracted as: " + t)
-//          case None => println("  the body could not be extracted. Is it pure Scala?")
-//        }
-//      }
-//      case _ => ;
-//    }
-
-    /** Populates the symbolDefMap and returns the symbol corresponding to
-     * the expected single top-level object. */
-    def extractSymbols: ObjectSymbol = {
-      null
-    }
-
-    def extractObject(name: Identifier, tmpl: Template): ObjectDef = {
-      var funDefs: List[FunDef] = Nil
-      var valDefs: List[ValDef] = Nil
-      var asserts: List[Expr] = Nil
-
-      val tTrees: List[Tree] = tmpl.body
+    /** Populates the symbolDefMap with object and class symbols, and returns
+     * the symbol corresponding to the expected single top-level object. */
+    def extractClassSymbols: purescala.Symbols.ObjectSymbol = {
+      val top = unit.body match {
+        case p @ PackageDef(name, lst) if lst.size == 0 => {
+          unit.error(p.pos, "No top-level definition found.")
+          None
+        }
 
-      println(tTrees)
+        case PackageDef(name, lst) if lst.size > 1 => {
+          unit.error(lst(1).pos, "Too many top-level definitions.")
+          None
+        }
 
-      tTrees.foreach(tree => tree match {
-        case cd @ ClassDef(_, name, tparams, impl) => {
-          println("--- " + name.toString)
-          println(cd.symbol.info)
-          println(cd.symbol.info.parents)
+        case PackageDef(name, lst) => {
+          assert(lst.size == 1)
+          lst(0) match {
+            case ExObjectDef(n, templ) => Some(extractObjectSym(n.toString, templ))
+            case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
+            None
+          }
         }
-        case _ => ;
-      })
+      }
 
-      ObjectDef(name, Nil, Nil)
+      stopIfErrors
+      top.get
     }
 
-    // Extraction of the definitions.
-    val program = unit.body match {
-      case p @ PackageDef(name, lst) if lst.size == 0 => {
-        unit.error(p.pos, "No top-level definition found.")
-        None
-      }
-
-      case PackageDef(name, lst) if lst.size > 1 => {
-        unit.error(lst(1).pos, "Too many top-level definitions.")
-        None
-      }
+    def extractObjectSym(name: Identifier, tmpl: Template): purescala.Symbols.ObjectSymbol = {
+      // we assume that the template actually corresponds to an object
+      // definition. Typically it should have been obtained from the proper
+      // extractor (ExObjectDef)
 
-      case PackageDef(name, lst) => {
-        assert(lst.size == 1)
-        lst(0) match {
-          case ExObjectDef(n, templ) => Some(Program(name.toString, extractObject(n.toString, templ)))
-          case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
-          None
-        }
-      }
-    }
+      var classSyms: List[purescala.Symbols.ClassSymbol] = Nil
+      var objectSyms: List[purescala.Symbols.ObjectSymbol] = Nil
 
-    // Extraction of the expressions.
+      tmpl.body.foreach(tree => tree match {
+        case ExObjectDef(o2, t2) => { objectSyms = extractObjectSym(o2, t2) :: objectSyms }
+        case ExAbstractClass(o2) => ;
+        case _ => ;
+      })
 
-//    (new ForeachTreeTraverser(trav)).traverse(unit.body)
+      val theSym = new purescala.Symbols.ObjectSymbol(name, classSyms.reverse, objectSyms.reverse)
+      // we register the tree associated to the symbol to be able to fill in
+      // the rest later
+      symbolDefMap(theSym) = tmpl
+      theSym
+    }
 
-    // Step-by-step algo:
-    // 1) extract class and object symbols (will already be nested)
-    // 2) extract function and val symbols (can now have a type, since we
+    // Step-by-step:
+    // 1) extract class and object symbols recursively (objects can have
+    //    objects as members)
+    // 2) set parents for classes
+    // 3) extract function and val symbols (can now have a type, since we
     //    have full class hierarchy)
-    // 3) extract val and function bodies (can do it, since we have all
+    // 4) extract val and function bodies (can do it, since we have all
     //    definitions, hence we can resolve all symbols)
 
+    // This extracts the class and object symbols recursively.
+    val topLevelObjSym: purescala.Symbols.ObjectSymbol = extractClassSymbols
+
     stopIfErrors
 
-    program.get
+    val programName: Identifier = unit.body match {
+      case PackageDef(name, _) => name.toString
+      case _ => "<program>"
+    }
+
+    println("Top level sym:")
+    println(topLevelObjSym)
+
+    Program(programName, ObjectDef("Object", Nil, Nil))
   }
 
   /** An exception thrown when non-purescala compatible code is encountered. */
diff --git a/src/funcheck/Extractors.scala b/src/funcheck/Extractors.scala
index 69fe4dec6cbee58317acf6ba3968fa038ece6d19..88f9ef0482ebbec66c12210f5568953b273c1c35 100644
--- a/src/funcheck/Extractors.scala
+++ b/src/funcheck/Extractors.scala
@@ -51,26 +51,30 @@ trait Extractors {
 
     object ExObjectDef {
       /** Matches an object with no type parameters, and regardless of its
-       * visibility. */
+       * visibility. Does not match on the automatically generated companion
+       * 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 && tparams.isEmpty) => Some((name.toString, impl))
+        case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass && tparams.isEmpty && !cd.symbol.hasFlag(symtab.Flags.SYNTHETIC)) => {
+          Some((name.toString, impl))
+        }
         case _ => None
       }
     }
 
     object ExAbstractClass {
-      /** Matches an abstract class with no type parameters, no constructor
-       * arguments, at most one parent class and an empty template. (Does _not_
-       * match such a trait). */
+      /** Matches an abstract class or a trait with no type parameters, no
+       * constrctor args (in the case of a class), no implementation details,
+       * no abstract members. */
       def unapply(cd: ClassDef): Option[(String)] = cd match {
+        case ClassDef(_, name, tparams, impl) if (cd.symbol.isTrait && tparams.isEmpty && impl.body.length == 2) => {
+          println(name + " seems to be a cool trait") 
+          Some(name.toString)
+        }
         case _ => None
       }
     }
 
     object ExCaseClass {
-      /** Matches a case class definition with no type parameters, at most one
-       * parent class and an empty template. */
-
 
     }
 
diff --git a/src/funcheck/purescala/Symbols.scala b/src/funcheck/purescala/Symbols.scala
index c950db3625493d60f94f5d1ad190f2f00a6f0115..42fcc1c4fd2913dc82c1490f0ac4b71552f37ce4 100644
--- a/src/funcheck/purescala/Symbols.scala
+++ b/src/funcheck/purescala/Symbols.scala
@@ -28,25 +28,72 @@ object Symbols {
     def getType = tpe
   }
 
+  // The object and class members have to be known at construction time. The
+  // typed members can be added anytime.
   class ObjectSymbol(
     val id: Identifier,
-    val fields: Seq[VariableSymbol],
-    val functions: Seq[FunctionSymbol],
     val classes: Seq[ClassSymbol],
-    val objects: Seq[ObjectSymbol]) extends Symbol
+    val objects: Seq[ObjectSymbol]) extends Symbol {
 
-  sealed abstract class ClassSymbol {
+    private var _fields: List[VariableSymbol] = Nil
+    private var _functions: List[FunctionSymbol] = Nil
+
+    def fields: Seq[VariableSymbol] = _fields
+    def  functions: Seq[FunctionSymbol] = _functions
+
+    def registerField(f: VariableSymbol): ObjectSymbol = {
+      _fields = _fields ::: List(f)
+      this
+    }
+
+    def registerFunction(f: FunctionSymbol): ObjectSymbol = {
+      _functions = _functions ::: List(f)
+      this
+    }
+
+    override def toString: String = withInc(0)
+
+    private def withInc(inc: Int): String = {
+      val ii: String = "    " * inc
+      ii + "[object: " + id + "\n" +
+      (if(!fields.isEmpty) {
+        ii + " fields: " + fields.map(_.toString).mkString("{ ", ", ", " }") + "\n"
+      } else { "" }) +
+      (if(!functions.isEmpty) {
+        ii + " functions: " + functions.map(_.toString).mkString("{ ", ", ", " }") + "\n"
+      } else { "" }) +
+      (if(!classes.isEmpty) {
+        ii + " classes: " + classes.map(_.toString).mkString("{ ", ", ", " }") + "\n" 
+      } else { "" }) +
+      (if(!objects.isEmpty) {
+        ii + " objects: " + objects.map(_.withInc(inc+1)).mkString("{\n", ",\n", "\n" + ii + " }") + "\n"
+      } else { "" }) +
+      ii + "]"
+    }
+  }
+
+  sealed abstract class ClassSymbol extends Symbol {
     val parents: Seq[AbstractClassSymbol]
+
+    protected val _pfx: String
+
+    override def toString = "[" + _pfx + ": " + id + (if (!parents.isEmpty) { " extends " + parents.mkString(", ") } else { "" }) + "]"
   }
 
   /** Symbols for abstract classes (or traits) */
-  class AbstractClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol
+  class AbstractClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol {
+    override protected val _pfx = "abstract class"
+  }
 
   /** Symbols for "regular" (= non-abstract, non-case) classes */
-  class RefClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol
+  class RefClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol {
+    override protected val _pfx = "class"
+  }
 
   /** Symbols for case classes. */
-  class CaseClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol
+  class CaseClassSymbol(val id: Identifier, val parents: Seq[AbstractClassSymbol]) extends ClassSymbol {
+    override protected val _pfx = "case class"
+  }
 
   class FunctionSymbol(val id: Identifier, val params: Seq[VariableSymbol], val returnType: TypeTree) extends Typed {
     def getType = returnType