lemastero · September 1, 2021 23:23
diff --git a/Queue.agda b/Queue.agda
 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 , ∙)) ⟫
	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 , ∙)) ⟫