getting somewhere, slowly. Starting to have functions extracted.

src/funcheck/AnalysisComponent.scala

@@ -37,8 +37,8 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
       
       // 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
+      // (new ForeachTreeTraverser(firstFilter(unit))).traverse(unit.body)
+      // stopIfErrors
 
       val prog: purescala.Definitions.Program = extractCode(unit)
       println("Extracted program for " + unit + ": ")
@@ -58,24 +58,24 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
     }
 
     /** Weeds out some programs containing unsupported features. */
-    def firstFilter(unit: CompilationUnit)(tree: Tree): Unit = {
-      def unsup(s: String): String = "FunCheck: Unsupported construct: " + s
+    // def firstFilter(unit: CompilationUnit)(tree: Tree): Unit = {
+    //   def unsup(s: String): String = "FunCheck: Unsupported construct: " + s
 
-      tree match {
-        case ValDef(mods, name, tpt, rhs) if mods.isVariable =>
-          unit.error(tree.pos, unsup("mutable variable/field."))
-        case LabelDef(name, params, rhs) => unit.error(tree.pos, unsup("loop."))
-        case Assign(lhs, rhs) => unit.error(tree.pos, unsup("assignment to mutable variable/field."))
-        case Return(expr) => unit.error(tree.pos, unsup("return statement."))
-        case Try(block, catches, finalizer) => unit.error(tree.pos, unsup("try block."))
-        case SingletonTypeTree(ref) => unit.error(tree.pos, unsup("singleton type."))
-        case SelectFromTypeTree(qualifier, selector) => unit.error(tree.pos, unsup("path-dependent type."))
-        case CompoundTypeTree(templ: Template) => unit.error(tree.pos, unsup("compound/refinement type."))
-        case TypeBoundsTree(lo, hi) => unit.error(tree.pos, unsup("type bounds."))
-        case ExistentialTypeTree(tpt, whereClauses) => unit.error(tree.pos, unsup("existential type."))
-        case _ => ;
-      }
-    }
+    //   tree match {
+    //     case ValDef(mods, name, tpt, rhs) if mods.isVariable =>
+    //       unit.error(tree.pos, unsup("mutable variable/field."))
+    //     case LabelDef(name, params, rhs) => unit.error(tree.pos, unsup("loop."))
+    //     case Assign(lhs, rhs) => unit.error(tree.pos, unsup("assignment to mutable variable/field."))
+    //     case Return(expr) => unit.error(tree.pos, unsup("return statement."))
+    //     case Try(block, catches, finalizer) => unit.error(tree.pos, unsup("try block."))
+    //     case SingletonTypeTree(ref) => unit.error(tree.pos, unsup("singleton type."))
+    //     case SelectFromTypeTree(qualifier, selector) => unit.error(tree.pos, unsup("path-dependent type."))
+    //     case CompoundTypeTree(templ: Template) => unit.error(tree.pos, unsup("compound/refinement type."))
+    //     case TypeBoundsTree(lo, hi) => unit.error(tree.pos, unsup("type bounds."))
+    //     case ExistentialTypeTree(tpt, whereClauses) => unit.error(tree.pos, unsup("existential type."))
+    //     case _ => ;
+    //   }
+    // }
   }
   
   

src/funcheck/CodeExtraction.scala

