From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import notation proofmode.

From lmpmc Require Import util.

Record basic_queue {Σ} `{!heapGS Σ} :=
  BasicQueue
    { new : val;
      enqueue : val;
      try_dequeue : val;

      queue_repr : loc → list val → iProp Σ;
      #[global] queue_repr_timeless ℓ vs :: Timeless (queue_repr ℓ vs);

      new_spec :
        {{{ True }}}
          new #()
        {{{ (ℓ_q : loc), RET #ℓ_q; queue_repr ℓ_q [] }}};

      enqueue_spec (ℓ_q : loc) (data : val) :
        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
            enqueue #ℓ_q data @ ∅
          <<{ queue_repr ℓ_q (vs ++ [data]) | RET #() }>>;

      try_dequeue_spec (ℓ_q : loc) :
        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs }>>
            try_dequeue #ℓ_q @ ∅
          <<{ queue_repr ℓ_q (tail vs) | RET (val_opt_hl (head vs)) }>>;
    }.
#[global] Arguments basic_queue _ {_} : assert.