(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 In-place Linked List Reversal} *)


theory ListReverse

  use export int.Int
  use export list.List
  use export list.HdTlNoOpt

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

  let rec lemma append_nil (l:list 'a)
    variant { l }
    ensures { append l Nil = l }
  = match l with
    | Nil -> ()
    | Cons _ t -> append_nil t
    end

  let rec lemma append_assoc (l1 l2 l3:list 'a)
    variant { l1 }
    ensures { append (append l1 l2) l3 = append l1 (append l2 l3) }
  = match l1 with
    | Nil -> ()
    | Cons _ t -> append_assoc t l2 l3
    end

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

  predicate mem (x:'a) (l:list 'a) =
    match l with
    | Nil -> false
    | Cons y r -> x=y \/ mem x r
    end

  predicate disjoint (l1:list 'a) (l2:list 'a) =
    forall x:'a. not (mem x l1 /\ mem x l2)

  predicate no_repet (l:list 'a) =
    match l with
    | Nil -> true
    | Cons x r -> not (mem x r) /\ no_repet r
    end

end







module InPlaceRev

  use ListReverse

  type loc

  val eq_loc (l1 l2:loc) : bool
    ensures { result <-> l1=l2 }

  val constant null:loc

  function store (f:'a->'b) (i:'a) (v:'b) : 'a -> 'b =
    fun j -> if i=j then v else f j

  val acc (ref field: loc -> 'a) (l:loc) : 'a
    requires { l <> null }
    reads { field }
    ensures { result = field l }

  val upd (ref field: loc -> 'a) (l:loc) (v:'a) : unit
    requires { l <> null }
    writes { field }
    ensures { field = store (old field) l v }


  predicate list_seg (p:loc) (next: loc -> loc) (l:list loc) (q:loc) =
    match l with
    | Nil -> p=q
    | Cons h t -> p <> null /\ h=p /\ list_seg (next p) next t q
    end









(*

  lemma empty_list : forall next: loc -> loc, q:loc, l: list loc.
    list_seg null next l q -> l = Nil

  lemma list_seg_no_repet:
    forall next: loc -> loc, p: loc, pM:list loc.
      list_seg p next pM null -> no_repet pM

  lemma list_seg_frame:
    forall next1 next2: loc -> loc, p q v: loc, pM:list loc.
      list_seg p next1 pM null /\ next2 = store next1 q v /\
      not (mem q pM) -> list_seg p next2 pM null

*)










  val ref next : loc -> loc

  let reverse (l:loc) (ghost lM:list loc) : loc
    requires { list_seg l next lM null }
    ensures { list_seg result next (rev lM) null }
  =
    let ref p = l in
    let ref r = null in
    while not (eq_loc p null) do
      variant { 0 }
      let n = acc next p in
      upd next p r;
      r <- p;
      p <- n;
    done;
    r

end



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