Library zoo_std.queue_2

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.option.
Require Import zoo_std.chain.
Require Export zoo_std.queue_2__code.
Require Import zoo_std.queue_2__types.
Require Import zoo.options.

Implicit Type l : location.
Implicit Type t v front back : val.
Implicit Type vs : list val.

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

  Definition queue_2 ۰ model t vs : iProp Σ :=
    ∃ l front back ,
    ⌜t = #l ⌝ ∗
    l .[front ] ↦ front ∗
    l .[back ] ↦ back ∗
    chain ۰ model (Some §Node) front vs back ∗
    chain ۰ model (Some §Node) back [()%V] ().
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %front & %back & -> & Hl_front & Hl_back & Hfront & Hback ) ".

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

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

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

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

  Lemma queue_2 ٠ pop ｰ spec t vs :
    {{{
      queue_2 ۰ model t vs
    }}}
      queue_2 ٠ pop t
    {{{
      RET head vs ;
      queue_2 ۰ model t (tail vs)
    }}}.
End zoo ۰ G.

Require zoo_std.queue_2__opaque.

#[global] Opaque queue_2 ۰ model.