Library zoo_persistent.pqueue

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_persistent.pqueue__code.
Require Import zoo_persistent.pqueue__types.
Require Import zoo.options.

Implicit Type v t : val.
Implicit Type back front : list val.

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

  Definition pqueue ۰ model t vs : iProp Σ :=
    ∃ front back ,
    ⌜t = (list ۰ to_val front , list ۰ to_val back )%V ∧ vs = front ++ reverse back ⌝.

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

  #[global] Instance pqueue ۰ model ｰ persistent t vs :
    Persistent (pqueue ۰ model t vs).

  Lemma pqueue ۰ model ｰ nil :
    ⊢ pqueue ۰ model pqueue ٠ empty [].

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

  Lemma pqueue ٠ push ｰ spec t vs v :
    {{{
      pqueue ۰ model t vs
    }}}
      pqueue ٠ push t v
    {{{
      t'
    , RET t';
      pqueue ۰ model t' (vs ++ [v])
    }}}.

  Lemma pqueue ٠ pop ｰ spec t vs :
    {{{
      pqueue ۰ model t vs
    }}}
      pqueue ٠ pop t
    {{{
      o
    , RET o ;
      match o with
      | None ⇒
          ⌜vs = []⌝
      | Some p ⇒
          ∃ v vs' t',
          ⌜vs = v :: vs'⌝ ∗
          ⌜p = (v , t')%V⌝ ∗
          pqueue ۰ model t' vs'
      end
    }}}.
End zoo ۰ G.

Require zoo_persistent.pqueue__opaque.

#[global] Opaque pqueue ۰ model.