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

From lmpmc Require Import util.

(* Doing this split because I don't know how to otherwise get a nice
   closed proof. *)

Record fin_queue_hl :=
  FinQueueHl
    { new : val;
      enqueue : val;
      finalize : val;
      try_dequeue : val;}.
Record fin_queue_iris {Σ} `{!heapGS Σ} (hl : fin_queue_hl) :=
  FinQueueIris
    { (** If [⊢ queue_repr ℓ vs mfin], then there is a queue at [ℓ]
          which currently holds the values [vs], and possibly a final
          value [mfin]. The dequeue and enqueue operations work in
          FIFO fashion, with [head vs] (if any) representing the next
          value that would be dequeued by a [try_dequeue ℓ] operation.

          Only non-finalized queues can be enqueued in. Non-finalized queues
          can be finalized using the [finalize ℓ v] operation, which sets
          [mfin] to [v]. Subsequent [try_dequeue ℓ] operations then first
          dequeue the remainder of [vs]; when [vs] is empty, they return [mfin]
          (but, critically, do not unset it). *)
      queue_repr : loc → list val → option val → iProp Σ;
      #[global] queue_repr_timeless ℓ vs mfin :: Timeless (queue_repr ℓ vs mfin);

      (** If [⊢ queue_fin ℓ v], then the queue at [ℓ] has been
          finalized and all elements except for the final element [v]
          have been dequeued.

          Queues that enter this state never leave this state; this
          allows [queue_fin ℓ v] to be a persistent proposition. *)
      queue_fin : loc → val → iProp Σ;
      #[global] queue_fin_persistent ℓ v :: Persistent (queue_fin ℓ v);
      #[global] queue_fin_timeless ℓ v :: Timeless (queue_fin ℓ v);
      queue_fin_obtain ℓ fin : queue_repr ℓ [] (Some fin) -∗ queue_fin ℓ fin;
      queue_fin_agree ℓ vs fin mfin :
        queue_fin ℓ fin -∗
        queue_repr ℓ vs mfin -∗
        ⌜vs = []⌝ ∗ ⌜mfin = Some fin⌝;

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

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

      finalize_spec (ℓ_q : loc) (data : val) :
        ⊢ <<{ ∀∀ vs, queue_repr ℓ_q vs None }>>
            hl.(finalize) #ℓ_q data @ ∅
          <<{ queue_repr ℓ_q vs (Some data) | RET #() }>>;

      try_dequeue_spec (ℓ_q : loc) :
        ⊢ <<{ ∀∀ vs mfin, queue_repr ℓ_q vs mfin }>>
            hl.(try_dequeue) #ℓ_q @ ∅
          <<{ queue_repr ℓ_q (tail vs) mfin
            | RET (if head vs is Some v then InjLV v else InjRV (val_opt_hl mfin)) }>>;
    }.
#[global] Arguments fin_queue_iris _ {_} _ : assert.