import leon.collection._
import leon.lang._
import scala.Any
import leon.annotation._
import leon.proof._
import leon.instrumentation._
import leon.invariant._
import leon.util.Random

object Scheduler {
   import Runqueue._

   case class Task(id: BigInt, tick: BigInt, core: Core) {
      require(tick >= 0)
      def updateTick(t:BigInt):Task = {
         require(t >= 0)
         Task(id, t, core)
      } ensuring(res =>
         containsEquivLemma(core.tasks, this, res) &&
         ((core.current.isDefined && res.id != core.current.get.id && !contains(core.tasks, res)) ==> containsLemma5(core.tasks, res, core.current.get))
      ); // ensure that the resulting task is equivalent to "this" from a core point of view
   }

   case class Core(id: BigInt, tasks: List[Task], current: Option[Task]) {
     require(isSorted(tasks) && isUnique(tasks) && (current.isDefined ==> !contains(tasks,current.get)))
   }

   def tick(t:Task):Task = {
      Task(t.id, t.tick + 1, t.core)
   }

   def insertBack(c: Core, t: Task): Core = {
      require(!contains(c.tasks, t))
      if(containsEquivLemma(c.tasks, t, tick(t))) {
         Core(c.id, sortedIns(c.tasks, tick(t)), None[Task]())
      } else {
         error[Core]("Tick changes task id\n");
      }
   }

   /* Comment me! */
   def test(c: Core): Core = {
      c
   } ensuring(rec < 5);
}

object Runqueue {
   import Scheduler._

   /*
    * 1/ Tasks in the runqueue must be unique ==> no two tasks can have the same id
   */
   @induct
   def contains(tasks: List[Task], v: Task): Boolean = (tasks match {
      case Cons(Task(id, tick, c), t) => id == v.id || contains(t, v)
      case Nil() => false
   }) ensuring(res => (!res ==> !tasks.contains(v)));

   def isUnique(tasks: List[Task]): Boolean = {
      tasks match {
         case Nil() => true
         case Cons(h, Nil()) => true
         case Cons(h, t) =>
            !contains(t,h) && isUnique(t)
      }
   }

   @induct // if two tasks have the same id, then they are both in the list or both not in the list
   def containsEquivLemma(l: List[Task], e:Task, t: Task) = {
      e.id == t.id ==> (contains(l, e) == contains(l, t))
   }.holds;


   @induct // super important lemma: if we were not in the a list, and not inserted in the list, then we are still not in the list!
   def containsLemma5(l: List[Task], e:Task, t: Task) = {
      require(isSorted(l) && isUnique(l) && !contains(l, e) && !contains(l, t) && e.id != t.id)
      !contains(sortedIns(l, e), t)
   }.holds;

   /*
   * 2/ A runqueue must also be sorted
   */
   def isSorted(tasks: List[Task]): Boolean = {
      tasks match {
         case Nil() => true
         case Cons(t, Nil()) => true
         case Cons(Task(_,t1, c1), ts@Cons(Task(_,t2, c2), _)) => t1 <= t2 && isSorted(ts)
      }
   }

   /*
    * 3/ The task => queue insert function that shows that a queue is still unique and sorted after the insert
   */
   @induct
   def sortedIns(l: List[Task], e:Task): List[Task] = {
      require(isSorted(l) && isUnique(l) && !contains(l, e))

      l match {
         case Nil() => Cons(e, Nil())
         case Cons(Task(id,x, c), xs) =>
            if (x <= e.tick) Cons(Task(id,x,c), sortedIns(xs, e))
            else Cons(e, l)
      }
   } ensuring(res => isSorted(res) && res.content == l.content ++ Set(e) && res.contains(e) && contains(res, e) && isUnique(res) because ({
      l match {
         case Nil() => isUnique(res)
         case Cons(t, xs) =>
            if(t.tick <= e.tick) isUnique(xs) && isSorted(xs) && !contains(xs, t) && !contains(xs, e) && e.id != t.id && containsLemma5(xs, e, t) && !contains(sortedIns(xs, e), t) && isUnique(res)
            else isUnique(res)
      }
   }));
}