Add Queue datatype

src/Data/Queue.agda

@@ -0,0 +1,11 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queues
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue where
+
+open import Data.Queue.TwoList.Base public

src/Data/Queue/QueueSpec.agda

@@ -0,0 +1,84 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queue specification
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue.QueueSpec where
+
+open import Data.Bool.Base using (Bool)
+open import Data.List.Base as List using (List; []; length; _∷_)
+open import Data.List.Relation.Unary.All using (Null)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Nat.Base using (ℕ)
+open import Data.Product.Base using (_×_; proj₁; proj₂)
+open import Function.Base using (_∘_)
+open import Level
+open import Relation.Binary.Core using (Rel; _=[_]⇒_)
+open import Relation.Binary.Definitions using (_Respects_)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False; does)
+open import Relation.Unary using (Pred; Decidable)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+-- RawQueue defines the 'computations' available on Queues
+-- without any of the associated proofs that determine its
+-- correctness.
+record RawQueue (Q : Set a → Set a) : Set (suc a) where
+
+  field
+    _≈_      : ∀ {A : Set a} → Rel (Q A) a
+    Empty    : ∀ {A : Set a} → Pred (Q A) a
+    empty?   : Decidable (Empty {A = A})
+    fromList : List A → Q A
+    toList   : Q A → List A
+    enqueue  : A → Q A → Q A
+    dequeue  : (q : Q A) → .{{False (empty? q)}} → A × Q A
+
+  empty : Q A
+  empty = fromList []
+
+  pure    : A → Q A
+  pure = fromList ∘ List.[_]
+
+  size : Q A → ℕ
+  size = length ∘ toList
+
+  to𝔹 : Q A → Bool
+  to𝔹 = isYes ∘ empty?
+
+  dequeue′ : Q A → Maybe (A × Q A)
+  dequeue′ q with empty? q in eq
+  ... | yes _ = nothing
+  ... | no _  = just (dequeue q)
+    where instance
+    _ : False (empty? q)
+    _ rewrite eq = _
+
+-- IsQueue bundles RawQueue with proofs of a Queues correctness,
+-- such as enqueue adding 1 to the Queue's size
+-- NOTE: not finished adding everything!
+record IsQueue {Q : Set a → Set a} (rawQ : RawQueue Q) : Set (suc a) where
+
+  open RawQueue rawQ
+
+  field
+    isEquivalence   : IsEquivalence (_≈_ {A = A})
+    ≈-resp-Empty    : Empty Respects (_≈_ {A = A})
+    ≈-=[toList]⇒-≡  : (_≈_ {A = A}) =[ toList ]⇒ _≡_
+    empty-toList    : ∀ {q : Q A} → Empty q → Null (toList q)
+    empty-fromList  : ∀ {xs : List A} → Null {A = A} xs → Empty (fromList xs)
+    toList-fromList : ∀ {q : Q A} {xs : List A} → q ≈ fromList xs → toList q ≡ xs
+    fromList-toList : ∀ {q : Q A} {xs : List A} → xs ≡ toList q → fromList xs ≈ q
+    toList-enqueue  : ∀ {q : Q A} {x : A} → toList (enqueue x q) ≡ toList q List.∷ʳ x
+    -- for some reason, let x , r = ... doesn't bind x and r??
+    toList-dequeue  : ∀ {q : Q A} → .{{i : False (empty? q)}} →
+                      let xr = dequeue q {{i}} in toList q ≡ proj₁ xr ∷ toList (proj₂ xr)

src/Data/Queue/TwoList/Base.agda

