Minor reorganization, and implementing trace-induct tactic

leon.out/Conqueue-edited.scala

@@ -7,6 +7,8 @@ import leon.lang.synthesis._
 import ConcTrees._
 import ConQ._
 import Conqueue._
+import conc.Conqueue
+import conc.ConcTrees
 
 object ConcTrees {
   abstract class Conc[T] { 

library/annotation/package.scala

@@ -10,6 +10,8 @@ package object annotation {
   @ignore
   class induct     extends StaticAnnotation
   @ignore
+  class traceInduct     extends StaticAnnotation
+  @ignore
   class ignore     extends StaticAnnotation
   @ignore
   class extern     extends StaticAnnotation

library/lazy/package.scala

@@ -5,6 +5,7 @@ package leon.lazyeval
 import leon.annotation._
 import leon.lang._
 import scala.language.implicitConversions
+import scala.annotation.StaticAnnotation
 
 @library
 object $ {
@@ -48,6 +49,16 @@ object $ {
 
   @inline
   implicit def toWithState[T](x: T) = new WithState(x)
+
+  /**
+   * annotations for monotonicity proofs.
+   * Note implemented as of now.
+   * Let foo be the method that has the annotation.
+   * The given name `methodname` should have the following form:
+   *  m(arg1, ..., argn, substate-Set1,..., substate-Setn, superstate-Set1, ..., superstate-Setn)
+   */
+  @ignore
+  class monoproof(methodname: String) extends StaticAnnotation
 }
 
 @library

src/main/scala/leon/verification/TraceInductionTactic.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package verification
+
+import purescala.Definitions._
+import purescala.Expressions._
+
+/**
+ * This tactic applies only to non-recursive functions.
+ * Inducts over the recursive calls of the first recursive procedure, in the body of `funDef`
+ */
+class TraceInductionTactic(vctx: VerificationContext) extends Tactic(vctx) {
+  val description : String =
+
+  implicit protected val ctx = vctx.context
+
+  def generateVCs(fd: FunDef): Seq[VC] = {
+    generatePostconditions(fd) ++
+    generatePreconditions(fd) ++
+    generateCorrectnessConditions(fd)
+  }
+
+  def generatePostconditions(function: FunDef): Seq[VC]
+  def generatePreconditions(function: FunDef): Seq[VC]
+  def generateCorrectnessConditions(function: FunDef): Seq[VC]
+
+  protected def sizeLimit(s: String, limit: Int) = {
+    require(limit > 3)
+    // Crop the call to display it properly
+    val res = s.takeWhile(_ != '\n').take(limit)
+    if (res == s) {
+      res
+    } else {
+      res + " ..."
+    }
+  }
+}

testcases/lazy-datastructures/LazyMegeSort.scala

@@ -54,9 +54,7 @@ object MergeSort {
   } ensuring (res => res._2.size == l.size - n && res._1.size == n && stack <= 25 * l.size - 1)
 
   /*
-   * Note: merge is not recursive due to closures.
-   * However, concretizing merge may invoke merge or msort recursively.
-   * So proving standalone bound for merge requires preconditions.
+   * Proving standalone bound for merge requires preconditions.
    */
   def merge(a: $[LList], b: $[LList]): LList = (b.value match {
     case SNil() => a.value

testcases/lazy-datastructures/FibonacciMemoized.scala → testcases/lazy-datastructures/Unproved/FibonacciMemoized.scala

-package lazybenchmarks
+package Unproved
 
 import leon.lazyeval._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
+import scala.math.BigInt.int2bigInt
 //import leon.invariant._
 
 object FibMem {

testcases/lazy-datastructures/HammingProblem.scala → testcases/lazy-datastructures/Unproved/HammingProblem.scala

-package lazybenchmarks
-
 import leon.lazyeval._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
+import leon.lazyeval.$.eagerToLazy
+import scala.math.BigInt.int2bigInt
 //import leon.invariant._
 
 /**

testcases/lazy-datastructures/ImplicitQueue.scala → testcases/lazy-datastructures/Unproved/ImplicitQueue.scala

@@ -3,6 +3,7 @@ import leon.lazyeval.$._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
+import scala.math.BigInt.int2bigInt
 
 /**
  * This is an version of the implicit recursive slowdwon queues of

testcases/lazy-datastructures/Conqueue.scala → testcases/lazy-datastructures/conc/Conqueue.scala

-package lazybenchmarks
+package conc
 
 import leon.lazyeval._
 import leon.lang._
@@ -7,6 +7,9 @@ import leon.annotation._
 import leon.instrumentation._
 import leon.lazyeval.$._
 
+import ConcTrees._
+import scala.math.BigInt.int2bigInt
+
 object ConcTrees {
 
   sealed abstract class Conc[T] {
@@ -30,8 +33,6 @@ object ConcTrees {
   case class Single[T](x: T) extends Conc[T]
   case class CC[T](left: Conc[T], right: Conc[T]) extends Conc[T]
 }
-
-import ConcTrees._
 object Conqueue {
 
   sealed abstract class ConQ[T] {