some refactoring in the trees. Moving on to extracting definitions.

src/funcheck/purescala/Definitions.scala

+package funcheck.purescala
+
+object Definitions {
+  import Common._
+  import Trees._
+  import TypeTrees._
+
+  sealed abstract class Definition {
+    val id: Identifier
+    override def toString: String = PrettyPrinter(this)
+  }
+
+  final case class VarDecl(id: Identifier, tpe: TypeTree)
+  type VarDecls = Seq[VarDecl]
+
+  /** Objects work as containers for class definitions, functions (def's) and
+   * val's. */
+  case class ObjectDef(id: Identifier, defs : Seq[Definition]) extends Definition
+
+  /** Useful because case classes and classes are somewhat unified in some
+   * patterns (of pattern-matching, that is) */
+  sealed trait ClassTypeDef extends Definition {
+    val id: Identifier
+    val parent: Option[AbstractClassDef]
+    val fields: VarDecls
+  }
+
+  /** Will be used at some point as a common ground for case classes (which
+   * implicitely define extractors) and explicitely defined unapply methods. */
+  sealed trait ExtractorTypeDef
+
+  /** Abstract classes. */
+  case class AbstractClassDef(id: Identifier, parent: Option[AbstractClassDef], fields: VarDecls) extends ClassTypeDef
+
+  /** Case classes. */
+  case class CaseClassDef(id: Identifier, parent: Option[AbstractClassDef], fields: VarDecls) extends ClassTypeDef with ExtractorTypeDef
+
+  /** "Regular" classes */
+  case class ClassDef(id: Identifier, parent: Option[AbstractClassDef], fields: VarDecls) extends ClassTypeDef
+  
+  /** Values */
+  case class ValDef(id: Identifier, value: Expr) extends Definition
+
+  /** Functions (= 'methods' of objects) */
+  case class FunDef(id: Identifier, args: VarDecls, body: Expr) extends Definition {
+    lazy val argTypes : Seq[TypeTree] = args.map(_.tpe) 
+    lazy val returnType : TypeTree = body.getType
+  }
+}

src/funcheck/purescala/PrettyPrinter.scala

 package funcheck.purescala
 
-import Trees._
-import Common._
 
