Automatically add type annotations to type ensuring

src/main/scala/leon/frontends/scalac/AddTypeAnnotations.scala

+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package frontends.scalac
+
+import scala.tools.nsc._
+import scala.tools.nsc.plugins._
+
+trait AddTypeAnnotations extends SubComponent with ASTExtractors {
+  import global._
+  import global.definitions._
+  import ExtractorHelpers._
+
+  val phaseName = "addtypeannotations"
+
+  val ctx: LeonContext
+
+  var imports : Map[RefTree,List[Import]] = Map()
+  
+  def newPhase(prev: scala.tools.nsc.Phase): StdPhase = new Phase(prev)
+
+  class Phase(prev: scala.tools.nsc.Phase) extends StdPhase(prev) {
+    def apply(unit: CompilationUnit): Unit = {
+      val transformer = new Transformer { 
+        override def transform(tree : Tree) : Tree = tree match { 
+          case d@DefDef(_,_,_,_,tpt,
+            a@Apply(
+              s@Select(
+                bd, 
+                nameEns@ExNamed("ensuring")
+              ),
+              f
+            )
+          ) => (bd,tpt.symbol) match {
+            case (Typed(_,_), _) | (_, null) => d
+            case _ => d.copy(rhs = 
+              Apply(
+                Select(
+                  Typed(bd,tpt.duplicate.setPos(bd.pos.focus)).setPos(bd.pos),
+                  nameEns
+                ).setPos(s.pos),
+                f         
+              ).setPos(a.pos)
+            ).setPos(d.pos)
+          }
+          case other => super.transform(other)
+        }
+      }
+      unit.body = transformer.transform(unit.body)
+    }
+  }
+}

src/main/scala/leon/frontends/scalac/ScalaCompiler.scala

@@ -22,9 +22,17 @@ class ScalaCompiler(settings : NSCSettings, ctx: LeonContext) extends Global(set
     val ctx = ScalaCompiler.this.ctx
   } with SaveImports
   
+  object addTypeAnnotations extends {
+    val global: ScalaCompiler.this.type = ScalaCompiler.this
+    val runsAfter = List[String]()
+    val runsRightAfter = Some("parser")
+    val ctx = ScalaCompiler.this.ctx
+  } with AddTypeAnnotations
+
   override protected def computeInternalPhases() : Unit = {
     val phs = List(
       syntaxAnalyzer          -> "parse source into ASTs, perform simple desugaring",
+      addTypeAnnotations      -> "add type annotations useful for Leon",
       analyzer.namerFactory   -> "resolve names, attach symbols to named trees",
       analyzer.packageObjects -> "load package objects",
       analyzer.typerFactory   -> "the meat and potatoes: type the trees",