diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index 44bb5ba95cd3e6c489ea380812744a9f2858f40c..84eed0db062e084948b6a45beb6b3750869373d6 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/src/funcheck/AnalysisComponent.scala
@@ -2,10 +2,11 @@ package funcheck
 
 import scala.tools.nsc._
 import scala.tools.nsc.plugins._
+import scalacheck._	
 
 class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin) extends PluginComponent
   with CodeExtraction
-  with ForallInjection
+  with ScalaCheckIntegrator[AnalysisComponent]
 {
   import global._
 
@@ -15,6 +16,9 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
 
   val phaseName = pluginInstance.name
 
+  /** this is initialized when the Funcheck phase starts*/
+  override var fresh: scala.tools.nsc.util.FreshNameCreator = null 
+  
   protected def stopIfErrors: Unit = {
     if(reporter.hasErrors) {
       println("There were errors.")
@@ -26,22 +30,28 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
 
   class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
     def apply(unit: CompilationUnit): Unit = {
+      //global ref to freshName creator
+      fresh = unit.fresh
+      
       // That filter just helps getting meaningful errors before the attempt to
       // extract the code, but it's really optional.
       (new ForeachTreeTraverser(firstFilter(unit))).traverse(unit.body)
       stopIfErrors
 
-      val prog: purescala.Definitions.Program = extractCode(unit)
-      println("Extracted program for " + unit + ": ")
-      println(prog)
+//      val prog: purescala.Definitions.Program = extractCode(unit)
+//      println("Extracted program for " + unit + ": ")
+//      println(prog)
 
       // Mirco your component can do its job here, as I leave the trees
       // unmodified.
+      val (genDef, arbDef) = createGeneratorDefDefs(unit)
+    
+      transform(genDef ::: arbDef, unit)
 
-      if(pluginInstance.stopAfterAnalysis) {
-        println("Analysis complete. Now terminating the compiler process.")
-        exit(0)
-      }
+//      if(pluginInstance.stopAfterAnalysis) {
+//        println("Analysis complete. Now terminating the compiler process.")
+//        exit(0)
+//      }
     }
 
     /** Weeds out some programs containing unsupported features. */
@@ -64,4 +74,7 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
       }
     }
   }
+  
+  
+  
 }
