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

From lmpmc Require Import util.

Record lmpmc_queue_hl :=
  LmpmcQueueHl
    { new : val;
      enqueue : val;
      try_dequeue : val;
      link : val;
    }.

Record lmpmc_queue_iris {Σ} `{!heapGS Σ} (hl : lmpmc_queue_hl) :=
  LmpmcQueueIris
    { queue_repr : loc → loc → list val → iProp Σ;
      #[global] queue_repr_timeless ℓ_deq ℓ_enq vs :: Timeless (queue_repr ℓ_deq ℓ_enq vs);

      new_spec :
        {{{ True }}}
          hl.(new) #()
        {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}};

      enqueue_spec (ℓ_enq : loc) (data : val) :
        ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
            hl.(enqueue) #ℓ_enq data @ ∅
          <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>;

      try_dequeue_spec (ℓ_deq : loc) :
        ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>>
            hl.(try_dequeue) #ℓ_deq @ ∅
          <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>;

      (** Linking two queues:
       *     _______________      _______________
       *    /      Q1       \    /       Q2      \
       *    ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2
       *    \          \ link op args /          /
       *     \          \____________/          /
       *      \            Q1 <> Q2            /
       *       \______________________________/
       *)
      link_spec (ℓ_enq1 ℓ_deq2 : loc) :
        ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗
                            if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>>
            hl.(link) #ℓ_enq1 #ℓ_deq2 @ ∅
          <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>;
    }.
#[global] Arguments lmpmc_queue_iris _ {_} _ : assert.