@@ -0,0 +1,155 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Queues, basic types and operations
+------------------------------------------------------------------------
+{-# OPTIONS --without-K --safe #-}
+
+-- Queues implemented with the two-list method described in
+-- "Purely Functional Data Structures", Chris Okasaki, 1996
+--
+-- Note that the weaker invariant is used here that only guarantees
+-- amortized O(1) when the structure is used non-persistently.
+
+module Data.Queue.TwoList.Base where
+
+open import Level using (Level)
+open import Data.Bool.Base using (Bool; true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.List.Base as List using (List; []; _∷_; reverse; _++_; length; null)
+open import Data.List.Relation.Unary.All using (Null; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties using (null⇒Null; Null⇒null)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Product using (_×_; _,_; proj₂)
+open import Data.Queue.QueueSpec using (RawQueue; IsQueue)
+open import Data.SnocList.Base as SnocList using (List<; toList>; fromList>; []; _<:_)
+open import Data.SnocList.Relation.Unary.All
+open import Data.Unit.Base using (⊤)
+open import Function.Base using (id; const; _∘_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable.Core using (yes; no; isYes; False)
+open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
+open import Relation.Unary using (Pred; Decidable)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+  ¬null : {a : A} {as : List A} → ¬ (Null (a ∷ as))
+  ¬null (() Data.List.Relation.Unary.All.∷ n)
+
+  ¬null< : {a : A} {as : List< A} → ¬ (Null< (as <: a))
+  ¬null< (() Data.SnocList.Relation.Unary.All.<: n)
+
+  null-[] : ∀ {xs : List A} → Null xs → Null {A = A} []
+  null-[] = const []
+
+  null<-[] : ∀ {xs : List< A} → Null< xs → Null {A = A} []
+  null<-[] = const []
+
+  null-∷ : ∀ {x} {xs ys : List A} → Null (x ∷ xs) → Null ys
+  null-∷ (()∷ _)
+
+  null-<: : ∀ {x} {xs : List< A} {ys : List A} → Null< (xs <: x) → Null ys
+  null-<: (()<: _)
+
+-- A Queue consists of a front (dequeue) and back (enqueue) list
+-- When enqueing (unless it is the first element), elements are cons'd
+-- to the enqueue list.
+--
+-- When dequeuing, elements are taken from the head of the dequeue
+-- list. If this is empty, the enqueue list is reversed and swapped
+-- with the dequeue list.
+--
+-- The dequeue-list should be empty iff the whole queue is empty.
+
+record Queue (A : Set a) : Set a where
+  constructor mkQ
+  field
+    front : List< A
+    back  : List A
+    inv : Null< front → Null back
+
+------------------------------------------------------------------------
+--- Basic Functions/Relations/Operators
+
+Empty    : ∀ {A : Set a} → Pred (Queue A) a
+Empty {a} {A} q = Null< (Queue.front q)
+
+empty? : Decidable (Empty {A = A})
+empty? (mkQ front back inv) .Relation.Nullary.does = SnocList.null front
+empty? (mkQ [] back inv) .Relation.Nullary.proof = ofʸ []
+empty? (mkQ (xs <: x) back inv) .Relation.Nullary.proof = ofⁿ (λ e → ⊥-elim (¬null< e))
+
+isEmpty : Queue A → Bool
+isEmpty q = SnocList.null (Queue.front q)
+
+------------------------------------------------------------------------
+--- Smart Constructor
+
+queue : List< A → List A → Queue A
+queue []          ys = mkQ (fromList> (reverse ys)) [] null<-[]
+queue xs@(_ <: _) ys = mkQ xs ys null-<:
+
+------------------------------------------------------------------------
+--- Conversion to/from List
+
+-- Create a List from a Queue, such that the last that would be dequeued
+-- becomes the head of the list
+toList : Queue A → List A
+toList q = (Queue.back q) ++ (toList> (Queue.front q))
+
+-- Create a Queue from a List, such that the elements
+-- of the list would be dequeued starting from its last element
+fromList : List A → Queue A
+fromList xs = queue (fromList> xs) []
+
+------------------------------------------------------------------------
+-- Construction & Destruction
+
+empty : Queue A
+empty = fromList []
+
+enqueue : A → Queue A → Queue A
+enqueue x q with bs ← Queue.back q | Queue.front q
+... | []            = queue ([] <: x) []
+... | front@(_ <: _) = queue front (x ∷ bs)
+
+dequeue : ∀ (q : Queue A) .{{_ : False (empty? q)}} → A × Queue A
+dequeue (mkQ (xs <: x) back _) = x , queue xs back
+
+-- Create a queue with a single element
+singleton : A → Queue A
+singleton = fromList ∘ List.[_]
+
+-- map : (A → B) → Queue A → Queue B
+-- map f empty = empty
+-- map f (queue x xs ys) = queue (f x) (List.map f xs) (List.map f ys)
+
+------------------------------------------------------------------------
+-- Relations
+
+-- Under the property that toList returns a list in
+-- the order of dequeue
+_≈_ : ∀ {A : Set a} → Rel (Queue A) a
+q ≈ q' = (toList q) ≡ (toList q')
+
+------------------------------------------------------------------------
+--- TwoList Queue is a Queue
+
+instance
+  TwoList-RawQueue : RawQueue {a} Queue
+  TwoList-RawQueue = record
+    { _≈_      = _≈_
+    ; Empty    = Empty
+    ; empty?   = empty?
+    ; fromList = fromList
+    ; toList   = toList
+    ; enqueue  = enqueue
+    ; dequeue  = dequeue
+    }