Allow adding definitions within a program

src/main/scala/leon/purescala/DefOps.scala

@@ -18,6 +18,12 @@ object DefOps {
     case u : UnitDef => Some(u)
     case other => other.owner flatMap inUnit
   }
+
+  def inModule(df : Definition) : Option[ModuleDef] = df match {
+    case p : Program => None
+    case m : ModuleDef => Some(m)
+    case other => other.owner flatMap inModule
+  }
   
   def inProgram(df : Definition) : Option[Program] = {
     df match {

src/main/scala/leon/purescala/Definitions.scala

@@ -10,6 +10,7 @@ object Definitions {
   import Common._
   import Trees._
   import TreeOps._
+  import DefOps._
   import Extractors._
   import TypeTrees._
   import TypeTreeOps._
@@ -80,6 +81,26 @@ object Definitions {
       copy(units = units.map{_.duplicate})
     }
 
+    // Use only to add functions around functions
+    def addDefinition(d: Definition, around: Definition): Program = {
+      val Some(m) = inModule(around)
+      val nm      = m.copy(defs = d +: m.defs)
+
+      m.owner match {
+        case Some(u: UnitDef) =>
+          val nu = u.copy(modules = u.modules.filterNot(_ == m) :+ nm)
+
+          u.owner match {
+            case Some(p: Program) =>
+              p.copy(units = p.units.filterNot(_ == u) :+ nu)
+            case _ =>
+              this
+          }
+        case _ =>
+          this
+      }
+    }
+
     lazy val library = Library(this)
     
     def writeScalaFile(filename: String) {

src/main/scala/leon/repair/Repairman.scala

@@ -23,9 +23,11 @@ import synthesis.rules._
 import synthesis.heuristics._
 import graph.DotGenerator
 
-class Repairman(ctx: LeonContext, program: Program, fd: FunDef, verifTimeout: Option[Long]) {
+class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout: Option[Long]) {
   val reporter = ctx.reporter
 
+  var program = initProgram
+
   implicit val debugSection = DebugSectionRepair
 
   def getSynthesizer(tests: List[Example]): Synthesizer = {
@@ -69,6 +71,8 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef, verifTimeout: Op
       passes
     )
 
+    program = program.addDefinition(nfd, fd)
+
     val p = focusRepair(tests, nfd, spec, out)
 
     val soptions0 = SynthesisPhase.processOptions(ctx);