
  0 | module Data.Compress.Utils.FiniteBuffer
  1 | 
  2 | import Data.Seq.Unsized
  3 | 
  4 | export
  5 | record FiniteBuffer a where
  6 |   constructor FB
  7 |   max_size : Int
  8 |   size : Int
  9 |   buffer : Seq a
 10 | 
 11 | export
 12 | empty : Nat -> FiniteBuffer a
 13 | empty n = FB (cast n) 0 empty
 14 | 
 15 | export
 16 | take_last : Nat -> FiniteBuffer a -> Maybe (List a)
 17 | take_last n fb = guard (cast n <= fb.size) $> (toList $ take n $ drop (cast (fb.size - cast n)) fb.buffer)
 18 | 
 19 | export infixr 5 +<
 20 | export infixr 5 +<><
 21 | 
 22 | export
 23 | (+<) : FiniteBuffer a -> a -> FiniteBuffer a
 24 | (FB max_size size buffer) +< x =
 25 |   let
 26 |     len = size + 1
 27 |     buf = snoc buffer x
 28 |   in
 29 |     if len > max_size then FB max_size max_size $ tail buf else FB max_size len buf
 30 | 
 31 | export
 32 | (+<><) : Foldable f => FiniteBuffer a -> f a -> FiniteBuffer a
 33 | buf +<>< elems = foldl (+<) buf elems
 34 | 
 35 | export
 36 | length : FiniteBuffer a -> Nat
 37 | length = cast . size
 38 |