import leon.collection._
import leon.lang._
import scala.Any
import leon.annotation._
import leon.proof._
//import scala.language.postfixOps

object Scheduler {

   import PrettyPrinting._

   case class Task(id: BigInt, tick: BigInt) {
      require(tick >= 0)
   }

   case class Core(tasks: List[Task], current: Option[Task]) {
      require(isSorted(tasks))
      //require(isSorted(tasks) && isUnique(tasks) && (current.isDefined ==> !tasks.contains(Task(current.get.id, current.get.tick + 1)))) // and also unique
   }

   def find(l:List[Task], e: Task): Option[BigInt] = { l match {
      case Nil() => None[BigInt]()
      case Cons(h, t) =>
         if (h == e) {
            Some[BigInt](0)
         } else {
            find(t, e) match {
               case None()  => None[BigInt]()
               case Some(i) => Some(i+1)
            }
         }
   }} ensuring { res => !res.isDefined || (l.content contains e) }

   @induct
   def notContainsLemma(l:List[Task], t:Task) = {
      !contains(l, t) ==> !l.contains(t);
   }.holds;

   @induct
   def testFind(l:List[Task], e:Task, t:Task) = {
      require(l.contains(e) && !contains(l, t))
      val res = Cons(t, l)
      ({notContainsLemma(l, t) && isHereLemma(l, e) && find(l, e).isDefined &&
            isHereLemma(res, e) && find(res, e).isDefined &&
            find(l, e).get + 1 == find(res, e).get })
   }.holds;

   def findExists(l:List[Task], e: Task): BigInt = {
      require(isSorted(l) && l.contains(e));
      l match {
         case Cons(h, t) =>
            if (h == e) {
               BigInt(0)
            } else {
               1 + findExists(t, e)
            }
         }
   }

   @induct
   def findEquiv(l:List[Task], e:Task) = {
      require(l.contains(e) && isSorted(l))
      find(l, e) == Some(findExists(l, e)) && findExists(l, e) == find(l, e).get
   }.holds;

   @induct
   def findMaxEquiv(l:List[Task], e:Task) = {
      require(l.contains(e) && isSorted(l))
      findEquiv(l, e) && maxSumBeforeSorted(l, e) == e.tick * findExists(l, e) && maxSumBeforeSorted(l, e) == e.tick * find(l, e).get
   }.holds;


   @induct
   def maxSumBeforeSortedLemma(l1:List[Task], l2:List[Task], e:Task):Boolean = {
      require(l1.contains(e) && l2.contains(e) && isSorted(l1) && isSorted(l2) && find(l1, e).get <= find(l2, e).get);
      findMaxEquiv(l1, e) && findMaxEquiv(l2, e) &&
      maxSumBeforeSorted(l1, e) <= maxSumBeforeSorted(l2, e)
   }.holds;


   def sumBefore(l: List[Task], e: Task): BigInt = {
      require(l.contains(e));
      l match {
         case Cons(h, t) =>
            if (h == e) {
               BigInt(0)
            } else {
               h.tick + sumBefore(t, e)
            }
      }
   }

   @induct
   def testSumBeforeHelperA(l: List[Task], e:Task, t:Task) = {
      require(l.contains(e) && isSorted(l) && t.tick < e.tick);
      val res = sortedIns(t, l)
      sumBefore(res, e) == sumBefore(l, e) + t.tick
   }.holds

   def testSumBeforeHelperB(l: List[Task], e:Task, t:Task): Boolean = {
      require(l.contains(e) && isSorted(l) && t.tick >= e.tick);
      val res = sortedIns(t, l)
      sumBefore(res, e) == sumBefore(l, e)
      l match {
        case Cons(x, xs) =>
          if (x == e)
            sumBefore(res, e) == sumBefore(l, e)
          else
            testSumBeforeHelperB(xs, e, t) &&
            sumBefore(res, e) == sumBefore(l, e)
      }
   }.holds;

