/*
   2. Implement insertion sort:
   
(a) implemented a method to swap two elements in an array.

   (b) implement a method insert that takes an array of integers, a position n into the array, assumes the range between 0 and n - 1 is sorted, and inserts the element at position n into the right place;

       pozitia n
           v
   1 4 5 8 3 7 10 2
   ^^^^^^^
   prefix cunoscut ca fiind sortat


   1 4 5 8 3    7 10 2
   1 4 5 3 8    7 10 2
   1 4 3 5 8    7 10 2
   1 3 4 5 8    7 10 2

   a b c   d e f
   a b d   c e f
   
   a <= b <= c
   d <= e <= f
   c > d
   ------------/
   d <= c <= e <= f
   -----------//
   

   
   1 4 5 8 3 7 10 2              (*) 3
   1 4 5 8 8 7 10 2
   1 4 5 5 8 7 10 2
   1 4 4 5 8 7 10 2
   1 3 4 5 8 7 10 2
   
   


(c) implement a method insertSort to sort an array by repeated calls to insert.

 */

method swap(a : array<int>, p : int, q : int)
  requires 0 <= p < a.Length && 0 <= q < a.Length
  modifies a
  ensures forall i :: 0 <= i < a.Length && i != p && i != q ==> a[i] == old(a[i])
  ensures a[p] == old(a[q])
  ensures a[q] == old(a[p])
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  var temp := a[p];
  a[p] := a[q];
  a[q] := temp;
}

method asdf()
{
  var x : multiset<int> := multiset{ 1, 3, 1 };
  var y : multiset<int> := multiset{ 1, 3, 1, 1 };
  var x' : set<int> := { 1, 3, 1 };
  var y' : set<int> := { 1, 3, 1, 1 };
  assert x != y;
  assert x' == y';
  assert x < y;
  assert x' <= y';
}


method insert(a : array<int>, n : int)
  requires 0 <= n < a.Length
  requires forall i, j :: 0 <= i < j < n ==> a[i] <= a[j] // sortat prefixul de lungime n
  modifies a
  ensures forall i, j :: 0 <= i < j <= n ==> a[i] <= a[j] // sortat prefixul de lungime n + 1
  ensures forall i :: n < i < a.Length ==> a[i] == old(a[i])
  // // metoda nu schimba sufixul (dupa pozitia n)
  ensures multiset(a[..]) == multiset(old(a[..]))
  // // metoda pastreaza toate elementele (inclusiv multiplicitatile lor)
  // // dar le pune, potential, in alta ordine
{
  var i := n;
  while (i > 0 && a[i - 1] > a[i])
    invariant forall i', j' :: 0 <= i' < j' <= n ==> a[i'] <= a[j'] || j' == i // (*)
    invariant forall i :: n < i < a.Length ==> a[i] == old(a[i])
    invariant multiset(a[..]) == multiset(old(a[..]))
  {
    swap(a, i - 1, i);
    i := i - 1;
  }  
}

method insertSort(a : array<int>)
  modifies a
  ensures forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures multiset(a[..]) == old(multiset(a[..]))
{
  for i := 0 to a.Length
    invariant forall i', j' :: 0 <= i' < j' < i ==> a[i'] <= a[j']
    invariant multiset(a[..]) == old(multiset(a[..]))
  {
    insert(a, i);
  }
}

