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

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


module ListAppend

  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 _ r -> append_nil r
    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 _ r -> append_assoc r l2 l3
   end

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

  let rec lemma length_non_neg (l:list 'a)
    variant { l }
    ensures { length l >= 0 }
  = match l with
    | Nil -> ()
    | Cons _ t -> length_non_neg 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

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

  let rec lemma mem_append (x:'a) (l1 l2:list 'a)
    variant { l1 }
    ensures { mem x (append l1 l2) <-> mem x l1 \/ mem x l2 }
  = match l1 with
    | Nil -> ()
    | Cons _ r -> mem_append x r l2
    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

  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

end



module InPlaceAppend

  use ListAppend

  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

  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

  let ghost head_in_model (p:loc) (next:loc -> loc) (l: list loc)
    requires { p <> null }
    requires { list_seg p next l null }
    ensures { mem p l }
  = match l with
    | Nil -> absurd
    | Cons _ _ -> ()
    end

  let rec lemma list_seg_frame_ext (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_ext next1 next2 (next1 p) q r v t
    end

  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 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
         let (l1,l2) = mem_decomp h t in
         list_seg_sublistl next (Cons h l1) l2 p h;
         list_seg_functional next pM (Cons h l2) p;
         assert { length pM > length (Cons h l2) }
      else
        list_seg_no_repet next (next p) t
    end

  let rec lemma list_seg_append (next: loc -> loc) (p q r: loc) (pM qM:list loc)
    requires { list_seg p next pM q }
    requires { list_seg q next qM r }
    variant  { pM }
    ensures  { list_seg p next (append pM qM) r }
  = ()

  val ref next : loc -> loc

  let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc
    requires { true }
    ensures { true }
  =
    if eq_loc l1 null then l2 else
    let ref p = l1 in
    while not (eq_loc (acc next p) null) do
      variant { 0 }
      p <- acc next p
    done;
    upd next p l2;
    l1

end






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