   def testSumBeforeHelper(l: List[Task], e:Task, t:Task) = {
      require(l.contains(e) && isSorted(l));
      var res = sortedIns(t, l);
      if(t.tick < e.tick) {
        testSumBeforeHelperA(l, e, t) &&
        sumBefore(res, e) == sumBefore(l, e) + t.tick;
      } else {
        testSumBeforeHelperB(l, e, t) &&
        sumBefore(res, e) == sumBefore(l, e);
      }
    }.holds

   def testSumBeforeDefined(c: Core, e:Task) = {
      require(c.tasks.contains(e) && c.current.isDefined);
      val res = timer(c);
      ({
         val t2 = Task(c.current.get.id, c.current.get.tick + 1);
         testSumBeforeHelper(c.tasks, e, t2) && ({
            if(t2.tick < e.tick) {
               sumBefore(res.tasks, e) == sumBefore(c.tasks, e) + t2.tick;
            } else {
               sumBefore(res.tasks, e) == sumBefore(c.tasks, e);
            }
         })
      })
   }.holds;

   def testSumBeforeUndefined(c:Core, e:Task) = {
      require(c.tasks.contains(e) && !c.current.isDefined);
      var res = timer(c);
      if(c.tasks.head == e) {
         res.current == Some(e)
      } else {
         sumBefore(res.tasks, e) == sumBefore(c.tasks, e) - c.tasks.head.tick;
      }
   }.holds


   def testSumBefore(c:Core, e:Task) = {
      require(c.tasks.contains(e))
      val res = timer(c);
      ({
         if(c.current.isDefined) {
            val t2 = Task(c.current.get.id, c.current.get.tick + 1);
            ({
               if(t2.tick < e.tick) {
                  sumBefore(res.tasks, e) == sumBefore(c.tasks, e) + t2.tick;
               } else {
                  sumBefore(res.tasks, e) == sumBefore(c.tasks, e);
               }
            }) because testSumBeforeDefined(c,e);
         } else {
            ({ if(c.tasks.head == e) {
               res.current == Some(e)
            } else {
               sumBefore(res.tasks, e) == sumBefore(c.tasks, e) - c.tasks.head.tick;
            } }) because testSumBeforeUndefined(c, e);
         }
      })
   }.holds;

   /*
   * Order
   */
   @induct
   def testOrderHelperA(l: List[Task], e:Task, t:Task) = {
      require(isSorted(l) && isUnique(l) && l.contains(e) && !contains(l, t) && t.tick < e.tick)
      val res = sortedIns(t, l)
      uniquenessPreserved(t, l) && res.contains(e) && isHereLemma(res, e) && find(res, e).get >= 0 && find(l, e).get >= 0 && testFind(l, e, t) && (find(res, e).get == find(l, e).get + 1)
   }.holds;

   @induct
   def testOrderHelperB(l: List[Task], e:Task, t:Task) = {
      require(isSorted(l) && isUnique(l) && l.contains(e) && !contains(l, t) && t.tick >= e.tick)
      val res = sortedIns(t, l)
      uniquenessPreserved(t, l) && res.contains(e) && isHereLemma(res, e) && find(res, e).get >= 0 && find(l, e).get >= 0 && testFind(l, e, t) && (find(res, e).get == find(l, e).get)
   }.holds;

