Skip to content

Instantly share code, notes, and snippets.

@lemastero
Forked from andrejbauer/Queue.agda
Created September 1, 2021 23:23
Show Gist options
  • Save lemastero/d2832e1807be776711422ebd19b5b928 to your computer and use it in GitHub Desktop.
Save lemastero/d2832e1807be776711422ebd19b5b928 to your computer and use it in GitHub Desktop.
An implementation of infinite queues fashioned after the von Neuman ordinals
open import Data.Nat
open import Data.Maybe
open import Data.Product
-- An implementation of infinite queues fashioned after the von Neuman ordinals
module Queue where
infixl 5 _⊕_
data queue (A : Set) : Set where
∙ : queue A -- the empty queue
[_] : A → queue A -- a singleton queue
_⊕_ : queue A → queue A → queue A -- join two queues, one after the other
⟪_⟫ : (ℕ → A × queue A) → queue A -- a queue of infinitely many non-empty queues
-- push an element to the end of the queue
push : ∀ {A} → queue A → A → queue A
push q x = q ⊕ [ x ]
-- pop the first element off the queue
pop : ∀ {A} → queue A → Maybe (A × queue A)
pop ∙ = nothing
pop [ x ] = just (x , ∙)
pop (q₁ ⊕ q₂) with pop q₁ | pop q₂
... | nothing | nothing = nothing
... | nothing | just (y , r) = just (y , r)
... | just (x , r) | _ = just (x , r ⊕ q₂)
pop {A} ⟪ qs ⟫ with (x , q ) ← (qs 0) = just (x , r)
where
r : queue A
r with pop q
... | nothing = ⟪ (λ n → qs (suc n)) ⟫
... | just (y , s) = ⟪ (λ {0 → y , s ; (suc n) → qs (suc n)}) ⟫
-- the queue 0, 1, 2, 3
example₁ = [ 0 ] ⊕ [ 1 ] ⊕ [ 2 ] ⊕ [ 3 ]
-- the queue 0, 1, 4, 9, 16, ...
example₂ = ⟪ (λ n → (n * n , ∙)) ⟫
-- the queue 0, 2, 4, 6, ..., 3
example₃ = push ⟪ (λ n → (2 * n , ∙)) ⟫ 3
-- the queue 0, 2, 4, ..., 1, 3, 5, ...
example₄ = ⟪ (λ n → (2 * n , ∙)) ⟫ ⊕ ⟪ (λ n → (2 * n + 1 , ∙)) ⟫
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment