Add Queue datatype

src/Data/List/Relation/Unary/All/Properties.agda

@@ -77,6 +77,12 @@ null⇒Null : T (null xs) → Null xs
 null⇒Null {xs = []   } _ = []
 null⇒Null {xs = _ ∷ _} ()
 
+nullxs→xs≡[] : Null xs → xs ≡ []
+nullxs→xs≡[] [] = refl
+
+xs≡[]→nullxs : xs ≡ [] → Null xs
+xs≡[]→nullxs xs≡[] rewrite xs≡[] = []
+
 ------------------------------------------------------------------------
 -- Properties of the "points-to" relation _[_]=_
 

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,82 @@
+------------------------------------------------------------------------
+-- 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)}} → Q A × A
+    size : Q A → ℕ
+
+  empty : Q A
+  empty = fromList []
+
+  pure    : A → Q A
+  pure = fromList ∘ List.[_]
+
+  to𝔹 : Q A → Bool
+  to𝔹 = isYes ∘ empty?
+
+  dequeue′ : Q A → Maybe (Q A × 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) ≡ x ∷ toList q
+    -- 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 ≡  toList (proj₁ xr) List.∷ʳ proj₂ xr

src/Data/Queue/TwoList/Base.agda

@@ -0,0 +1,129 @@
+------------------------------------------------------------------------
+-- 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.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.SnocList.Relation.Unary.All.Properties using (¬null-<:; null-<:→nullxs)
+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.Negation using (contradiction)
+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
+
+-- 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ⁿ λ null< → contradiction null< ¬null-<:
+
+isEmpty : Queue A → Bool
+isEmpty q = SnocList.null (Queue.front q)
+
+------------------------------------------------------------------------
+--- Smart Constructor
+
+queue : List< A → List A → Queue A
+queue []          ys = mkQ ([] <>< ys) [] (const [])
+queue xs@(_ <: _) ys = mkQ xs ys null-<:→nullxs
+
+------------------------------------------------------------------------
+--- 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 [] 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)}} → Queue A × A
+dequeue (mkQ (xs <: x) back _) = queue xs back , x
+
+-- 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')
+
+------------------------------------------------------------------------
+-- Size
+
+size : Queue A → ℕ
+size = length ∘ toList

src/Data/Queue/TwoList/Instances.agda

@@ -0,0 +1,56 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances of TwoLisQueue
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Queue.TwoList.Instances where
+
+open import Data.Queue.TwoList.Base
+open import Data.Queue.TwoList.Properties
+open import Data.Queue.QueueSpec using (RawQueue; IsQueue)
+open import Level using (Level)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+------------------------------------------------------------------------
+--- TwoList Queue is a Raw Queue
+
+instance
+  TwoList-RawQueue : RawQueue {a} Queue
+  TwoList-RawQueue = record
+    { _≈_      = _≈_
+    ; Empty    = Empty
+    ; empty?   = empty?
+    ; fromList = fromList
+    ; toList   = toList
+    ; enqueue  = enqueue
+    ; dequeue  = dequeue
+    ; size     = size
+    }
+
+------------------------------------------------------------------------
+-- TwoList Queue is a Queue!
+
+-- for some reason, unless manually passing some implicits, other implicits remain
+-- unsolved? This is also means that you can't assign fields with record syntax and
+-- have to use co-pattern matching. My knowledge of implicits isn't good enough to know
+-- why or if this indicates 'bad ergonomics'
+
+instance
+  TwoList-IsQueue : IsQueue {a} TwoList-RawQueue
+  TwoList-IsQueue .IsQueue.isEquivalence = ≈-isEquivalence
+  TwoList-IsQueue .IsQueue.≈-resp-Empty {x = x} {y} = ≈-resp-Empty {x = x} {y = y}
+  TwoList-IsQueue .IsQueue.≈-=[toList]⇒-≡ {x = x} {y} = ≈-=[toList]⇒-≡ {x = x} {y = y}
+  TwoList-IsQueue .IsQueue.empty-toList {q = q} = empty-toList {q = q}
+  TwoList-IsQueue .IsQueue.empty-fromList = empty-fromList
+  TwoList-IsQueue .IsQueue.toList-fromList {q = q} = toList-fromList {q = q}
+  TwoList-IsQueue .IsQueue.fromList-toList {q = q} = fromList-toList {q = q}
+  TwoList-IsQueue .IsQueue.toList-enqueue {q = q} = toList-enqueue {q = q}
+  TwoList-IsQueue .IsQueue.toList-dequeue {q = q} = toList-dequeue {q = q}