Merge pull request #12 from Matthew-Mosior/seq

[ new ] Seq

containers.ipkg

@@ -9,6 +9,9 @@ depends    = base         >= 0.6.0
 
 modules = Data.Map
         , Data.Map.Internal
+        , Data.Seq.Internal
+        , Data.Seq.Sized
+        , Data.Seq.Unsized
         , Data.Set
         , Data.Set.Internal
         , Data.Queue

src/Data/Queue.idr

@@ -14,18 +14,18 @@ record Queue a where
   front : List a
   back  : SnocList a
 
-||| The empty queue. O(1)
+||| The empty `Queue`. O(1)
 export %inline
 empty : Queue a
 empty = Q [] [<]
 
-||| Converts a list to a queue, keeping the order of
+||| Converts a list to a `Queue`, keeping the order of
 ||| elements. O(1)
 export %inline
 fromList : List a -> Queue a
 fromList vs = Q vs [<]
 
-||| Converts a `SnocList` to a queue, keeping the order of
+||| Converts a `SnocList` to a `Queue`, keeping the order of
 ||| elements. O(1)
 export %inline
 fromSnocList : SnocList a -> Queue a
@@ -37,21 +37,21 @@ export %inline
 toSnocList : Queue a -> SnocList a
 toSnocList (Q f b) = b <>< f
 
-||| Append a value at the back of the queue. O(1)
+||| Append a value at the back of the `Queue`. O(1)
 export
 enqueue : Queue a -> a -> Queue a
 enqueue (Q f b) v = Q f (b :< v)
 
-||| Append a list of values at the back of the queue. O(1)
+||| Append a list of values at the back of the `Queue`. O(1)
 export
 enqueueAll : Queue a -> List a -> Queue a
 enqueueAll (Q f b) vs = Q f (b <>< vs)
 
-||| Take a value from the front of the queue.
+||| Take a value from the front of the `Queue`.
 |||
 ||| In case of the front being empty, this transfers
 ||| the back to the front, which runs in O(n). However,
-||| every element in the queue is thus shifted at most
+||| every element in the `Queue` is thus shifted at most
 ||| once before being dequeued, so this runs in amortized
 ||| O(1).
 export
@@ -74,12 +74,12 @@ export
 prepend : a -> Queue a -> Queue a
 prepend x (Q f b) = Q (x::f) b
 
-||| Return the last element of the queue, plus the unmodified
-||| queue.
+||| Return the last element of the `Queue`, plus the unmodified
+||| `Queue`.
 |||
 ||| Note: `peekOldest` might involve a rearrangement of the elements
 |||       just like `dequeue`. In order to keep our amortized O(1)
-|||       runtime behavior, the newly arranged queue should be used
+|||       runtime behavior, the newly arranged `Queue` should be used
 |||       henceforth.
 export
 peekOldest : Queue a -> Maybe (a, Queue a)
@@ -88,7 +88,7 @@ peekOldest q =
     Just (v,Q f b) => Just (v, Q (v::f) b)
     Nothing     => Nothing
 
-||| Appends two `Queues`. O(m + n)
+||| Appends two `Queue`s. O(m + n)
 export
 (++) : Queue a -> Queue a -> Queue a
 Q f1 b1 ++ Q f2 b2 = Q (f1 ++ (b1 <>> f2)) b2