Require Import List.

Require Import Ynot.

Set Implicit Arguments.

Open Local Scope hprop_scope.


Module Type LIST.
  Parameter ilist : Set -> Set.
  Parameter rep : forall elem, ilist elem -> list elem -> hprop.

  Parameter new : forall elem,
    Cmd emp (fun ils : ilist elem => rep ils nil).
  Parameter free : forall elem (ils : ilist elem),
    Cmd (rep ils nil) (fun _ : unit => emp).

  Parameter prepend : forall elem (ils : ilist elem) (x : elem) (ls : list elem),
    Cmd (rep ils ls) (fun _ : unit => rep ils (x :: ls)).
  Parameter append : forall elem (ils : ilist elem) (x : elem) (ls : list elem),
    Cmd (rep ils ls) (fun _ : unit => rep ils (ls ++ x :: nil)).
End LIST.

Module List : LIST.
  Section List.
    Variable elem : Set.

    Record node : Set := Node {
      data : elem;
      next : option ptr
    }.

    Fixpoint listRep (ls : list elem) (hptr : option ptr) {struct ls} : hprop :=
      match ls with
        | nil => [hptr = None]
        | h :: t => match hptr with
                      | None => [False]
                      | Some hptr => Exists p :@ option ptr,
                        hptr --> Node h p * listRep t p
                    end
      end.

    Definition rep (p : ptr) (ls : list elem) :=
      Exists po :@ option ptr, p --> po * listRep ls po.

    Theorem listRep_None : forall ls,
      listRep ls None ==> [ls = nil].
      destruct ls; sep fail idtac.
    Qed.

    Theorem listRep_Some : forall ls hptr,
      listRep ls (Some hptr) ==> Exists h :@ elem, Exists t :@ list elem, Exists po :@ option ptr,
        [ls = h :: t] * hptr --> Node h po * listRep t po.
      destruct ls; sep fail ltac:(try discriminate).
    Qed.

    Ltac simp_prem :=
      simpl_IfNull;
      simpl_prem ltac:(apply listRep_None || apply listRep_Some).

    Ltac simplr :=
      repeat (unfold value in *;
        match goal with
          | _ => discriminate
          | [ H : Some _ = Some _ |- _ ] => injection H; clear H; intros; subst
          | [ H : head ?x = Some _ |- _ ] => destruct x; simpl in *
        end).

    Ltac t := unfold rep; sep simp_prem simplr.
    
    Open Scope stsepi_scope.

    Definition new : Cmd emp (fun ils : ptr => rep ils nil).
      refine {{New (@None ptr)}}; t.
    Qed.

    Definition free : forall p : ptr, Cmd (rep p nil) (fun _ : unit => emp).
      refine (fun p => {{Free p}}); t.
    Qed.

    Definition prepend : forall (p : ptr) (x : elem) (ls : list elem),
      Cmd (rep p ls) (fun _ : unit => rep p (x :: ls)).
      refine (fun p x ls => hptr <- !p;
        nd <- New (Node x hptr);
        {{p ::= Some nd}}
      ); t.
    Qed.

    Lemma cons_cong : forall ls' x ls p p',
      ls' = x :: ls
      -> listRep ls p * p' --> Node x p ==> listRep ls' (Some p').
      t.
    Qed.

    Hint Resolve cons_cong.

    Definition append' : forall (x : elem) (p : option ptr) (ls : list elem),
      Cmd (listRep ls p) (fun p' : ptr => listRep (ls ++ x :: nil) (Some p')).
      refine (fun x => Fix2 (ran := fun _ _ => ptr)
        (fun (p : option ptr) (ls : list elem) =>
          listRep ls p)
        (fun (p : option ptr) (ls : list elem) (p' : ptr) =>
          listRep (ls ++ x :: nil) (Some p'))
        (fun self p ls =>
          IfNull p Then
            {{New (Node x None)}}
          Else
            nd <- !p;
            p' <- self (next nd) (tail ls)
              <@> ([head ls = Some (data nd)] * p --> Node (data nd) (next nd));
            p ::= Node (data nd) (Some p');;
            {{Return p}})); t.
    Qed.

    Definition append : forall (p : ptr) (x : elem) (ls : list elem),
      Cmd (rep p ls) (fun _ : unit => rep p (ls ++ x :: nil)).
      refine (fun p x ls =>
        p' <- !p;
        p'' <- append' x p' ls <@> _;
        {{p ::= Some p''}}); (t; t).
    Qed.
  End List.

  Definition ilist (_ : Set) := ptr.
End List.

Recursive Extraction List.