// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// A Dafny rendition of an F* version of QuickSort (included at the bottom of this file).
// Unlike the F* version, Dafny also proves termination and does not use any axioms.  However,
// Dafny needs help with a couple of lemmas in places where F* does not need them.
// Comments below show differences between the F* and Dafny versions.

datatype Pair<T, U> = P(T, U)

datatype List<T> = Nil | Cons(T, List)

function length(list: List): nat  // for termination proof
{
  match list
  case Nil => 0
  case Cons(_, tl) => 1 + length(tl)
}

// In(x, list) returns the number of occurrences of x in list
function In(x: int, list: List<int>): nat
{
  match list
  case Nil => 0
  case Cons(y, tl) => (if x == y then 1 else 0) + In(x, tl)
}

predicate SortedRange(m: int, n: int, list: List<int>)
  decreases list;  // for termination proof
{
  match list
  case Nil => m <= n
  case Cons(hd, tl) => m <= hd <= n && SortedRange(hd, n, tl)
}

function append(n0: int, n1: int, n2: int, n3: int, i: List<int>, j: List<int>): List<int>
  requires n0 <= n1 <= n2 <= n3;
  requires SortedRange(n0, n1, i) && SortedRange(n2, n3, j);
  ensures SortedRange(n0, n3, append(n0, n1, n2, n3, i, j));
  ensures forall x :: In(x, append(n0, n1, n2, n3, i, j)) == In(x, i) + In(x, j);
  decreases i;  // for termination proof
{
  match i
  case Nil => j
  case Cons(hd, tl) => Cons(hd, append(hd, n1, n2, n3, tl, j))
}

function partition(x: int, l: List<int>): Pair<List<int>, List<int>>
  ensures var P(lo, hi) := partition(x, l);
    (forall y :: In(y, lo) == if y <= x then In(y, l) else 0) &&
    (forall y :: In(y, hi) == if x < y then In(y, l) else 0) &&
    length(l) == length(lo) + length(hi);  // for termination proof
{
  match l
  case Nil => P(Nil, Nil)
  case Cons(hd, tl) =>
    var P(lo, hi) := partition(x, tl);
    if hd <= x then
      P(Cons(hd, lo), hi)
    else
      P(lo, Cons(hd, hi))
}

function sort(min: int, max: int, i: List<int>): List<int>
  requires min <= max;
  requires forall x :: In(x, i) != 0 ==> min <= x <= max;
  ensures SortedRange(min, max, sort(min, max, i));
  ensures forall x :: In(x, i) == In(x, sort(min, max, i));
  decreases length(i);  // for termination proof
{
  match i
  case Nil => Nil
  case Cons(hd, tl) =>
    assert In(hd, i) != 0;  // this proof line not needed in F*
    var P(lo, hi) := partition(hd, tl);
    assert forall y :: In(y, lo) <= In(y, i);  // this proof line not needed in F*
    var i' := sort(min, hd, lo);
    var j' := sort(hd, max, hi);
    append(min, hd, hd, max, i', Cons(hd, j'))
}

/*
module Sort

type SortedRange : int => int => list int => E
assume Nil_Sorted : forall (n:int) (m:int). n <= m <==> SortedRange n m [] 
assume Cons_Sorted: forall (n:int) (m:int) (hd:int) (tl:list int). 
               SortedRange hd m tl && (n <= hd) && (hd <= m)
          <==> SortedRange n m (hd::tl)

val append: n1:int -> n2:int{n1 <= n2} -> n3:int{n2 <= n3} -> n4:int{n3 <= n4} 
         -> i:list int{SortedRange n1 n2 i} 
         -> j:list int{SortedRange n3 n4 j}
         -> k:list int{SortedRange n1 n4 k 
                      /\ (forall x. In x k <==> In x i \/ In x j)}
let rec append n1 n2 n3 n4 i j = match i with 
  | [] -> 
    (match j with
      | [] -> j
      | _::_ -> j)
  | hd::tl -> hd::(append hd n2 n3 n4 tl j)

val partition: x:int
            -> l:list int
            -> (lo:list int
                * hi:list int{(forall y. In y lo ==> y <= x /\ In y l)
                               /\ (forall y. In y hi ==> x < y /\ In y l)
                               /\ (forall y. In y l ==> In y lo \/ In y hi)})
let rec partition x l = match l with
  | [] -> ([], [])
  | hd::tl ->
    let lo, hi = partition x tl in
    if hd <= x
    then (hd::lo, hi)
    else (lo, hd::hi)

val sort: min:int  
       -> max:int{min <= max} 
       -> i:list int {forall x. In x i ==> (min <= x /\ x <= max)}
       -> j:list int{SortedRange min max j /\ (forall x. In x i <==> In x j)}
let rec sort min max i = match i with
  | [] -> []
  | hd::tl ->
    let lo,hi = partition hd tl in
    let i' = sort min hd lo in 
    let j' = sort hd max hi in
    append min hd hd max i' (hd::j')

*/