+/** This pretty-printer uses Unicode for some operators, to make sure we
+ * distinguish PureScala from "real" Scala (and also because it's cute). */
 object PrettyPrinter {
+  import Common._
+  import Trees._
+  import TypeTrees._
+  import Definitions._
+
+  import java.lang.StringBuffer
+
   def apply(tree: Expr): String = {
     val retSB = pp(tree, new StringBuffer)
     retSB.toString
   }
 
-  import java.lang.StringBuffer
+  def apply(tpe: TypeTree): String = {
+    val retSB = pp(tpe, new StringBuffer)
+    retSB.toString
+  }
 
-  private def pp(tree: Expr, sb: StringBuffer): StringBuffer = tree match {
-    case And(exprs) => {
-      var nsb = sb
-      nsb.append("(")
-      val sz = exprs.size
-      var c = 0
-      exprs.foreach(ex => { nsb = pp(ex, nsb) ; c += 1 ; if(c < sz) nsb.append(" \u2227 ") })
-      nsb.append(")")
-      nsb
-    }
-
-    case Or(exprs) => {
-      var nsb = sb
-      nsb.append("(")
-      val sz = exprs.size
-      var c = 0
-      exprs.foreach(ex => { nsb = pp(ex, nsb) ; c += 1 ; if(c < sz) nsb.append(" \u2228 ") })
-      nsb.append(")")
-      nsb
-    }
-
-    case Not(expr) => {
-      sb.append("\u00AC(")
-      pp(expr, sb)
-      sb.append(")")
-    }
+  def apply(defn: Definition): String = {
+    val retSB = pp(defn, new StringBuffer, 0)
+    retSB.toString
+  }
 
-    case IntLiteral(v) => sb.append(v)
+  // EXPRESSIONS
+  private def ppUnary(sb: StringBuffer, expr: Expr, op: String): StringBuffer = {
+    var nsb: StringBuffer = sb
+    nsb.append(op)
+    nsb.append("(")
+    nsb = pp(expr, nsb)
+    nsb.append(")")
+    nsb
+  }
 
+  private def ppBinary(sb: StringBuffer, left: Expr, right: Expr, op: String): StringBuffer = {
+    var nsb: StringBuffer = sb
+    nsb.append("(")
+    nsb = pp(left, nsb)
+    nsb.append(op)
+    nsb = pp(right, nsb)
+    nsb.append(")")
+    nsb
+  }
+
+  private def ppNary(sb: StringBuffer, exprs: Seq[Expr], op: String): StringBuffer = {
+    var nsb = sb
+    nsb.append("(")
+    val sz = exprs.size
+    var c = 0
+
+    exprs.foreach(ex => {
+      nsb = pp(ex, nsb) ; c += 1 ; if(c < sz) nsb.append(op)
+    })
+
+    nsb.append(")")
+    nsb
+  }
+
+  private def pp(tree: Expr, sb: StringBuffer): StringBuffer = tree match {
+    case And(exprs) => ppNary(sb, exprs, " \u2227 ")            // \land
+    case Or(exprs) => ppNary(sb, exprs, " \u2228 ")             // \lor
+    case Not(Equals(l, r)) => ppBinary(sb, l, r, " \u2260 ")    // \neq
+    case Not(expr) => ppUnary(sb, expr, "\u00AC")               // \neg
+    case Equals(l,r) => ppBinary(sb, l, r, " = ")
+    case IntLiteral(v) => sb.append(v)
     case BooleanLiteral(v) => sb.append(v)
 
-    case _ => sb.append("?")
+    case _ => sb.append("Expr?")
   }
 
+  // TYPE TREES
+  private def pp(tpe: TypeTree, sb: StringBuffer): StringBuffer = tpe match {
+    case _ => sb.append("Type?")
+  }
+
+  // DEFINITIONS
+  private def pp(defn: Definition, sb: StringBuffer, lvl: Int): StringBuffer = defn match {
+    case _ => sb.append("Defn?")
+  }
 }

src/funcheck/purescala/Trees.scala

 package funcheck.purescala
 
-import Common._
 
 /** AST definitions for Pure Scala. */
 object Trees {
+  import Common._
+  import TypeTrees._
+  import Definitions._
 
   /* EXPRESSIONS */
 
@@ -16,16 +18,6 @@ object Trees {
   }
 
   /** 
-   Go through each type, add the operations.
-     map update
-     concatenation of lists
-     random access on lists
-     set union, intersection, etc.
-
-   Lambda abstraction and application of function values
-
-   Separately, function calls
-
    equality on sets, ADTs etc. (equality on function types?!)
 
    forall, exists - optionally bounded quantifiers
@@ -331,49 +323,4 @@ see examples in:
     assert(list.getType.isInstanceOf[ListType] && index.getType == Int32Type)
     lazy val getType = OptionType(list.getType.asInstanceOf[ListType].base)
   }
-
-  /* TYPES */
-
-  trait Typed {
-    def getType: TypeTree
-  }
-
-  sealed abstract class TypeTree
-
-  case object AnyType extends TypeTree
-  case object BooleanType extends TypeTree
-  case object Int32Type extends TypeTree
-
-  case class ListType(base: TypeTree) extends TypeTree
-  case class TupleType(bases: Seq[TypeTree]) extends TypeTree { lazy val dimension: Int = bases.length }
-  case class FunctionType(arg: TypeTree, res: TypeTree) extends TypeTree
-  case class SetType(base: TypeTree) extends TypeTree
-  case class MultisetType(base: TypeTree) extends TypeTree
-  case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
-  case class ClassType(id: Identifier) extends TypeTree
-  case class CaseClassType(id: Identifier) extends TypeTree
-  case class OptionType(base: TypeTree) extends TypeTree
-
-  /* DEFINTIONS */
-
-  type VarDecl = (Identifier,TypeTree)
-  type VarDecls = Seq[VarDecl]
-
-  sealed abstract class Definition(name : Identifier)
-
-  /** Useful because case classes and classes are somewhat unified in some
-   * patterns (of pattern-matching, that is) */
-  sealed trait ClassTypeDef
-  sealed trait ExtractorTypeDef
-
-  case class CaseClassDef(name : Identifier, fields : VarDecls) extends Definition(name) with ClassTypeDef with ExtractorTypeDef
-  case class ClassDef(name : Identifier, fields : VarDecls) extends Definition(name) with ClassTypeDef
-  // case class ExtractorDef extends FunDef ...
-  
-  case class ValDef(name : Identifier, value : Expr) extends Definition(name)
-  case class FunDef(name : Identifier, args : VarDecls, body : Expr) extends Definition(name) {
-    lazy val argTypes : Seq[TypeTree] = args.map(_._2) 
-    lazy val returnType : TypeTree = body.getType
-  }
-  case class ObjectDef(name : Identifier, defs : Seq[Definition]) extends Definition(name)
 }

src/funcheck/purescala/TypeTrees.scala

+package funcheck.purescala
+
+object TypeTrees {
+  import Common._
+  import Trees._
+  import Definitions._
+
+  trait Typed {
+    def getType: TypeTree
+  }
+
+  sealed abstract class TypeTree {
+    override def toString: String = PrettyPrinter(this)
+  }
+
+  case object AnyType extends TypeTree
+  case object BooleanType extends TypeTree
+  case object Int32Type extends TypeTree
+
+  case class ListType(base: TypeTree) extends TypeTree
+  case class TupleType(bases: Seq[TypeTree]) extends TypeTree { lazy val dimension: Int = bases.length }
+  case class FunctionType(arg: TypeTree, res: TypeTree) extends TypeTree
+  case class SetType(base: TypeTree) extends TypeTree
+  case class MultisetType(base: TypeTree) extends TypeTree
+  case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
+  case class ClassType(id: Identifier) extends TypeTree
+  case class CaseClassType(id: Identifier) extends TypeTree
+  case class OptionType(base: TypeTree) extends TypeTree
+}