we have pattern matching

ParseMe.scala

@@ -5,20 +5,17 @@ object ParseMe {
   case class Node(left: Tree, value: Int, right: Tree) extends Tree
   case class Leaf() extends Tree
 
-  def inside(n: Node): Int = getIt().value
 
-  def getIt() : Node = Node(Leaf(), 12, Leaf())
 
   def insert(v: Int, t: Tree): Tree = t match {
-    case Leaf() if v == 5 => Leaf()
     case Leaf() => Node(Leaf(), v, Leaf())
-    case Node(Leaf(), 12, Leaf()) => Leaf()
-    case _ => Leaf()
+    case Node(left, v2, right) if v2 > v => Node(insert(v, left), v2, right)
+    case Node(left, v2, right) if v2 < v => Node(left, v2, insert(v, right))
+    case n @ Node(left, v2, right) if v2 == v => n
   }
 
   def emptySet() : Tree = {
     Leaf()
   }
 
-  def withIf(a: Int) : Int = { if(a < 0) -a else if(a > 0) a+1 else a-1 } ensuring (_ > 17)
 }

src/funcheck/CodeExtraction.scala

@@ -273,8 +273,30 @@ trait CodeExtraction extends Extractors {
    * errors. */
   private def scala2PureScala(unit: CompilationUnit, silent: Boolean)(tree: Tree): Expr = {
     def rewriteCaseDef(cd: CaseDef): MatchCase = {
-      def pat2pat(p: Tree): Pattern = {
-        WildcardPattern(None)
+      def pat2pat(p: Tree): Pattern = p match {
+        case Ident(nme.WILDCARD) => WildcardPattern(None)
+        case b @ Bind(name, Ident(nme.WILDCARD)) => {
+          val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(b.symbol.tpe))
+          varSubsts(b.symbol) = (() => Variable(newID))
+          WildcardPattern(Some(newID))
+        }
+        case a @ Apply(fn, args) if fn.isType && a.tpe.typeSymbol.isCase && classesToClasses.keySet.contains(a.tpe.typeSymbol) => {
+          val cd = classesToClasses(a.tpe.typeSymbol).asInstanceOf[CaseClassDef]
+          assert(args.size == cd.fields.size)
+          CaseClassPattern(None, cd, args.map(pat2pat(_)))
+        }
+        case b @ Bind(name, a @ Apply(fn, args)) if fn.isType && a.tpe.typeSymbol.isCase && classesToClasses.keySet.contains(a.tpe.typeSymbol) => {
+          val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(b.symbol.tpe))
+          varSubsts(b.symbol) = (() => Variable(newID))
+          val cd = classesToClasses(a.tpe.typeSymbol).asInstanceOf[CaseClassDef]
+          assert(args.size == cd.fields.size)
+          CaseClassPattern(Some(newID), cd, args.map(pat2pat(_)))
+        }
+        case _ => {
+          if(!silent)
+            unit.error(p.pos, "Unsupported pattern.")
+          throw ImpureCodeEncounteredException(p)
+        }
       }
 
       if(cd.guard == EmptyTree) {
@@ -289,7 +311,10 @@ trait CodeExtraction extends Extractors {
       case ExBooleanLiteral(v) => BooleanLiteral(v)
       case ExIdentifier(sym,tpt) => varSubsts.get(sym) match {
         case Some(fun) => fun()
-        case None => Variable(FreshIdentifier(sym.name.toString)) // TODO this is SO wrong
+        case None => {
+          unit.error(tr.pos, "Unidentified variable.")
+          throw ImpureCodeEncounteredException(tr)
+        }
       }
       case ExCaseClassConstruction(tpt, args) => {
         val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)

src/purescala/PrettyPrinter.scala

@@ -121,8 +121,20 @@ object PrettyPrinter {
       def ppc(sb: StringBuffer, p: Pattern): StringBuffer = p match {
         //case InstanceOfPattern(None,     ctd) =>
         //case InstanceOfPattern(Some(id), ctd) =>
-        //case CaseClassPattern(None,     ccd, subps) =>
-        //case CaseClassPattern(Some(id), ccd, subps) => 
+        case CaseClassPattern(bndr,     ccd, subps) => {
+          var nsb = sb
+          bndr.foreach(b => nsb.append(b + " @ "))
+          nsb.append(ccd.id).append("(")
+          var c = 0
+          val sz = subps.size
+          subps.foreach(sp => {
+            nsb = ppc(nsb, sp)
+            if(c < sz - 1)
+              nsb.append(", ")
+            c = c + 1
+          })
+          nsb.append(")")
+        }
         case WildcardPattern(None)     => sb.append("_")
         case WildcardPattern(Some(id)) => sb.append(id)
         case _ => sb.append("Pattern?")