method bubbleSort(a : array<int>)
  modifies a
  //ensures forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures multiset(a[..]) == old(multiset(a[..]))
{  
  if a.Length <= 1 {
    return;
  }
  var done : bool := false;
  var n := 0;
  while (!done)
    invariant 0 <= n <= a.Length
    invariant multiset(a[..]) == old(multiset(a[..]))
    invariant forall i, j :: a.Length - n <= i < j < a.Length ==> a[i] <= a[j]
    // ultimele n elemente sunt in ordine crescatoare
    invariant forall i', j' :: 0 <= i' < a.Length - n <= j' < a.Length  ==>
    a[i'] <= a[j']
    // primele a.Length - n elemente sunt mai mici decat ultimele n
    decreases a.Length - n
  {
    assume false;
    done := true;
    for i := 0 to a.Length - 1
      invariant multiset(a[..]) == old(multiset(a[..]))
      invariant forall j :: 0 <= j < i ==> a[j] <= a[i]
      invariant i < a.Length - n ==> forall k :: a.Length - n <= k < a.Length ==> a[i] <= a[k]
      // a[i] este maximum dintre a[0..i+1]
      invariant forall i, j :: a.Length - n <= i < j < a.Length ==> a[i] <= a[j]
      invariant forall i', j' :: 0 <= i' < a.Length - n <= j' < a.Length  ==>
      a[i'] <= a[j']
    {
      if (a[i] > a[i + 1]) {
        assert i + 1 < a.Length - n;
        swap(a, i, i + 1);
        done := false;
      }
    }
    n := n + 1;
  }
}


/*

   10 5 8 3 2

   5 10 8 3 2
   5 8 10 3 2
   5 8 3 10 2
   5 8 3 2 10
           ^^

   invariant forall i', j' :: 0 <= i' < a.Length - n <= j' < a.Length  ==>  a[i'] <= a[j']

   { 5 8 3 2 } <= { 10 }
   { 5 3 8 2 } <= { 10 }

   { 5 3 2 } <= { 8 10 }
   
   
   5 8 3 2 10
   5 8 3 2 10
   5 3 8 2 10
   5 3 2 8 10
         ^^^^
   
   5 3 2 8 10
   3 5 2 8 10
   3 2 5 8 10
       ^^^^^^
   
   3 2 5 8 10
   2 3 5 8 10
     ^^^^^^^^
   
   
   
   */

method Main()
{
  var a : array<int> := new int [ ] [ 1, 4, 5, 8, 3, 7, 10, 2 ];
  insert(a, 4);
  print a[..];
//    1 4 5 8 3 7 10 2
}

method merge(a : array<int>, b : array<int>) returns (r : array<int>)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  requires forall i, j :: 0 <= i < j < b.Length ==> b[i] <= b[j]
  ensures forall i, j :: 0 <= i < j < r.Length ==> r[i] <= r[j]
{
  /*

     1 3 6 7 10
     x x
     
     4 8 11
     x 

     1 3 4
     
     */
  r := new int [ a.Length + b.Length ];
  var i := 0;
  var j := 0;
  var k := 0;
  while (i < a.Length && j < b.Length)
    invariant k == i + j
    invariant 0 <= i <= a.Length
    invariant 0 <= j <= b.Length
    invariant forall i, j :: 0 <= i < j < k ==> r[i] <= r[j]
    invariant forall i', l' :: 0 <= i' < k && i <= l' < a.Length ==> r[i'] <= a[l']
    invariant forall i', l' :: 0 <= i' < k && j <= l' < b.Length ==> r[i'] <= b[l']
  {
    if (a[i] < b[j]) {
      r[k] := a[i];
      i := i + 1;
    } else {
      r[k] := b[j];
      j := j + 1;
    }
    k := k + 1;
  }
  while (i < a.Length)
    invariant 0 <= i <= a.Length
    invariant k == i + j
    invariant forall i, j :: 0 <= i < j < k ==> r[i] <= r[j]
    invariant forall i', l' :: 0 <= i' < k && i <= l' < a.Length ==> r[i'] <= a[l']
    invariant forall i', l' :: 0 <= i' < k && j <= l' < b.Length ==> r[i'] <= b[l']
  {
    r[k] := a[i];
    i := i + 1;
    k := k + 1;
  }
  while (j < b.Length)
    invariant 0 <= j <= b.Length
    invariant k == i + j
    invariant forall i, j :: 0 <= i < j < k ==> r[i] <= r[j]
    invariant forall i', l' :: 0 <= i' < k && i <= l' < a.Length ==> r[i'] <= a[l']
    invariant forall i', l' :: 0 <= i' < k && j <= l' < b.Length ==> r[i'] <= b[l']
  {
    r[k] := b[j];
    j := j + 1;
    k := k + 1;
  }
}

method mergeSort()
{
}