use int.Int

type list 'a = Nil | Cons 'a (list 'a)

function append (l1:list 'a) (l2:list 'a) : list 'a =
  match l1 with
  | Nil -> l2
  | Cons x l -> Cons x (append l l2)
  end

(*

lemma append_nil: forall l:list 'a. append l Nil = l

lemma append_assoc:
  forall l1 l2 l3:list 'a.
    append (append l1 l2) l3 = append l1 (append l2 l3)
*)

function length (l:list 'a) : int =
  match l with
  | Nil -> 0
  | Cons _ r -> 1 + length r
  end

(*
lemma length_nonneg: forall l:list 'a. length l >= 0
*)

function rev (l:list 'a) : list 'a =
  match l with
  | Nil -> Nil
  | Cons x r -> append (rev r) (Cons x Nil)
  end

val ref l : list int

let rec rev_append (r:list int) : unit
  variant { ? }
  writes  { l }
  ensures { ? }
  =
  match r with
  | Nil -> ()
  | Cons x r ->
     l <- Cons x l;
     rev_append r
  end

let reverse (r:list int) : unit
  writes  { l }
  ensures { l = rev r }
  =
    l <- Nil; ?


(*
Local Variables:
compile-command: "why3 ide rev.mlw"
End:
*)