diff --git a/src/funcheck/scalacheck/FilterGeneratorAnnotations.scala b/src/funcheck/scalacheck/FilterGeneratorAnnotations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..00748c5dc781faea830c3b784c7e1d3f8da9cdf2
--- /dev/null
+++ b/src/funcheck/scalacheck/FilterGeneratorAnnotations.scala
@@ -0,0 +1,62 @@
+package funcheck.scalacheck
+
+import scala.tools.nsc.{Global, SubComponent}
+
+/** 
+ * A tree traverser which filter the trees elements that contain the 
+ * <code>@generator</code> annotation, defined in <code>funcheck.lib.Specs</code> 
+ * module.  
+ * 
+ * Note: For the moment this is working only for <code>ClassDef</code> and 
+ * <code>DefDef</code> tree elements.  
+ *  
+ * This trait is meant to be used with the <code>FilterTreeTraverser</code> 
+ * class, available in the <code>scala.tools.nsc.ast.Trees</code> trait. 
+ * 
+ * 
+ * Usage Example:
+ * 
+ * new FilterTreeTraverser(filterTreesWithGeneratorAnnotation(unit))
+ * 
+ * where <code>unit</code> is the current Compilation Unit.
+ */
+trait FilterGeneratorAnnotations[T <: SubComponent] { self: T =>
+  // [[INFO]] "hasAttribute" is "hasAnnotation" in future compiler release 2.8
+  import global._
+  
+  /** Funcheck <code>@generator</code> annotation. */
+  private lazy val generator: Symbol = definitions.getClass("funcheck.lib.Specs.generator")
+  
+  
+  /**
+   * Check for <code>@generator</code> annotation only for class and method 
+   * definitions. A class is considered to be annotated if either the class itself 
+   * has the annotation, or if the class inherit from an annotated abstract class.
+   */
+  def filterTreesWithGeneratorAnnotation(Unit: CompilationUnit)(tree: Tree): Boolean = {
+    lazy val sym = tree.symbol
+    tree match {
+      case cd: ClassDef => sym.hasAttribute(generator) || abstractSuperClassHasGeneratorAnnotation(sym.superClass)
+      case d: DefDef    => sym.hasAttribute(generator)
+      case _ => false
+    }
+  }
+  
+  
+  /** Return true if the class (or superclass) symbol is flagged as being ABSTRACT and contains 
+   * the <code>@generator</code> annotation.*/
+  private def abstractSuperClassHasGeneratorAnnotation(superclass: Symbol): Boolean = { 
+    //require(superclass.isInstanceOf[ClassSymbol], "expected ClassSymbol, found "+superclass)
+    superclass match {
+      case NoSymbol => false
+      case cs: ClassSymbol =>
+        (cs.hasFlag(scala.tools.nsc.symtab.Flags.ABSTRACT) &&  
+           cs.hasAttribute(generator)) || 
+          abstractSuperClassHasGeneratorAnnotation(cs.superClass)
+      case _ => 
+        assert(false, "expected ClassSymbol, found "+superclass)
+        false
+    }
+    
+  }
+}
diff --git a/src/funcheck/scalacheck/GeneratorDefDefInjector.scala b/src/funcheck/scalacheck/GeneratorDefDefInjector.scala
new file mode 100644
index 0000000000000000000000000000000000000000..516d814d561090400701bf614581f002e0ced780
--- /dev/null
+++ b/src/funcheck/scalacheck/GeneratorDefDefInjector.scala
@@ -0,0 +1,87 @@
+package funcheck.scalacheck
+
+import scala.tools.nsc.{Global, SubComponent}
+import scala.tools.nsc.transform.TypingTransformers
+
+trait GeneratorDefDefInjector[T <: SubComponent] extends TypingTransformers { self: T =>
+   import global._
+  
+  def transform(injecting: List[DefDef], unit: CompilationUnit): Unit = 
+    unit.body = new GenDefDefTransformer(injecting, unit).transform(unit.body)
+  
+  class GenDefDefTransformer(injecting: List[DefDef], unit: CompilationUnit) 
+    extends /*Code Injection*/ TypingTransformer(unit) 
+  { 
+    override def transform(tree: Tree): Tree = { 
+      curTree = tree
+      tree match {
+        
+        case impl @ Template(parents, self, body) => 
+          atOwner(currentOwner) {
+       	    val newBody: List[Tree] = body ::: (injecting.map(localTyper.typed(_)))  
+            val cd = copy.Template(impl, parents, self, newBody)
+            cd
+          }
+         
+        /** Delegates the recursive traversal of the tree. */
+       	case _ => super.transform(tree)
+      }
+    }
+       
+  }
+} 
+    
+    
+//    val cdSym = c.symbol
+//         if(cdSym.hasFlag(ABSTRACT)) { 
+//           DefGenerator.addAbstr(c)
+//           println(cdSym.children)
+//         }
+//         else {
+//           val Template(_, _, body) = impl
+//           for { b <- body } b match {
+//             case d @ DefDef(_, nme.CONSTRUCTOR, _, _, _, _) =>
+//               DefGenerator.addDef(d)
+//             case _ => ;
+//           }
+//         }
+  
+  
+   
+   //   lazy val specsModule: Symbol = definitions.getModule("funcheck.lib.Specs")
+   //val neededGenerators = scala.collection.mutable.Set.empty[Symbol]
+   
+   
+   /*********************************************************************************/
+//   private def isForall(s: Select): Boolean = {
+//     val Select(selector,_) = s
+//     
+//     selector.symbol == specsModule &&
+//     s.symbol == specsModule.tpe.decl("forAll")
+//   }
+//   
+//    
+//   /*********************************************************************************/
+//   def collectProperties(Unit: CompilationUnit)(tree: Tree): Unit = tree match {
+//     case TypeApply( s: Select, tpes: List[Tree]) =>
+//       if(isForall(s)) {
+//         for { treeTpe <- tpes } treeTpe.tpe match {
+//           case TypeRef(_, _, args: List[Type]) => 
+//             for {arg <- args} arg match {
+//               case TypeRef(_,sym,_) => {
+//                 //generators are needed only for user-defined types (assuming Pure Scala as input language)   
+//                 if (!definitions.isValueClass(sym)) 
+//                   neededGenerators += sym
+//               }
+//               case _ => error("Don't know what to do with "+ arg)
+//             }
+//           case _ => error("don't know what to do with " + treeTpe + " with associated symbol: "+treeTpe.symbol)
+//         }
+//         //println(neededGenerators)
+//       } 
+//       
+//     case _ =>
+//   }
+   
+   
+ 
diff --git a/src/funcheck/scalacheck/ScalaCheck.scala b/src/funcheck/scalacheck/ScalaCheck.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bae8bd0ee21f04215ec6048b97f377c0f4dd07f2
--- /dev/null
+++ b/src/funcheck/scalacheck/ScalaCheck.scala
@@ -0,0 +1,257 @@
+package funcheck.scalacheck
+
+import scala.tools.nsc.{Global, SubComponent}
+
+/**
+ * Utilitarity class that is used as a factory for creating Tree nodes for method 
+ * calls of classes and modules in the <code>org.scalacheck</code> package. 
+ */
+trait ScalaCheck[T <: SubComponent] {self: T =>
+  import global._
+  
+  
+  /** Transform string name in method symbols from the <code>symDecl</code> 
+    * class symbol. */
+  private def symDecl(sym: Symbol, name: String) = sym.tpe.decl(name)
+  
+  /** Retrieve the constructor Symbol for the passed <code>cs</code> class symbol. */
+  private def constructorDecl(cs: ClassSymbol) = cs.tpe.decl(nme.CONSTRUCTOR)
+  
+  /** Module for creating scalac Tree nodes for calling methods of the 
+   * <code>org.scalacheck.Gen</code> class and module.*/
+  trait Gen {
+  
+    /** Symbol for the <code>org.scalacheck.Gen</code> module definition. */
+    private lazy val moduleGenSym = definitions.getModule("org.scalacheck.Gen")
+    
+    /** Symbol for the <code>org.scalacheck.Gen</code> class definition. */
+    private lazy val classGenSym = moduleGenSym.linkedClassOfModule                  
+  
+  
+    /**
+     * Apply <code>polyTpe</code> to the polymorphic type <code>org.scalacheck.Gen</code>.
+     * 
+     * @param polyTpe the type to be applied to <code>org.scalacheck.Gen</code>.
+     * @return The polymorphic type resulting from applying <code>polyTpe</code> 
+     *         to the polymorphic type <code>org.scalacheck.Gen</code>, i.e., 
+     *         <code>Gen[polyTpe]</code>.
+     */
+    private def applyType(polyTpe: Type) = appliedType(classGenSym.tpe, List(polyTpe))
+    
+    
+    /**
+     * This creates a Tree node for the call <code>org.scalacheck.Gen.value[T](rhs)</code>, 
+     * where the polymorphic type <code>T</code> will be inferred during the next 
+     * typer phase (this usually means that the typer has to be called explictly, 
+     * so it is the developer duty to ensure that this happen at some point).
+     */
+    def value(rhs: Tree): Tree =
+      Apply(Select(Ident(moduleGenSym), symDecl(moduleGenSym, "value")), List(rhs))
+    
+    
+    /**
+     * This creates a Tree node for the call <code>org.scalacheck.Gen.oneOf[T](generators)</code>, 
+     * where the polymorphic type <code>T</code> will be inferred during the next 
+     * typer phase (this usually means that the typer has to be called explictly, 
+     * so it is the developer duty to ensure that this happen at some point).
+     */
+    def oneOf(generators: List[Symbol]): Tree = 
+      Apply(Select(Ident(moduleGenSym), symDecl(moduleGenSym, "oneOf")), generators.map(Ident(_)))
+    
+    
+    /**
+     * This creates a Tree node for the call <code>org.scalacheck.Gen.flatMap[T](body)</code>, 
+     * where the polymorphic type <code>T</code> will be inferred during the next 
+     * typer phase (this usually means that the typer has to be called explictly, 
+     * so it is the developer duty to ensure that this happen at some point).
+     */
+    def flatMap(qualifier: Tree, body: Tree): Tree = 
+      Apply(Select(qualifier, symDecl(classGenSym, "flatMap")),List(body))
+     
+    
+    /**
+     * This creates a Tree node for the call <code>org.scalacheck.Gen.map[T](rhs)</code>, 
+     * where the polymorphic type <code>T</code> will be inferred during the next 
+     * typer phase (this usually means that the typer has to be called explictly, 
+     * so it is the developer duty to ensure that this happen at some point).
+     */
+    def map(qualifier: Tree, body: Tree): Tree = 
+      Apply(Select(qualifier, symDecl(classGenSym, "map")), List(body))
+     
+    /**
+     * Utilitary method for creating a method symbol for a <code>org.scalacheck.Gen</codee>
+     * generator method. 
+     * 
+     * @param owner   The owner of the method (DefDef) which will use the returned method symbol.
+     * @param genName The name of the method symbol (which will also be the name of the method).
+     * @param retTpe  The method's returning type.
+     * @return The method symbol for a generator method.
+     */
+    def createGenDefSymbol(owner: Symbol, genName: String, retTpe: Type): Symbol = {
+      // returning type of the new method, i.e., Gen["retTpe"]
+      val genDefRetTpe = applyType(retTpe)
+      
+      // create a symbol for the generator method that will be created next
+      owner.newMethod(owner.pos,genName).setInfo(PolyType(List(), genDefRetTpe))
+    }
+    
+    
+    
+   
+    
+//    def buildGenDefDef(cd: ClassDef, genDefSym: Symbol): DefDef = {
+//      val constructorSym = constructorDecl(cd.symbol.asInstanceOf[ClassSymbol])
+//      val paramss = constructorSym.typeParams
+//       
+//      assert(paramss.size <= 1, "currying is not supported. Change signature of "+constructorSym)
+//      
+//      
+//      if(cd.symbol.hasFlag(scala.tools.nsc.symtab.Flags.ABSTRACT)) {
+//        val generators = constructorSym.children.toList.map(s => genForTpe(s.tpe)).flatMap(v=>v)
+//        DefDef(genDefSym, Modifiers(0), List(), Gen.oneOf(generators))
+//      } 
+//      else {
+//        
+//        val constrObj = resetAttrs(d.tpt.duplicate)
+//        val instance = Select(New(constrObj), nme.CONSTRUCTOR)
+//        
+//        if(paramss.isEmpty) {
+//          DefDef(genDefSym, Modifiers(0), List(), Gen.value(Apply(instance, Nil)))
+//        } 
+//        else {
+//          //should use Tree.duplicate instead!!
+//          val body = rhsGenDef(instance)(d)(genDef)
+//        
+//          DefDef(genDef, Modifiers(0), List(), body)
+//        }
+//      }
+//    }
+    
+  }
+  
+  
+  
+  /** Module for creating scalac Tree nodes for calling methods of the 
+   * <code>org.scalacheck.Arbitrary</code> class and module.*/
+  trait Arbitrary {
+   
+    /** Symbol for the <code>org.scalacheck.Arbitrary</code> module definition. */
+    private val moduleArbitrarySym = definitions.getModule("org.scalacheck.Arbitrary")
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary</code> class definition. */
+    private val classArbitrarySym = moduleArbitrarySym.linkedClassOfModule 
+    
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbInt</code> method definition. */
+    private val arbInt          =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbInt"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbBool</code> method definition. */
+    private val arbBool         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbBool"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbLong</code> method definition. */
+    private val arbLong         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbLong"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbThrowable</code> method definition. */
+    private val arbThrowable    =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbThrowable"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbDouble</code> method definition. */
+    private val arbDouble       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbDouble"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbChar</code> method definition. */
+    private val arbChar         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbChar"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbString</code> method definition. */
+    private val arbString       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbString"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbOption</code> method definition. */
+    private val arbOption       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbOption"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbImmutableMap</code> method definition. */
+    private val arbImmutableMap =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbImmutableMap"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbList</code> method definition. */
+    private val arbList         =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbList"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbSet</code> method definition. */
+    private val arbSet          =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbSet"))
+    
+    /** Symbol for the <code>org.scalacheck.Arbitrary.arbTuple2</code> method definition. */
+    private val arbTuple2       =  Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbTuple2"))
+    
+    //[[TODO]]
+    //lazy val arbMultiSet       =  Select(Ident(arbitraryModule), arbitraryModule.tpe.decl("arbMultiSet"))
+    
+    
+    
+    /** Map that stores <code>org.scalacheck.Arbitrary.arbitrary[Type]</code> calls. */
+    protected val tpe2arbApp    = scala.collection.mutable.Map.empty[Type,Apply]
+    
+    // initialize map with ScalaCheck built-in types that are part of our PureScala language
+    tpe2arbApp += definitions.IntClass.typeConstructor       -> applyArbitrary(arbInt)
+    tpe2arbApp += definitions.BooleanClass.typeConstructor   -> applyArbitrary(arbBool)
+    tpe2arbApp += definitions.LongClass.typeConstructor      -> applyArbitrary(arbLong)
+    tpe2arbApp += definitions.ThrowableClass.typeConstructor -> applyArbitrary(arbThrowable)
+    tpe2arbApp += definitions.DoubleClass.typeConstructor    -> applyArbitrary(arbDouble)
+    tpe2arbApp += definitions.CharClass.typeConstructor      -> applyArbitrary(arbChar)
+    tpe2arbApp += definitions.StringClass.typeConstructor    -> applyArbitrary(arbString)
+    
+    /**
+     * Apply <code>polyTpe</code> to the polymorphic type <code>org.scalacheck.Arbitrary</code>.
+     * 
+     * @param polyTpe the type to be applied to <code>org.scalacheck.Arbitrary</code>.
+     * @return The polymorphic type resulting from applying <code>polyTpe</code> 
+     *         to the polymorphic type <code>org.scalacheck.Arbitrary</code>, i.e., 
+     *         <code>Arbitrary[polyTpe]</code>.
+     */
+    private def applyType(tpe: Type) = appliedType(classArbitrarySym.tpe, List(tpe))
+    
+    /**
+     * Creates a Tree node for the call <code>org.scalacheck.Arbitrary.apply[T](generator)</code>, 
+     * where the polymorphic type <code>T</code> will be inferred during the next 
+     * typer phase (this usually means that the typer has to be called explictly, 
+     * so it is the developer duty to ensure that this happen at some point).
+     */
+    def apply(generator: Tree): Tree = 
+      Apply(Select(Ident(moduleArbitrarySym),symDecl(moduleArbitrarySym, "apply")), List(generator))
+    
+    /**
+     * 
+     */
+    def arbitrary(polyTpe: TypeTree): Apply = {
+      val symbol = polyTpe.symbol
+      val tpe = symbol.tpe
+      tpe2arbApp.get(tpe) match {
+        case Some(appliedArbitrary) => appliedArbitrary
+        case None => arbitrary(symbol)
+      }
+    }
+    
+    protected def arbitrary(tpeSym: Symbol): Apply 
+    
+                                  
+    protected def applyArbitrary(param: Tree): Apply =
+      Apply(Select(Ident(moduleArbitrarySym), symDecl(moduleArbitrarySym, "arbitrary")), List(param))
+    
+    
+    /**
+     * Utilitary method for creating a method symbol for a <code>org.scalacheck.Arbitrary</codee>
+     * generator method. 
+     * 
+     * @param owner   The owner of the method (DefDef) which will use the returned method symbol.
+     * @param arbName The name of the method symbol (which will also be the name of the method).
+     * @param retTpe  The method's returning type.
+     * @return The method symbol for a generator method.
+     */
+    def createArbitraryDefSymbol(owner: Symbol, arbName: String, retTpe: Type): Symbol = {
+      // returning type of the new method, i.e., Arbitrary["retTpe"]
+      val arbRetTpe = applyType(retTpe)
+      
+      // Create the DefDef for the new Arbitrary object
+      val arbDef = owner.newMethod(owner.pos, arbName).setInfo(PolyType(List(), arbRetTpe))
+      // Implicit only because of ScalaCheck rational (not really needed since we are injecting code)
+      arbDef.setFlag(scala.tools.nsc.symtab.Flags.IMPLICIT)
+      
+      arbDef
+    }
+  }
+}
diff --git a/src/funcheck/scalacheck/ScalaCheckIntegrator.scala b/src/funcheck/scalacheck/ScalaCheckIntegrator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..27e4df13f3751907e385bde1839531b8208140f1
--- /dev/null
+++ b/src/funcheck/scalacheck/ScalaCheckIntegrator.scala
@@ -0,0 +1,224 @@
+package funcheck.scalacheck
+
+import scala.tools.nsc.{Global, SubComponent}
+import funcheck.util.FreshNameCreator
+
+trait ScalaCheckIntegrator[T <: SubComponent] extends ScalaCheck[T] 
+  with FilterGeneratorAnnotations[T]
+  with GeneratorDefDefInjector[T]
+  with FreshNameCreator 
+{
+  self: T =>
+  import global._
+  
+  
+  def createGeneratorDefDefs(unit: CompilationUnit): (List[DefDef], List[DefDef]) = {
+    val filteredGenTree = new FilterTreeTraverser(filterTreesWithGeneratorAnnotation(unit))
+    filteredGenTree.traverse(unit.body)
+    
+    val klasses = collection.mutable.Set.empty[ClassDef]
+    val defs = collection.mutable.Set.empty[DefDef]
+    
+    for {tree <- filteredGenTree.hits} tree match {
+      case c: ClassDef => klasses + c
+      case d: DefDef => defs + d
+    }  
+    
+    (Gen.createGenDefDef(klasses.toList,defs.toList), Arbitrary.getArbitraryDefDefs)
+  }
+  
+  object Gen extends Gen {
+    /** 
+     * Map that stores for each @generator annotated ClassDef or DefDef the automatically  
+     * generated DefDef for creating instances of the <code>org.scalacheck.Gen</code> class.
+     * The <code>Type</code> that is associated to the DefDef is either the type of the 
+     * ClassDef or the returning type of the DefDef.
+     */
+    private val tpe2listGen = scala.collection.mutable.Map.empty[Type, List[DefDef]]
+    private val tpe2listGenSym = scala.collection.mutable.Map.empty[Type, List[Symbol]]
+    
+     /** 
+     * Add the <code>gen</code> generator DefDef declaration to the list of 
+     * generators for <code>tpe</code>.
+     * 
+     * @param tpe The type of elements generated by the <code>gen</code>.
+     * @param gen The DefDef declaration for the generator method.
+     */
+    def +[T](map: collection.mutable.Map[Type, List[T]], key: Type, value: T): Unit = map.get(key) match {
+      case None         => map += key -> List(value)
+      case Some(values) => map += key -> (value :: values)
+    }
+   
+    /** List of generator DefDef symbols for a given type <code>tpe</code>*/
+    def genSymbolsForType(tpe: Type): List[Symbol] = tpe2listGenSym.get(tpe) match {
+      case None => Nil
+      case Some(symbols) => symbols
+    } 
+    
+    /** 
+     * Second Pass: Create symbols for the generator DefDef that will be created
+     * durind the Third Pass.
+     */
+    def createGenDefDef(klasses: List[ClassDef], defs: List[DefDef]): List[DefDef] = {
+      val generable: List[(Symbol,Tree)] = createGenDefSyms(klasses, defs)
+      
+      for { (genSym, genTree) <- generable } genTree match {
+        case cd: ClassDef => 
+          val tpe = cd.symbol.tpe
+          Gen + (tpe2listGen, tpe, Gen.createGenDef(cd, genSym))
+        
+        case d: DefDef =>
+          val tpe = d.tpt.symbol.tpe
+          val generated = DefDef(genSym, Modifiers(0), List(), rhsGenDef(Ident(d.name))(d)(genSym))
+          Gen + (tpe2listGen, tpe, generated)
+      }
+      
+      // flatten into single list values of Gen.tpe2listGen
+      (List[DefDef]() /: Gen.tpe2listGen.values) {
+        case (xs, xss) => xs ::: xss
+      }
+    }
+    
+    
+    /** 
+     * Create method symbols for each <code>@generator</code> annotated ClassDef
+     * and DefDef.
+     */
+    private def createGenDefSyms(klasses: List[ClassDef], defs: List[DefDef]): List[(Symbol, Tree)] = {
+    
+      val genKlasses: List[(Symbol, ClassDef)] = for(klass <- klasses) yield {
+        val genName = fresh.newName("gen"+klass.name)
+        val tpe = klass.symbol.tpe
+        val genSym = createGenDefSymbol(klass.symbol.enclClass.owner, genName, tpe)
+        
+        Gen + (tpe2listGenSym, tpe, genSym)
+        
+        (genSym, klass)
+      }
+    
+      val genDefs: List[(Symbol, DefDef)] = for(d <- defs) yield {
+        val genName = fresh.newName("gen"+d.name)
+        val tpe = d.tpt.symbol.tpe
+        val genSym = createGenDefSymbol(d.symbol.owner, genName, tpe)
+        
+        Gen + (tpe2listGenSym, tpe, genSym)
+        
+        (genSym, d)
+      }
+    
+      genKlasses ::: genDefs
+    }
+    
+    
+    
+    def createGenDef(cd: ClassDef, genDef: Symbol): DefDef = {
+      val d: DefDef = getConstructorOf(cd)
+      val DefDef(_,_,_,vparamss,retTpe,_) = d 
+      assert(vparamss.size <= 1, "currying is not supported. Change signature of "+cd.symbol)
+      
+      
+      if(cd.symbol.hasFlag(scala.tools.nsc.symtab.Flags.ABSTRACT)) {
+        val generators = retTpe.symbol.children.toList.map(s => genSymbolsForType(s.tpe)).flatMap(v=>v)
+        DefDef(genDef, Modifiers(0), List(), Gen.oneOf(generators))
+      } 
+      else {
+        
+        val constrObj = resetAttrs(d.tpt.duplicate)
+        val instance = Select(New(constrObj), nme.CONSTRUCTOR)
+        
+        assert(d.tpt.isInstanceOf[TypeTree])
+        
+        val body = rhsGenDef(instance)(d)(genDef)
+        DefDef(genDef, Modifiers(0), List(), body)
+      }
+    }
+    
+    
+     /** <code>base</code> is either 
+     *       - Select(New(tpe),constructor) [constructor] 
+     *       - Ident(name)   [method call]
+     */
+    private def rhsGenDef(base: Tree)(d: DefDef)(extOwner: Symbol): Tree = {
+      val DefDef(_,name,_,vparamss,retTpe,_) = d
+      assert(vparamss.size <= 1, "currying is not supported. Change signature of "+d.symbol)
+      
+      if(vparamss.head.isEmpty)
+        Gen.value(Apply(base, Nil))
+      
+      else {
+        var owner = extOwner
+      
+        val paramssTpe: List[ValDef] = vparamss.flatMap(v=>v).map(p => 
+          ValDef(Modifiers(0), fresh.newName("v"), resetAttrs(p.tpt.duplicate), EmptyTree))
+      
+      
+        var last = true
+      
+      
+        val z :Tree = Apply(base, paramssTpe.map(p => Ident(p.name)))
+        val body = (paramssTpe :\ z) {
+          case (param,apply) => {
+            val body = Function(List(param), apply)
+            body.symbol.owner = owner
+            owner = body.symbol
+            //XXX: it is not flatMap in general. fix this!!
+            if(last) {
+              last = false
+              Gen.map(Arbitrary.arbitrary(param.tpt.asInstanceOf[TypeTree]), body)
+            } else
+              Gen.flatMap(Arbitrary.arbitrary(param.tpt.asInstanceOf[TypeTree]), body)
+          }
+        }
+      
+        body
+      }
+    }
+   
+    
+    
+    private def getConstructorOf(cd: ClassDef): DefDef = {
+      val Template(parents, self, body) = cd.impl
+      var dd: DefDef  = null
+      for { b <- body } b match {
+        case d @ DefDef(_, nme.CONSTRUCTOR, _, _, _, _) => dd = d
+        case _ => ;
+      }
+      dd
+    } ensuring (res => res != null)
+
+  }
+  
+  
+  object Arbitrary extends Arbitrary {
+    
+    /** Map that stores not built-in <code>org.scalacheck.Arbitrary</code> DefDef definitions. */
+    private val tpe2arbDefDef = scala.collection.mutable.Map.empty[Type,DefDef]
+    
+    def getArbitraryDefDefs: List[DefDef] = tpe2arbDefDef.values.toList
+    
+    override protected def arbitrary(tpeSym: Symbol): Apply = {
+      require(tpe2arbApp.get(tpeSym.tpe).isEmpty, "Arbitrary.arbitrary["+tpeSym.tpe+"] is already in the map")
+      
+      val owner = tpeSym.toplevelClass
+      val arbName = fresh.newName("arb"+tpeSym.name)
+      val tpe = tpeSym.tpe
+      
+      val arbDef = createArbitraryDefSymbol(owner, arbName, tpe)
+      
+            
+      val genNames = Gen.genSymbolsForType(tpe)
+      
+      
+      val generated = DefDef(arbDef, Modifiers(0), List(), Arbitrary(Gen.oneOf(genNames)))
+      tpe2arbDefDef += tpe -> generated  
+      
+      val result = applyArbitrary(Ident(arbDef))
+      tpe2arbApp += tpe -> result
+        
+      result
+            
+    }
+    
+    
+  }
+}
diff --git a/src/funcheck/util/FreshNameCreator.scala b/src/funcheck/util/FreshNameCreator.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b5115b77b0c8c0fbf64339c3e6e2fe0371e6171b
--- /dev/null
+++ b/src/funcheck/util/FreshNameCreator.scala
@@ -0,0 +1,6 @@
+package funcheck.util
+
+
+trait FreshNameCreator {
+  var fresh: scala.tools.nsc.util.FreshNameCreator
+}