(** {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 length (l:list 'a) : int =
    match l with
    | Nil -> 0
    | Cons _ r -> 1 + length r
    end

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

  let rec lemma length_append (l1 l2:list 'a)
    variant { l1 }
    ensures { length (append l1 l2) = length l1 + length l2 }
  = match l1 with
    | Nil -> ()
    | Cons _ t -> length_append t l2
    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









  (** Trivial lemma, we need to state it explicitly to help provers
      prove the post-condition from the loop invariant *)

  let lemma empty_list (next:loc -> loc) (q:loc) (l: list loc)
    requires { list_seg null next l q }
    ensures { l = Nil }
  = match l with
    | Nil -> ()
    | Cons _ _ -> absurd
    end

  (** Frame lemma for [list_seg] predicate *)

  let rec lemma list_seg_frame (next1 next2:loc -> loc)
    (p q r v: loc) (pM:list loc)
    requires { list_seg p next1 pM r }
    requires { next2 = store next1 q v }
    requires { not (mem q pM) }
    variant  { pM }
    ensures  { list_seg p next2 pM r }
  = match pM with
    | Nil -> ()
    | Cons h t ->
       assert { p = h };
       list_seg_frame next1 next2 (next1 p) q r v t
    end


  (* no repetition property in a null-terminated list,
     requires auxiliary lemmas:
     1) unicity of the model list
     2) extraction of a sub-list segment
     3) a general lemma 'mem_decomp' on pure lists
  *)

  let rec lemma list_seg_functional (next:loc -> loc) (l1 l2:list loc) (p: loc)
    requires { list_seg p next l1 null }
    requires { list_seg p next l2 null }
    variant  { l1 }
    ensures  { l1 = l2 }
  = match l1,l2 with
    | Nil, Nil -> ()
    | Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (next p)
    | _ -> absurd
    end

  let rec lemma list_seg_sublistl (next:loc -> loc) (l1 l2:list loc) (p q: loc)
    requires { list_seg p next (append l1 (Cons q l2)) null }
    variant { l1 }
    ensures { list_seg q next (Cons q l2) null }
  = match l1 with
    | Nil -> ()
    | Cons _ r -> list_seg_sublistl next r l2 (next p) q
    end

  let rec ghost mem_decomp (x: 'a) (l: list 'a) : (list 'a, list 'a)
    requires { mem x l }
    variant  { l }
    returns { (l1,l2) -> l = append l1 (Cons x l2) }
  = match l with
    | Nil -> absurd
    | Cons h t -> if pure { h = x } then (Nil,t) else
       let (r1,r2) = mem_decomp x t in (Cons h r1,r2)
    end


  let rec lemma list_seg_no_repet (next:loc -> loc) (p: loc) (pM:list loc)
    requires { list_seg p next pM null }
    variant  { pM }
    ensures  { no_repet pM }
  = match pM with
    | Nil -> ()
    | Cons h t ->
      if mem h t then
         (* if h occurs in t, we want to prove 'false' *)
         (* since h is in t, t can be decomposed into
            l1++h++l2 *)
         let (l1,l2) = mem_decomp h t in
         (* then there is a list segment from h to null
            whose model is h++l2 *)
         list_seg_sublistl next (Cons h l1) l2 p h;
         (* but pM is also a path from h to null, so
            unicity implies pM = h++l2 *)
         list_seg_functional next pM (Cons h l2) p;
         (* a contradiction, because of lengths *)
         assert { length pM > length (Cons h l2) }
      else
        list_seg_no_repet next (next p) t
    end










  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 ghost ref pM = lM in
    let ref r = null in
    let ghost ref rM = Nil in
    while not (eq_loc p null) do
      invariant { list_seg p next pM null }
      invariant { list_seg r next rM null }
      invariant { append (rev pM) rM = rev lM }
      invariant { disjoint rM pM }
      variant  { pM }
        let n = acc next p in
        upd next p r;
        r <- p;
        p <- n;
        rM <- Cons (hd pM) rM;
        pM <- tl pM
    done;
    r

end



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