Library zoo_std.queue_1

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.queue_1__code.
Require Import zoo_std.queue_1__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_1 ۰ model t vs : iProp Σ :=
    ∃ l front back ,
    ⌜t = #l ⌝ ∗
    l .[front ] ↦ front ∗
    l .[back ] ↦ back ∗
    chain ۰ model None front vs back ∗
    chain ۰ model None back [()%V] ().
  #[local] Instance : CustomIpat "model" :=
    " ( %l & %front & %back & -> & Hl_front & Hl_back & Hfront & Hback ) ".

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

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

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

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

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

Require zoo_std.queue_1__opaque.

#[global] Opaque queue_1 ۰ model.