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