   def testOrderTimerUndefined(c: Core, e:Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined)
      val res = timer(c);
      res.current == Some(e) || (res.tasks.contains(e) && isHereLemma(res.tasks, e) && isHereLemma(c.tasks, e) && (find(res.tasks, e).get == find(c.tasks,e).get - 1))
   }.holds;

   def testOrderTimerDefined(c: Core, e:Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && c.current.isDefined && !contains(c.tasks, Task(c.current.get.id, c.current.get.tick + 1)))
      val res = timer(c);
      val t2 = Task(c.current.get.id, c.current.get.tick + 1);
      uniquenessPreserved(t2, c.tasks) && isUnique(res.tasks) &&
         isHereLemma(res.tasks, e) && isHereLemma(c.tasks, e) && ({
            if(t2.tick < e.tick) {
               testOrderHelperA(c.tasks, e, t2) && (find(res.tasks, e).get == find(c.tasks, e).get + 1)
            } else {
               testOrderHelperB(c.tasks, e, t2) && (find(res.tasks, e).get == find(c.tasks, e).get)
            }
         });
   }.holds;

   def testOrder(c: Core, e:Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && (c.current.isDefined ==> !contains(c.tasks, Task(c.current.get.id, c.current.get.tick + 1))))
      val res= timer(c);
      if(c.current.isDefined) {
         testOrderTimerDefined(c, e) && ({
         val t2 = Task(c.current.get.id, c.current.get.tick + 1);
         if(t2.tick < e.tick) {
            find(res.tasks, e).get == find(c.tasks, e).get + 1
         } else {
            find(res.tasks, e).get == find(c.tasks, e).get
         } });
      } else {
         testOrderTimerUndefined(c, e) && ({ res.current == Some(e) || (find(res.tasks, e).get == find(c.tasks,e).get - 1) });
      }
   }.holds;

   /*def findFirst(c:Core, e:Task) = {
      (find(c.tasks, e).isDefined && find(c.tasks, e).get == 0) ==> (c.tasks.head == e)
   }.holds;*/

   /*def isTaken(c:Core, e:Task) = {
      require(isSorted(c.tasks) && c.tasks.contains(e) && find(c.tasks, e).get == 0)
      var res = takeFirst(c)
      true
      //res.current == Some(e)
   }.holds;*/

   /*def testLemma(c: Core, e: Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && c.current.isDefined && !c.tasks.contains(Task(c.current.get.id, c.current.get.tick + 1)))
      var res = timer(c);
      testSumBefore(c, e) && testOrder(c, e) && ({
         sumBefore(res.tasks, e) <= find(res.tasks, e).get * e.tick
      });
   }.holds;*/

   /*
   * Def bounds
   */
   @induct
   def boundTest(l:List[Task], e:Task) = {
      require(isSorted(l) && l.contains(e))
      e.tick >= l.head.tick
   }.holds;

   @induct
   def isSortedLemma(l:List[Task], e:Task) = {
      require(isSorted(l) && l.contains(e))
      l match {
         case Cons(h, t) =>
            if (h == e) {
               true
            } else {
               h.tick <= e.tick && boundTest(t, e)
            }
      }
   }.holds;

   def maxSumBeforeSorted(l: List[Task], e: Task): BigInt = {
      require(l.contains(e) && isSorted(l));
      l match {
         case Cons(h, t) =>
            if (h == e) {
               BigInt(0)
            } else {
               e.tick + maxSumBeforeSorted(t, e)
            }
      }
   }

   /*@induct
   def maxSumBeforeSortedLemma(l1:List[Task], l2:List[Task], e:Task):Boolean = {
      require(l1.contains(e) && l2.contains(e) && isSorted(l1) && isSorted(l2) && find(l1, e).get <= find(l2, e).get);
      maxSumBeforeSorted(l1, e) <= maxSumBeforeSorted(l2, e)
   }.holds;*/

   @induct
   def sumBeforeLemma(l: List[Task], e: Task) = {
      require(l.contains(e) && isSorted(l));
      var res = sumBefore(l, e);
      isSortedLemma(l, e) && (res <= maxSumBeforeSorted(l, e));
   }.holds;


   def testMax(c: Core, e: Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && c.current.isDefined && !contains(c.tasks, Task(c.current.get.id, c.current.get.tick + 1)))
      var res = timer(c);
      sumBeforeLemma(res.tasks, e) && sumBefore(res.tasks, e) <= maxSumBeforeSorted(res.tasks, e)
   }.holds;

   def uniquenessPreservedTimer(c:Core) = {
      require(isUnique(c.tasks) && c.current.isDefined && !contains(c.tasks, Task(c.current.get.id, c.current.get.tick + 1)))
      var res = timer(c)
      val t2 = Task(c.current.get.id, c.current.get.tick + 1);
      uniquenessPreserved(t2, c.tasks) && isUnique(res.tasks)
   }.holds;

   def uniquenessPreservedTimer2(c:Core) = {
      require(isUnique(c.tasks) && !c.current.isDefined && !c.tasks.isEmpty)
      var res = timer(c)
      isUnique(res.tasks) && !contains(res.tasks, res.current.get)
   }.holds;


   /*
   * All together
   */
   def theoryOfEveything(c: Core, e: Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined)
      var res = timer(timer(c)); //double call
      if(timer(c).current == Some(e)) {
         true
      } else {
         val t2 = Task(timer(c).current.get.id, timer(c).current.get.tick + 1);
         timer(c).tasks.contains(e) && testSumBeforeUndefined(c, e) && testOrderTimerUndefined(c, e) && testSumBeforeDefined(timer(c), e) &&
         uniquenessPreservedTimer2(c) && isUnique(timer(c).tasks)  &&
         timer(c).tasks.contains(e) && !contains(timer(c).tasks, timer(c).current.get) && containsEquivLemma(timer(c).tasks, timer(c).current.get, t2) && !contains(timer(c).tasks, t2) && testOrderTimerDefined(timer(c), e) && testMax(timer(c), e) &&
         ({
            /* With all of the stuff before we should be able to prove order-- unless sum++ */
           if(t2.tick < e.tick) {
              sumBefore(res.tasks, e) == sumBefore(c.tasks, e) + 1 && find(res.tasks, e).get == find(c.tasks, e).get//whouhou
           } else {
              sumBefore(res.tasks, e) == sumBefore(c.tasks, e) - timer(c).current.get.tick && find(res.tasks, e).get == find(c.tasks, e).get - 1
           }
         }) && sumBefore(res.tasks, e) <= maxSumBeforeSorted(res.tasks, e) &&
         maxSumBeforeSortedLemma(res.tasks, c.tasks, e) && sumBefore(res.tasks, e) <= maxSumBeforeSorted(c.tasks, e) //whouhou, fixed bound with c
      }
   }.holds;

   def theoryOfEveythingLemma(c: Core, e: Task) = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined)
      var res = timer(timer(c)); //double call
      theoryOfEveything(c,e) && ({
         if(timer(c).current == Some(e)) {
            true
         } else {
            if(!(find(res.tasks, e).get == find(c.tasks, e).get - 1)) {
               sumBefore(res.tasks, e) == sumBefore(c.tasks, e) + 1 && sumBefore(res.tasks, e) <= maxSumBeforeSorted(c.tasks, e) && maxSumBeforeSorted(res.tasks, e) == maxSumBeforeSorted(c.tasks, e)
            } else {
               find(res.tasks, e).get == find(c.tasks, e).get - 1
            }
         }
      })
   }.holds;

   def testEvolutionSimple(c: Core, e:Task): Core = {
      require(isUnique(c.tasks) && c.tasks.contains(e) && !c.current.isDefined && theoryOfEveythingLemma(c, e))
      if(timer(c).current == Some(e)) {
         c;
      } else {
         val res = timer(timer(c));
         /*if(find(res.tasks, e).get == find(c.tasks, e).get - 1) {
            c;
         } else {
            testEvolutionSimple(res, e);
         }*/
         if(sumBefore(res.tasks, e) == sumBefore(c.tasks, e) + 1) {
            testEvolutionSimple(res, e);
         } else {
            c
         }
      }
   }

   /*def testEvolution(c:Core, e:Task):Core = {
      require((c.current == Some(e)) || (c.tasks.contains(e)))
      c.current match {
         case Some(t) =>
            if(t == e) c
            else testEvolution(timer(c), e)
         case None() =>
            testEvolution(timer(c), e)
      }
   }*//* ensuring(res => res.current == Some(e))*/




















   @induct
   def equivLemma(l: List[Task], e:Task) = {
      l.contains(e) ==> l.find((a:Task) => a.id == e.id).isDefined;
   }.holds;

   @induct
   def isHereLemma(l: List[Task], e:Task) = {
      l.contains(e) ==> find(l, e).isDefined;
   }.holds;

   /*def isHereLemma(e: Task, l: List[Task]) = {
      var t = l.find((a:Task) => a.id == e.id);
      t.isDefined ==> l.contains(t.get)
   }.holds;*/

   @induct
   def isHereLemmaBis(e: Task, l: List[Task]) = {
      var t = l.find((a:Task) => a.id == e.id);
      t.isDefined  ==> find(l, t.get).isDefined
   }.holds;


   @induct
   def sortedIns(e: Task, l: List[Task]): List[Task] = {
      require(isSorted(l))

      l match {
         case Nil() => Cons(e, Nil())
         case Cons(Task(id,x), xs) =>
            if (x <= e.tick) Cons(Task(id,x), sortedIns(e, xs))
            else Cons(e, l)
      }
   } ensuring(res => isSorted(res) && res.content == l.content ++ Set(e) && res.find((a:Task) => a.id == e.id).isDefined && find(res, e).get >= 0);

   def insertBack(c: Core, t: Task): Core = {
      Core(sortedIns(Task(t.id, t.tick + 1), c.tasks), None[Task]())
   } ensuring(res => res.tasks.find((a:Task) => a.id == t.id).isDefined);

   def takeFirst(c: Core): Core = {
      require(!c.tasks.isEmpty && isSorted(c.tasks))

      c.tasks match {
         case Cons(t, ts) =>
            Core(ts, Some(t))
      }
   }

   def timer(c: Core): Core = {
      require((!c.current.isDefined && !c.tasks.isEmpty) || (c.current.isDefined))

      c.current match {
         case None() => takeFirst(c)
         case Some(t) => insertBack(c, c.current.get)
      }
   } ensuring(res => (
      (c.current.isDefined && res.tasks.find((a:Task) => a.id == c.current.get.id).isDefined)
      ||
      (!c.current.isDefined)
   ));

  /* A Task does not disappear */
 def doesNotDisapearTest(c:Core, t:Task) = {
    require(!c.tasks.isEmpty && c.tasks.contains(t))
    var res = timer(c);
    (res.current != Some(t)) ==> (res.tasks.contains(t))
 }.holds;

 @induct
 def orderInList(l: List[Task], e: Task):List[Task] = {
    require(isSorted(l))
    sortedIns(e, l)
 } ensuring(res => find(res, e).get >= 0);

 @induct
 def orderInList2(l: List[Task], e: Task):List[Task] = {
    require(isSorted(l))
    sortedIns(e, l)
 } ensuring(res => find(res, res.find((a:Task) => a.id == e.id).get).get >= 0);
}

