389 lines
14 KiB
Haskell
389 lines
14 KiB
Haskell
{-# LANGUAGE BangPatterns #-}
|
|
{-# LANGUAGE DeriveDataTypeable #-}
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
{-# LANGUAGE RebindableSyntax #-}
|
|
{-# LANGUAGE NoImplicitPrelude #-}
|
|
-- |
|
|
-- Module : Basement.Sized.List
|
|
-- License : BSD-style
|
|
-- Maintainer : Vincent Hanquez <vincent@snarc.org>
|
|
-- Stability : experimental
|
|
-- Portability : portable
|
|
--
|
|
-- A Nat-sized list abstraction
|
|
--
|
|
-- Using this module is limited to GHC 7.10 and above.
|
|
--
|
|
{-# LANGUAGE KindSignatures #-}
|
|
{-# LANGUAGE DataKinds #-}
|
|
{-# LANGUAGE GADTs #-}
|
|
{-# LANGUAGE TypeOperators #-}
|
|
{-# LANGUAGE TypeFamilies #-}
|
|
{-# LANGUAGE ExistentialQuantification #-}
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
|
{-# LANGUAGE UndecidableInstances #-}
|
|
{-# LANGUAGE AllowAmbiguousTypes #-}
|
|
{-# LANGUAGE DeriveDataTypeable #-}
|
|
{-# LANGUAGE DeriveGeneric #-}
|
|
{-# LANGUAGE FlexibleContexts #-}
|
|
module Basement.Sized.List
|
|
( ListN
|
|
, toListN
|
|
, toListN_
|
|
, unListN
|
|
, length
|
|
, create
|
|
, createFrom
|
|
, empty
|
|
, singleton
|
|
, uncons
|
|
, cons
|
|
, unsnoc
|
|
, snoc
|
|
, index
|
|
, indexStatic
|
|
, updateAt
|
|
, map
|
|
, mapi
|
|
, elem
|
|
, foldl
|
|
, foldl'
|
|
, foldl1'
|
|
, scanl'
|
|
, scanl1'
|
|
, foldr
|
|
, foldr1
|
|
, reverse
|
|
, append
|
|
, minimum
|
|
, maximum
|
|
, head
|
|
, tail
|
|
, init
|
|
, take
|
|
, drop
|
|
, splitAt
|
|
, zip, zip3, zip4, zip5
|
|
, unzip
|
|
, zipWith, zipWith3, zipWith4, zipWith5
|
|
, replicate
|
|
-- * Applicative And Monadic
|
|
, replicateM
|
|
, sequence
|
|
, sequence_
|
|
, mapM
|
|
, mapM_
|
|
) where
|
|
|
|
import Data.Proxy
|
|
import qualified Data.List
|
|
import Basement.Compat.Base
|
|
import Basement.Compat.CallStack
|
|
import Basement.Compat.Natural
|
|
import Basement.Nat
|
|
import Basement.NormalForm
|
|
import Basement.Numerical.Additive
|
|
import Basement.Numerical.Subtractive
|
|
import Basement.Types.OffsetSize
|
|
import Basement.Compat.ExtList ((!!))
|
|
import qualified Prelude
|
|
import qualified Control.Monad as M (replicateM, mapM, mapM_, sequence, sequence_)
|
|
|
|
impossible :: HasCallStack => a
|
|
impossible = error "ListN: internal error: the impossible happened"
|
|
|
|
-- | A Typed-level sized List equivalent to [a]
|
|
newtype ListN (n :: Nat) a = ListN { unListN :: [a] }
|
|
deriving (Eq,Ord,Typeable,Generic)
|
|
|
|
instance Show a => Show (ListN n a) where
|
|
show (ListN l) = show l
|
|
|
|
instance NormalForm a => NormalForm (ListN n a) where
|
|
toNormalForm (ListN l) = toNormalForm l
|
|
|
|
-- | Try to create a ListN from a List, succeeding if the length is correct
|
|
toListN :: forall (n :: Nat) a . (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
|
|
toListN l
|
|
| expected == Prelude.fromIntegral (Prelude.length l) = Just (ListN l)
|
|
| otherwise = Nothing
|
|
where
|
|
expected = natValInt (Proxy :: Proxy n)
|
|
|
|
-- | Create a ListN from a List, expecting a given length
|
|
--
|
|
-- If this list contains more or less than the expected length of the resulting type,
|
|
-- then an asynchronous error is raised. use 'toListN' for a more friendly functions
|
|
toListN_ :: forall n a . (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
|
|
toListN_ l
|
|
| expected == got = ListN l
|
|
| otherwise = error ("toListN_: expecting list of " <> show expected <> " elements, got " <> show got <> " elements")
|
|
where
|
|
expected = natValInt (Proxy :: Proxy n)
|
|
got = Prelude.length l
|
|
|
|
-- | performs a monadic action n times, gathering the results in a List of size n.
|
|
replicateM :: forall (n :: Nat) m a . (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
|
|
replicateM action = ListN <$> M.replicateM (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) action
|
|
|
|
-- | Evaluate each monadic action in the list sequentially, and collect the results.
|
|
sequence :: Monad m => ListN n (m a) -> m (ListN n a)
|
|
sequence (ListN l) = ListN <$> M.sequence l
|
|
|
|
-- | Evaluate each monadic action in the list sequentially, and ignore the results.
|
|
sequence_ :: Monad m => ListN n (m a) -> m ()
|
|
sequence_ (ListN l) = M.sequence_ l
|
|
|
|
-- | Map each element of a List to a monadic action, evaluate these
|
|
-- actions sequentially and collect the results
|
|
mapM :: Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
|
|
mapM f (ListN l) = ListN <$> M.mapM f l
|
|
|
|
-- | Map each element of a List to a monadic action, evaluate these
|
|
-- actions sequentially and ignore the results
|
|
mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
|
|
mapM_ f (ListN l) = M.mapM_ f l
|
|
|
|
-- | Create a list of n elements where each element is the element in argument
|
|
replicate :: forall (n :: Nat) a . (NatWithinBound Int n, KnownNat n) => a -> ListN n a
|
|
replicate a = ListN $ Prelude.replicate (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) a
|
|
|
|
-- | Decompose a list into its head and tail.
|
|
uncons :: (1 <= n) => ListN n a -> (a, ListN (n-1) a)
|
|
uncons (ListN (x:xs)) = (x, ListN xs)
|
|
uncons _ = impossible
|
|
|
|
-- | prepend an element to the list
|
|
cons :: a -> ListN n a -> ListN (n+1) a
|
|
cons a (ListN l) = ListN (a : l)
|
|
|
|
-- | Decompose a list into its first elements and the last.
|
|
unsnoc :: (1 <= n) => ListN n a -> (ListN (n-1) a, a)
|
|
unsnoc (ListN l) = (ListN $ Data.List.init l, Data.List.last l)
|
|
|
|
-- | append an element to the list
|
|
snoc :: ListN n a -> a -> ListN (n+1) a
|
|
snoc (ListN l) a = ListN (l Prelude.++ [a])
|
|
|
|
-- | Create an empty list of a
|
|
empty :: ListN 0 a
|
|
empty = ListN []
|
|
|
|
-- | Get the length of a list
|
|
length :: forall a (n :: Nat) . (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
|
|
length _ = CountOf $ natValInt (Proxy :: Proxy n)
|
|
|
|
-- | Create a new list of size n, repeately calling f from 0 to n-1
|
|
create :: forall a (n :: Nat) . KnownNat n => (Natural -> a) -> ListN n a
|
|
create f = ListN $ Prelude.map (f . Prelude.fromIntegral) [0..(len-1)]
|
|
where
|
|
len = natVal (Proxy :: Proxy n)
|
|
|
|
-- | Same as create but apply an offset
|
|
createFrom :: forall a (n :: Nat) (start :: Nat) . (KnownNat n, KnownNat start)
|
|
=> Proxy start -> (Natural -> a) -> ListN n a
|
|
createFrom p f = ListN $ Prelude.map (f . Prelude.fromIntegral) [idx..(idx+len-1)]
|
|
where
|
|
len = natVal (Proxy :: Proxy n)
|
|
idx = natVal p
|
|
|
|
-- | create a list of 1 element
|
|
singleton :: a -> ListN 1 a
|
|
singleton a = ListN [a]
|
|
|
|
-- | Check if a list contains the element a
|
|
elem :: Eq a => a -> ListN n a -> Bool
|
|
elem a (ListN l) = Prelude.elem a l
|
|
|
|
-- | Append 2 list together returning the new list
|
|
append :: ListN n a -> ListN m a -> ListN (n+m) a
|
|
append (ListN l1) (ListN l2) = ListN (l1 <> l2)
|
|
|
|
-- | Get the maximum element of a list
|
|
maximum :: (Ord a, 1 <= n) => ListN n a -> a
|
|
maximum (ListN l) = Prelude.maximum l
|
|
|
|
-- | Get the minimum element of a list
|
|
minimum :: (Ord a, 1 <= n) => ListN n a -> a
|
|
minimum (ListN l) = Prelude.minimum l
|
|
|
|
-- | Get the head element of a list
|
|
head :: (1 <= n) => ListN n a -> a
|
|
head (ListN (x:_)) = x
|
|
head _ = impossible
|
|
|
|
-- | Get the tail of a list
|
|
tail :: (1 <= n) => ListN n a -> ListN (n-1) a
|
|
tail (ListN (_:xs)) = ListN xs
|
|
tail _ = impossible
|
|
|
|
-- | Get the list with the last element missing
|
|
init :: (1 <= n) => ListN n a -> ListN (n-1) a
|
|
init (ListN l) = ListN $ Data.List.init l
|
|
|
|
-- | Take m elements from the beggining of the list.
|
|
--
|
|
-- The number of elements need to be less or equal to the list in argument
|
|
take :: forall a (m :: Nat) (n :: Nat) . (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
|
|
take (ListN l) = ListN (Prelude.take n l)
|
|
where n = natValInt (Proxy :: Proxy m)
|
|
|
|
-- | Drop elements from a list keeping the m remaining elements
|
|
drop :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a
|
|
drop (ListN l) = ListN (Prelude.drop n l)
|
|
where n = natValInt (Proxy :: Proxy d)
|
|
|
|
-- | Split a list into two, returning 2 lists
|
|
splitAt :: 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)
|
|
splitAt (ListN l) = let (l1, l2) = Prelude.splitAt n l in (ListN l1, ListN l2)
|
|
where n = natValInt (Proxy :: Proxy d)
|
|
|
|
-- | Get the i'th elements
|
|
--
|
|
-- This only works with TypeApplication:
|
|
--
|
|
-- > indexStatic @1 (toListN_ [1,2,3] :: ListN 3 Int)
|
|
indexStatic :: forall i n a . (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
|
|
indexStatic (ListN l) = l !! (natValOffset (Proxy :: Proxy i))
|
|
|
|
-- | Get the i'the element
|
|
index :: ListN n ty -> Offset ty -> ty
|
|
index (ListN l) ofs = l !! ofs
|
|
|
|
-- | Update the value in a list at a specific location
|
|
updateAt :: forall n a
|
|
. Offset a
|
|
-> (a -> a)
|
|
-> ListN n a
|
|
-> ListN n a
|
|
updateAt o f (ListN l) = ListN (doUpdate 0 l)
|
|
where doUpdate _ [] = []
|
|
doUpdate i (x:xs)
|
|
| i == o = f x : xs
|
|
| otherwise = x : doUpdate (i+1) xs
|
|
|
|
-- | Map all elements in a list
|
|
map :: (a -> b) -> ListN n a -> ListN n b
|
|
map f (ListN l) = ListN (Prelude.map f l)
|
|
|
|
-- | Map all elements in a list with an additional index
|
|
mapi :: (Natural -> a -> b) -> ListN n a -> ListN n b
|
|
mapi f (ListN l) = ListN . loop 0 $ l
|
|
where loop _ [] = []
|
|
loop i (x:xs) = f i x : loop (i+1) xs
|
|
|
|
-- | Fold all elements from left
|
|
foldl :: (b -> a -> b) -> b -> ListN n a -> b
|
|
foldl f acc (ListN l) = Prelude.foldl f acc l
|
|
|
|
-- | Fold all elements from left strictly
|
|
foldl' :: (b -> a -> b) -> b -> ListN n a -> b
|
|
foldl' f acc (ListN l) = Data.List.foldl' f acc l
|
|
|
|
-- | Fold all elements from left strictly with a first element
|
|
-- as the accumulator
|
|
foldl1' :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
|
|
foldl1' f (ListN l) = Data.List.foldl1' f l
|
|
|
|
-- | Fold all elements from right
|
|
foldr :: (a -> b -> b) -> b -> ListN n a -> b
|
|
foldr f acc (ListN l) = Prelude.foldr f acc l
|
|
|
|
-- | Fold all elements from right assuming at least one element is in the list.
|
|
foldr1 :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
|
|
foldr1 f (ListN l) = Prelude.foldr1 f l
|
|
|
|
-- | 'scanl' is similar to 'foldl', but returns a list of successive
|
|
-- reduced values from the left
|
|
--
|
|
-- > scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
|
|
scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n+1) b
|
|
scanl' f initialAcc (ListN start) = ListN (go initialAcc start)
|
|
where
|
|
go !acc l = acc : case l of
|
|
[] -> []
|
|
(x:xs) -> go (f acc x) xs
|
|
|
|
-- | 'scanl1' is a variant of 'scanl' that has no starting value argument:
|
|
--
|
|
-- > scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
|
|
scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
|
|
scanl1' f (ListN l) = case l of
|
|
[] -> ListN []
|
|
(x:xs) -> ListN $ Data.List.scanl' f x xs
|
|
|
|
-- | Reverse a list
|
|
reverse :: ListN n a -> ListN n a
|
|
reverse (ListN l) = ListN (Prelude.reverse l)
|
|
|
|
-- | Zip 2 lists of the same size, returning a new list of
|
|
-- the tuple of each elements
|
|
zip :: ListN n a -> ListN n b -> ListN n (a,b)
|
|
zip (ListN l1) (ListN l2) = ListN (Prelude.zip l1 l2)
|
|
|
|
-- | Unzip a list of tuple, to 2 List of the deconstructed tuples
|
|
unzip :: ListN n (a,b) -> (ListN n a, ListN n b)
|
|
unzip l = (map fst l, map snd l)
|
|
|
|
-- | Zip 3 lists of the same size
|
|
zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a,b,c)
|
|
zip3 (ListN x1) (ListN x2) (ListN x3) = ListN (loop x1 x2 x3)
|
|
where loop (l1:l1s) (l2:l2s) (l3:l3s) = (l1,l2,l3) : loop l1s l2s l3s
|
|
loop [] _ _ = []
|
|
loop _ _ _ = impossible
|
|
|
|
-- | Zip 4 lists of the same size
|
|
zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
|
|
zip4 (ListN x1) (ListN x2) (ListN x3) (ListN x4) = ListN (loop x1 x2 x3 x4)
|
|
where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) = (l1,l2,l3,l4) : loop l1s l2s l3s l4s
|
|
loop [] _ _ _ = []
|
|
loop _ _ _ _ = impossible
|
|
|
|
-- | Zip 5 lists of the same size
|
|
zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a,b,c,d,e)
|
|
zip5 (ListN x1) (ListN x2) (ListN x3) (ListN x4) (ListN x5) = ListN (loop x1 x2 x3 x4 x5)
|
|
where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) (l5:l5s) = (l1,l2,l3,l4,l5) : loop l1s l2s l3s l4s l5s
|
|
loop [] _ _ _ _ = []
|
|
loop _ _ _ _ _ = impossible
|
|
|
|
-- | Zip 2 lists using a function
|
|
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
|
|
zipWith f (ListN (v1:vs)) (ListN (w1:ws)) = ListN (f v1 w1 : unListN (zipWith f (ListN vs) (ListN ws)))
|
|
zipWith _ (ListN []) _ = ListN []
|
|
zipWith _ _ _ = impossible
|
|
|
|
-- | Zip 3 lists using a function
|
|
zipWith3 :: (a -> b -> c -> x)
|
|
-> ListN n a
|
|
-> ListN n b
|
|
-> ListN n c
|
|
-> ListN n x
|
|
zipWith3 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) =
|
|
ListN (f v1 w1 x1 : unListN (zipWith3 f (ListN vs) (ListN ws) (ListN xs)))
|
|
zipWith3 _ (ListN []) _ _ = ListN []
|
|
zipWith3 _ _ _ _ = impossible
|
|
|
|
-- | Zip 4 lists using a function
|
|
zipWith4 :: (a -> b -> c -> d -> x)
|
|
-> ListN n a
|
|
-> ListN n b
|
|
-> ListN n c
|
|
-> ListN n d
|
|
-> ListN n x
|
|
zipWith4 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) =
|
|
ListN (f v1 w1 x1 y1 : unListN (zipWith4 f (ListN vs) (ListN ws) (ListN xs) (ListN ys)))
|
|
zipWith4 _ (ListN []) _ _ _ = ListN []
|
|
zipWith4 _ _ _ _ _ = impossible
|
|
|
|
-- | Zip 5 lists using a function
|
|
zipWith5 :: (a -> b -> c -> d -> e -> x)
|
|
-> ListN n a
|
|
-> ListN n b
|
|
-> ListN n c
|
|
-> ListN n d
|
|
-> ListN n e
|
|
-> ListN n x
|
|
zipWith5 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) (ListN (z1:zs)) =
|
|
ListN (f v1 w1 x1 y1 z1 : unListN (zipWith5 f (ListN vs) (ListN ws) (ListN xs) (ListN ys) (ListN zs)))
|
|
zipWith5 _ (ListN []) _ _ _ _ = ListN []
|
|
zipWith5 _ _ _ _ _ _ = impossible
|