@@ -12,6 +12,7 @@ trait CodeExtraction extends Extractors {
   self: AnalysisComponent =>
 
   import global._
+  import global.definitions._
   import StructuralExtractors._
   import ExpressionExtractors._
 
@@ -23,12 +24,10 @@ trait CodeExtraction extends Extractors {
 
     def s2ps(tree: Tree): Expr = toPureScala(unit)(tree) match {
       case Some(ex) => ex
-      case None => stopIfErrors; throw new Error("unreachable?")
+      case None => stopIfErrors; scala.Predef.error("unreachable error.")
     }
 
-    /** Populates the symbolDefMap with object and class symbols, and returns
-     * the symbol corresponding to the expected single top-level object. */
-    def extractClassSymbols: ObjectDef = {
+    def extractTopLevelDef: ObjectDef = {
       val top = unit.body match {
         case p @ PackageDef(name, lst) if lst.size == 0 => {
           unit.error(p.pos, "No top-level definition found.")
@@ -43,7 +42,7 @@ trait CodeExtraction extends Extractors {
         case PackageDef(name, lst) => {
           assert(lst.size == 1)
           lst(0) match {
-            case ExObjectDef(n, templ) => Some(extractObjectSym(n.toString, templ))
+            case ExObjectDef(n, templ) => Some(extractObjectDef(n.toString, templ))
             case other @ _ => unit.error(other.pos, "Expected: top-level single object.")
             None
           }
@@ -54,38 +53,40 @@ trait CodeExtraction extends Extractors {
       top.get
     }
 
-    def extractObjectSym(name: Identifier, tmpl: Template): ObjectDef = {
+    def extractObjectDef(name: Identifier, tmpl: Template): ObjectDef = {
       // we assume that the template actually corresponds to an object
       // definition. Typically it should have been obtained from the proper
       // extractor (ExObjectDef)
 
       var classDefs: List[ClassTypeDef] = Nil
-      var objectDefs: List[purescala.Symbols.ObjectSymbol] = Nil
+      var objectDefs: List[ObjectDef] = Nil
+      var funDefs: List[FunDef] = Nil
 
-      tmpl.body.foreach(tree => tree match {
-        case ExObjectDef(o2, t2) => { objectSyms = extractObjectSym(o2, t2) :: objectSyms }
+      tmpl.body.foreach(tree => {
+        println("[[[ " + tree + "]]]\n");
+        tree match {
+        case ExObjectDef(o2, t2) => { objectDefs = extractObjectDef(o2, t2) :: objectDefs }
         case ExAbstractClass(o2) => ;
+        case ExConstructorDef() => ;
+        case ExMainFunctionDef() => ;
+        case ExFunctionDef(n,p,t,b) => { funDefs = extractFunDef(n,p,t,b) :: funDefs }
         case _ => ;
-      })
+      }})
 
       // 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
+      val theDef = new ObjectDef(name, objectDefs.reverse ::: classDefs.reverse ::: funDefs.reverse, Nil)
+      theDef
     }
 
-    // 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)
-    // 4) extract val and function bodies (can do it, since we have all
-    //    definitions, hence we can resolve all symbols)
+    def extractFunDef(name: Identifier, params: Seq[ValDef], tpt: Tree, body: Tree) = {
+      FunDef(name, scalaType2PureScala(unit, false)(tpt), Nil, null, None, None)
+    }
 
-    // This extracts the class and object symbols recursively.
-    val topLevelObjSym: purescala.Symbols.ObjectSymbol = extractClassSymbols
+    // THE EXTRACTION CODE STARTS HERE
+    val topLevelObjDef: ObjectDef = extractTopLevelDef
 
     stopIfErrors
 
@@ -95,9 +96,11 @@ trait CodeExtraction extends Extractors {
     }
 
     println("Top level sym:")
-    println(topLevelObjSym)
+    println(topLevelObjDef)
+
 
-    Program(programName, ObjectDef("Object", Nil, Nil))
+    //Program(programName, ObjectDef("Object", Nil, Nil))
+    Program(programName, topLevelObjDef)
   }
 
   /** An exception thrown when non-purescala compatible code is encountered. */
@@ -130,6 +133,19 @@ trait CodeExtraction extends Extractors {
     }
   }
 
+  private def scalaType2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Tree): funcheck.purescala.TypeTrees.TypeTree = {
+    tree match {
+      case tt: TypeTree if tt.tpe == IntClass.tpe => Int32Type
+
+      case _ => {
+        if(!silent) {
+          unit.error(tree.pos, "Could not extract type as PureScala.")
+        }
+        throw ImpureCodeEncounteredException(tree)
+      }
+    }
+  }
+
 //  def findContracts(tree: Tree): Unit = tree match {
 //    case DefDef(/*mods*/ _, name, /*tparams*/ _, /*vparamss*/ _, /*tpt*/ _, body) => {
 //      var realBody = body

src/funcheck/Extractors.scala

@@ -78,6 +78,23 @@ trait Extractors {
 
     }
 
+    object ExConstructorDef {
+      def unapply(dd: DefDef): Boolean = dd match {
+        case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name.toString == "<init>" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 0) => true
+        case _ => false
+      }
+    }
+
+    object ExMainFunctionDef {
+      def unapply(dd: DefDef): Boolean = dd match {
+        case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name.toString == "main" && tparams.isEmpty && vparamss.size == 1 && vparamss(0).size == 1) => {
+          println("Looks like main " + vparamss(0)(0).symbol.tpe);
+          true
+        }
+        case _ => false
+      }
+    }
+
     object ExFunctionDef {
       /** Matches a function with a single list of arguments, no type
        * parameters and regardless of its visibility. */

src/funcheck/purescala/Definitions.scala

@@ -100,8 +100,8 @@ object Definitions {
   }
 
   /** Functions (= 'methods' of objects) */
-  case class FunDef(id: Identifier, args: VarDecls, body: Expr, precondition: Option[Expr], postcondition: Option[Expr]) extends Definition {
-    lazy val argTypes : Seq[TypeTree] = args.map(_.tpe) 
-    lazy val returnType : TypeTree = body.getType
+  case class FunDef(id: Identifier, returnType: TypeTree, args: VarDecls, body: Expr, precondition: Option[Expr], postcondition: Option[Expr]) extends Definition {
+    //lazy val argTypes : Seq[TypeTree] = args.map(_.tpe) 
+    //lazy val returnType : TypeTree = body.getType
   }
 }

src/funcheck/purescala/PrettyPrinter.scala

@@ -87,6 +87,7 @@ object PrettyPrinter {
   // TYPE TREES
   // all type trees are printed in-line
   private def pp(tpe: TypeTree, sb: StringBuffer): StringBuffer = tpe match {
+    case Int32Type => sb.append("Int")
     case _ => sb.append("Type?")
   }
 
@@ -121,6 +122,29 @@ object PrettyPrinter {
         ind(nsb); nsb.append("}\n")
       }
 
+      case FunDef(id, rt, args, body, pre, post) => {
+        var nsb = sb
+        ind(nsb)
+        nsb.append("def ")
+        nsb.append(id)
+        nsb.append("(")
+
+        args.foreach(a => {
+            nsb.append("ARG ")
+        })
+
+        nsb.append(") : ")
+        nsb = pp(rt, nsb)
+        nsb.append(" = {\n")
+
+        ind(nsb)
+        nsb = pp(body, nsb)
+        nsb.append("\n")
+
+        ind(nsb)
+        nsb.append("}\n")
+      }
+
       case _ => sb.append("Defn?")
     }
   }

src/funcheck/util/FreshNameCreator.scala

 package funcheck.util
 
-
 trait FreshNameCreator {
   var fresh: scala.tools.nsc.util.FreshNameCreator
 }