Library zoo_std.deque

Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.deque__code.
Require Import zoo_std.deque__types.
Require Import zoo.options.

Implicit Type fn : val.

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

  Definition deque ۰ model t vs : iProp Σ :=
    ∃ nodes ,
    xdeque ۰ model t nodes ∗
    [∗ list ] node ; v ∈ nodes ; vs , node .[xdeque ٠ data ] ↦ v.

  #[global] Instance deque ۰ model ｰ timeless t vs :
    Timeless (deque ۰ model t vs).

  Lemma deque ۰ model ｰ exclusive t vs1 vs2 :
    deque ۰ model t vs1 -∗
    deque ۰ model t vs2 -∗
    False.

  Lemma deque ٠ create ｰ spec :
    {{{
      True
    }}}
      deque ٠ create ()
    {{{
      t
    , RET t ;
      deque ۰ model t []
    }}}.

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

  Lemma deque ٠ push_front ｰ spec t vs v :
    {{{
      deque ۰ model t vs
    }}}
      deque ٠ push_front t v
    {{{
      RET ();
      deque ۰ model t (v :: vs)
    }}}.

  Lemma deque ٠ push_back ｰ spec t vs v :
    {{{
      deque ۰ model t vs
    }}}
      deque ٠ push_back t v
    {{{
      RET ();
      deque ۰ model t (vs ++ [v])
    }}}.

  Lemma deque ٠ pop_front ｰ spec t vs :
    {{{
      deque ۰ model t vs
    }}}
      deque ٠ pop_front t
    {{{
      RET head vs ;
      deque ۰ model t (tail vs)
    }}}.

  Lemma deque ٠ pop_back ｰ spec t vs :
    {{{
      deque ۰ model t vs
    }}}
      deque ٠ pop_back t
    {{{
      o
    , RET o ;
      match o with
      | None ⇒
          ⌜vs = []⌝ ∗
          deque ۰ model t []
      | Some v ⇒
          ∃ vs',
          ⌜vs = vs' ++ [v]⌝ ∗
          deque ۰ model t vs'
      end
    }}}.

  Lemma deque ٠ iter ｰ spec Ψ fn t vs :
    {{{
      ▷ Ψ [] ∗
      deque ۰ model t vs ∗
      □ (
        ∀ vs_done v vs_todo ,
        ⌜vs = vs_done ++ v :: vs_todo ⌝ -∗
        Ψ vs_done -∗
        WP fn v {{ res ,
          ⌜res = ()%V⌝ ∗
          ▷ Ψ (vs_done ++ [v])
        }}
      )
    }}}
      deque ٠ iter fn t
    {{{
      RET ();
      deque ۰ model t vs ∗
      Ψ vs
    }}}.
End zoo ۰ G.

Require zoo_std.deque__opaque.

#[global] Opaque deque ۰ model.