
   0 | ||| Linear Bounded Queues
   1 | module Data.BoundedQueue1.Unsized
   2 | 
   3 | import Data.BoundedQueue.Unsized.Internal
   4 | import Data.BoundedQueue1.Unsized.Internal
   5 | import Data.Seq.Unsized
   6 | 
   7 | import Data.Linear.Ref1
   8 | import Derive.Prelude
   9 | 
  10 | %language ElabReflection
  11 | 
  12 | %default total
  13 | 
  14 | ||| The empty `BoundedQueue1`. O(1)
  15 | export
  16 | empty :  Nat
  17 |       -> F1 s (BoundedQueue1 s a)
  18 | empty l t =
  19 |   let bq # t := ref1 ( MkBoundedQueue Data.Seq.Unsized.empty
  20 |                                       l
  21 |                                       Z
  22 |                      ) t
  23 |     in (MkBoundedQueue1 bq) # t
  24 | 
  25 | ||| Is the `BoundedQueuei1` empty? O(1)
  26 | export
  27 | null :  BoundedQueue1 s a
  28 |      -> F1 s Bool
  29 | null (MkBoundedQueue1 bq) t =
  30 |   let (MkBoundedQueue _ _ s) # t := read1 bq t
  31 |     in case s of
  32 |          Z =>
  33 |            True # t
  34 |          _ =>
  35 |            False # t
  36 | 
  37 | ||| Naively keeps the first `n` values of a list, and converts
  38 | ||| into a `BoundedQueue1` (keeps the order of the elements). O(1)
  39 | export
  40 | fromList :  (n : Nat)
  41 |          -> (vs : List a)
  42 |          -> F1 s (BoundedQueue1 s a)
  43 | fromList n vs t =
  44 |   let vs'    := take n vs
  45 |       bq # t := ref1 ( MkBoundedQueue (Data.Seq.Unsized.fromList vs')
  46 |                                       n
  47 |                                       (Prelude.List.length vs')
  48 |                      ) t
  49 |     in (MkBoundedQueue1 bq) # t
  50 | 
  51 | ||| Naively keeps the first `n` values of a `SnocList`, and converts
  52 | ||| into a `BoundedQueue1` (keeps the order of the elements). O(1)
  53 | export
  54 | fromSnocList :  (n : Nat)
  55 |              -> (sv : SnocList a)
  56 |              -> F1 s (BoundedQueue1 s a)
  57 | fromSnocList n sv t =
  58 |   let sv'    := take n $ cast sv
  59 |       bq # t := ref1 ( MkBoundedQueue (Data.Seq.Unsized.fromList sv')
  60 |                                       n
  61 |                                       (Prelude.List.length sv')
  62 |                      ) t
  63 |     in (MkBoundedQueue1 bq) # t
  64 | 
  65 | ||| Converts a `BoundedQueue1` to a `List`, keeping the order
  66 | ||| of elements. O(n)
  67 | export
  68 | toList :  BoundedQueue1 s a
  69 |        -> F1 s (List a)
  70 | toList (MkBoundedQueue1 bq) t =
  71 |   let (MkBoundedQueue q _ _) # t := read1 bq t
  72 |     in (toList q) # t
  73 | 
  74 | ||| Converts a `BoundedQueue1` to a `SnocList`, keeping the order
  75 | ||| of elements. O(n)
  76 | export
  77 | toSnocList :  BoundedQueue1 s a
  78 |            -> F1 s (SnocList a)
  79 | toSnocList (MkBoundedQueue1 bq) t =
  80 |   let (MkBoundedQueue q _ _) # t := read1 bq t
  81 |     in (cast $ toList q) # t
  82 | 
  83 | ||| Append a value at the back of the `BoundedQueue1`.
  84 | ||| This function returns `True` if the value was enqueued,
  85 | ||| and `False` if the queue was full. O(1)
  86 | export
  87 | enqueue :  BoundedQueue1 s a
  88 |         -> a
  89 |         -> F1 s Bool
  90 | enqueue (MkBoundedQueue1 bq) v t =
  91 |   casupdate1 bq
  92 |     (\(MkBoundedQueue q l s) =>
  93 |       case l == s of
  94 |         True  =>
  95 |           (MkBoundedQueue q l s, False)
  96 |         False =>
  97 |           (MkBoundedQueue (q `snoc` v) l (s `plus` 1), True)
  98 |     ) t
  99 | 
 100 | ||| Take a value from the front of the `BoundedQueue1`. O(1)
 101 | export
 102 | dequeue :  BoundedQueue1 s a
 103 |         -> F1 s (Maybe a)
 104 | dequeue (MkBoundedQueue1 bq) t =
 105 |   casupdate1 bq
 106 |     (\(MkBoundedQueue q l s) =>
 107 |       case viewl q of
 108 |         Nothing      =>
 109 |           (MkBoundedQueue q l s, Nothing)
 110 |         Just (h, q') =>
 111 |           ( MkBoundedQueue q' l (s `minus` 1)
 112 |           , Just h
 113 |           )
 114 |     ) t
 115 | 
 116 | ||| We can prepend an element to our `BoundedQueue1`, making it the new
 117 | ||| "oldest" element. O(1)
 118 | ||| This function returns `True` is the value was pre-pended,
 119 | ||| and `False` if the queue was full. O(1)
 120 | export
 121 | prepend :  a
 122 |         -> BoundedQueue1 s a
 123 |         -> F1 s Bool
 124 | prepend x (MkBoundedQueue1 bq) t =
 125 |   casupdate1 bq
 126 |     (\(MkBoundedQueue q l s) =>
 127 |       case l == s of
 128 |         True  =>
 129 |           (MkBoundedQueue q l s, False)
 130 |         False =>
 131 |           (MkBoundedQueue (x `cons` q) l (s `plus` 1), True)
 132 |     ) t
 133 | 
 134 | ||| Return the last element of the `BoundedQueue1`, plus the unmodified
 135 | ||| queue.
 136 | |||
 137 | ||| Note: `peekOldest` might involve a rearrangement of the elements
 138 | |||       just like `dequeue`. In order to keep our amortized O(1)
 139 | |||       runtime behavior, the newly arranged queue should be used
 140 | |||       henceforth.
 141 | export
 142 | peekOldest :  BoundedQueue1 s a
 143 |            -> F1 s (Maybe (a, BoundedQueue1 s a))
 144 | peekOldest (MkBoundedQueue1 bq) t =
 145 |   let (MkBoundedQueue q l s) # t := read1 bq t
 146 |     in case viewl q of
 147 |          Nothing     =>
 148 |            Nothing # t
 149 |          Just (v, _) =>
 150 |            Just (v, MkBoundedQueue1 bq) # t
 151 | 
 152 | ||| Returns the length of the `BoundedQueue1`. O(1).
 153 | export
 154 | length :  BoundedQueue1 s a
 155 |        -> F1 s Nat
 156 | length (MkBoundedQueue1 bq) t =
 157 |   let (MkBoundedQueue _ _ s) # t := read1 bq t
 158 |     in s # t
 159 |