object PrettyPrinting {
   import Scheduler._

   def taskToString(t: Task) = {
      val Task(id, tick) = t
      "Task(" + id + "," + tick + ")"
   }
   def optTaskToString(o: Option[Task]) = {
      o match {
         case None() => "None"
         case Some(t) => taskToString(t)
      }
   }

   def tasksToString(tasks: List[Task]): String = {
      tasks match {
         case Nil() => "[]"
         case Cons(t, ts) => taskToString(t) + "; " + tasksToString(ts)
      }
   }


   def coreToString(c: Core): String = {
      "\n\ncurrent: " + optTaskToString(c.current) + "\n" +
      "tasks: " + tasksToString(c.tasks) + "\n\n"
   }

   def isSorted(tasks: List[Task]): Boolean = {
      tasks match {
         case Nil() => true
         case Cons(t, Nil()) => true
         case Cons(Task(_,t1), ts@Cons(Task(_,t2), _)) => t1 <= t2 && isSorted(ts)
      }
   }

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

   def contains(tasks: List[Task], v: Task): Boolean = (tasks match {
      case Cons(Task(id, tick), t) => id == v.id || contains(t, v)
      case Nil() => false
   })

   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
   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(e, l), t)
   }.holds;

   @induct
   def containsEquivLemma(l: List[Task], e:Task, t: Task) = {
      e.id == t.id ==> (contains(l, e) == contains(l, t))
   }.holds;

   @induct
   def uniquenessPreserved(e:Task, l:List[Task]):Boolean = {
      require(isSorted(l) && isUnique(l) && !contains(l, e))
      val res = sortedIns(e, l);
      isUnique(res)
      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(e, xs), t) && isUnique(res)
            else isUnique(res)
      }
   }.holds;

}