1-- |
2-- Module      : Basement.Sized.List
3-- License     : BSD-style
4-- Maintainer  : Vincent Hanquez <vincent@snarc.org>
5-- Stability   : experimental
6-- Portability : portable
7--
8-- A Nat-sized list abstraction
9--
10-- Using this module is limited to GHC 7.10 and above.
11--
12{-# LANGUAGE KindSignatures            #-}
13{-# LANGUAGE DataKinds                 #-}
14{-# LANGUAGE GADTs                     #-}
15{-# LANGUAGE TypeOperators             #-}
16{-# LANGUAGE TypeFamilies              #-}
17{-# LANGUAGE ExistentialQuantification #-}
18{-# LANGUAGE ScopedTypeVariables       #-}
19{-# LANGUAGE UndecidableInstances      #-}
20{-# LANGUAGE AllowAmbiguousTypes       #-}
21{-# LANGUAGE DeriveDataTypeable        #-}
22{-# LANGUAGE DeriveGeneric             #-}
23{-# LANGUAGE FlexibleContexts          #-}
24module Basement.Sized.List
25    ( ListN
26    , toListN
27    , toListN_
28    , unListN
29    , length
30    , create
31    , createFrom
32    , empty
33    , singleton
34    , uncons
35    , cons
36    , unsnoc
37    , snoc
38    , index
39    , indexStatic
40    , updateAt
41    , map
42    , mapi
43    , elem
44    , foldl
45    , foldl'
46    , foldl1'
47    , scanl'
48    , scanl1'
49    , foldr
50    , foldr1
51    , reverse
52    , append
53    , minimum
54    , maximum
55    , head
56    , tail
57    , init
58    , take
59    , drop
60    , splitAt
61    , zip, zip3, zip4, zip5
62    , unzip
63    , zipWith, zipWith3, zipWith4, zipWith5
64    , replicate
65    -- * Applicative And Monadic
66    , replicateM
67    , sequence
68    , sequence_
69    , mapM
70    , mapM_
71    ) where
72
73import           Data.Proxy
74import qualified Data.List
75import           Basement.Compat.Base
76import           Basement.Compat.CallStack
77import           Basement.Compat.Natural
78import           Basement.Nat
79import           Basement.NormalForm
80import           Basement.Numerical.Additive
81import           Basement.Numerical.Subtractive
82import           Basement.Types.OffsetSize
83import           Basement.Compat.ExtList ((!!))
84import qualified Prelude
85import qualified Control.Monad as M (replicateM, mapM, mapM_, sequence, sequence_)
86
87impossible :: HasCallStack => a
88impossible = error "ListN: internal error: the impossible happened"
89
90-- | A Typed-level sized List equivalent to [a]
91newtype ListN (n :: Nat) a = ListN { unListN :: [a] }
92    deriving (Eq,Ord,Typeable,Generic)
93
94instance Show a => Show (ListN n a) where
95    show (ListN l) = show l
96
97instance NormalForm a => NormalForm (ListN n a) where
98    toNormalForm (ListN l) = toNormalForm l
99
100-- | Try to create a ListN from a List, succeeding if the length is correct
101toListN :: forall (n :: Nat) a . (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
102toListN l
103    | expected == Prelude.fromIntegral (Prelude.length l) = Just (ListN l)
104    | otherwise                                           = Nothing
105  where
106    expected = natValInt (Proxy :: Proxy n)
107
108-- | Create a ListN from a List, expecting a given length
109--
110-- If this list contains more or less than the expected length of the resulting type,
111-- then an asynchronous error is raised. use 'toListN' for a more friendly functions
112toListN_ :: forall n a . (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
113toListN_ l
114    | expected == got = ListN l
115    | otherwise       = error ("toListN_: expecting list of " <> show expected <> " elements, got " <> show got <> " elements")
116  where
117    expected = natValInt (Proxy :: Proxy n)
118    got      = Prelude.length l
119
120-- | performs a monadic action n times, gathering the results in a List of size n.
121replicateM :: forall (n :: Nat) m a . (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
122replicateM action = ListN <$> M.replicateM (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) action
123
124-- | Evaluate each monadic action in the list sequentially, and collect the results.
125sequence :: Monad m => ListN n (m a) -> m (ListN n a)
126sequence (ListN l) = ListN <$> M.sequence l
127
128-- | Evaluate each monadic action in the list sequentially, and ignore the results.
129sequence_ :: Monad m => ListN n (m a) -> m ()
130sequence_ (ListN l) = M.sequence_ l
131
132-- | Map each element of a List to a monadic action, evaluate these
133-- actions sequentially and collect the results
134mapM :: Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
135mapM f (ListN l) = ListN <$> M.mapM f l
136
137-- | Map each element of a List to a monadic action, evaluate these
138-- actions sequentially and ignore the results
139mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
140mapM_ f (ListN l) = M.mapM_ f l
141
142-- | Create a list of n elements where each element is the element in argument
143replicate :: forall (n :: Nat) a . (NatWithinBound Int n, KnownNat n) => a -> ListN n a
144replicate a = ListN $ Prelude.replicate (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) a
145
146-- | Decompose a list into its head and tail.
147uncons :: (1 <= n) => ListN n a -> (a, ListN (n-1) a)
148uncons (ListN (x:xs)) = (x, ListN xs)
149uncons _ = impossible
150
151-- | prepend an element to the list
152cons :: a -> ListN n a -> ListN (n+1) a
153cons a (ListN l) = ListN (a : l)
154
155-- | Decompose a list into its first elements and the last.
156unsnoc :: (1 <= n) => ListN n a -> (ListN (n-1) a, a)
157unsnoc (ListN l) = (ListN $ Data.List.init l, Data.List.last l)
158
159-- | append an element to the list
160snoc :: ListN n a -> a -> ListN (n+1) a
161snoc (ListN l) a = ListN (l Prelude.++ [a])
162
163-- | Create an empty list of a
164empty :: ListN 0 a
165empty = ListN []
166
167-- | Get the length of a list
168length :: forall a (n :: Nat) . (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
169length _ = CountOf $ natValInt (Proxy :: Proxy n)
170
171-- | Create a new list of size n, repeately calling f from 0 to n-1
172create :: forall a (n :: Nat) . KnownNat n => (Natural -> a) -> ListN n a
173create f = ListN $ Prelude.map (f . Prelude.fromIntegral) [0..(len-1)]
174  where
175    len = natVal (Proxy :: Proxy n)
176
177-- | Same as create but apply an offset
178createFrom :: forall a (n :: Nat) (start :: Nat) . (KnownNat n, KnownNat start)
179           => Proxy start -> (Natural -> a) -> ListN n a
180createFrom p f = ListN $ Prelude.map (f . Prelude.fromIntegral) [idx..(idx+len-1)]
181  where
182    len = natVal (Proxy :: Proxy n)
183    idx = natVal p
184
185-- | create a list of 1 element
186singleton :: a -> ListN 1 a
187singleton a = ListN [a]
188
189-- | Check if a list contains the element a
190elem :: Eq a => a -> ListN n a -> Bool
191elem a (ListN l) = Prelude.elem a l
192
193-- | Append 2 list together returning the new list
194append :: ListN n a -> ListN m a -> ListN (n+m) a
195append (ListN l1) (ListN l2) = ListN (l1 <> l2)
196
197-- | Get the maximum element of a list
198maximum :: (Ord a, 1 <= n) => ListN n a -> a
199maximum (ListN l) = Prelude.maximum l
200
201-- | Get the minimum element of a list
202minimum :: (Ord a, 1 <= n) => ListN n a -> a
203minimum (ListN l) = Prelude.minimum l
204
205-- | Get the head element of a list
206head :: (1 <= n) => ListN n a -> a
207head (ListN (x:_)) = x
208head _ = impossible
209
210-- | Get the tail of a list
211tail :: (1 <= n) => ListN n a -> ListN (n-1) a
212tail (ListN (_:xs)) = ListN xs
213tail _ = impossible
214
215-- | Get the list with the last element missing
216init :: (1 <= n) => ListN n a -> ListN (n-1) a
217init (ListN l) = ListN $ Data.List.init l
218
219-- | Take m elements from the beggining of the list.
220--
221-- The number of elements need to be less or equal to the list in argument
222take :: forall a (m :: Nat) (n :: Nat) . (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
223take (ListN l) = ListN (Prelude.take n l)
224  where n = natValInt (Proxy :: Proxy m)
225
226-- | Drop elements from a list keeping the m remaining elements
227drop :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a
228drop (ListN l) = ListN (Prelude.drop n l)
229  where n = natValInt (Proxy :: Proxy d)
230
231-- | Split a list into two, returning 2 lists
232splitAt :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> (ListN m a, ListN (n-m) a)
233splitAt (ListN l) = let (l1, l2) = Prelude.splitAt n l in (ListN l1, ListN l2)
234  where n = natValInt (Proxy :: Proxy d)
235
236-- | Get the i'th elements
237--
238-- This only works with TypeApplication:
239--
240-- > indexStatic @1 (toListN_ [1,2,3] :: ListN 3 Int)
241indexStatic :: forall i n a . (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
242indexStatic (ListN l) = l !! (natValOffset (Proxy :: Proxy i))
243
244-- | Get the i'the element
245index :: ListN n ty -> Offset ty -> ty
246index (ListN l) ofs = l !! ofs
247
248-- | Update the value in a list at a specific location
249updateAt :: forall n a
250         .  Offset a
251         -> (a -> a)
252         -> ListN n a
253         -> ListN n a
254updateAt o f (ListN l) = ListN (doUpdate 0 l)
255  where doUpdate _ []     = []
256        doUpdate i (x:xs)
257            | i == o      = f x : xs
258            | otherwise   = x : doUpdate (i+1) xs
259
260-- | Map all elements in a list
261map :: (a -> b) -> ListN n a -> ListN n b
262map f (ListN l) = ListN (Prelude.map f l)
263
264-- | Map all elements in a list with an additional index
265mapi :: (Natural -> a -> b) -> ListN n a -> ListN n b
266mapi f (ListN l) = ListN . loop 0 $ l
267  where loop _ []     = []
268        loop i (x:xs) = f i x : loop (i+1) xs
269
270-- | Fold all elements from left
271foldl :: (b -> a -> b) -> b -> ListN n a -> b
272foldl f acc (ListN l) = Prelude.foldl f acc l
273
274-- | Fold all elements from left strictly
275foldl' :: (b -> a -> b) -> b -> ListN n a -> b
276foldl' f acc (ListN l) = Data.List.foldl' f acc l
277
278-- | Fold all elements from left strictly with a first element
279-- as the accumulator
280foldl1' :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
281foldl1' f (ListN l) = Data.List.foldl1' f l
282
283-- | Fold all elements from right
284foldr :: (a -> b -> b) -> b -> ListN n a -> b
285foldr f acc (ListN l) = Prelude.foldr f acc l
286
287-- | Fold all elements from right assuming at least one element is in the list.
288foldr1 :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
289foldr1 f (ListN l) = Prelude.foldr1 f l
290
291-- | 'scanl' is similar to 'foldl', but returns a list of successive
292-- reduced values from the left
293--
294-- > scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
295scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n+1) b
296scanl' f initialAcc (ListN start) = ListN (go initialAcc start)
297  where
298    go !acc l = acc : case l of
299                        []     -> []
300                        (x:xs) -> go (f acc x) xs
301
302-- | 'scanl1' is a variant of 'scanl' that has no starting value argument:
303--
304-- > scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
305scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
306scanl1' f (ListN l) = case l of
307                        []     -> ListN []
308                        (x:xs) -> ListN $ Data.List.scanl' f x xs
309
310-- | Reverse a list
311reverse :: ListN n a -> ListN n a
312reverse (ListN l) = ListN (Prelude.reverse l)
313
314-- | Zip 2 lists of the same size, returning a new list of
315-- the tuple of each elements
316zip :: ListN n a -> ListN n b -> ListN n (a,b)
317zip (ListN l1) (ListN l2) = ListN (Prelude.zip l1 l2)
318
319-- | Unzip a list of tuple, to 2 List of the deconstructed tuples
320unzip :: ListN n (a,b) -> (ListN n a, ListN n b)
321unzip l = (map fst l, map snd l)
322
323-- | Zip 3 lists of the same size
324zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a,b,c)
325zip3 (ListN x1) (ListN x2) (ListN x3) = ListN (loop x1 x2 x3)
326  where loop (l1:l1s) (l2:l2s) (l3:l3s) = (l1,l2,l3) : loop l1s l2s l3s
327        loop []       _        _        = []
328        loop _        _        _        = impossible
329
330-- | Zip 4 lists of the same size
331zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
332zip4 (ListN x1) (ListN x2) (ListN x3) (ListN x4) = ListN (loop x1 x2 x3 x4)
333  where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) = (l1,l2,l3,l4) : loop l1s l2s l3s l4s
334        loop []       _        _        _        = []
335        loop _        _        _        _        = impossible
336
337-- | Zip 5 lists of the same size
338zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a,b,c,d,e)
339zip5 (ListN x1) (ListN x2) (ListN x3) (ListN x4) (ListN x5) = ListN (loop x1 x2 x3 x4 x5)
340  where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) (l5:l5s) = (l1,l2,l3,l4,l5) : loop l1s l2s l3s l4s l5s
341        loop []       _        _        _        _        = []
342        loop _        _        _        _        _        = impossible
343
344-- | Zip 2 lists using a function
345zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
346zipWith f (ListN (v1:vs)) (ListN (w1:ws)) = ListN (f v1 w1 : unListN (zipWith f (ListN vs) (ListN ws)))
347zipWith _ (ListN [])       _ = ListN []
348zipWith _ _                _ = impossible
349
350-- | Zip 3 lists using a function
351zipWith3 :: (a -> b -> c -> x)
352         -> ListN n a
353         -> ListN n b
354         -> ListN n c
355         -> ListN n x
356zipWith3 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) =
357    ListN (f v1 w1 x1 : unListN (zipWith3 f (ListN vs) (ListN ws) (ListN xs)))
358zipWith3 _ (ListN []) _       _ = ListN []
359zipWith3 _ _          _       _ = impossible
360
361-- | Zip 4 lists using a function
362zipWith4 :: (a -> b -> c -> d -> x)
363         -> ListN n a
364         -> ListN n b
365         -> ListN n c
366         -> ListN n d
367         -> ListN n x
368zipWith4 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) =
369    ListN (f v1 w1 x1 y1 : unListN (zipWith4 f (ListN vs) (ListN ws) (ListN xs) (ListN ys)))
370zipWith4 _ (ListN []) _       _       _ = ListN []
371zipWith4 _ _          _       _       _ = impossible
372
373-- | Zip 5 lists using a function
374zipWith5 :: (a -> b -> c -> d -> e -> x)
375         -> ListN n a
376         -> ListN n b
377         -> ListN n c
378         -> ListN n d
379         -> ListN n e
380         -> ListN n x
381zipWith5 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) (ListN (z1:zs)) =
382    ListN (f v1 w1 x1 y1 z1 : unListN (zipWith5 f (ListN vs) (ListN ws) (ListN xs) (ListN ys) (ListN zs)))
383zipWith5 _ (ListN []) _       _       _       _ = ListN []
384zipWith5 _ _          _       _       _       _ = impossible
385