
  0 | ||| Bounded Queue Internals
  1 | module Data.BoundedQueue.Unsized.Internal
  2 | 
  3 | import Data.Seq.Unsized
  4 | import Derive.Prelude
  5 | 
  6 | %language ElabReflection
  7 | 
  8 | %default total
  9 | 
 10 | ||| An immutable, bounded first-in first-out structure which keeps
 11 | ||| track of its size, with amortized O(1) enqueue and dequeue operations.
 12 | public export
 13 | data BoundedQueue : (a : Type) -> Type where
 14 |   MkBoundedQueue :  Seq a -- queue
 15 |                  -> Nat   -- limit
 16 |                  -> Nat   -- size
 17 |                  -> BoundedQueue a
 18 | 
 19 | %runElab derive "BoundedQueue" [Show,Eq,Ord]
 20 |