module Muller

  use import int.Int
  use import module stdlib.Refint
  use import module stdlib.Array

  type param = map int
  logic pr (a : param) (n : int) = a[n] <> 0
  clone import int.NumOfParam with type param = param, logic pr = pr

  let compact (a : array int) =
    let count = ref 0 in
    for i = 0 to length a - 1 do 
      invariant { 0 <= count = num_of a 0 i <= i}
      if a[i] <> 0 then incr count
    done;
    let u = make !count 0 in
    count := 0;
    for i = 0 to length a - 1 do
      invariant { 0 <= count = num_of a 0 i <= i and 
                  length u = num_of a 0 (length a) }
      if a[i] <> 0 then begin u[!count <- a[i]]; incr count end
    done

end

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/muller.gui"
End: 
*)