// ---------------------------------------------------------
// Sorting lists by the Merge Sort Algorithm
// ---------------------------------------------------------

//****************************************
//CONSTANTS
//****************************************
val M:ℕ;
val N:ℕ;

//****************************************
//VARIABLES
//****************************************
type nat = ℕ[M];
type index = ℕ[N-1];
type array = Array[N,nat];
rectype(N) list = nil | cons(nat,list);

//****************************************
//SUPPORTING FUNCTIONS
//****************************************
//listLength(a:list)
//  returns the length of a list
fun listLengthRec(a:list,out:ℕ[N]):ℕ[N]
  decreases N-out;
= match a with
  {
    nil -> out;
    cons(elem:nat,rem:list) -> listLengthRec(rem,out+1);
  };
fun listLength(a:list):ℕ[N] = listLengthRec(a,0);

//toArray(a:list):array
//  returns an array representation of a list
//  empty slots get filled with 0.
proc toArray(a:list):array
{
  var out:array ≔ Array[N,nat](0);
  var b:list ≔ a;
  for var i:ℤ[-1,N-1] ≔ N-1; i ≥ 0; i ≔ i-1 do
  {
    match b with
    {
      nil -> ;
      cons(elem:nat,rem:list) ->
      {
        out[i] ≔ elem;
        b ≔ rem;
      }
    }
  }
  return out;
}

//append(a:list,b:list)
//  appends b to a
fun append(a:list,b:list):list
  decreases listLength(a);
= match a with
  {
    nil -> b;
    cons(elem:nat,rem:list) ->
      list!cons(elem,append(rem,b));
  };
  
//merge(a:list,b:list):list
//  merging two lists
fun merge(a:list,b:list):list
  decreases listLength(a) + listLength(b);
= match a with
  {
    nil -> b;
    cons(elem_a:nat,rem_a:list) ->
      match b with
      {
        nil -> a;
        cons(elem_b:nat,rem_b:list) ->
          if elem_a > elem_b then
            list!cons(elem_a,merge(rem_a,b))
          else
            list!cons(elem_b,merge(a,rem_b));
      };
  };
    
fun split(a:list,out1:list,out2:list):Tuple[list,list]
  decreases listLength(a)+1;
= match a with
  {
    nil -> ⟨out1,out2⟩;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> ⟨list!cons(elem,out1),out2⟩;
        cons(elem2:nat,rem2:list) ->
          split(
            rem2,list!cons(elem,out1),list!cons(elem2,out2)
          );
      };
  };

fun split(a:list):Tuple[list,list]
  = split(a,list!nil,list!nil);
  
//****************************************
//SUPPORTING STATEMENTS
//****************************************
//isSorted(a:list)
//  returns if all elements of a are sorted
//  (high in front, low at the back)
pred isSorted(a:list)
  decreases listLength(a);
⇔ match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) ->
    match rem with
    {
      nil -> true;
      cons(elem2:nat,rem2:list) ->
        elem2 ≤ elem ∧ isSorted(rem);
    };
  };

//isPermutationOf(a:array,b:array)
//  returns if a is a permutation of b
pred isPermutationOf(a:array,b:array)
⇔ ∃p:Array[N,index].
    (∀i:index,j:index. i ≠ j ⇒ p[i] ≠ p[j])
    ∧ (∀i:index. a[i] = b[p[i]]);

//****************************************
//CONDITIONS
//****************************************
//pre-Condition
//  (*) true
pred pre(a:list) ⇔ true;

//post-Condition
//  (*) result is sorted
//  (*) result is a permutation of a
pred post(a:list,result:list)
⇔ listLength(a) = listLength(result)
  ∧ isSorted(result)
  ∧ isPermutationOf(toArray(a),toArray(result));

//pre-Condition for the merge algorithm
//  (*) a and b are sorted
//  (*) the length of the combined list a+b is not bigger N
pred pre_merge(a:list,b:list)
⇔ isSorted(a)
  ∧ isSorted(b)
  ∧ listLength(a)+listLength(b) ≤ N;

//post-Condition for the merge algorithm
//  (*) result is a permutation of the list (a,b)
//  (*) result is sorted
pred post_merge(a:list,b:list,result:list)
⇔ listLength(result) = listLength(a)+listLength(b)
  ∧ isPermutationOf(toArray(result),toArray(append(a,b)))
  ∧ isSorted(result);

//termination term for the merge sort algorithm
// lenth of the list
fun termin(a:list):ℕ[N+1] = listLength(a)+1;

//****************************************
//FUNCTION SPECIFICATIONS
//****************************************
//Function Specification 1
//   given the precondition,
//   (*) all preconditions of the subfunctions hold.
theorem FS_pre(a:list)
  requires pre(a);
⇔ match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> true;
        cons(elem2:nat,rem2:list) ->
          pre(split(a).1)
          ∧ pre(split(a).2)
          ∧ ∀b:list.post(split(a).1,b)
          ⇒ ∀c:list.post(split(a).2,c)
          ⇒ pre_merge(b,c);
      };
  };

//Function Specification 2
//  given the precondition,
//  (*) the postcondition holds given that all subfunctions
//      can be defined by there postconditions.
theorem FS_post(a:list)
  requires pre(a);
⇔ match a with
  {
    nil -> post(a,a);
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> post(a,a);
        cons(elem2:nat,rem2:list) ->
          ∀b:list.post(split(a).1,b)
          ⇒ ∀c:list.post(split(a).2,c)
          ⇒ ∀d:list.post_merge(b,c,d)
          ⇒ post(a,d);
      };
  };

//Function Specification 3
//  given the precondition,
//  (*) the termination term always positive or zero
//  (*) each recursion reduces the termination term
theorem FS_termination(a:list)
  requires pre(a);
⇔ termin(a) ≥ 0
  ∧ match a with
  {
    nil -> true;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> true;
        cons(elem2:nat,rem2:list) ->
          (
            ∀b:list.post(split(a).1,b)
            ⇒ termin(b) < termin(a)
          )
          ∧ (
            ∀c:list.post(split(a).2,c)
            ⇒ termin(c) < termin(a)
          );
      };
  };

//****************************************
//  IMPLEMENTATION
//****************************************
fun mergeSort(a:list):list
  requires pre(a);
  ensures post(a,result);
  decreases termin(a);
= match a with
  {
    nil -> a;
    cons(elem:nat,rem:list) ->
      match rem with
      {
        nil -> a;
        cons(elem2:nat,rem2:list) ->
          merge(
            mergeSort(split(a).1),
            mergeSort(split(a).2)
          );
      };
  };