Library zoo_std.xdeque

Require Import zoo.prelude.
Require Import zoo.common.option.
Require Import zoo.common.list.
Require Import zoo.base.
Require Import zoo_std.option.
Require Import zoo_std.xdlchain.
Require Export zoo_std.xdeque__code.
Require Import zoo_std.xdeque__types.
Require Import zoo.options.

Implicit Type l node : location.
Implicit Type nodes : list location.
Implicit Type fn : val.

Section zoo ۰ G.
  Context `{zoo ۰ G : !ZooG Σ}.

  Definition xdeque ۰ model t nodes : iProp Σ :=
    ∃ l ,
    ⌜t = #l ⌝ ∗
    l .[prev ] ↦ from_option #@{location } t (last nodes) ∗
    l .[next ] ↦ from_option #@{location } t (head nodes) ∗
    xdlchain t nodes t.

  #[global] Instance xdeque ۰ model ｰ timeless t nodes :
    Timeless (xdeque ۰ model t nodes).

  Lemma xdeque ۰ model ｰ exclusive t nodes1 nodes2 :
    xdeque ۰ model t nodes1 -∗
    xdeque ۰ model t nodes2 -∗
    False.

  Lemma xdeque ۰ model ｰ NoDup t nodes :
    xdeque ۰ model t nodes ⊢
    ⌜NoDup nodes ⌝.

  Lemma xdeque ٠ create ｰ spec :
    {{{
      True
    }}}
      xdeque ٠ create ()
    {{{
      t
    , RET t ;
      (∃ l , ⌜t = #l ⌝ ∗ meta_token l ⊤) ∗
      xdeque ۰ model t []
    }}}.

  Lemma xdeque ٠ is_empty ｰ spec t nodes :
    {{{
      xdeque ۰ model t nodes
    }}}
      xdeque ٠ is_empty t
    {{{
      RET #(bool_decide (nodes = []%list));
      xdeque ۰ model t nodes
    }}}.

  #[local] Lemma xdeque ٠ link ｰ spec node1 v1 node2 v2 :
    {{{
      node1 .[next ] ↦ v1 ∗
      node2 .[prev ] ↦ v2
    }}}
      xdeque ٠ link #node1 #node2
    {{{
      RET ();
      node1 .[next ] ↦ #node2 ∗
      node2 .[prev ] ↦ #node1
    }}}.

  Lemma xdeque ٠ push_front ｰ spec t nodes node prev next :
    {{{
      xdeque ۰ model t nodes ∗
      node .[prev ] ↦ prev ∗
      node .[next ] ↦ next
    }}}
      xdeque ٠ push_front t #node
    {{{
      RET ();
      xdeque ۰ model t (node :: nodes)
    }}}.

  Lemma xdeque ٠ push_back ｰ spec t nodes node prev next :
    {{{
      xdeque ۰ model t nodes ∗
      node .[prev ] ↦ prev ∗
      node .[next ] ↦ next
    }}}
      xdeque ٠ push_back t #node
    {{{
      RET ();
      xdeque ۰ model t (nodes ++ [node])
    }}}.

  Lemma xdeque ٠ pop_front ｰ spec t nodes :
    {{{
      xdeque ۰ model t nodes
    }}}
      xdeque ٠ pop_front t
    {{{
      RET #*@{location } $ head nodes : option val ;
      xdeque ۰ model t (tail nodes)
    }}}.

  Lemma xdeque ٠ pop_back ｰ spec t nodes :
    {{{
      xdeque ۰ model t nodes
    }}}
      xdeque ٠ pop_back t
    {{{
      o
    , RET #*@{location } o : option val ;
      match o with
      | None ⇒
          ⌜nodes = []⌝ ∗
          xdeque ۰ model t []
      | Some node ⇒
          ∃ nodes',
          ⌜nodes = nodes' ++ [node]⌝ ∗
          xdeque ۰ model t nodes'
      end
    }}}.

  Lemma xdeque ٠ remove ｰ spec {t nodes} i node :
    nodes !! i = Some node →
    {{{
      xdeque ۰ model t nodes
    }}}
      xdeque ٠ remove #node
    {{{
      RET ();
      xdeque ۰ model t (delete i nodes)
    }}}.

  #[local] Lemma xdeque ٠ iter_aux ｰ spec Ψ i fn l nodes node :
    (nodes ++ [l]) !! i = Some node →
    {{{
      ▷ Ψ (take i nodes) ∗
      xdeque ۰ model #l nodes ∗
      □ (
        ∀ nodes_done node nodes_todo ,
        ⌜nodes = nodes_done ++ node :: nodes_todo ⌝ -∗
        Ψ nodes_done -∗
        WP fn #node {{ res ,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (nodes_done ++ [#node ])
        }}
      )
    }}}
      xdeque ٠ iter_aux fn #l #node
    {{{
      RET ();
      xdeque ۰ model #l nodes ∗
      Ψ nodes
    }}}.
  Lemma xdeque ٠ iter ｰ spec Ψ fn t nodes :
    {{{
      ▷ Ψ [] ∗
      xdeque ۰ model t nodes ∗
      □ (
        ∀ nodes_done node nodes_todo ,
        ⌜nodes = nodes_done ++ node :: nodes_todo ⌝ -∗
        Ψ nodes_done -∗
        WP fn #node {{ res ,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (nodes_done ++ [#node ])
        }}
      )
    }}}
      xdeque ٠ iter fn t
    {{{
      RET ();
      xdeque ۰ model t nodes ∗
      Ψ nodes
    }}}.
End zoo ۰ G.

Require zoo_std.xdeque__opaque.

#[global] Opaque xdeque ۰ model.