Library zoo_persistent.pqueue

From zoo Require Import
  prelude.
From zoo.common Require Import
  list.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  option
  list.
From zoo_persistent Require Export
  base
  pqueue__code.
From zoo_persistent Require Import
  pqueue__types.
From zoo Require Import
  options.

Implicit Types v t : val.
Implicit Types 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.

From zoo_persistent Require
  pqueue__opaque.

#[global] Opaque pqueue_model.