Esthetic changes in transformers + unary minus in DSL

src/main/scala/inox/ast/DSL.scala

@@ -30,6 +30,7 @@ trait DSL {
     def - = Minus(e, _: Expr)
     def % = Modulo(e, _: Expr)
     def / = Division(e, _: Expr)
+    def unary_- = UMinus(e)
 
     // Comparisons
     def <   = LessThan(e, _: Expr)

src/main/scala/inox/transformers/Collector.scala

@@ -11,9 +11,10 @@ trait Collector extends Transformer {
   /** The type of collected objects */
   type R
   final type Result = (R, Env)
-  import trees.Expr
   private var results: List[Result] = Nil
 
+  import trees._
+
   /** Does one step of collection for the current [[Expr]] and [[Env]] */
   protected def step(e: Expr, env: Env): List[Result]
 
@@ -23,9 +24,12 @@ trait Collector extends Transformer {
   }
 
   /** Traverses the expression and collects */
-  final def collect(e: Expr) = {
+  final def collect(e: Expr): List[Result] = {
     results = Nil
     transform(e)
     results
   }
+
+  /** Collect the expressions in a [[FunDef]]'s body */
+  final def collect(fd: FunDef): List[Result] = collect(fd.fullBody)
 }

src/main/scala/inox/transformers/CollectorWithPC.scala

@@ -4,18 +4,22 @@ package inox
 package transformers
 
 /** A [[Collector]] that collects path conditions */
-trait CollectorWithPC extends TransformerWithPC with Collector
+trait CollectorWithPC extends TransformerWithPC with Collector {
+  import program.trees._
+  import program.symbols._
+
+  lazy val initEnv: Path = Path.empty
+}
 
 object CollectorWithPC {
-  def apply[T](p: Program)(f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]): CollectorWithPC { type R = T; val program: p.type } = {
+  def apply[T](p: Program)
+              (f: PartialFunction[(p.trees.Expr, p.symbols.Path), T]):
+               CollectorWithPC { type R = T; val program: p.type } = {
     new CollectorWithPC {
-
       type R = T
       val program: p.type = p
-      import program._
-      import symbols._
-      import trees._
-      val initEnv: Path = Path.empty
+      import program.trees._
+      import program.symbols._
 
       private val fLifted = f.lift
 

src/main/scala/inox/transformers/SimplifierWithPC.scala

@@ -12,7 +12,7 @@ trait SimplifierWithPC extends TransformerWithPC { self =>
   import trees._
   import symbols._
 
-  protected val sf: SolverFactory{ val program: self.program.type }
+  protected val sf: SolverFactory { val program: self.program.type }
   protected lazy val s = SimpleSolverAPI(sf)
 
   private def querie(e: Expr, path: Path, implied: Boolean) = {