module Implementation

use import int.Int
use import int.ComputerDivision
(*use import map.Map*)

use import heap_model.Model
use import bag_of_integers.Bag_integers
use import elements.Elements
use import heap.Heap

lemma Is_heap_min:
  forall a:map, n :int. n > 0 ->
    is_heap_array a 0 n -> a[0] = min_bag (model (a, n))

use import module ref.Ref

(* implementation of heaps *)
let create () : ref logic_heap =
  { true }
    let x = (A.const 0, 0) in ref x
  { is_heap !result /\
    model !result = empty_bag }

exception Break

let insert (this : ref logic_heap) (e : int) : unit  =
{ is_heap !this }
  let (a, n) = !this in
  let arr = ref a in
  let i = ref n in
  try
  while (!i > 0) do
    invariant {
      0 <= !i <= n /\
      (!i = n ->
         is_heap_array !arr 0 n  /\
         model (!arr, n) = model (a, n)) /\
      (!i < n ->
         is_heap_array !arr 0 (n + 1) /\
         !arr[!i] > e /\
         model (!arr, n+1) = add !arr[!i] (model (a, n)))
    }
    variant { !i }
    let parent = div (!i - 1) 2 in
    let p = A.get !arr parent in
    if (e >= p) then raise Break;
    arr := !arr[!i<-p];
    i := parent
  done
  with Break -> ()
  end;
  arr := !arr[!i<-e];
  this := (!arr, n + 1);
  assert { 0 < !i < n -> is_heap !this };
  assert { !i < n -> model !this = add e (model (a,n)) } 
{ is_heap !this /\
    model !this = add e (model (old !this)) }

let extractMin (this : ref logic_heap) : int =
{ model !this <> empty_bag /\ is_heap !this }
  let (a, n) = !this in
  assert {n > 0};
  let min = a[0] in
  let n' = n-1 in
  let last = a[n'] in
  assert { n' > 0 -> nb_occ last (diff (model (a,n))
                        (singleton min)) > 0 } ;
  let arr = ref a in
  let i = ref 0 in
  try
    while ( !i < n') do
      invariant {
        0 <= !i /\
        (n' > 0 -> !i < n') /\
        is_heap_array !arr 0 n' /\
        (!i = 0 -> !arr = a) /\
        (n' > 0 ->
          elements !arr 0 n' =
            add !arr[!i] (diff (diff (model (a,n))
                 (singleton last))
               (singleton min))) /\
        (!i > 0 -> !arr[parent !i] < last) }
      variant {n' - !i}
      let left = 2 * !i + 1 in
      let right = 2 * !i + 2 in
      if (left >= n') then raise Break;
      let smaller = ref left in
      if right < n' then
        if !arr[left] > !arr[right]
          then smaller := right;
      if last <= !arr[!smaller] then raise Break;
      arr := !arr[!i <- !arr[!smaller]];
      i := !smaller
    done;
    assert { n' = 0 }
  with Break -> ()
  end;
  if !i < n' then
    begin
      arr := !arr[!i <- last];
      assert { !i > 0 -> is_heap_array !arr 0 n' };
      assert { is_heap_array !arr 0 n' };
      assert { n' > 0 -> elements !arr 0 n' =
                  (diff (model (a,n)) (singleton min)) }
    end;
  this := (!arr, n');
  min
{ is_heap !this /\
  result = min_bag (model (old !this)) /\
  model (old !this) = add result (model !this) }

(*

let extractMin0 (this : ref logic_heap) : int =
{ model !this <> empty_bag }
  let (a, n) = !this in
  assert {n > 0};
  let min = a[0] in
  let n' = n-1 in
  let last = a[n'] in
  assert { n' > 0 -> nb_occ last (diff (model (a,n))
                        (singleton min)) > 0 } ;
  let arr = ref a in
  let i = ref 0 in
  try
    while ( !i < n') do
      invariant {
        0 <= !i /\
        (n' > 0 -> !i < n') /\
        (!i = 0 -> !arr = a) /\
        (n' > 0 ->
          elements !arr 0 n' =
            add !arr[!i] (diff (diff (model (a,n))
                 (singleton last))
               (singleton min))) /\
        (!i > 0 -> !arr[parent !i] < last) }
      variant {n' - !i}
      let left = 2 * !i + 1 in
      let right = 2 * !i + 2 in
      if (left >= n') then raise Break;
      let smaller = ref left in
      if right < n' then
        if !arr[left] > !arr[right]
          then smaller := right;
      if last <= !arr[!smaller] then raise Break;
      arr := !arr[!i <- !arr[!smaller]];
      i := !smaller
    done;
    assert { n' = 0 }
  with Break -> ()
  end;
  if !i < n' then
    begin
      arr := !arr[!i <- last];
      assert { n' > 0 -> elements !arr 0 n' =
                  (diff (model (a,n)) (singleton min)) }
    end;
  this := (!arr, n');
  min
{ model !this = diff (model (old !this)) (singleton result) }
*)

end

(*
Local Variables:
compile-command: "why3ide -I . heap_implem.mlw"
End:
*)