diff --git a/Data/Sized.hs b/Data/Sized.hs deleted file mode 100644 --- a/Data/Sized.hs +++ /dev/null @@ -1,1309 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds #-} -{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-} -{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-} -{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables, RankNTypes #-} -{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies #-} -{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-} -#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} -#endif - -{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-} -{-# OPTIONS_GHC -fenable-rewrite-rules #-} --- | This module provides the functionality to make length-parametrized types --- from existing 'ListLike' and 'Functor' sequential types. --- --- Most of the complexity of operations for @Sized f n a@ are the same as --- original operations for @f@. For example, '!!' is O(1) for --- @Sized Vector n a@ but O(i) for @Sized [] n a@. --- --- This module also provides powerful view types and pattern synonyms to --- inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail. -module Data.Sized - ( -- * Main Data-types - Sized(), SomeSized(..), - instLL, instFunctor, ListLikeF, - withListLikeF, withListLikeF', - -- * Accessors - -- ** Length information - length, sLength, null, - -- ** Indexing - (!!), (%!!), index, sIndex, head, last, - uncons, uncons', unsnoc, unsnoc', - -- ** Slicing - tail, init, take, takeAtMost, drop, splitAt, splitAtMost, - -- * Construction - -- ** Initialisation - empty, singleton, toSomeSized, replicate, replicate', generate, - -- ** Concatenation - cons, (<|), snoc, (|>), append, (++), concat, - -- ** Zips - zip, zipSame, zipWith, zipWithSame, unzip, - -- * Transformation - map, fmap, reverse, intersperse, nub, sort, sortBy, insert, insertBy, - -- * Conversion - -- ** List - toList, fromList, fromList', unsafeFromList, unsafeFromList', - fromListWithDefault, fromListWithDefault', - -- ** Base container - unsized, - toSized, toSized', unsafeToSized, unsafeToSized', - toSizedWithDefault, toSizedWithDefault', - -- * Querying - -- ** Partitioning - Partitioned(..), - takeWhile, dropWhile, span, break, partition, - -- ** Searching - elem, notElem, find, findF, findIndex, findIndexIF, - sFindIndex, sFindIndexIF, - findIndices, findIndicesIF, sFindIndices, sFindIndicesIF, - elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, - -- * Views and Patterns - -- $ViewsAndPatterns - - -- ** Views - -- $views - - -- ** Patterns - -- $patterns - - -- ** Definitions - viewCons, ConsView (..), viewSnoc, SnocView(..), - - pattern (:<), pattern NilL , pattern (:>), pattern NilR, - ) where - -import Data.Sized.Internal - -import Control.Applicative ((<$>), (<*>), ZipList(..)) -import Control.Lens.Indexed (FoldableWithIndex (..), ifind) -import Data.Foldable (Foldable) -import qualified Data.Foldable as F -import Data.Kind (Type) -import qualified Data.List as L -import Data.ListLike (ListLike) -import qualified Data.ListLike as LL -import Data.Monoid (Endo (..), First (..)) -import qualified Data.Sequence as Seq -import Data.Singletons.Prelude.Bool -import Data.Singletons.Prelude (SomeSing(..), PNum (..), POrd (..)) -import Data.Singletons.Prelude (Sing (..), SingI (..)) -import Data.Singletons.Prelude (withSing, withSingI) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Natural as Peano -import Data.Type.Natural.Class -import Data.Type.Ordinal (HasOrdinal, Ordinal (..), enumOrdinal) -import Data.Type.Ordinal (ordToNatural, unsafeNaturalToOrd) -import Data.Typeable (Typeable) -import qualified Data.Vector as V -import qualified Data.Vector.Storable as SV -import qualified Data.Vector.Unboxed as UV -import qualified GHC.TypeLits as TL -import Prelude (Bool (..), Enum (..), Eq (..)) -import Prelude (Functor, Int, Maybe (..)) -import Prelude (Num (..), Ord (..), Ordering) -import Prelude (Show (..), flip, fst, ($), (.)) -import qualified Prelude as P -import Unsafe.Coerce (unsafeCoerce) - --------------------------------------------------------------------------------- --- Main data-types --------------------------------------------------------------------------------- - --- | 'Sized' vector with the length is existentially quantified. --- This type is used mostly when the return type's length cannot --- be statically determined beforehand. --- --- @SomeSized sn xs :: SomeSized f a@ stands for the 'Sized' sequence --- @xs@ of element type @a@ and length @sn@. --- --- Since 0.1.0.0 -data SomeSized f nat a where - SomeSized :: (ListLike (f a) a) - => Sing n - -> Sized f (n :: nat) a - -> SomeSized f nat a - -deriving instance Typeable SomeSized - -instance Show (f a) => Show (SomeSized f nat a) where - showsPrec d (SomeSized _ s) = P.showParen (d > 9) $ - P.showString "SomeSized _ " . showsPrec 10 s -instance Eq (f a) => Eq (SomeSized f nat a) where - (SomeSized _ (Sized xs)) == (SomeSized _ (Sized ys)) = xs == ys - --------------------------------------------------------------------------------- --- Accessors --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- Length infromation --------------------------------------------------------------------------------- - --- | Returns the length of wrapped containers. --- If you use @unsafeFromList@ or similar unsafe functions, --- this function may return different value from type-parameterized length. --- --- Since 0.1.0.0 -length :: ListLike (f a) a => Sized f n a -> Int -length = LL.length . runSized -{-# INLINE CONLIKE [1] length #-} - -lengthTLZero :: Sized f 0 a -> Int -lengthTLZero = P.const 0 -{-# INLINE lengthTLZero #-} - -lengthPeanoZero :: Sized f 'Peano.Z a -> Int -lengthPeanoZero = P.const 0 -{-# INLINE lengthPeanoZero #-} - -{-# RULES -"length/0" [~1] length = lengthTLZero -"length/Z" [~1] length = lengthPeanoZero - #-} - --- | @Sing@ version of 'length'. --- --- Since 0.5.0.0 (type changed) -sLength :: forall f nat (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sized f n a -> Sing n -sLength (Sized xs) = - case fromNatural (P.fromIntegral $ LL.length xs) of - SomeSing (n :: Sing (k :: nat)) -> unsafeCoerce n -{-# INLINE[2] sLength #-} - --- | Test if the sequence is empty or not. --- --- Since 0.1.0.0 -null :: ListLike (f a) a => Sized f n a -> Bool -null = LL.null . runSized -{-# INLINE CONLIKE [2] null #-} - -nullTL0 :: Sized f 0 a -> Bool -nullTL0 = P.const True -{-# INLINE nullTL0 #-} - -nullPeano0 :: Sized f 'Peano.Z a -> Bool -nullPeano0 = P.const True -{-# INLINE nullPeano0 #-} - -nullPeanoSucc :: Sized f (S n) a -> Bool -nullPeanoSucc = P.const False -{-# INLINE nullPeanoSucc #-} - -nullTLSucc :: Sized f (n + 1) a -> Bool -nullTLSucc = P.const False -{-# INLINE nullTLSucc #-} - -{-# RULES -"null/0" [~2] null = nullTL0 -"null/0" [~1] forall (vec :: (1 TL.<= n) => Sized f n a). - null vec = False -"null/0" [~2] null = nullTLSucc -"null/Z" [~2] null = nullPeano0 -"null/Sn" [~2] null = nullPeanoSucc -#-} - --------------------------------------------------------------------------------- ---- Indexing --------------------------------------------------------------------------------- - --- | (Unsafe) indexing with @Int@s. --- If you want to check boundary statically, use '%!!' or 'sIndex'. --- --- Since 0.1.0.0 -(!!) :: (ListLike (f a) a) => Sized f (Succ m) a -> Int -> a -Sized xs !! n = LL.index xs n -{-# INLINE (!!) #-} - --- | Safe indexing with 'Ordinal's. --- --- Since 0.1.0.0 -(%!!) :: (HasOrdinal nat, LL.ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c -Sized xs %!! n = LL.index xs $ P.fromIntegral $ ordToNatural n -{-# INLINE (%!!) #-} -{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-} - --- | Flipped version of '!!'. --- --- Since 0.1.0.0 -index :: (ListLike (f a) a) => Int -> Sized f (Succ m) a -> a -index n (Sized xs) = LL.index xs n -{-# INLINE index #-} - --- | Flipped version of '%!!'. --- --- Since 0.1.0.0 -sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c -sIndex = flip (%!!) -{-# INLINE sIndex #-} - --- | Take the first element of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat < n) ~ 'True) => Sized f n a -> b -head = LL.head . runSized -{-# INLINE head #-} - --- | Take the last element of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -last :: (HasOrdinal nat, (Zero nat < n) ~ 'True, ListLike (f a) b) => Sized f n a -> b -last = LL.last . runSized -{-# INLINE last #-} - --- | Take the 'head' and 'tail' of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a) -uncons = ((,) <$> LL.head <*> Sized . LL.tail) . runSized - -unconsList :: Sized [] (Succ n) a -> (a, Sized [] n a) -unconsList (Sized ~(x : xs)) = (x, Sized xs) -{-# INLINE unconsList #-} - -unconsSeq :: Sized Seq.Seq (Succ n) a -> (a, Sized Seq.Seq n a) -unconsSeq (Sized ~(Seq.viewl -> x Seq.:< xs)) = (x, Sized xs) -{-# INLINE unconsSeq #-} - -{-# INLINE [1] uncons #-} -{-# RULES -"uncons/[]" [~1] uncons = unconsList -"uncons/Seq" [~1] uncons = unconsSeq - #-} - -uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a) -uncons' _ = uncons -{-# INLINE uncons' #-} - --- | Take the 'init' and 'last' of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b) -unsnoc = ((,) <$> Sized . LL.init <*> LL.last) . runSized -{-# NOINLINE [1] unsnoc #-} - -unsnocSeq :: Sized Seq.Seq (Succ n) a -> (Sized Seq.Seq n a, a) -unsnocSeq (Sized ~(Seq.viewr -> xs Seq.:> x)) = (Sized xs, x) -{-# INLINE unsnocSeq #-} - -unsnocVector :: Sized V.Vector (Succ n) a -> (Sized V.Vector n a, a) -unsnocVector (Sized v) = (Sized (V.init v), V.last v) -{-# INLINE unsnocVector #-} - -{-# RULES -"unsnoc/Seq" [~1] unsnoc = unsnocSeq -"unsnoc/Vector" [~1] unsnoc = unsnocVector - #-} - - -unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b) -unsnoc' _ = unsnoc -{-# INLINE unsnoc' #-} - - --------------------------------------------------------------------------------- ---- Slicing --------------------------------------------------------------------------------- - --- | Take the tail of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -tail :: (HasOrdinal nat, ListLike (f a) a)=> Sized f (Succ n) a -> Sized f (n :: nat) a -tail = Sized . LL.tail . runSized -{-# INLINE tail #-} - --- | Take the initial segment of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a -init = Sized . LL.init . runSized -{-# INLINE init #-} - --- | @take k xs@ takes first @k@ element of @xs@ where --- the length of @xs@ should be larger than @k@. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -take :: (ListLike (f a) a, (n <= m) ~ 'True, HasOrdinal nat) - => Sing (n :: nat) -> Sized f m a -> Sized f n a -take sn = Sized . LL.genericTake (toNatural sn) . runSized -{-# INLINE take #-} - --- | @take k xs@ takes first @k@ element of @xs@ at most. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -takeAtMost :: (ListLike (f a) a, HasOrdinal nat) - => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a -takeAtMost sn = Sized . LL.genericTake (toNatural sn) . runSized -{-# INLINE takeAtMost #-} - --- | @drop k xs@ drops first @k@ element of @xs@ and returns --- the rest of sequence, where the length of @xs@ should be larger than @k@. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -drop :: (HasOrdinal nat, ListLike (f a) a, (n <= m) ~ 'True) - => Sing (n :: nat) -> Sized f m a -> Sized f (m - n) a -drop sn = Sized . LL.genericDrop (toNatural sn) . runSized -{-# INLINE drop #-} - --- | @splitAt k xs@ split @xs@ at @k@, where --- the length of @xs@ should be less than or equal to @k@. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -splitAt :: (ListLike (f a) a , (n <= m) ~ 'True, HasOrdinal nat) - => Sing (n :: nat) -> Sized f m a -> (Sized f n a, Sized f (m -. n) a) -splitAt n (Sized xs) = - let (as, bs) = LL.genericSplitAt (toNatural n) xs - in (Sized as, Sized bs) -{-# INLINE splitAt #-} - --- | @splitAtMost k xs@ split @xs@ at @k@. --- If @k@ exceeds the length of @xs@, then the second result value become empty. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -splitAtMost :: (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a) -splitAtMost n (Sized xs) = - let (as, bs) = LL.genericSplitAt (toNatural n) xs - in (Sized as, Sized bs) -{-# INLINE splitAtMost #-} - - --------------------------------------------------------------------------------- --- Construction --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- Initialisation --------------------------------------------------------------------------------- - --- | Empty sequence. --- --- Since 0.5.0.0 (type changed) -empty :: forall f nat a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a -empty = Sized LL.empty -{-# INLINE empty #-} - --- | Sequence with one element. --- --- Since 0.1.0.0 -singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a -singleton = Sized . LL.singleton -{-# INLINE singleton #-} - --- | Consruct the 'Sized' sequence from base type, but --- the length parameter is dynamically determined and --- existentially quantified; see also 'SomeSized'. --- --- Since 0.1.0.0 -toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a) - => f a -> SomeSized f nat a -toSomeSized = \xs -> - case fromNatural $ LL.genericLength xs of - SomeSing sn -> withSingI sn $ SomeSized sn $ unsafeToSized sn xs - --- | Replicates the same value. --- --- Since 0.1.0.0 -replicate :: forall f nat (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sing n -> a -> Sized f n a -replicate sn a = Sized $ LL.genericReplicate (toNatural sn) a -{-# INLINE replicate #-} - --- | 'replicate' with the length inferred. --- --- Since 0.1.0.0 -replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a -replicate' = withSing replicate -{-# INLINE replicate' #-} - -generate :: forall (nat :: Type) (n :: nat) (a :: Type) f. - (ListLike (f a) a, HasOrdinal nat) - => Sing n -> (Ordinal n -> a) -> Sized f n a -generate n f = unsafeFromList n [f i | i <- enumOrdinal n ] -{-# INLINE [1] generate #-} - -genVector :: forall nat (n :: nat) a. - (HasOrdinal nat) - => Sing n -> (Ordinal n -> a) -> Sized V.Vector n a -genVector n f = withSingI n $ Sized $ V.generate (P.fromIntegral $ toNatural n) (f . toEnum) -{-# INLINE genVector #-} - -genSVector :: forall nat (n :: nat) a. - (HasOrdinal nat, SV.Storable a) - => Sing n -> (Ordinal n -> a) -> Sized SV.Vector n a -genSVector n f = withSingI n $ Sized $ SV.generate (P.fromIntegral $ toNatural n) (f . toEnum) -{-# INLINE genSVector #-} - -genSeq :: forall nat (n :: nat) a. - (HasOrdinal nat) - => Sing n -> (Ordinal n -> a) -> Sized Seq.Seq n a -genSeq n f = withSingI n $ Sized $ Seq.fromFunction (P.fromIntegral $ toNatural n) (f . toEnum) -{-# INLINE genSeq #-} - -{-# RULES -"generate/Vector" [~1] generate = genVector -"generate/SVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) - (f :: SV.Storable a => Ordinal n -> a). - generate n f = genSVector n f -"generate/UVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) - (f :: UV.Unbox a => Ordinal n -> a). - generate n f = withSingI n $ Sized (UV.generate (P.fromIntegral $ toNatural n) (f . toEnum)) -"generate/Seq" [~1] generate = genSeq -#-} - --------------------------------------------------------------------------------- ---- Concatenation --------------------------------------------------------------------------------- - --- | Append an element to the head of sequence. --- --- Since 0.1.0.0 -cons :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a -cons a = Sized . LL.cons a . runSized -{-# INLINE cons #-} - --- | Infix version of 'cons'. --- --- Since 0.1.0.0 -(<|) :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a -(<|) = cons -{-# INLINE (<|) #-} -infixr 5 <| - --- | Append an element to the tail of sequence. --- --- Since 0.1.0.0 -snoc :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a -snoc (Sized xs) a = Sized $ LL.snoc xs a -{-# INLINE snoc #-} - --- | Infix version of 'snoc'. --- --- Since 0.1.0.0 -(|>) :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a -(|>) = snoc -{-# INLINE (|>) #-} -infixl 5 |> - --- | Append two lists. --- --- Since 0.1.0.0 -append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n + m) a -append (Sized xs) (Sized ys) = Sized $ LL.append xs ys -{-# INLINE append #-} - --- | Infix version of 'append'. --- --- Since 0.1.0.0 -(++) :: (ListLike (f a) a) => Sized f n a -> Sized f m a -> Sized f (n + m) a -(++) = append -infixr 5 ++ - --- | Concatenates multiple sequences into one. --- --- Since 0.1.0.0 -concat :: forall f f' m n a. (Functor f', Foldable f', ListLike (f a) a) - => Sized f' m (Sized f n a) -> Sized f (m * n) a -concat = Sized . F.foldr LL.append LL.empty . P.fmap runSized -{-# INLINE [2] concat #-} - -{-# RULES -"concat/list-list" [~1] - concat = Sized . L.concatMap runSized . runSized -"concat/list-list" [~2] forall (xss :: (ListLike (f a) a, ListLike (f (Sized f n a)) (Sized f n a)) - => Sized f m (Sized f n a)). - concat xss = Sized (LL.concatMap runSized (runSized xss)) - #-} - --------------------------------------------------------------------------------- ---- Zips --------------------------------------------------------------------------------- - --- | Zipping two sequences. Length is adjusted to shorter one. --- --- Since 0.1.0.0 -zip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) - => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) -zip (Sized xs) (Sized ys) = Sized $ LL.zip xs ys -{-# INLINE [1] zip #-} -{-# RULES -"zip/Seq" [~1] - zip = (Sized .) . (. runSized) . Seq.zip . runSized -"zip/List" [~1] - zip = (Sized .) . (. runSized) . P.zip . runSized -"zip/Vector" [~1] - zip = (Sized .) . (. runSized) . V.zip . runSized -"zip/UVector" [~1] - forall (xs :: UV.Unbox a => Sized UV.Vector n a) (ys :: UV.Unbox b => Sized UV.Vector m b). - zip xs ys = Sized (UV.zip (runSized xs) (runSized ys)) - #-} - --- | 'zip' for the sequences of the same length. --- --- Since 0.1.0.0 -zipSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) - => Sized f n a -> Sized f n b -> Sized f n (a, b) -zipSame (Sized xs) (Sized ys) = Sized $ LL.zip xs ys -{-# INLINE [1] zipSame #-} -{-# RULES -"zipSame/Seq" [~1] - zipSame = (Sized .) . (. runSized) . Seq.zip . runSized -"zipSame/List" [~1] - zipSame = (Sized .) . (. runSized) . P.zip . runSized -"zipSame/Vector" [~1] - zipSame = (Sized .) . (. runSized) . V.zip . runSized -"zipSame/UVector" [~1] - forall (xs :: UV.Unbox a => Sized UV.Vector n a) (ys :: UV.Unbox b => Sized UV.Vector n b). - zipSame xs ys = Sized (UV.zip (runSized xs) (runSized ys)) - #-} - --- | Zipping two sequences with funtion. Length is adjusted to shorter one. --- --- Since 0.1.0.0 -zipWith :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) - => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c -zipWith f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys -{-# INLINE [1] zipWith #-} - -{-# RULES -"zipWith/Seq" [~1] forall f. - zipWith f = (Sized .) . (. runSized) . Seq.zipWith f . runSized -"zipWith/List" [~1] forall f. - zipWith f = (Sized .) . (. runSized) . P.zipWith f . runSized -"zipWith/Vector" [~1] forall f. - zipWith f = (Sized .) . (. runSized) . V.zipWith f . runSized -"zipWith/UVector" [~1] - forall (f :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) => a -> b -> c). - zipWith f = (Sized .) . (. runSized) . UV.zipWith f . runSized -"zipWith/MVector" [~1] - forall (f :: (SV.Storable a, SV.Storable b, SV.Storable c) => a -> b -> c). - zipWith f = (Sized .) . (. runSized) . SV.zipWith f . runSized - #-} - --- | 'zipWith' for the sequences of the same length. --- --- Since 0.1.0.0 -zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) - => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c -zipWithSame f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys -{-# INLINE [1] zipWithSame #-} - -{-# RULES -"zipWithSame/Seq" [~1] forall f. - zipWithSame f = (Sized .) . (. runSized) . Seq.zipWith f . runSized -"zipWithSame/List" [~1] forall f. - zipWithSame f = (Sized .) . (. runSized) . P.zipWith f . runSized -"zipWithSame/Vector" [~1] forall f. - zipWithSame f = (Sized .) . (. runSized) . V.zipWith f . runSized -"zipWithSame/UVector" [~1] - forall (f :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) => a -> b -> c). - zipWithSame f = (Sized .) . (. runSized) . UV.zipWith f . runSized -"zipWithSame/MVector" [~1] - forall (f :: (SV.Storable a, SV.Storable b, SV.Storable c) => a -> b -> c). - zipWithSame f = (Sized .) . (. runSized) . Seq.zipWith f . runSized - #-} - --- | Unzipping the sequence of tuples. --- --- Since 0.1.0.0 -unzip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a,b)) - => Sized f n (a, b) -> (Sized f n a, Sized f n b) -unzip (Sized xys) = - let (xs, ys) = LL.unzip xys - in (Sized xs, Sized ys) -{-# INLINE unzip #-} - - --------------------------------------------------------------------------------- --- Transformation --------------------------------------------------------------------------------- - --- | Map function. --- --- Since 0.1.0.0 -map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b -map f = Sized . LL.map f . runSized -{-# INLINE map #-} - -fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b -fmap f = Sized . P.fmap f . runSized -{-# INLINE fmap #-} - --- | Reverse function. --- --- Since 0.1.0.0 -reverse :: ListLike (f a) a => Sized f n a -> Sized f n a -reverse = Sized . LL.reverse . runSized -{-# INLINE reverse #-} - --- | Intersperces. --- --- Since 0.1.0.0 -intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 TL.* n) -. 1) a -intersperse a = Sized . LL.intersperse a . runSized -{-# INLINE intersperse #-} - --- | Remove all duplicates. --- --- Since 0.1.0.0 -nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a -nub = toSomeSized . LL.nub . runSized - --- | Sorting sequence by ascending order. --- --- Since 0.1.0.0 -sort :: (ListLike (f a) a, Ord a) - => Sized f n a -> Sized f n a -sort = Sized . LL.sort . runSized - --- | Generalized version of 'sort'. --- --- Since 0.1.0.0 -sortBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a -sortBy cmp = Sized . LL.sortBy cmp . runSized - --- | Insert new element into the presorted sequence. --- --- Since 0.1.0.0 -insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a -insert a = Sized . LL.insert a . runSized - --- | Generalized version of 'insert'. --- --- Since 0.1.0.0 -insertBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a -insertBy cmp a = Sized . LL.insertBy cmp a . runSized - - --------------------------------------------------------------------------------- --- Conversion --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- List --------------------------------------------------------------------------------- - --- | Convert to list. --- --- Since 0.1.0.0 -toList :: ListLike (f a) a => Sized f n a -> [a] -toList = LL.toList . runSized -{-# INLINE [2] toList #-} - -{-# RULES -"toList/List" - Data.Sized.toList = runSized - #-} - --- | If the given list is shorter than @n@, then returns @Nothing@ --- Otherwise returns @Sized f n a@ consisting of initial @n@ element --- of given list. --- --- Since 0.5.0.0 (type changed) -fromList :: forall f nat (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sing n -> [a] -> Maybe (Sized f n a) -fromList Zero _ = Just $ Sized (LL.empty :: f a) -fromList sn xs = - let len = P.fromIntegral $ toNatural sn - in if P.length xs < len - then Nothing - else Just $ unsafeFromList sn $ P.take len xs -{-# INLINABLE [2] fromList #-} - --- | 'fromList' with the result length inferred. --- --- Since 0.1.0.0 -fromList' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => [a] -> Maybe (Sized f n a) -fromList' = withSing fromList -{-# INLINE fromList' #-} - --- | Unsafe version of 'fromList'. If the length of the given list does not --- equal to @n@, then something unusual happens. --- --- Since 0.1.0.0 -unsafeFromList :: forall (nat :: Type) f (n :: nat) a. ListLike (f a) a => Sing n -> [a] -> Sized f n a -unsafeFromList _ xs = Sized $ LL.fromList xs -{-# INLINE [1] unsafeFromList #-} -{-# RULES -"unsafeFromList/List" [~1] - unsafeFromList = P.const Sized -"unsafeFromList/Vector" [~1] - unsafeFromList = P.const (Sized . V.fromList) -"unsafeFromList/Seq" [~1] - unsafeFromList = P.const (Sized . Seq.fromList) -"unsafeFromList/SVector" [~1] forall s (xs :: SV.Storable a => [a]). - unsafeFromList s xs = Sized (SV.fromList xs) -"unsafeFromList/UVector" [~1] forall s (xs :: UV.Unbox a => [a]). - unsafeFromList s xs = Sized (UV.fromList xs) - #-} - --- | 'unsafeFromList' with the result length inferred. --- --- Since 0.1.0.0 -unsafeFromList' :: (SingI (n :: TL.Nat), ListLike (f a) a) => [a] -> Sized f n a -unsafeFromList' = withSing unsafeFromList -{-# INLINE [1] unsafeFromList' #-} -{-# RULES -"unsafeFromList'/List" [~1] - unsafeFromList' = Sized -"unsafeFromList'/Vector" [~1] - unsafeFromList' = Sized . V.fromList -"unsafeFromList'/Seq" [~1] - unsafeFromList' = Sized . Seq.fromList -"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]). - unsafeFromList' xs = Sized (SV.fromList xs) -"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]). - unsafeFromList' xs = Sized (UV.fromList xs) - #-} - - --- | Construct a @Sized f n a@ by padding default value if the given list is short. --- --- Since 0.5.0.0 (type changed) -fromListWithDefault :: forall f nat (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sing n -> a -> [a] -> Sized f n a -fromListWithDefault sn def xs = - let len = toNatural sn - in Sized $ LL.fromList (L.genericTake len xs) `LL.append` LL.genericReplicate (len - L.genericLength xs) def -{-# INLINABLE fromListWithDefault #-} - --- | 'fromListWithDefault' with the result length inferred. --- --- Since 0.1.0.0 -fromListWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> [a] -> Sized f n a -fromListWithDefault' = withSing fromListWithDefault -{-# INLINE fromListWithDefault' #-} - --------------------------------------------------------------------------------- ---- Base containes --------------------------------------------------------------------------------- - --- | Forget the length and obtain the wrapped base container. --- --- Since 0.1.0.0 -unsized :: Sized f n a -> f a -unsized = runSized -{-# INLINE unsized #-} - --- | If the length of the input is shorter than @n@, then returns @Nothing@. --- Otherwise returns @Sized f n a@ consisting of initial @n@ element --- of the input. --- --- Since 0.1.0.0 -toSized :: (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> f a -> Maybe (Sized f n a) -toSized sn xs = - let len = toNatural sn - in if LL.genericLength xs < len - then Nothing - else Just $ unsafeToSized sn $ LL.genericTake len xs -{-# INLINABLE [2] toSized #-} - --- | 'toSized' with the result length inferred. --- --- Since 0.1.0.0 -toSized' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => f a -> Maybe (Sized f n a) -toSized' = withSing toSized -{-# INLINE toSized' #-} - --- | Unsafe version of 'toSized'. If the length of the given list does not --- equal to @n@, then something unusual happens. --- --- Since 0.1.0.0 -unsafeToSized :: Sing n -> f a -> Sized f n a -unsafeToSized _ = Sized -{-# INLINE [2] unsafeToSized #-} - --- | 'unsafeToSized' with the result length inferred. --- --- Since 0.1.0.0 -unsafeToSized' :: (SingI (n :: TL.Nat), ListLike (f a) a) => f a -> Sized f n a -unsafeToSized' = withSing unsafeToSized -{-# INLINE unsafeToSized' #-} - --- | Construct a @Sized f n a@ by padding default value if the given list is short. --- --- Since 0.1.0.0 -toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> a -> f a -> Sized f n a -toSizedWithDefault sn def xs = - let len = P.fromIntegral $ toNatural sn - in Sized $ LL.take len xs `LL.append` LL.replicate (len - LL.length xs) def -{-# INLINABLE toSizedWithDefault #-} - --- | 'toSizedWithDefault' with the result length inferred. --- --- Since 0.1.0.0 -toSizedWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> f a -> Sized f n a -toSizedWithDefault' = withSing toSizedWithDefault -{-# INLINE toSizedWithDefault' #-} - - --------------------------------------------------------------------------------- --- Querying --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- Partitioning --------------------------------------------------------------------------------- - --- | The type @Partitioned f n a@ represents partitioned sequence of length @n@. --- Value @Partitioned lenL ls lenR rs@ stands for: --- --- * Entire sequence is divided into @ls@ and @rs@, and their length --- are @lenL@ and @lenR@ resp. --- --- * @lenL + lenR = n@ --- --- Since 0.1.0.0 -data Partitioned f n a where - Partitioned :: (ListLike (f a) a) - => Sing n - -> Sized f (n :: TL.Nat) a - -> Sing m - -> Sized f (m :: TL.Nat) a - -> Partitioned f (n + m) a - --- | Take the initial segment as long as elements satisfys the predicate. --- --- Since 0.1.0.0 -takeWhile :: (HasOrdinal nat, ListLike (f a) a) - => (a -> Bool) -> Sized f n a -> SomeSized f nat a -takeWhile p = toSomeSized . LL.takeWhile p . runSized -{-# INLINE takeWhile #-} - --- | Drop the initial segment as long as elements satisfys the predicate. --- --- Since 0.1.0.0 -dropWhile :: (HasOrdinal nat, ListLike (f a) a) - => (a -> Bool) -> Sized f n a -> SomeSized f nat a -dropWhile p = toSomeSized . LL.dropWhile p . runSized -{-# INLINE dropWhile #-} - --- | Invariant: @'ListLike' (f a) a@ instance must be implemented --- to satisfy the following property: --- @length (fst (span p xs)) + length (snd (span p xs)) == length xs@ --- Otherwise, this function introduces severe contradiction. --- --- Since 0.1.0.0 -span :: ListLike (f a) a - => (a -> Bool) -> Sized f n a -> Partitioned f n a -span p xs = - let (as, bs) = LL.span p $ runSized xs - in case (toSomeSized as, toSomeSized bs) of - (SomeSized lenL ls, SomeSized lenR rs) -> - unsafeCoerce $ Partitioned lenL ls lenR rs -{-# INLINE span #-} - --- | Invariant: @'ListLike' (f a) a@ instance must be implemented --- to satisfy the following property: --- @length (fst (break p xs)) + length (snd (break p xs)) == length xs@ --- Otherwise, this function introduces severe contradiction. --- --- Since 0.1.0.0 -break :: ListLike (f a) a - => (a -> Bool) -> Sized f n a -> Partitioned f n a -break p (Sized xs) = - let (as, bs) = LL.break p xs - in case (toSomeSized as, toSomeSized bs) of - (SomeSized lenL ls, SomeSized lenR rs) -> - unsafeCoerce $ Partitioned lenL ls lenR rs -{-# INLINE break #-} - --- | Invariant: @'ListLike' (f a) a@ instance must be implemented --- to satisfy the following property: --- @length (fst (partition p xs)) + length (snd (partition p xs)) == length xs@ --- Otherwise, this function introduces severe contradiction. --- --- Since 0.1.0.0 -partition :: ListLike (f a) a - => (a -> Bool) -> Sized f n a -> Partitioned f n a -partition p (Sized xs) = - let (as, bs) = LL.partition p xs - in case (toSomeSized as, toSomeSized bs) of - (SomeSized lenL ls, SomeSized lenR rs) -> - unsafeCoerce $ Partitioned lenL ls lenR rs -{-# INLINE partition #-} - --------------------------------------------------------------------------------- ---- Searching --------------------------------------------------------------------------------- --- | Membership test; see also 'notElem'. --- --- Since 0.1.0.0 -elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool -elem a = LL.elem a . runSized -{-# INLINE elem #-} - --- | Negation of 'elem'. --- --- Since 0.1.0.0 -notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool -notElem a = LL.notElem a . runSized -{-# INLINE notElem #-} - --- | Find the element satisfying the predicate. --- --- Since 0.1.0.0 -find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a -find p = F.find p -{-# INLINE[1] find #-} -{-# RULES -"find/List" [~1] forall p. - find p = L.find p . runSized -"find/Vector" [~1] forall p. - find p = V.find p . runSized -"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool). - find p = SV.find p . runSized -"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool). - find p = UV.find p . runSized - #-} - --- | @'Foldable'@ version of @'find'@. -findF :: (Foldable f) => (a -> Bool) -> Sized f n a -> Maybe a -findF p = getFirst. F.foldMap (\a -> if p a then First (Just a) else First Nothing) . runSized -{-# INLINE [1] findF #-} -{-# SPECIALISE [0] findF :: (a -> Bool) -> Sized Seq.Seq n a -> Maybe a #-} -{-# RULES -"findF/list" [~1] findF = (. runSized) . L.find -"findF/Vector" [~1] findF = (. runSized) . V.find - #-} - --- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists. --- --- Since 0.1.0.0 -findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int -findIndex p = LL.findIndex p . runSized -{-# INLINE findIndex #-} - --- | 'Ordinal' version of 'findIndex'. --- --- Since 0.1.0.0 -sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) - => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) -sFindIndex p = P.fmap toEnum . findIndex p -{-# INLINE sFindIndex #-} - --- | @'findIndex'@ implemented in terms of @'FoldableWithIndex'@ -findIndexIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> Maybe i -findIndexIF p = P.fmap fst . ifind (P.const p) . runSized -{-# INLINE [1] findIndexIF #-} -{-# RULES -"findIndexIF/list" [~1] forall p. - findIndexIF p = L.findIndex p . runSized -"findIndexIF/vector" [~1] forall p. - findIndexIF p = V.findIndex p . runSized - #-} - --- | @'sFindIndex'@ implemented in terms of @'FoldableWithIndex'@ -sFindIndexIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n) - => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n) -sFindIndexIF p = P.fmap fst . ifind (P.const p) -{-# INLINE [1] sFindIndexIF #-} -{-# RULES -"sFindIndexIF/list" [~1] forall p . - sFindIndexIF p = P.fmap toEnum . L.findIndex p . runSized -"sFindIndexIF/vector" [~1] forall p. - sFindIndexIF p = P.fmap toEnum . V.findIndex p . runSized - #-} - --- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. --- --- Since 0.1.0.0 -findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int] -findIndices p = LL.findIndices p . runSized -{-# INLINE findIndices #-} -{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-} - --- | @'findIndices'@ implemented in terms of @'FoldableWithIndex'@ -findIndicesIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> [i] -findIndicesIF p = flip appEndo [] . ifoldMap (\i x -> if p x then Endo (i:) else Endo P.id) . runSized -{-# INLINE [1] findIndicesIF #-} -{-# RULES -"findIndicesIF/list" [~1] forall p. - findIndicesIF p = L.findIndices p . runSized -"findIndicesIF/vector" [~1] forall p. - findIndicesIF p = V.toList . V.findIndices p . runSized - #-} - - --- | 'Ordinal' version of 'findIndices'. --- --- Since 0.1.0.0 -sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) - => (a -> Bool) -> Sized f n a -> [Ordinal n] -sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p -{-# INLINE sFindIndices #-} - -sFindIndicesIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n) - => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n] -sFindIndicesIF p = flip appEndo [] . - ifoldMap (\i x -> if p x then Endo (P.toEnum (P.fromIntegral i):) else Endo P.id) . - runSized -{-# INLINE [1] sFindIndicesIF #-} -{-# RULES -"sFindIndicesIF/list" [~1] forall p. - sFindIndicesIF p = P.map toEnum . L.findIndices p . runSized -"sFindIndicesIF/vector" [~1] forall p. - sFindIndicesIF p = V.toList . V.map toEnum . V.findIndices p . runSized - #-} - -{-# RULES -"Foldable.sum/Vector" - F.sum = V.sum . runSized - #-} - --- | Returns the index of the given element in the list, if exists. --- --- Since 0.1.0.0 -elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int -elemIndex a (Sized xs) = LL.elemIndex a xs -{-# INLINE elemIndex #-} - --- | Ordinal version of 'elemIndex' --- It statically checks boundary invariants. --- If you don't internal structure on @'Sized'@, --- then @'sUnsafeElemIndex'@ is much faster and --- also safe for most cases. --- --- Since 0.5.0.0 (type changed) -sElemIndex :: forall nat (n :: nat) f a. - (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) - => a -> Sized f n a -> Maybe (Ordinal n) -sElemIndex a (Sized xs) = do - i <- LL.elemIndex a xs - case fromNatural (P.fromIntegral i) of - SomeSing sn -> - case sn %< (sing :: Sing n) of - STrue -> Just (OLt sn) - SFalse -> Nothing -{-# INLINE sElemIndex #-} - --- | Since 0.5.0.0 (type changed) -sUnsafeElemIndex :: forall nat (n :: nat) f a. - (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) - => a -> Sized f n a -> Maybe (Ordinal n) -sUnsafeElemIndex a (Sized xs) = - unsafeNaturalToOrd . P.fromIntegral <$> LL.elemIndex a xs - --- | Returns all indices of the given element in the list. --- --- Since 0.1.0.0 -elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int] -elemIndices a = LL.elemIndices a . runSized -{-# INLINE elemIndices #-} - --- | Ordinal version of 'elemIndices' --- --- Since 0.1.0.0 -sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a) - => a -> Sized f n a -> [Ordinal n] -sElemIndices p = P.fmap (unsafeNaturalToOrd . P.fromIntegral) . elemIndices p -{-# INLINE sElemIndices #-} - --------------------------------------------------------------------------------- --- Views and Patterns --------------------------------------------------------------------------------- - -{-$ViewsAndPatterns #ViewsAndPatterns# - - With GHC's @ViewPatterns@ and @PatternSynonym@ extensions, - we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor. - Curretnly, there are two direction view and patterns: Cons and Snoc. - Assuming underlying sequence type @f@ has O(1) implementation for 'LL.null', 'LL.head' - (resp. 'LL.last') and 'LL.tail' (resp. 'LL.init'), We can view and pattern-match on - cons (resp. snoc) of @Sized f n a@ in O(1). --} - -{-$views #views# - - With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows: - -@ -slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n -slen ('viewCons' -> 'NilCV') = 'SZ' -slen ('viewCons' -> _ ':-' as) = 'SS' (slen as) -slen _ = error "impossible" -@ - - The constraint @('SingI' n, 'ListLike (f a) a' f)@ is needed for view function. - In the above, we have extra wildcard pattern (@_@) at the last. - Code compiles if we removed it, but current GHC warns for incomplete pattern, - although we know first two patterns exhausts all the case. - - Equivalently, we can use snoc-style pattern-matching: - -@ -slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n -slen ('viewSnoc' -> 'NilSV') = 'SZ' -slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as) -@ --} - --- | View of the left end of sequence (cons-side). --- --- Since 0.1.0.0 -data ConsView f n a where - NilCV :: ConsView f (Zero nat) a - (:-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a - -infixr 5 :- - --- | Case analysis for the cons-side of sequence. --- --- Since 0.5.0.0 (type changed) -viewCons :: forall f a nat (n :: nat). (HasOrdinal nat, ListLike (f a) a) - => Sized f n a - -> ConsView f n a -viewCons sz = case zeroOrSucc (sLength sz) of - IsZero -> NilCV - IsSucc n' -> withSingI n' $ P.uncurry (:-) (uncons' n' sz) - --- | View of the left end of sequence (snoc-side). --- --- Since 0.1.0.0 -data SnocView f n a where - NilSV :: SnocView f (Zero nat) a - (:-::) :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a -infixl 5 :-:: - --- | Case analysis for the snoc-side of sequence. --- --- Since 0.5.0.0 (type changed) -viewSnoc :: forall f nat (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sized f n a - -> SnocView f n a -viewSnoc sz = case zeroOrSucc (sLength sz) of - IsZero -> NilSV - IsSucc n' -> - withSingI n' $ P.uncurry (:-::) (unsnoc' n' sz) - -{-$patterns #patterns# - - So we can pattern match on both end of sequence via views, but - it is rather clumsy to nest it. For example: - -@ -nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a -nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a -@ - - In such a case, with @PatternSynonyms@ extension we can write as follows: - -@ -nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a -nextToHead (_ ':<' a ':<' _) = a -@ - - Of course, we can also rewrite above @slen@ example using @PatternSynonyms@: - -@ -slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n -slen 'NilL' = 'SZ' -slen (_ ':<' as) = 'SS' (slen as) -slen _ = error "impossible" -@ - - So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to - pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. - @':<'@, @'NilL'@, @':>'@ and @'NilR'@ are neither functions nor data constructors, - but pattern synonyms so we cannot use them in expression contexts. - For more detail on pattern synonyms, see - - and - . --} - -infixr 5 :< --- | Pattern synonym for cons-side uncons. -pattern (:<) :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). - (n ~ Succ n1, SingI n1) - => a -> Sized f n1 a -> Sized f n a -pattern a :< as <- (viewCons -> a :- as) where - a :< as = a <| as - -pattern NilL :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => (n ~ Zero nat) => Sized f n a -pattern NilL <- (viewCons -> NilCV) where - NilL = empty - -infixl 5 :> - -pattern (:>) :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). - (n ~ Succ n1, SingI n1) - => Sized f n1 a -> a -> Sized f n a -pattern a :> b <- (viewSnoc -> a :-:: b) where - a :> b = a |> b - -pattern NilR :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => n ~ Zero nat => Sized f n a -pattern NilR <- (viewSnoc -> NilSV) where - NilR = empty - --- | Applicative instance, generalizing @'Data.Monoid.ZipList'@. -instance (Functor f, HasOrdinal nat, SingI n, ListLikeF f) - => P.Applicative (Sized f (n :: nat)) where - {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.Nat)) #-} - - pure (x :: a) = - withListLikeF (Nothing :: Maybe (f a)) $ - replicate' x - {-# INLINE pure #-} - - (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) = - withListLikeF (Nothing :: Maybe (f (a -> b))) $ - withListLikeF (Nothing :: Maybe (f a)) $ - withListLikeF (Nothing :: Maybe (f b)) $ - zipWithSame ($) fs xs - {-# INLINE [1] (<*>) #-} -{-# RULES -"<*>/List" [~1] forall fs xs. - Sized fs <*> Sized xs = Sized (getZipList (ZipList fs <*> ZipList xs)) -"<*>/Seq" [~1] forall fs xs. - Sized fs <*> Sized xs = Sized (Seq.zipWith ($) fs xs) -"<*>/Vector" [~1] forall fs xs. - Sized fs <*> Sized xs = Sized (V.zipWith ($) fs xs) - #-} diff --git a/Data/Sized/Builtin.hs b/Data/Sized/Builtin.hs deleted file mode 100644 --- a/Data/Sized/Builtin.hs +++ /dev/null @@ -1,48 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} -{-# LANGUAGE ViewPatterns #-} -#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} -#endif --- | This module exports @'S.Sized'@ type specialized to --- GHC's built-in type numeral @'TL.Nat'@. -module Data.Sized.Builtin - (Ordinal, Sized, module Data.Sized, - pattern (:<), pattern NilL, pattern (:>), pattern NilR) where -import Data.Sized hiding ((:<), (:>), NilL, NilR, Sized) -import qualified Data.Sized as S - -import Data.ListLike (ListLike) -import Data.Singletons.Prelude (SingI) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Ordinal as O -import qualified GHC.TypeLits as TL - -type Ordinal (n :: TL.Nat) = O.Ordinal n -type Sized f (n :: TL.Nat) = S.Sized f n - -pattern (:<) :: forall f (n :: TL.Nat) a. - (ListLike (f a) a) - => forall (n1 :: TL.Nat). - (n ~ Succ n1, SingI n1) - => a -> Sized f n1 a -> Sized f n a -pattern a :< b = a S.:< b -infixr 5 :< - -pattern NilL :: forall f (n :: TL.Nat) a. - (ListLike (f a) a) - => n ~ 0 => Sized f n a -pattern NilL = S.NilL - -pattern (:>) :: forall f (n :: TL.Nat) a. - (ListLike (f a) a) - => forall (n1 :: TL.Nat). - (n ~ Succ n1, SingI n1) - => Sized f n1 a -> a -> Sized f n a -pattern a :> b = a S.:> b -infixl 5 :> - -pattern NilR :: forall f (n :: TL.Nat) a. - (ListLike (f a) a, SingI n) - => n ~ 0 => Sized f n a -pattern NilR = S.NilR diff --git a/Data/Sized/Flipped.hs b/Data/Sized/Flipped.hs deleted file mode 100644 --- a/Data/Sized/Flipped.hs +++ /dev/null @@ -1,96 +0,0 @@ -{-# LANGUAGE CPP, ConstraintKinds, DataKinds, DeriveDataTypeable #-} -{-# LANGUAGE DeriveFunctor, DeriveTraversable, EmptyDataDecls #-} -{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} -{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-} -{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-} -#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} -#endif -module Data.Sized.Flipped (Flipped(..), - pattern (:<), pattern NilL, - pattern (:>), pattern NilR) where -import qualified Data.Sized as Orig -import Data.Sized.Internal - -import Control.DeepSeq (NFData (..)) -import Control.Lens.At (Index, IxValue, Ixed (..)) -import Control.Lens.TH (makeWrapped) -import Control.Lens.Wrapped (_Wrapped) -import Data.Hashable (Hashable (..)) -import Data.Kind (Type) -import qualified Data.ListLike as LL -import Data.MonoTraversable (Element, MonoFoldable (..)) -import Data.MonoTraversable (MonoFunctor (..)) -import Data.MonoTraversable (MonoTraversable (..)) -import qualified Data.Sequence as Seq -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Natural as PN -import Data.Type.Natural.Class (Zero) -import Data.Type.Ordinal (HasOrdinal, Ordinal (..)) -import Data.Typeable (Typeable) -import qualified Data.Vector as V -import qualified Data.Vector.Storable as SV -import qualified Data.Vector.Unboxed as UV -import qualified GHC.TypeLits as TL - --- | Wrapper for @'Sized'@ which takes length as its last element, instead of the second. --- --- Since 0.2.0.0 -newtype Flipped f a n = Flipped { runFlipped :: Sized f n a } - deriving (Show, Eq, Ord, Typeable, NFData, Hashable) - -makeWrapped ''Flipped - -type instance Index (Flipped f a n) = Ordinal n -type instance IxValue (Flipped f a n) = IxValue (f a) -type instance Element (Flipped f a n) = Element (Sized f n a) -deriving instance MonoFunctor (f a) => MonoFunctor (Flipped f a n) -deriving instance MonoFoldable (f a) => MonoFoldable (Flipped f a n) -instance (MonoTraversable (f a)) => MonoTraversable (Flipped f a n) where - otraverse = _Wrapped . otraverse - {-# INLINE otraverse #-} - - omapM = _Wrapped . omapM - {-# INLINE omapM #-} - -instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat) - => Ixed (Flipped f a (n :: nat)) where - {-# SPECIALISE instance Ixed (Flipped [] a (n :: TL.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped [] a (n :: PN.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-} - ix o = _Wrapped . ix o - {-# INLINE ix #-} - -pattern (:<) :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1) - => a -> Flipped f a n1 -> Flipped f a n -pattern a :< as <- Flipped (a Orig.:< (Flipped -> as)) where - a :< Flipped as = Flipped (a Orig.:< as) - -pattern NilL :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => n ~ Zero nat => Flipped f a n -pattern NilL = Flipped Orig.NilL - -pattern (:>) :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1) - => Flipped f a n1 -> a -> Flipped f a n -pattern as :> a <- Flipped ((Flipped -> as) Orig.:> a) where - Flipped as :> a = Flipped (as Orig.:> a) - -pattern NilR :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => n ~ Zero nat => Flipped f a n -pattern NilR = Flipped Orig.NilR diff --git a/Data/Sized/Internal.hs b/Data/Sized/Internal.hs deleted file mode 100644 --- a/Data/Sized/Internal.hs +++ /dev/null @@ -1,261 +0,0 @@ -{-# LANGUAGE CPP, ConstraintKinds, DataKinds, DeriveDataTypeable #-} -{-# LANGUAGE DeriveFunctor, DeriveTraversable, ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} -{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-} -{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-} -#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} -#endif -{-# OPTIONS_GHC -fno-warn-orphans #-} -module Data.Sized.Internal - (Sized(..),instLL, instFunctor, ListLikeF, - withListLikeF, withListLikeF' - ) where -import Control.DeepSeq (NFData (..)) -import Control.Lens.At (Index, IxValue, Ixed (..)) -import Control.Lens.Indexed (FoldableWithIndex (..), - FunctorWithIndex (..), - TraversableWithIndex (..)) -import Data.Constraint ((:-) (..), (:=>) (..), Class (..), - Dict (..), trans, weaken1, weaken2, - (&&&), (\\)) -import Data.Constraint.Forall (Forall, inst) -import Data.Foldable (Foldable) -import Data.Hashable (Hashable (..)) -import Data.Kind (Type) -import Data.ListLike (ListLike) -import Data.MonoTraversable (Element, MonoFoldable (..), - MonoFunctor (..), - MonoTraversable (..)) -import Data.Proxy (Proxy (..)) -import qualified Data.Sequence as Seq -import Data.Singletons.Prelude (SingI) -import Data.Traversable (Traversable) -import qualified Data.Type.Natural as PN -import Data.Type.Ordinal (HasOrdinal, Ordinal (..), - ordToNatural, unsafeNaturalToOrd) -import Data.Typeable (Typeable) -import qualified Data.Vector as V -import qualified Data.Vector.Storable as SV -import qualified Data.Vector.Unboxed as UV -import qualified GHC.TypeLits as TL - --- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version. --- --- Here, 'f' must be the instance of 'Functor' and @'ListLike' (f a) a@ for all @a@. --- This constraint is expressed by 'ListLikeF'. --- Folding and traversing function such as 'all' and 'foldl'' is available --- via 'Foldable' or 'Traversable' class, if 'f' is the instance of them. --- --- Since 0.2.0.0 -newtype Sized (f :: Type -> Type) (n :: nat) a = - Sized { runSized :: f a - } deriving (Eq, Ord, Typeable, - Functor, Foldable, Traversable) - -type instance Element (Sized f n a) = Element (f a) - --- | Since 0.2.0.0 -deriving instance MonoFoldable (f a) - => MonoFoldable (Sized f n a) - --- | Since 0.2.0.0 -deriving instance MonoFunctor (f a) - => MonoFunctor (Sized f n a) - --- | Since 0.2.0.0 -instance {-# OVERLAPPABLE #-} (MonoTraversable (f a)) - => MonoTraversable (Sized f n a) where - {-# SPECIALISE instance MonoTraversable (Sized [] n a) #-} - {-# SPECIALISE instance MonoTraversable (Sized V.Vector n a) #-} - {-# SPECIALISE instance MonoTraversable (Sized Seq.Seq n a) #-} - {-# SPECIALISE instance UV.Unbox a => MonoTraversable (Sized UV.Vector n a) #-} - {-# SPECIALISE instance SV.Storable a => MonoTraversable (Sized SV.Vector n a) #-} - otraverse f = fmap Sized . otraverse f . runSized - omapM f = fmap Sized . omapM f. runSized - --- | Since 0.6.0.0 -instance {-# OVERLAPPING #-} SV.Storable a => MonoTraversable (Sized SV.Vector n a) where - otraverse f = fmap Sized . otraverse f . runSized - omapM f = fmap Sized . omapM f . runSized - --- | Since 0.6.0.0 -instance {-# OVERLAPPING #-} UV.Unbox a => MonoTraversable (Sized UV.Vector n a) where - otraverse f = fmap Sized . otraverse f . runSized - omapM f = fmap Sized . omapM f . runSized - -deriving instance NFData (f a) => NFData (Sized f n a) -deriving instance Hashable (f a) => Hashable (Sized f n a) - -instance Show (f a) => Show (Sized f n a) where - showsPrec d (Sized x) = showsPrec d x - --- | Since 0.2.0.0 -type instance Index (Sized f n a) = Ordinal n - --- | Since 0.3.0.0 -type instance IxValue (Sized f n a) = IxValue (f a) -instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat) - => Ixed (Sized f (n :: nat) a) where - {-# SPECIALISE instance Ixed (Sized [] (n :: TL.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized [] (n :: PN.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized V.Vector (n :: TL.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized V.Vector (n :: PN.Nat) a) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: TL.Nat) a) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: PN.Nat) a) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: TL.Nat) a) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: PN.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: TL.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: PN.Nat) a) #-} - {-# INLINE ix #-} - ix n f = fmap Sized . ix (fromIntegral $ ordToNatural n) f . runSized - --- | Since 0.2.0.0 -instance (Integral i, FunctorWithIndex i f, HasOrdinal nat, SingI n) - => FunctorWithIndex (Ordinal (n :: nat)) (Sized f n) where - imap f = Sized . imap (f . unsafeNaturalToOrd . fromIntegral) . runSized - {-# INLINE imap #-} - {-# SPECIALISE instance TL.KnownNat n - => FunctorWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FunctorWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} - --- | Since 0.4.0.0 -instance {-# OVERLAPPABLE #-} (Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n) - => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where - ifoldMap f = ifoldMap (f . unsafeNaturalToOrd . fromIntegral) . runSized - {-# INLINE ifoldMap #-} - - ifoldr f e = ifoldr (f . unsafeNaturalToOrd . fromIntegral) e . runSized - {-# INLINE ifoldr #-} - - ifoldl f e = ifoldl (f . unsafeNaturalToOrd . fromIntegral) e . runSized - {-# INLINE ifoldl #-} - - ifoldr' f e = ifoldr' (f . unsafeNaturalToOrd . fromIntegral) e . runSized - {-# INLINE ifoldr' #-} - - ifoldl' f e = ifoldl' (f . unsafeNaturalToOrd . fromIntegral) e . runSized - {-# INLINE ifoldl' #-} - - {-# SPECIALISE instance TL.KnownNat n - => FoldableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FoldableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} - --- | Since 0.2.0.0 -instance (Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n) - => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where - itraverse f = fmap Sized . itraverse (f . unsafeNaturalToOrd . fromIntegral) . runSized - {-# INLINE itraverse #-} - - {-# SPECIALISE instance TL.KnownNat n - => TraversableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => TraversableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} - -class (ListLike (f a) a) => LLF f a -instance (ListLike (f a) a) => LLF f a - -instance Class (ListLike (f a) a) (LLF f a) where - cls = Sub Dict -instance (LLF f a) :=> (ListLike (f a) a) where - ins = Sub Dict - --- | Functor @f@ such that there is instance @ListLike (f a) a@ for any @a@. --- --- Since 0.1.0.0 -type ListLikeF f = (Functor f, Forall (LLF f)) - -instLLF :: forall f a. Forall (LLF f) :- ListLike (f a) a -instLLF = trans ins inst -{-# INLINE [1] instLLF #-} -{-# RULES -"instLLF/List" [~1] - instLLF = Sub Dict :: Forall (LLF []) :- ListLike [a] a -"instLLF/Seq" [~1] - instLLF = Sub Dict :: Forall (LLF Seq.Seq) :- ListLike (Seq.Seq a) a -"instLLF/Vector" [~1] - instLLF = Sub Dict :: Forall (LLF V.Vector) :- ListLike (V.Vector a) a - #-} - -instLL :: forall f a. ListLikeF f :- ListLike (f a) a -instLL = trans instLLF weaken2 -{-# INLINE [1] instLL #-} -{-# RULES -"instLL/List" [~1] - instLL = Sub Dict :: ListLikeF [] :- ListLike [a] a -"instLL/Seq" [~1] - instLL = Sub Dict :: ListLikeF Seq.Seq :- ListLike (Seq.Seq a) a -"instLL/Vector" [~1] - instLL = Sub Dict :: ListLikeF V.Vector :- ListLike (V.Vector a) a - #-} - - -instFunctor :: ListLikeF f :- Functor f -instFunctor = weaken1 -{-# INLINE [1] instFunctor #-} -{-# RULES -"instFunctor/List" [~1] - instFunctor = Sub Dict :: ListLikeF [] :- Functor [] -"instFunctor/Seq" [~1] - instFunctor = Sub Dict :: ListLikeF Seq.Seq :- Functor Seq.Seq -"instFunctor/Vector" [~1] - instFunctor = Sub Dict :: ListLikeF V.Vector :- Functor V.Vector - #-} - -withListLikeF :: forall pxy f a b. ListLikeF f - => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b -withListLikeF _ b = b \\ llDic &&& instFunctor - where - llDic = instLL :: ListLikeF f :- ListLike (f a) a -{-# RULES -"withListLikeF/List" [~1] forall (pxy :: proxy [a]). - withListLikeF pxy = id -"withListLikeF/Seq" [~1] forall (pxy :: proxy (Seq.Seq a)). - withListLikeF pxy = id -"withListLikeF/Vector" [~1] forall (pxy :: proxy (V.Vector a)). - withListLikeF pxy = id - #-} -{-# INLINE [1] withListLikeF #-} - -withListLikeF' :: ListLikeF f => f a -> ((Functor f, ListLike (f a) a) => b) -> b -withListLikeF' xs = withListLikeF (toProxy xs) -{-# RULES -"withListLikeF'/List" [~1] forall (pxy :: [a]). - withListLikeF' pxy = id -"withListLikeF'/Seq" [~1] forall (pxy :: (Seq.Seq a)). - withListLikeF' pxy = id -"withListLikeF'/Vector" [~1] forall (pxy ::(V.Vector a)). - withListLikeF' pxy = id - #-} -{-# INLINE [1] withListLikeF' #-} - -toProxy :: a -> Proxy a -toProxy _ = Proxy diff --git a/Data/Sized/Peano.hs b/Data/Sized/Peano.hs deleted file mode 100644 --- a/Data/Sized/Peano.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} -{-# LANGUAGE ViewPatterns #-} --- | This module exports @'S.Sized'@ type specialized to --- type-level Peano numeral @'PN.Nat'@. -module Data.Sized.Peano - (Ordinal, Sized, module Data.Sized, - pattern (:<), pattern NilL, pattern (:>), pattern NilR) where -import Data.Sized hiding ((:<), (:>), NilL, NilR, Sized) -import qualified Data.Sized as S - -import Data.ListLike (ListLike) -import Data.Singletons.Prelude (SingI) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Ordinal as O -import qualified Data.Type.Natural as PN - -type Ordinal (n :: PN.Nat) = O.Ordinal n -type Sized f (n :: PN.Nat) = S.Sized f n - -pattern (:<) :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => forall (n1 :: PN.Nat). - (n ~ Succ n1, SingI n1) - => a -> Sized f n1 a -> Sized f n a -pattern a :< b = a S.:< b -infixr 5 :< - -pattern NilL :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => n ~ 'PN.Z => Sized f n a -pattern NilL = S.NilL - -pattern (:>) :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => forall (n1 :: PN.Nat). - (n ~ Succ n1, SingI n1) - => Sized f n1 a -> a -> Sized f n a -pattern a :> b = a S.:> b -infixl 5 :> - -pattern NilR :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => n ~ 'PN.Z => Sized f n a -pattern NilR = S.NilR diff --git a/sized.cabal b/sized.cabal --- a/sized.cabal +++ b/sized.cabal @@ -1,46 +1,68 @@ --- Initial sized-sequences.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/ +cabal-version: >=2.0 +name: sized +version: 0.7.0.0 +license: BSD3 +license-file: LICENSE +maintainer: konn.jinro_at_gmail.com +author: Hiromi ISHII +tested-with: + ghc ==8.6.5, ghc ==8.8.3, ghc ==8.10.1 -name: sized -version: 0.6.0.0 -synopsis: Sized sequence data-types -description: A wrapper to make length-parametrized data-type from ListLike data-types. -license: BSD3 -license-file: LICENSE -author: Hiromi ISHII -maintainer: konn.jinro_at_gmail.com --- copyright: -category: Data -build-type: Simple --- extra-source-files: -cabal-version: >=1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.2, - GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.1 +synopsis: Sized sequence data-types +description: + A wrapper to make length-parametrized data-type from functorial data-types. +category: Data +build-type: Simple + source-repository head - Type: git - Location: git://github.com/konn/sized.git + type: git + location: git://github.com/konn/sized.git library - exposed-modules: Data.Sized - , Data.Sized.Builtin - , Data.Sized.Peano - , Data.Sized.Flipped - other-modules: Data.Sized.Internal - -- other-extensions: - build-depends: base == 4.* - , type-natural >= 0.8.1.0 - , ghc-typelits-presburger >= 0.2.0.0 - , mono-traversable >= 0.10 - , ListLike >= 4.5 - , singletons >= 2.0 - , deepseq >= 1.4 - , hashable >= 1.2 - , vector >= 0.12 - , containers >= 0.5 - , constraints >= 0.9 - , equational-reasoning >= 0.5 - , lens >= 0.14 - -- hs-source-dirs: - default-language: Haskell2010 - ghc-options: -O2 -Wall -Wno-redundant-constraints + exposed-modules: + Data.Sized + Data.Sized.Builtin + Data.Sized.Peano + Data.Sized.Flipped + + hs-source-dirs: src + other-modules: Data.Sized.Internal + default-language: Haskell2010 + ghc-options: -O2 -Wall -Wno-redundant-constraints + build-depends: + base ==4.*, + constraints, + these, + type-natural >=0.8.1.0, + ghc-typelits-presburger >=0.2.0.0, + ghc-typelits-knownnat, + mono-traversable >=0.10, + singletons >=2.0, + subcategories, + deepseq >=1.4, + hashable >=1.2, + vector >=0.12, + containers >=0.5, + equational-reasoning >=0.5, + lens >=0.14 + +test-suite optimisaion-test + type: exitcode-stdio-1.0 + main-is: opt-test.hs + hs-source-dirs: test + other-modules: Shared + default-language: Haskell2010 + ghc-options: -O2 -Wall -Wno-redundant-constraints -fno-hpc + build-depends: + base -any, + containers -any, + hspec -any, + inspection-testing ^>=0.4, + mono-traversable -any, + singletons -any, + sized -any, + template-haskell -any, + th-lift -any, + subcategories -any, + vector -any diff --git a/src/Data/Sized.hs b/src/Data/Sized.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized.hs @@ -0,0 +1,1397 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds #-} +{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-} +{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-} +{-# LANGUAGE PatternSynonyms, PolyKinds, QuantifiedConstraints, ScopedTypeVariables, RankNTypes #-} +{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies #-} +{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-} +#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 +{-# LANGUAGE NoStarIsType #-} +#endif + +{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-} +{-# OPTIONS_GHC -fenable-rewrite-rules #-} +-- | This module provides the functionality to make length-parametrized types +-- from existing 'CFreeMonoid' sequential types. +-- +-- Most of the complexity of operations for @Sized f n a@ are the same as +-- original operations for @f@. For example, '!!' is O(1) for +-- @Sized Vector n a@ but O(i) for @Sized [] n a@. +-- +-- This module also provides powerful view types and pattern synonyms to +-- inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail. +module Data.Sized + ( -- * Main Data-types + Sized(), SomeSized'(..), + DomC(), + -- * Accessors + -- ** Length information + length, sLength, null, + -- ** Indexing + (!!), (%!!), index, sIndex, head, last, + uncons, uncons', Uncons(..), + unsnoc, unsnoc', Unsnoc(..), + -- ** Slicing + tail, init, take, takeAtMost, drop, splitAt, splitAtMost, + -- * Construction + -- ** Initialisation + empty, singleton, toSomeSized, replicate, replicate', generate, + -- ** Concatenation + cons, (<|), snoc, (|>), append, (++), concat, + -- ** Zips + zip, zipSame, zipWith, zipWithSame, unzip, unzipWith, + -- * Transformation + map, reverse, intersperse, nub, sort, sortBy, insert, insertBy, + -- * Conversion + -- ** List + toList, fromList, fromList', unsafeFromList, unsafeFromList', + fromListWithDefault, fromListWithDefault', + -- ** Base container + unsized, + toSized, toSized', unsafeToSized, unsafeToSized', + toSizedWithDefault, toSizedWithDefault', + -- * Querying + -- ** Partitioning + Partitioned(..), + takeWhile, dropWhile, span, break, partition, + -- ** Searching + elem, notElem, find, findIndex, sFindIndex, + findIndices, sFindIndices, + elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, + -- * Views and Patterns + -- $ViewsAndPatterns + + -- ** Views + -- $views + + -- ** Patterns + -- $patterns + + -- ** Definitions + viewCons, ConsView (..), viewSnoc, SnocView(..), + + pattern (:<), pattern NilL , pattern (:>), pattern NilR, + ) where + +import Data.Sized.Internal + +import qualified Data.Foldable as F +import Data.Kind (Type) +import Data.Monoid +import Control.Applicative ((<*>), ZipList(..)) +import qualified Data.List as L +import qualified Data.Sequence as Seq +import Data.Singletons.Prelude.Bool +import Data.Constraint +import Data.Singletons.Prelude (SomeSing(..)) +import Data.Singletons.Prelude (SingI (..)) +import Data.Singletons.Prelude (withSing, withSingI) +import Control.Subcategory +import Data.Singletons.Prelude.Enum (sSucc, sPred, PEnum (..)) +import qualified Data.Type.Natural as Peano +import Data.Type.Natural.Class +import Data.Type.Ordinal (HasOrdinal, Ordinal (..)) +import Data.Type.Ordinal (ordToNatural) +import Data.Typeable (Typeable) +import qualified Data.Vector as V +import qualified Data.Vector.Storable as SV +import qualified Data.Vector.Unboxed as UV +import qualified GHC.TypeLits as TL +import Prelude (fmap, uncurry, fromIntegral, const, Bool (..), Enum (..), Eq (..)) +import Prelude (Functor, Int, Maybe (..)) +import Prelude (Num (..), Ord (..), Ordering) +import Prelude (Show (..), flip, ($), (.)) +import qualified Prelude as P +import Unsafe.Coerce (unsafeCoerce) +import Data.Coerce (coerce) +import Data.Maybe (fromJust) +import Data.These (These(..)) +import Data.Type.Equality (gcastWith) +import Proof.Propositional (withWitness, IsTrue(Witness)) +import Data.Type.Equality ((:~:)(..)) + +-------------------------------------------------------------------------------- +-- Main data-types +-------------------------------------------------------------------------------- + +-- | 'Sized' vector with the length is existentially quantified. +-- This type is used mostly when the return type's length cannot +-- be statically determined beforehand. +-- +-- @SomeSized' sn xs :: SomeSized' f a@ stands for the 'Sized' sequence +-- @xs@ of element type @a@ and length @sn@. +-- +-- Since 0.7.0.0 +data SomeSized' f nat a where + SomeSized' :: Sing n + -> Sized f (n :: nat) a + -> SomeSized' f nat a + +deriving instance Typeable SomeSized' + +instance Show (f a) => Show (SomeSized' f nat a) where + showsPrec d (SomeSized' _ s) = P.showParen (d > 9) $ + P.showString "SomeSized' _ " . showsPrec 10 s +instance Eq (f a) => Eq (SomeSized' f nat a) where + (SomeSized' _ (Sized xs)) == (SomeSized' _ (Sized ys)) = xs == ys + +-------------------------------------------------------------------------------- +-- Accessors +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Length infromation +-------------------------------------------------------------------------------- + +-- | Returns the length of wrapped containers. +-- If you use @unsafeFromList@ or similar unsafe functions, +-- this function may return different value from type-parameterized length. +-- +-- Since 0.7.0.0 +length + :: forall nat f (n :: nat) a. + (IsPeano nat, CFoldable f, Dom f a, SingI n) + => Sized f n a -> Int +length = const $ fromIntegral $ toNatural $ sing @n +{-# INLINE CONLIKE [1] length #-} + +lengthTLZero :: Sized f 0 a -> Int +lengthTLZero = P.const 0 +{-# INLINE lengthTLZero #-} + +lengthPeanoZero :: Sized f 'Peano.Z a -> Int +lengthPeanoZero = P.const 0 +{-# INLINE lengthPeanoZero #-} + +{-# RULES +"length/0" [~1] length = lengthTLZero +"length/Z" [~1] length = lengthPeanoZero + #-} + +-- | @Sing@ version of 'length'. +-- +-- Since 0.7.0.0 (type changed) +sLength :: forall nat f (n :: nat) a. (HasOrdinal nat, CFoldable f, Dom f a) + => Sized f n a -> Sing n +sLength (Sized xs) = + case fromNatural (P.fromIntegral $ clength xs) of + SomeSing (n :: Sing (k :: nat)) -> unsafeCoerce n +{-# INLINE[2] sLength #-} + +-- | Test if the sequence is empty or not. +-- +-- Since 0.7.0.0 +null + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) + => Sized f n a -> Bool +null = coerce $ cnull @f @a +{-# INLINE CONLIKE [2] null #-} + +nullTL0 :: Sized f 0 a -> Bool +nullTL0 = P.const True +{-# INLINE nullTL0 #-} + +nullPeano0 :: Sized f 'Peano.Z a -> Bool +nullPeano0 = P.const True +{-# INLINE nullPeano0 #-} + +nullPeanoSucc :: Sized f (S n) a -> Bool +nullPeanoSucc = P.const False +{-# INLINE nullPeanoSucc #-} + +nullTLSucc :: Sized f (n + 1) a -> Bool +nullTLSucc = P.const False +{-# INLINE nullTLSucc #-} + +{-# RULES +"null/0" [~2] null = nullTL0 +"null/0" [~1] forall (vec :: (1 TL.<= n) => Sized f n a). + null vec = False +"null/0" [~2] null = nullTLSucc +"null/Z" [~2] null = nullPeano0 +"null/Sn" [~2] null = nullPeanoSucc +#-} + +-------------------------------------------------------------------------------- +--- Indexing +-------------------------------------------------------------------------------- + +-- | (Unsafe) indexing with @Int@s. +-- If you want to check boundary statically, use '%!!' or 'sIndex'. +-- +-- Since 0.7.0.0 +(!!) + :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True) + => Sized f m a -> Int -> a +(!!) = coerce $ cindex @f @a +{-# INLINE (!!) #-} + +-- | Safe indexing with 'Ordinal's. +-- +-- Since 0.7.0.0 +(%!!) + :: forall nat f (n :: nat) c. + (HasOrdinal nat, CFoldable f, Dom f c) + => Sized f n c -> Ordinal n -> c +(%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c +{-# INLINE (%!!) #-} +{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-} +{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-} + +-- | Flipped version of '!!'. +-- +-- Since 0.7.0.0 +index + :: forall nat f (m :: nat) a. + (CFoldable f, Dom f a, (One nat <= m) ~ 'True) + => Int -> Sized f m a -> a +index = flip (!!) +{-# INLINE index #-} + +-- | Flipped version of '%!!'. +-- +-- Since 0.7.0.0 +sIndex + :: forall nat f (n :: nat) c. (HasOrdinal nat, CFoldable f, Dom f c) + => Ordinal n -> Sized f n c -> c +sIndex = flip $ (%!!) @nat @f @n @c +{-# INLINE sIndex #-} + +-- | Take the first element of non-empty sequence. +-- If you want to make case-analysis for general sequence, +-- see <#ViewsAndPatterns Views and Patterns> section. +-- +-- Since 0.7.0.0 +head + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True) + => Sized f n a -> a +head = coerce $ chead @f @a +{-# INLINE head #-} + +-- | Take the last element of non-empty sequence. +-- If you want to make case-analysis for general sequence, +-- see <#ViewsAndPatterns Views and Patterns> section. +-- +-- Since 0.7.0.0 +last :: forall nat f (n :: nat) a. + (HasOrdinal nat, (Zero nat < n) ~ 'True, CFoldable f, Dom f a) + => Sized f n a -> a +last = coerce $ clast @f @a +{-# INLINE last #-} + +-- | Take the 'head' and 'tail' of non-empty sequence. +-- If you want to make case-analysis for general sequence, +-- see <#ViewsAndPatterns Views and Patterns> section. +-- +-- Since 0.7.0.0 +uncons :: forall nat f (n :: nat) a. + (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True) + => Sized f n a -> Uncons f n a +uncons = + withSingI + (sPred $ sing @n) + $ gcastWith + (lneqRightPredSucc sZero (sing @n) Witness + ) + $ uncurry (Uncons @nat @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a) + +uncons' + :: forall nat f (n :: nat) a proxy. + (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) + => proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a +uncons' _ = withSingI (sSucc $ sing @n) + $ withWitness (lneqZero $ sing @n) uncons +{-# INLINE uncons' #-} + +data Uncons f (n :: nat) a where + Uncons :: forall nat f (n :: nat) a. SingI n + => a -> Sized f n a -> Uncons f (Succ n) a + +-- | Take the 'init' and 'last' of non-empty sequence. +-- If you want to make case-analysis for general sequence, +-- see <#ViewsAndPatterns Views and Patterns> section. +-- +-- Since 0.7.0.0 +unsnoc + :: forall nat f (n :: nat) a. + (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True) + => Sized f n a -> Unsnoc f n a +unsnoc = withSingI + (sPred $ sing @n) + $ gcastWith + (lneqRightPredSucc sZero (sing @n) Witness + ) + $ uncurry (Unsnoc @nat @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a) +{-# NOINLINE [1] unsnoc #-} + +data Unsnoc f n a where + Unsnoc :: forall nat f n a. Sized f (n :: nat) a -> a -> Unsnoc f (Succ n) a + +unsnoc' + :: forall nat f (n :: nat) a proxy. + (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) + => proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a +unsnoc' _ = + withSingI (sSucc $ sing @n) + $ withWitness (lneqZero $ sing @n) unsnoc +{-# INLINE unsnoc' #-} + + +-------------------------------------------------------------------------------- +--- Slicing +-------------------------------------------------------------------------------- + +-- | Take the tail of non-empty sequence. +-- If you want to make case-analysis for general sequence, +-- see <#ViewsAndPatterns Views and Patterns> section. +-- +-- Since 0.7.0.0 +tail + :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sized f (One nat + n) a -> Sized f n a +tail = coerce $ ctail @f @a +{-# INLINE tail #-} + +-- | Take the initial segment of non-empty sequence. +-- If you want to make case-analysis for general sequence, +-- see <#ViewsAndPatterns Views and Patterns> section. +-- +-- Since 0.7.0.0 +init + :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sized f (n + One nat) a -> Sized f n a +init = coerce $ cinit @f @a +{-# INLINE init #-} + +-- | @take k xs@ takes first @k@ element of @xs@ where +-- the length of @xs@ should be larger than @k@. +-- +-- Since 0.7.0.0 +take + :: forall nat (n :: nat) f (m :: nat) a. + (CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat) + => Sing n -> Sized f m a -> Sized f n a +take = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n +{-# INLINE take #-} + +-- | @take k xs@ takes first @k@ element of @xs@ at most. +-- +-- Since 0.7.0.0 +takeAtMost + :: forall nat (n :: nat) f m a. + (CFreeMonoid f, Dom f a, HasOrdinal nat) + => Sing n -> Sized f m a -> Sized f (Min n m) a +takeAtMost = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n +{-# INLINE takeAtMost #-} + +-- | @drop k xs@ drops first @k@ element of @xs@ and returns +-- the rest of sequence, where the length of @xs@ should be larger than @k@. +-- +-- Since 0.7.0.0 +drop + :: forall nat (n :: nat) f (m :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True) + => Sing n -> Sized f m a -> Sized f (m - n) a +drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @nat @n +{-# INLINE drop #-} + +-- | @splitAt k xs@ split @xs@ at @k@, where +-- the length of @xs@ should be less than or equal to @k@. +-- +-- Since 0.7.0.0 +splitAt + :: forall nat (n :: nat) f m a. + (CFreeMonoid f, Dom f a , (n <= m) ~ 'True, HasOrdinal nat) + => Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a) +splitAt = + coerce $ csplitAt @f @a . P.fromIntegral . toNatural @nat @n +{-# INLINE splitAt #-} + +-- | @splitAtMost k xs@ split @xs@ at @k@. +-- If @k@ exceeds the length of @xs@, then the second result value become empty. +-- +-- Since 0.7.0.0 +splitAtMost + :: forall nat (n :: nat) f (m :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a) +splitAtMost = + coerce $ csplitAt @f @a . P.fromIntegral . toNatural @nat @n +{-# INLINE splitAtMost #-} + + +-------------------------------------------------------------------------------- +-- Construction +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Initialisation +-------------------------------------------------------------------------------- + +-- | Empty sequence. +-- +-- Since 0.7.0.0 (type changed) +empty + :: forall nat f a. (Monoid (f a), HasOrdinal nat, Dom f a) + => Sized f (Zero nat) a +empty = coerce $ mempty @(f a) +{-# INLINE empty #-} + +-- | Sequence with one element. +-- +-- Since 0.7.0.0 +singleton :: forall nat f a. (CPointed f, Dom f a) => a -> Sized f (One nat) a +singleton = coerce $ cpure @f @a +{-# INLINE singleton #-} + +-- | Consruct the 'Sized' sequence from base type, but +-- the length parameter is dynamically determined and +-- existentially quantified; see also 'SomeSized''. +-- +-- Since 0.7.0.0 +toSomeSized + :: forall nat f a. (HasOrdinal nat, Dom f a, CFoldable f) + => f a -> SomeSized' f nat a +toSomeSized = \xs -> + case fromNatural $ P.fromIntegral $ clength xs of + SomeSing sn -> withSingI sn $ SomeSized' sn $ unsafeToSized sn xs + +-- | Replicates the same value. +-- +-- Since 0.7.0.0 +replicate :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sing n -> a -> Sized f n a +replicate = coerce $ creplicate @f @a . P.fromIntegral . toNatural @nat @n +{-# INLINE replicate #-} + +-- | 'replicate' with the length inferred. +-- +-- Since 0.7.0.0 +replicate' + :: forall nat f (n :: nat) a. + (HasOrdinal nat, SingI (n :: nat), CFreeMonoid f, Dom f a) + => a -> Sized f n a +replicate' = withSing replicate +{-# INLINE replicate' #-} + +-- | Since 0.7.0.0 +generate + :: forall (nat :: Type) f (n :: nat) (a :: Type). + (CFreeMonoid f, Dom f a, HasOrdinal nat) + => Sing n -> (Ordinal n -> a) -> Sized f n a +generate = coerce $ \sn -> withSingI sn $ + cgenerate @f @a (P.fromIntegral $ toNatural @nat @n sn) + . (. toEnum @(Ordinal n)) +{-# INLINE [1] generate #-} + +genVector :: forall nat (n :: nat) a. + (HasOrdinal nat) + => Sing n -> (Ordinal n -> a) -> Sized V.Vector n a +genVector n f = withSingI n $ Sized $ V.generate (P.fromIntegral $ toNatural n) (f . toEnum) +{-# INLINE genVector #-} + +genSVector :: forall nat (n :: nat) a. + (HasOrdinal nat, SV.Storable a) + => Sing n -> (Ordinal n -> a) -> Sized SV.Vector n a +genSVector n f = withSingI n $ Sized $ SV.generate (P.fromIntegral $ toNatural n) (f . toEnum) +{-# INLINE genSVector #-} + +genSeq :: forall nat (n :: nat) a. + (HasOrdinal nat) + => Sing n -> (Ordinal n -> a) -> Sized Seq.Seq n a +genSeq n f = withSingI n $ Sized $ Seq.fromFunction (P.fromIntegral $ toNatural n) (f . toEnum) +{-# INLINE genSeq #-} + +{-# RULES +"generate/Vector" [~1] generate = genVector +"generate/SVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) + (f :: SV.Storable a => Ordinal n -> a). + generate n f = genSVector n f +"generate/UVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) + (f :: UV.Unbox a => Ordinal n -> a). + generate n f = withSingI n $ Sized (UV.generate (P.fromIntegral $ toNatural n) (f . toEnum)) +"generate/Seq" [~1] generate = genSeq +#-} + +-------------------------------------------------------------------------------- +--- Concatenation +-------------------------------------------------------------------------------- + +-- | Append an element to the head of sequence. +-- +-- Since 0.7.0.0 +cons + :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a) + => a -> Sized f n a -> Sized f (Succ n) a +cons = coerce $ ccons @f @a +{-# INLINE cons #-} + +-- | Infix version of 'cons'. +-- +-- Since 0.7.0.0 +(<|) + :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) + => a -> Sized f n a -> Sized f (Succ n) a +(<|) = cons +{-# INLINE (<|) #-} +infixr 5 <| + +-- | Append an element to the tail of sequence. +-- +-- Since 0.7.0.0 +snoc + :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a) + => Sized f n a -> a -> Sized f (n + One nat) a +snoc (Sized xs) a = Sized $ csnoc xs a +{-# INLINE snoc #-} + +-- | Infix version of 'snoc'. +-- +-- Since 0.7.0.0 +(|>) :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a +(|>) = snoc +{-# INLINE (|>) #-} +infixl 5 |> + +-- | Append two lists. +-- +-- Since 0.7.0.0 +append + :: forall nat f (n :: nat) (m :: nat) a. + (CFreeMonoid f, Dom f a) + => Sized f n a -> Sized f m a -> Sized f (n + m) a +append = coerce $ mappend @(f a) +{-# INLINE append #-} + +-- | Infix version of 'append'. +-- +-- Since 0.7.0.0 +(++) + :: forall nat f (n :: nat) (m :: nat) a. + (CFreeMonoid f, Dom f a) + => Sized f n a -> Sized f m a -> Sized f (n + m) a +(++) = append +infixr 5 ++ + +-- | Concatenates multiple sequences into one. +-- +-- Since 0.7.0.0 +concat :: forall nat f' (m :: nat) f (n :: nat) a. + (CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a), + Dom f' (Sized f n a) + ) + => Sized f' m (Sized f n a) -> Sized f (m * n) a +concat = coerce $ cfoldMap @f' @(Sized f n a) runSized +{-# INLINE [2] concat #-} + +-------------------------------------------------------------------------------- +--- Zips +-------------------------------------------------------------------------------- + +-- | Zipping two sequences. Length is adjusted to shorter one. +-- +-- Since 0.7.0.0 +zip + :: forall nat f (n :: nat) a (m :: nat) b. + (Dom f a, CZip f, Dom f b, Dom f (a, b)) + => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) +zip = coerce $ czip @f @a @b + +-- | 'zip' for the sequences of the same length. +-- +-- Since 0.7.0.0 +zipSame + :: forall nat f (n :: nat) a b. + (Dom f a, CZip f, Dom f b, Dom f (a, b)) + => Sized f n a -> Sized f n b -> Sized f n (a, b) +zipSame = coerce $ czip @f @a @b +{-# INLINE [1] zipSame #-} + +-- | Zipping two sequences with funtion. Length is adjusted to shorter one. +-- +-- Since 0.7.0.0 +zipWith + :: forall nat f (n :: nat) a (m :: nat) b c. + (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) + => (a -> b -> c) + -> Sized f n a + -> Sized f m b + -> Sized f (Min n m) c +zipWith = coerce $ czipWith @f @a @b @c +{-# INLINE [1] zipWith #-} + +-- | 'zipWith' for the sequences of the same length. +-- +-- Since 0.7.0.0 +zipWithSame + :: forall nat f (n :: nat) a b c. + (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) + => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c +{-# SPECIALISE INLINE [1] zipWithSame + :: (a -> b -> c) -> Sized [] n a -> Sized [] n b -> Sized [] n c + #-} +{-# SPECIALISE INLINE [1] zipWithSame + :: (a -> b -> c) + -> Sized V.Vector n a -> Sized V.Vector n b -> Sized V.Vector n c + #-} +{-# SPECIALISE INLINE [1] zipWithSame + :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) + => (a -> b -> c) + -> Sized UV.Vector n a -> Sized UV.Vector n b -> Sized UV.Vector n c + #-} +{-# SPECIALISE INLINE [1] zipWithSame + :: (SV.Storable a, SV.Storable b, SV.Storable c) + => (a -> b -> c) + -> Sized SV.Vector n a -> Sized SV.Vector n b -> Sized SV.Vector n c + #-} +zipWithSame = coerce $ czipWith @f @a @b @c +{-# INLINE [1] zipWithSame #-} + +-- | Unzipping the sequence of tuples. +-- +-- Since 0.7.0.0 +unzip + :: forall nat f (n :: nat) a b. + (CUnzip f, Dom f a, Dom f b, Dom f (a, b)) + => Sized f n (a, b) -> (Sized f n a, Sized f n b) +unzip = coerce $ cunzip @f @a @b +{-# INLINE unzip #-} + +-- | Unzipping the sequence of tuples. +-- +-- Since 0.7.0.0 +unzipWith + :: forall nat f (n :: nat) a b c. + (CUnzip f, Dom f a, Dom f b, Dom f c) + => (a -> (b, c)) + -> Sized f n a -> (Sized f n b, Sized f n c) +unzipWith = coerce $ cunzipWith @f @a @b @c +{-# INLINE unzipWith #-} + +-------------------------------------------------------------------------------- +-- Transformation +-------------------------------------------------------------------------------- + +-- | Map function. +-- +-- Since 0.7.0.0 +map + :: forall nat f (n :: nat) a b. + (CFreeMonoid f, Dom f a, Dom f b) + => (a -> b) -> Sized f n a -> Sized f n b +map f = Sized . cmap f . runSized +{-# INLINE map #-} + +-- | Reverse function. +-- +-- Since 0.7.0.0 +reverse + :: forall nat f (n :: nat) a. + (Dom f a, CFreeMonoid f) + => Sized f n a -> Sized f n a +reverse = coerce $ creverse @f @a +{-# INLINE reverse #-} + +-- | Intersperces. +-- +-- Since 0.7.0.0 +intersperse + :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a) + => a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a +intersperse = coerce $ cintersperse @f @a +{-# INLINE intersperse #-} + +-- | Remove all duplicates. +-- +-- Since 0.7.0.0 +nub + :: forall nat f (n :: nat) a. + (HasOrdinal nat, Dom f a, Eq a, CFreeMonoid f) + => Sized f n a -> SomeSized' f nat a +nub = toSomeSized . coerce (cnub @f @a) + +-- | Sorting sequence by ascending order. +-- +-- Since 0.7.0.0 +sort :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a, Ord a) + => Sized f n a -> Sized f n a +sort = coerce $ csort @f @a + +-- | Generalized version of 'sort'. +-- +-- Since 0.7.0.0 +sortBy + :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) + => (a -> a -> Ordering) -> Sized f n a -> Sized f n a +sortBy = coerce $ csortBy @f @a + +-- | Insert new element into the presorted sequence. +-- +-- Since 0.7.0.0 +insert + :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a, Ord a) + => a -> Sized f n a -> Sized f (Succ n) a +insert = coerce $ cinsert @f @a + +-- | Generalized version of 'insert'. +-- +-- Since 0.7.0.0 +insertBy + :: forall nat f (n :: nat) a. + (CFreeMonoid f, Dom f a) + => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a +insertBy = coerce $ cinsertBy @f @a + +-------------------------------------------------------------------------------- +-- Conversion +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- List +-------------------------------------------------------------------------------- + +-- | Convert to list. +-- +-- Since 0.7.0.0 +toList + :: forall nat f (n :: nat) a. + (CFoldable f, Dom f a) + => Sized f n a -> [a] +toList = coerce $ ctoList @f @a +{-# INLINE [2] toList #-} + +{-# RULES +"toList/List" + Data.Sized.toList = runSized + #-} + +-- | If the given list is shorter than @n@, then returns @Nothing@ +-- Otherwise returns @Sized f n a@ consisting of initial @n@ element +-- of given list. +-- +-- Since 0.7.0.0 (type changed) +fromList + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sing n -> [a] -> Maybe (Sized f n a) +fromList Zero _ = Just $ Sized (mempty :: f a) +fromList sn xs = + let len = P.fromIntegral $ toNatural sn + in if P.length xs < len + then Nothing + else Just $ Sized $ ctake len $ cfromList xs +{-# INLINABLE [2] fromList #-} + +-- | 'fromList' with the result length inferred. +-- +-- Since 0.7.0.0 +fromList' + :: forall nat f (n :: nat) a. + (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n) + => [a] -> Maybe (Sized f n a) +fromList' = withSing fromList +{-# INLINE fromList' #-} + +-- | Unsafe version of 'fromList'. If the length of the given list does not +-- equal to @n@, then something unusual happens. +-- +-- Since 0.7.0.0 +unsafeFromList + :: forall (nat :: Type) f (n :: nat) a. + (CFreeMonoid f, Dom f a) + => Sing n -> [a] -> Sized f n a +unsafeFromList = const $ coerce $ cfromList @f @a +{-# INLINE [1] unsafeFromList #-} + +-- | 'unsafeFromList' with the result length inferred. +-- +-- Since 0.7.0.0 +unsafeFromList' + :: forall nat f (n :: nat) a. + (SingI n, CFreeMonoid f, Dom f a) + => [a] -> Sized f n a +unsafeFromList' = withSing unsafeFromList +{-# INLINE [1] unsafeFromList' #-} +{-# RULES +"unsafeFromList'/List" [~1] + unsafeFromList' = Sized +"unsafeFromList'/Vector" [~1] + unsafeFromList' = Sized . V.fromList +"unsafeFromList'/Seq" [~1] + unsafeFromList' = Sized . Seq.fromList +"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]). + unsafeFromList' xs = Sized (SV.fromList xs) +"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]). + unsafeFromList' xs = Sized (UV.fromList xs) + #-} + +-- | Construct a @Sized f n a@ by padding default value if the given list is short. +-- +-- Since 0.5.0.0 (type changed) +fromListWithDefault + :: forall nat f (n :: nat) a. + (HasOrdinal nat, Dom f a, CFreeMonoid f) + => Sing n -> a -> [a] -> Sized f n a +fromListWithDefault sn def xs = + let len = P.fromIntegral $ toNatural sn + in Sized $ cfromList (ctake len xs) <> + creplicate (len - clength xs) def +{-# INLINABLE fromListWithDefault #-} + +-- | 'fromListWithDefault' with the result length inferred. +-- +-- Since 0.7.0.0 +fromListWithDefault' + :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a) + => a -> [a] -> Sized f n a +fromListWithDefault' = withSing fromListWithDefault +{-# INLINE fromListWithDefault' #-} + +-------------------------------------------------------------------------------- +--- Base containes +-------------------------------------------------------------------------------- + +-- | Forget the length and obtain the wrapped base container. +-- +-- Since 0.7.0.0 +unsized :: forall nat f (n :: nat) a. Sized f n a -> f a +unsized = runSized +{-# INLINE unsized #-} + +-- | If the length of the input is shorter than @n@, then returns @Nothing@. +-- Otherwise returns @Sized f n a@ consisting of initial @n@ element +-- of the input. +-- +-- Since 0.7.0.0 +toSized + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sing (n :: nat) -> f a -> Maybe (Sized f n a) +toSized sn xs = + let len = P.fromIntegral $ toNatural sn + in if clength xs < len + then Nothing + else Just $ unsafeToSized sn $ ctake len xs +{-# INLINABLE [2] toSized #-} + +-- | 'toSized' with the result length inferred. +-- +-- Since 0.7.0.0 +toSized' + :: forall nat f (n :: nat) a. + (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n) + => f a -> Maybe (Sized f n a) +toSized' = withSing toSized +{-# INLINE toSized' #-} + +-- | Unsafe version of 'toSized'. If the length of the given list does not +-- equal to @n@, then something unusual happens. +-- +-- Since 0.7.0.0 +unsafeToSized :: forall nat f (n :: nat) a. Sing n -> f a -> Sized f n a +unsafeToSized _ = Sized +{-# INLINE [2] unsafeToSized #-} + +-- | 'unsafeToSized' with the result length inferred. +-- +-- Since 0.7.0.0 +unsafeToSized' + :: forall nat f (n :: nat) a. + (SingI n, Dom f a) + => f a -> Sized f n a +unsafeToSized' = withSing unsafeToSized +{-# INLINE unsafeToSized' #-} + +-- | Construct a @Sized f n a@ by padding default value if the given list is short. +-- +-- Since 0.7.0.0 +toSizedWithDefault + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => Sing (n :: nat) -> a -> f a -> Sized f n a +toSizedWithDefault sn def xs = + let len = P.fromIntegral $ toNatural sn + in Sized $ ctake len xs <> creplicate (len - clength xs) def +{-# INLINABLE toSizedWithDefault #-} + +-- | 'toSizedWithDefault' with the result length inferred. +-- +-- Since 0.7.0.0 +toSizedWithDefault' + :: forall nat f (n :: nat) a. + (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a) + => a -> f a -> Sized f n a +toSizedWithDefault' = withSing toSizedWithDefault +{-# INLINE toSizedWithDefault' #-} + + +-------------------------------------------------------------------------------- +-- Querying +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Partitioning +-------------------------------------------------------------------------------- + +-- | The type @Partitioned f n a@ represents partitioned sequence of length @n@. +-- Value @Partitioned lenL ls lenR rs@ stands for: +-- +-- * Entire sequence is divided into @ls@ and @rs@, and their length +-- are @lenL@ and @lenR@ resp. +-- +-- * @lenL + lenR = n@ +-- +-- Since 0.7.0.0 +data Partitioned f n a where + Partitioned :: (Dom f a) + => Sing n + -> Sized f n a + -> Sing m + -> Sized f m a + -> Partitioned f (n + m) a + +-- | Take the initial segment as long as elements satisfys the predicate. +-- +-- Since 0.7.0.0 +takeWhile + :: forall nat f (n :: nat) a. + (HasOrdinal nat, Dom f a, CFreeMonoid f) + => (a -> Bool) -> Sized f n a -> SomeSized' f nat a +takeWhile = (toSomeSized .) . coerce (ctakeWhile @f @a) +{-# INLINE takeWhile #-} + +-- | Drop the initial segment as long as elements satisfys the predicate. +-- +-- Since 0.7.0.0 +dropWhile + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => (a -> Bool) -> Sized f n a -> SomeSized' f nat a +dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a) +{-# INLINE dropWhile #-} + +-- | Since 0.7.0.0 +span + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => (a -> Bool) -> Sized f n a -> Partitioned f n a +span = (unsafePartitioned @nat @n .) . coerce (cspan @f @a) +{-# INLINE span #-} + +-- | Since 0.7.0.0 +break + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => (a -> Bool) -> Sized f n a -> Partitioned f n a +break = (unsafePartitioned @nat @n .) . coerce (cbreak @f @a) +{-# INLINE break #-} + +-- | Since 0.7.0.0 +partition + :: forall nat f (n :: nat) a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => (a -> Bool) -> Sized f n a -> Partitioned f n a +partition = (unsafePartitioned @nat @n .) . coerce (cpartition @f @a) +{-# INLINE partition #-} + +unsafePartitioned + :: forall nat (n :: nat) f a. + (HasOrdinal nat, CFreeMonoid f, Dom f a) + => (f a, f a) -> Partitioned f n a +unsafePartitioned (l, r) = + case (toSomeSized @nat l, toSomeSized @nat r) of + ( SomeSized' (lenL :: Sing nl) ls, + SomeSized' (lenR :: Sing nr) rs + ) -> + gcastWith + (unsafeCoerce $ Refl @() + :: n :~: nl + nr + ) + $ Partitioned lenL ls lenR rs + +-------------------------------------------------------------------------------- +--- Searching +-------------------------------------------------------------------------------- +-- | Membership test; see also 'notElem'. +-- +-- Since 0.7.0.0 +elem + :: forall nat f (n :: nat) a. + (CFoldable f, Dom f a, Eq a) + => a -> Sized f n a -> Bool +elem = coerce $ celem @f @a +{-# INLINE elem #-} + +-- | Negation of 'elem'. +-- +-- Since 0.7.0.0 +notElem + :: forall nat f (n :: nat) a. + (CFoldable f, Dom f a, Eq a) + => a -> Sized f n a -> Bool +notElem = coerce $ cnotElem @f @a +{-# INLINE notElem #-} + +-- | Find the element satisfying the predicate. +-- +-- Since 0.7.0.0 +find + :: forall nat f (n :: nat) a. + (CFoldable f, Dom f a) + => (a -> Bool) -> Sized f n a -> Maybe a +find = coerce $ cfind @f @a +{-# INLINE[1] find #-} +{-# RULES +"find/List" [~1] forall p. + find p = L.find @[] p . runSized +"find/Vector" [~1] forall p. + find p = V.find p . runSized +"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool). + find p = SV.find p . runSized +"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool). + find p = UV.find p . runSized + #-} + +-- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists. +-- +-- Since 0.7.0.0 +findIndex + :: forall nat f (n :: nat) a . + (CFoldable f, Dom f a) + => (a -> Bool) -> Sized f n a -> Maybe Int +findIndex = coerce $ cfindIndex @f @a +{-# INLINE findIndex #-} + +-- | 'Ordinal' version of 'findIndex'. +-- +-- Since 0.7.0.0 +sFindIndex + :: forall nat f (n :: nat) a . + (SingI (n :: nat), CFoldable f, Dom f a, HasOrdinal nat) + => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) +sFindIndex = (fmap toEnum .) . coerce (cfindIndex @f @a) +{-# INLINE sFindIndex #-} + + +-- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. +-- +-- Since 0.7.0.0 +findIndices + :: forall nat f (n :: nat) a . + (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> [Int] +findIndices = coerce $ cfindIndices @f @a +{-# INLINE findIndices #-} +{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-} + +-- | 'Ordinal' version of 'findIndices'. +-- +-- Since 0.7.0.0 +sFindIndices + :: forall nat f (n :: nat) a . + (HasOrdinal nat, CFoldable f, Dom f a, SingI (n :: nat)) + => (a -> Bool) -> Sized f n a -> [Ordinal n] +sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p +{-# INLINE sFindIndices #-} + + +{-# RULES +"Foldable.sum/Vector" + F.sum = V.sum . runSized + #-} + +-- | Returns the index of the given element in the list, if exists. +-- +-- Since 0.7.0.0 +elemIndex :: forall nat f (n :: nat) a . + (CFoldable f, Eq a, Dom f a) => a -> Sized f n a -> Maybe Int +elemIndex = coerce $ celemIndex @f @a +{-# INLINE elemIndex #-} + +-- | Ordinal version of 'elemIndex'. +-- Since 0.7.0.0, we no longer do boundary check inside the definition. +-- +-- Since 0.7.0.0 +sElemIndex, sUnsafeElemIndex :: forall nat f (n :: nat) a. + (SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat) + => a -> Sized f n a -> Maybe (Ordinal n) +sElemIndex = (fmap toEnum .) . coerce (celemIndex @f @a) +{-# INLINE sElemIndex #-} + +-- | Since 0.5.0.0 (type changed) +sUnsafeElemIndex = sElemIndex +{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-} + +-- | Returns all indices of the given element in the list. +-- +-- Since 0.7.0.0 +elemIndices + :: forall nat f (n :: nat) a . + (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> [Int] +elemIndices = coerce $ celemIndices @f @a +{-# INLINE elemIndices #-} + +-- | Ordinal version of 'elemIndices' +-- +-- Since 0.7.0.0 +sElemIndices + :: forall nat f (n :: nat) a . + (CFoldable f, HasOrdinal nat, SingI (n :: nat), Dom f a, Eq a) + => a -> Sized f n a -> [Ordinal n] +sElemIndices = (fmap toEnum .) . elemIndices +{-# INLINE sElemIndices #-} + +-------------------------------------------------------------------------------- +-- Views and Patterns +-------------------------------------------------------------------------------- + +{-$ViewsAndPatterns #ViewsAndPatterns# + + With GHC's @ViewPatterns@ and @PatternSynonym@ extensions, + we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor. + Curretnly, there are two direction view and patterns: Cons and Snoc. + Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead' + (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on + cons (resp. snoc) of @Sized f n a@ in O(1). +-} + +{-$views #views# + + With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows: + +@ +slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen ('viewCons' -> 'NilCV') = 'SZ' +slen ('viewCons' -> _ ':-' as) = 'SS' (slen as) +slen _ = error "impossible" +@ + + The constraint @('SingI' n, 'Dom f a' f)@ is needed for view function. + In the above, we have extra wildcard pattern (@_@) at the last. + Code compiles if we removed it, but current GHC warns for incomplete pattern, + although we know first two patterns exhausts all the case. + + Equivalently, we can use snoc-style pattern-matching: + +@ +slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen ('viewSnoc' -> 'NilSV') = 'SZ' +slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as) +@ +-} + +-- | View of the left end of sequence (cons-side). +-- +-- Since 0.7.0.0 +data ConsView f n a where + NilCV :: ConsView f (Zero nat) a + (:-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a + +infixr 5 :- + +-- | Case analysis for the cons-side of sequence. +-- +-- Since 0.5.0.0 (type changed) +viewCons :: forall nat f (n :: nat) a . + (HasOrdinal nat, SingI n, CFreeMonoid f,Dom f a) + => Sized f n a + -> ConsView f n a +viewCons sz = case zeroOrSucc $ sing @n of + IsZero -> NilCV + IsSucc n' -> + withSingI n' + $ withSingI (sSucc n') + $ case uncons' n' sz of + Uncons a xs -> (a :- xs) + +-- | View of the left end of sequence (snoc-side). +-- +-- Since 0.7.0.0 +data SnocView f n a where + NilSV :: SnocView f (Zero nat) a + (:-::) :: SingI (n :: nat) => Sized f n a -> a -> SnocView f (n + One nat) a +infixl 5 :-:: + +-- | Case analysis for the snoc-side of sequence. +-- +-- Since 0.5.0.0 (type changed) +viewSnoc :: forall nat f (n :: nat) a. + (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) + => Sized f n a + -> SnocView f n a +viewSnoc sz = case zeroOrSucc (sing @n) of + IsZero -> NilSV + IsSucc (n' :: Sing n') -> + withSingI n' $ + gcastWith (succAndPlusOneR n') $ + case unsnoc' n' sz of + Unsnoc (xs :: Sized f m a) a -> + gcastWith + (unsafeCoerce (Refl @()) :: n' :~: m) + $ xs :-:: a + +{-$patterns #patterns# + + So we can pattern match on both end of sequence via views, but + it is rather clumsy to nest it. For example: + +@ +nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a +nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a +@ + + In such a case, with @PatternSynonyms@ extension we can write as follows: + +@ +nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a +nextToHead (_ ':<' a ':<' _) = a +@ + + Of course, we can also rewrite above @slen@ example using @PatternSynonyms@: + +@ +slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n +slen 'NilL' = 'SZ' +slen (_ ':<' as) = 'SS' (slen as) +slen _ = error "impossible" +@ + + So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to + pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. + @':<'@, @'NilL'@, @':>'@ and @'NilR'@ are neither functions nor data constructors, + but pattern synonyms so we cannot use them in expression contexts. + For more detail on pattern synonyms, see + + and + . +-} + +infixr 5 :< +-- | Pattern synonym for cons-side uncons. +pattern (:<) + :: forall nat (f :: Type -> Type) a (n :: nat). + (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) + => forall (n1 :: nat). (n ~ Succ n1, SingI n1) + => a -> Sized f n1 a -> Sized f n a +pattern a :< as <- (viewCons -> a :- as) where + a :< as = a <| as + +pattern NilL :: forall nat f (n :: nat) a. + (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) + => (n ~ Zero nat) => Sized f n a +pattern NilL <- (viewCons -> NilCV) where + NilL = empty + +infixl 5 :> + +pattern (:>) + :: forall nat (f :: Type -> Type) a (n :: nat). + (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) + => forall (n1 :: nat). (n ~ (n1 + One nat), SingI n1) + => Sized f n1 a -> a -> Sized f n a +pattern a :> b <- (viewSnoc -> a :-:: b) where + a :> b = a |> b + +pattern NilR :: forall nat f (n :: nat) a. + (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) + => n ~ Zero nat => Sized f n a +pattern NilR <- (viewSnoc -> NilSV) where + NilR = empty + +class Dom f a => DomC f a +instance Dom f a => DomC f a + +-- | Applicative instance, generalizing @'Data.Monoid.ZipList'@. +instance + ( Functor f, CFreeMonoid f, CZip f, + HasOrdinal nat, SingI n, forall a. DomC f a) + => P.Applicative (Sized f (n :: nat)) where + {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.Nat)) #-} + + pure (x :: a) = withDict (Dict @(DomC f a)) + $ replicate' x + {-# INLINE pure #-} + + (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) = + withDict (Dict @(DomC f b)) + $ withDict (Dict @(DomC f a)) + $ withDict (Dict @(DomC f (a -> b))) + $ zipWithSame ($) fs xs + {-# INLINE [1] (<*>) #-} +{-# RULES +"<*>/List" [~1] forall fs xs. + Sized fs <*> Sized xs = Sized (getZipList (ZipList fs <*> ZipList xs)) +"<*>/Seq" [~1] forall fs xs. + Sized fs <*> Sized xs = Sized (Seq.zipWith ($) fs xs) +"<*>/Vector" [~1] forall fs xs. + Sized fs <*> Sized xs = Sized (V.zipWith ($) fs xs) + #-} + +instance (CFreeMonoid f, PeanoOrder nat, SingI (n :: nat)) + => CPointed (Sized f n) where + cpure = replicate' + +instance (CFreeMonoid f, CZip f) + => CApplicative (Sized f n) where + pair = zipSame + (<.>) = zipWithSame ($) + (<.) = P.const + (.>) = P.flip P.const + +-- | __N.B.__ Since @calign@ is just zipping for fixed @n@, +-- we require more strong 'CZip' constraint here. +instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where + calignWith = coerce (\f -> czipWith @f @a @b @c ((f .) . These)) + :: forall a b c. + (Dom f a, Dom f b, Dom f c) + => (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c + {-# INLINE [1] calignWith #-} + calign = coerce $ czipWith @f @a @b These + :: forall a b. + (Dom f a, Dom f b, Dom f (These a b)) + => Sized f n a -> Sized f n b -> Sized f n (These a b) + {-# INLINE [1] calign #-} + +instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where + czipWith = coerce $ czipWith @f @a @b @c + :: forall a b c. + (Dom f a, Dom f b, Dom f c) + => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c + {-# INLINE [1] czipWith #-} + czip = coerce $ czip @f @a @b + :: forall a b. + (Dom f a, Dom f b, Dom f (a, b)) + => Sized f n a -> Sized f n b -> Sized f n (a, b) + {-# INLINE [1] czip #-} + +instance + (PeanoOrder nat, SingI (n :: nat), CZip f, CFreeMonoid f) + => CRepeat (Sized f n) where + crepeat = replicate' + {-# INLINE [1] crepeat #-} + +instance CTraversable f => CTraversable (Sized f n) where + ctraverse = \f -> fmap coerce . ctraverse f . runSized + {-# INLINE ctraverse #-} diff --git a/src/Data/Sized/Builtin.hs b/src/Data/Sized/Builtin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Builtin.hs @@ -0,0 +1,432 @@ +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE TypeOperators, NoImplicitPrelude #-} +{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoStarIsType #-} +-- | This module exports @'S.Sized'@ type and +-- functions specialized to +-- GHC's built-in type numeral @'Nat'@. +module Data.Sized.Builtin + ( -- * Main Data-types + Sized(), SomeSized, pattern SomeSized, Ordinal, + DomC(), + -- * Accessors + -- ** Length information + length, sLength, null, + -- ** Indexing + (!!), (%!!), index, sIndex, head, last, + uncons, uncons', Uncons, pattern Uncons, + unsnoc, unsnoc', Unsnoc, pattern Unsnoc, + -- ** Slicing + tail, init, take, takeAtMost, drop, splitAt, splitAtMost, + -- * Construction + -- ** Initialisation + empty, singleton, toSomeSized, replicate, replicate', generate, + -- ** Concatenation + cons, (<|), snoc, (|>), append, (++), concat, + -- ** Zips + zip, zipSame, zipWith, zipWithSame, unzip, unzipWith, + -- * Transformation + map, reverse, intersperse, nub, sort, sortBy, insert, insertBy, + -- * Conversion + -- ** List + toList, fromList, fromList', unsafeFromList, unsafeFromList', + fromListWithDefault, fromListWithDefault', + -- ** Base container + unsized, + toSized, toSized', unsafeToSized, unsafeToSized', + toSizedWithDefault, toSizedWithDefault', + -- * Querying + -- ** Partitioning + Partitioned(), pattern Partitioned, + takeWhile, dropWhile, span, break, partition, + -- ** Searching + elem, notElem, find, findIndex, sFindIndex, + findIndices, sFindIndices, + elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, + -- * Views and Patterns + -- $ViewsAndPatterns + + -- ** Views + -- $views + + -- ** Patterns + -- $patterns + + -- ** Definitions + viewCons, ConsView, + pattern (S.:-), pattern S.NilCV, + viewSnoc, SnocView, + pattern (S.:-::), pattern S.NilSV, + + pattern (:<), pattern NilL , pattern (:>), pattern NilR, + ) where +import qualified Data.Sized as S +import Data.Sized (DomC) + +import Control.Subcategory +import Data.Kind (Type) +import Data.Singletons.Prelude (SingI) +import Data.Singletons.Prelude.Enum (PEnum (..)) +import qualified Data.Type.Ordinal as O +import GHC.TypeNats (KnownNat, Nat) +import Prelude (Maybe, Ordering, Ord, Eq, Monoid, Bool(..), Int) +import Data.Singletons.TypeLits (SNat) +import Data.Singletons.Prelude (POrd((<=))) +import Data.Type.Natural.Class (type (-.), type (<)) +import Data.Type.Natural (Min, type (-), type (+), type (*)) + +type Ordinal = (O.Ordinal :: Nat -> Type) +type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type) + +type SomeSized f a = S.SomeSized' f Nat a + +pattern SomeSized + :: forall (f :: Type -> Type) a. () + => forall (n :: Nat). SNat n + -> Sized f n a -> SomeSized f a +{-# COMPLETE SomeSized #-} +pattern SomeSized n s = S.SomeSized' n s + +length :: (Dom f a, CFoldable f, KnownNat n) => Sized f n a -> Int +length = S.length @Nat + +sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n +sLength = S.sLength @Nat + +null :: (Dom f a, CFoldable f) => Sized f n a -> Bool +null = S.null @Nat + +(!!) :: (Dom f a, CFoldable f, (1 <= m) ~ 'True) => Sized f m a -> Int -> a +(!!) = (S.!!) @Nat + +(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c +(%!!) = (S.%!!) @Nat + +index + :: (Dom f a, CFoldable f, (1 <= m) ~ 'True) + => Int -> Sized f m a -> a +index = S.index @Nat + +sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c +sIndex = S.sIndex @Nat + +head :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a +head = S.head @Nat + +last :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a +last = S.last @Nat + +uncons + :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) + => Sized f n a -> Uncons f n a +uncons = S.uncons @Nat + +uncons' + :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) + => Sized f n a + -> Uncons f n a +uncons' = S.uncons @Nat + +unsnoc + :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) + => Sized f n a -> Unsnoc f n a +unsnoc = S.unsnoc @Nat + +unsnoc' :: (Dom f a, KnownNat n, CFreeMonoid f) => proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) a +unsnoc' = S.unsnoc' @Nat + +type Uncons f (n :: Nat) a = S.Uncons f n a +pattern Uncons + :: forall (f :: Type -> Type) (n :: Nat) a. () + => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) + => a -> Sized f n1 a -> Uncons f n a +pattern Uncons a as = S.Uncons a as + +type Unsnoc f (n :: Nat) a = S.Unsnoc f n a + +pattern Unsnoc + :: forall (f :: Type -> Type) (n :: Nat) a. () + => forall (n1 :: Nat). (n ~ Succ n1) + => Sized f n1 a -> a -> Unsnoc f n a +pattern Unsnoc xs x = S.Unsnoc xs x + +tail :: (Dom f a, CFreeMonoid f) => Sized f (1 + n) a -> Sized f n a +tail = S.tail @Nat + +init :: (Dom f a, CFreeMonoid f) => Sized f (n + 1) a -> Sized f n a +init = S.init @Nat + +take + :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) + => SNat n -> Sized f m a -> Sized f n a +take = S.take @Nat + +takeAtMost + :: (Dom f a, CFreeMonoid f) + => SNat n -> Sized f m a -> Sized f (Min n m) a +takeAtMost = S.takeAtMost @Nat + +drop + :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) + => SNat n -> Sized f m a -> Sized f (m - n) a +drop = S.drop @Nat + +splitAt + :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) + => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a) +splitAt = S.splitAt @Nat + +splitAtMost + :: (Dom f a, CFreeMonoid f) + => SNat n -> Sized f m a + -> (Sized f (Min n m) a, Sized f (m -. n) a) +splitAtMost = S.splitAtMost @Nat + +empty :: (Dom f a, Monoid (f a)) => Sized f 0 a +empty = S.empty @Nat + +singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f 1 a +singleton = S.singleton @Nat + +toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a +toSomeSized = S.toSomeSized @Nat + +replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a +replicate = S.replicate @Nat + +replicate' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> Sized f n a +replicate' = S.replicate' @Nat + +generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a +generate = S.generate @Nat + +cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a +cons = S.cons @Nat + +snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a +snoc = S.snoc @Nat + +(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a +(<|) = (S.<|) @Nat + +(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a +(|>) = (S.|>) @Nat + +(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a +(++) = (S.++) @Nat + +append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a +append = S.append @Nat + +concat + :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a), + CFreeMonoid f, CFunctor f', CFoldable f' + ) => Sized f' m (Sized f n a) -> Sized f (m * n) a +concat = S.concat @Nat + +zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f) + => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) +zip = S.zip @Nat + +zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f) + => Sized f n a -> Sized f n b -> Sized f n (a, b) +zipSame = S.zipSame @Nat + +zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) + => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c +zipWith = S.zipWith @Nat + +zipWithSame + :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) + => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c +zipWithSame = S.zipWithSame @Nat + +unzip + :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f) + => Sized f n (a, b) -> (Sized f n a, Sized f n b) +unzip = S.unzip @Nat + +unzipWith + :: (Dom f a, Dom f b, Dom f c, CUnzip f) + => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c) +unzipWith = S.unzipWith @Nat + +map + :: (Dom f a, Dom f b, CFreeMonoid f) + => (a -> b) -> Sized f n a -> Sized f n b +map = S.map @Nat + +reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a +reverse = S.reverse @Nat + +intersperse + :: (Dom f a, CFreeMonoid f) + => a -> Sized f n a -> Sized f ((2 * n) -. 1) a +intersperse = S.intersperse @Nat + +nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a +nub = S.nub @Nat + +sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a +sort = S.sort @Nat + +sortBy + :: (Dom f a, CFreeMonoid f) + => (a -> a -> Ordering) + -> Sized f n a -> Sized f n a +sortBy = S.sortBy @Nat + +insert + :: (Dom f a, CFreeMonoid f, Ord a) + => a -> Sized f n a -> Sized f (n + 1) a +insert = S.insert @Nat + +insertBy + :: (Dom f a, CFreeMonoid f) + => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (n + 1) a +insertBy = S.insertBy @Nat + +toList :: (Dom f a, CFoldable f) => Sized f n a -> [a] +toList = S.toList @Nat + +fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a) +fromList = S.fromList @Nat + +fromList' :: (Dom f a, CFreeMonoid f, KnownNat n) => [a] -> Maybe (Sized f n a) +fromList' = S.fromList' @Nat + +unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a +unsafeFromList = S.unsafeFromList @Nat + +unsafeFromList' :: (Dom f a, KnownNat n, CFreeMonoid f) => [a] -> Sized f n a +unsafeFromList' = S.unsafeFromList' @Nat + +fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a +fromListWithDefault = S.fromListWithDefault @Nat + +fromListWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f) + => a -> [a] -> Sized f n a +fromListWithDefault' = S.fromListWithDefault' @Nat + +unsized :: Sized f n a -> f a +unsized = S.unsized @Nat + +toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a) +toSized = S.toSized @Nat + +toSized' :: (Dom f a, CFreeMonoid f, KnownNat n) => f a -> Maybe (Sized f n a) +toSized' = S.toSized' @Nat + +unsafeToSized :: SNat n -> f a -> Sized f n a +unsafeToSized = S.unsafeToSized @Nat + +unsafeToSized' :: (Dom f a, KnownNat n) => f a -> Sized f n a +unsafeToSized' = S.unsafeToSized' @Nat + +toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a +toSizedWithDefault = S.toSizedWithDefault @Nat + +toSizedWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f) + => a -> f a -> Sized f n a +toSizedWithDefault' = S.toSizedWithDefault' @Nat + +type Partitioned f (n :: Nat) a = S.Partitioned f n a + +pattern Partitioned + :: forall (f :: Type -> Type) (n :: Nat) a. () + => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a) + => SNat n1 -> Sized f n1 a -> SNat m + -> Sized f m a -> Partitioned f n a +{-# COMPLETE Partitioned #-} +pattern Partitioned ls l rs r = S.Partitioned ls l rs r + +takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a +takeWhile = S.takeWhile @Nat + +dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a +dropWhile = S.dropWhile @Nat + +span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +span = S.span @Nat + +break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +break = S.break @Nat + +partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +partition = S.partition @Nat + +elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool +elem = S.elem @Nat + +notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool +notElem = S.notElem @Nat + +find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a +find = S.find @Nat + +findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int +findIndex = S.findIndex @Nat + +sFindIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) +sFindIndex = S.sFindIndex @Nat + +findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] +findIndices = S.findIndices @Nat + +sFindIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n] +sFindIndices = S.sFindIndices @Nat + +elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int +elemIndex = S.findIndex @Nat + +sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) +{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-} +sUnsafeElemIndex = S.sElemIndex @Nat + +sElemIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) +sElemIndex = S.sFindIndex @Nat + +elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] +elemIndices = S.findIndices @Nat + +sElemIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n] +sElemIndices = S.sFindIndices @Nat + +type ConsView f (n :: Nat) a = S.ConsView f n a + +viewCons :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a +viewCons = S.viewCons @Nat + +type SnocView f (n :: Nat) a = S.SnocView f n a + +viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a +viewSnoc = S.viewCons @Nat + +pattern (:<) + :: forall (f :: Type -> Type) a (n :: Nat). + (Dom f a, SingI n, CFreeMonoid f) + => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) + => a -> Sized f n1 a -> Sized f n a +pattern a :< b = a S.:< b +infixr 5 :< + +pattern NilL :: forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) + => n ~ 0 => Sized f n a +pattern NilL = S.NilL + +pattern (:>) + :: forall (f :: Type -> Type) a (n :: Nat). + (Dom f a, SingI n, CFreeMonoid f) + => forall (n1 :: Nat). (n ~ (n1 + 1), SingI n1) + => Sized f n1 a -> a -> Sized f n a +pattern a :> b = a S.:> b +infixl 5 :> + +pattern NilR :: forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a, SingI n) + => n ~ 0 => Sized f n a +pattern NilR = S.NilR diff --git a/src/Data/Sized/Flipped.hs b/src/Data/Sized/Flipped.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Flipped.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE CPP, ConstraintKinds, DataKinds, DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor, DeriveTraversable, EmptyDataDecls #-} +{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} +{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms #-} +{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-} +{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-} +#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 +{-# LANGUAGE NoStarIsType #-} +#endif +module Data.Sized.Flipped (Flipped(..)) where +import Data.Sized.Internal + +import Control.DeepSeq (NFData (..)) +import Control.Lens.At (Index, IxValue, Ixed (..)) +import Control.Lens.TH (makeWrapped) +import Control.Lens.Wrapped (_Wrapped) +import Data.Hashable (Hashable (..)) +import Data.MonoTraversable (Element, MonoFoldable (..)) +import Data.MonoTraversable (MonoFunctor (..)) +import Data.MonoTraversable (MonoTraversable (..)) +import qualified Data.Sequence as Seq +import qualified Data.Type.Natural as PN +import Data.Type.Ordinal (HasOrdinal, Ordinal (..)) +import Data.Typeable (Typeable) +import qualified Data.Vector as V +import qualified Data.Vector.Storable as SV +import qualified Data.Vector.Unboxed as UV +import qualified GHC.TypeLits as TL + +-- | Wrapper for @'Sized'@ which takes length as its last element, instead of the second. +-- +-- Since 0.2.0.0 +newtype Flipped f a n = Flipped { runFlipped :: Sized f n a } + deriving (Show, Eq, Ord, Typeable, NFData, Hashable) + +makeWrapped ''Flipped + +type instance Index (Flipped f a n) = Ordinal n +type instance IxValue (Flipped f a n) = IxValue (f a) +type instance Element (Flipped f a n) = Element (Sized f n a) +deriving instance MonoFunctor (f a) => MonoFunctor (Flipped f a n) +deriving instance MonoFoldable (f a) => MonoFoldable (Flipped f a n) +instance (MonoTraversable (f a)) => MonoTraversable (Flipped f a n) where + otraverse = _Wrapped . otraverse + {-# INLINE otraverse #-} + + omapM = _Wrapped . omapM + {-# INLINE omapM #-} + +instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat) + => Ixed (Flipped f a (n :: nat)) where + {-# SPECIALISE instance Ixed (Flipped [] a (n :: TL.Nat)) #-} + {-# SPECIALISE instance Ixed (Flipped [] a (n :: PN.Nat)) #-} + {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-} + {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-} + {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-} + {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-} + {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-} + {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-} + {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-} + {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-} + ix o = _Wrapped . ix o + {-# INLINE ix #-} diff --git a/src/Data/Sized/Internal.hs b/src/Data/Sized/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Internal.hs @@ -0,0 +1,170 @@ +{-# LANGUAGE CPP, ConstraintKinds, DataKinds, DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor, DeriveTraversable, DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} +{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-} +{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-} +#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 +{-# LANGUAGE NoStarIsType #-} +#endif +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Data.Sized.Internal (Sized(..)) where +import Control.DeepSeq (NFData (..)) +import Control.Lens.At (Index, IxValue, Ixed (..)) +import Control.Lens.Indexed (FoldableWithIndex (..), + FunctorWithIndex (..), + TraversableWithIndex (..)) +import Control.Subcategory (CFoldable, CFunctor, Constrained) +import Data.Hashable (Hashable (..)) +import Data.Kind (Type) +import Data.MonoTraversable (Element, MonoFoldable (..), + MonoFunctor (..), + MonoTraversable (..)) +import qualified Data.Sequence as Seq +import Data.Singletons.Prelude (SingI) +import qualified Data.Type.Natural as PN +import Data.Type.Ordinal (HasOrdinal, Ordinal (..), + ordToNatural, unsafeNaturalToOrd) +import Data.Typeable (Typeable) +import qualified Data.Vector as V +import qualified Data.Vector.Storable as SV +import qualified Data.Vector.Unboxed as UV +import qualified GHC.TypeLits as TL + +-- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version. +-- +-- Here, 'f' must be the instance of 'CFreeMonoid' (f a) a@ for all @a@. +-- +-- Since 0.2.0.0 +newtype Sized (f :: Type -> Type) (n :: nat) a = + Sized { runSized :: f a + } deriving (Eq, Ord, Typeable, + Functor, Foldable, Traversable) + deriving newtype + (Constrained, CFoldable, CFunctor) + +type instance Element (Sized f n a) = Element (f a) + +-- | Since 0.2.0.0 +deriving instance MonoFoldable (f a) + => MonoFoldable (Sized f n a) + +-- | Since 0.2.0.0 +deriving instance MonoFunctor (f a) + => MonoFunctor (Sized f n a) + +-- | Since 0.2.0.0 +instance {-# OVERLAPPABLE #-} (MonoTraversable (f a)) + => MonoTraversable (Sized f n a) where + {-# SPECIALISE instance MonoTraversable (Sized [] n a) #-} + {-# SPECIALISE instance MonoTraversable (Sized V.Vector n a) #-} + {-# SPECIALISE instance MonoTraversable (Sized Seq.Seq n a) #-} + {-# SPECIALISE instance UV.Unbox a => MonoTraversable (Sized UV.Vector n a) #-} + {-# SPECIALISE instance SV.Storable a => MonoTraversable (Sized SV.Vector n a) #-} + otraverse f = fmap Sized . otraverse f . runSized + omapM f = fmap Sized . omapM f. runSized + +-- | Since 0.6.0.0 +instance {-# OVERLAPPING #-} SV.Storable a => MonoTraversable (Sized SV.Vector n a) where + otraverse f = fmap Sized . otraverse f . runSized + omapM f = fmap Sized . omapM f . runSized + +-- | Since 0.6.0.0 +instance {-# OVERLAPPING #-} UV.Unbox a => MonoTraversable (Sized UV.Vector n a) where + otraverse f = fmap Sized . otraverse f . runSized + omapM f = fmap Sized . omapM f . runSized + +deriving instance NFData (f a) => NFData (Sized f n a) +deriving instance Hashable (f a) => Hashable (Sized f n a) + +instance Show (f a) => Show (Sized f n a) where + showsPrec d (Sized x) = showsPrec d x + +-- | Since 0.2.0.0 +type instance Index (Sized f n a) = Ordinal n + +-- | Since 0.3.0.0 +type instance IxValue (Sized f n a) = IxValue (f a) +instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat) + => Ixed (Sized f (n :: nat) a) where + {-# SPECIALISE instance Ixed (Sized [] (n :: TL.Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized [] (n :: PN.Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized V.Vector (n :: TL.Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized V.Vector (n :: PN.Nat) a) #-} + {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: TL.Nat) a) #-} + {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: PN.Nat) a) #-} + {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: TL.Nat) a) #-} + {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: PN.Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: TL.Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: PN.Nat) a) #-} + {-# INLINE ix #-} + ix n f = fmap Sized . ix (fromIntegral $ ordToNatural n) f . runSized + +-- | Since 0.2.0.0 +instance (Integral i, FunctorWithIndex i f, HasOrdinal nat, SingI n) + => FunctorWithIndex (Ordinal (n :: nat)) (Sized f n) where + imap f = Sized . imap (f . unsafeNaturalToOrd . fromIntegral) . runSized + {-# INLINE imap #-} + {-# SPECIALISE instance TL.KnownNat n + => FunctorWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => FunctorWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n + => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n + => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} + +-- | Since 0.4.0.0 +instance {-# OVERLAPPABLE #-} (Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n) + => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where + ifoldMap f = ifoldMap (f . unsafeNaturalToOrd . fromIntegral) . runSized + {-# INLINE ifoldMap #-} + + ifoldr f e = ifoldr (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldr #-} + + ifoldl f e = ifoldl (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldl #-} + + ifoldr' f e = ifoldr' (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldr' #-} + + ifoldl' f e = ifoldl' (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldl' #-} + + {-# SPECIALISE instance TL.KnownNat n + => FoldableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => FoldableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n + => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n + => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} + +-- | Since 0.2.0.0 +instance (Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n) + => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where + itraverse f = fmap Sized . itraverse (f . unsafeNaturalToOrd . fromIntegral) . runSized + {-# INLINE itraverse #-} + + {-# SPECIALISE instance TL.KnownNat n + => TraversableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => TraversableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n + => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} + {-# SPECIALISE instance TL.KnownNat n + => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} + {-# SPECIALISE instance SingI n + => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} diff --git a/src/Data/Sized/Peano.hs b/src/Data/Sized/Peano.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Peano.hs @@ -0,0 +1,431 @@ +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE TypeOperators, NoImplicitPrelude #-} +{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoStarIsType #-} +-- | This module exports @'S.Sized'@ type specialized to +-- type-level Peano numeral @'PN.Nat'@. +module Data.Sized.Peano + ( -- * Main Data-types + Sized(), SomeSized, pattern SomeSized, Ordinal, + DomC(), + -- * Accessors + -- ** Length information + length, sLength, null, + -- ** Indexing + (!!), (%!!), index, sIndex, head, last, + uncons, uncons', Uncons, pattern Uncons, + unsnoc, unsnoc', Unsnoc, pattern Unsnoc, + -- ** Slicing + tail, init, take, takeAtMost, drop, splitAt, splitAtMost, + -- * Construction + -- ** Initialisation + empty, singleton, toSomeSized, replicate, replicate', generate, + -- ** Concatenation + cons, (<|), snoc, (|>), append, (++), concat, + -- ** Zips + zip, zipSame, zipWith, zipWithSame, unzip, unzipWith, + -- * Transformation + map, reverse, intersperse, nub, sort, sortBy, insert, insertBy, + -- * Conversion + -- ** List + toList, fromList, fromList', unsafeFromList, unsafeFromList', + fromListWithDefault, fromListWithDefault', + -- ** Base container + unsized, + toSized, toSized', unsafeToSized, unsafeToSized', + toSizedWithDefault, toSizedWithDefault', + -- * Querying + -- ** Partitioning + Partitioned(), pattern Partitioned, + takeWhile, dropWhile, span, break, partition, + -- ** Searching + elem, notElem, find, findIndex, sFindIndex, + findIndices, sFindIndices, + elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, + -- * Views and Patterns + -- $ViewsAndPatterns + + -- ** Views + -- $views + + -- ** Patterns + -- $patterns + + -- ** Definitions + viewCons, ConsView, + pattern (S.:-), pattern S.NilCV, + viewSnoc, SnocView, + pattern (S.:-::), pattern S.NilSV, + + pattern (:<), pattern NilL , pattern (:>), pattern NilR, + ) where +import qualified Data.Sized as S +import Data.Sized (DomC) + +import Control.Subcategory +import Data.Kind (Type) +import Data.Singletons.Prelude (SingI) +import Data.Singletons.Prelude.Enum (PEnum (..)) +import qualified Data.Type.Ordinal as O +import Prelude (Maybe, Ordering, Ord, Eq, Monoid, Bool(..), Int) +import Data.Type.Natural (Two, Nat(..), SNat) +import Data.Singletons.Prelude (POrd((<=))) +import Data.Type.Natural.Class (type (-.), type (<)) +import Data.Type.Natural (Min, type (-), type (+), type (*)) +import Data.Type.Natural (One) + +type Ordinal = (O.Ordinal :: Nat -> Type) +type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type) + +type SomeSized f a = S.SomeSized' f Nat a + +pattern SomeSized + :: forall (f :: Type -> Type) a. () + => forall (n :: Nat). SNat n + -> Sized f n a -> SomeSized f a +{-# COMPLETE SomeSized #-} +pattern SomeSized n s = S.SomeSized' n s + +length :: (Dom f a, CFoldable f, SingI n) => Sized f n a -> Int +length = S.length @Nat + +sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n +sLength = S.sLength @Nat + +null :: (Dom f a, CFoldable f) => Sized f n a -> Bool +null = S.null @Nat + +(!!) :: (Dom f a, CFoldable f, (One <= m) ~ 'True) => Sized f m a -> Int -> a +(!!) = (S.!!) @Nat + +(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c +(%!!) = (S.%!!) @Nat + +index + :: (Dom f a, CFoldable f, (One <= m) ~ 'True) + => Int -> Sized f m a -> a +index = S.index @Nat + +sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c +sIndex = S.sIndex @Nat + +head :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a +head = S.head @Nat + +last :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a +last = S.last @Nat + +uncons + :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True) + => Sized f n a -> Uncons f n a +uncons = S.uncons @Nat + +uncons' + :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True) + => Sized f n a + -> Uncons f n a +uncons' = S.uncons @Nat + +unsnoc + :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True) + => Sized f n a -> Unsnoc f n a +unsnoc = S.unsnoc @Nat + +unsnoc' :: (Dom f a, SingI n, CFreeMonoid f) => proxy n -> Sized f ('S n) a -> Unsnoc f ('S n) a +unsnoc' = S.unsnoc' @Nat + +type Uncons f (n :: Nat) a = S.Uncons f n a +pattern Uncons + :: forall (f :: Type -> Type) (n :: Nat) a. () + => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) + => a -> Sized f n1 a -> Uncons f n a +pattern Uncons a as = S.Uncons a as + +type Unsnoc f (n :: Nat) a = S.Unsnoc f n a + +pattern Unsnoc + :: forall (f :: Type -> Type) (n :: Nat) a. () + => forall (n1 :: Nat). (n ~ Succ n1) + => Sized f n1 a -> a -> Unsnoc f n a +pattern Unsnoc xs x = S.Unsnoc xs x + +tail :: (Dom f a, CFreeMonoid f) => Sized f (One + n) a -> Sized f n a +tail = S.tail @Nat + +init :: (Dom f a, CFreeMonoid f) => Sized f (n + One) a -> Sized f n a +init = S.init @Nat + +take + :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) + => SNat n -> Sized f m a -> Sized f n a +take = S.take @Nat + +takeAtMost + :: (Dom f a, CFreeMonoid f) + => SNat n -> Sized f m a -> Sized f (Min n m) a +takeAtMost = S.takeAtMost @Nat + +drop + :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) + => SNat n -> Sized f m a -> Sized f (m - n) a +drop = S.drop @Nat + +splitAt + :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) + => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a) +splitAt = S.splitAt @Nat + +splitAtMost + :: (Dom f a, CFreeMonoid f) + => SNat n -> Sized f m a + -> (Sized f (Min n m) a, Sized f (m -. n) a) +splitAtMost = S.splitAtMost @Nat + +empty :: (Dom f a, Monoid (f a)) => Sized f 'Z a +empty = S.empty @Nat + +singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f One a +singleton = S.singleton @Nat + +toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a +toSomeSized = S.toSomeSized @Nat + +replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a +replicate = S.replicate @Nat + +replicate' :: (Dom f a, CFreeMonoid f, SingI n) => a -> Sized f n a +replicate' = S.replicate' @Nat + +generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a +generate = S.generate @Nat + +cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a +cons = S.cons @Nat + +snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a +snoc = S.snoc @Nat + +(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a +(<|) = (S.<|) @Nat + +(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a +(|>) = (S.|>) @Nat + +(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a +(++) = (S.++) @Nat + +append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a +append = S.append @Nat + +concat + :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a), + CFreeMonoid f, CFunctor f', CFoldable f' + ) => Sized f' m (Sized f n a) -> Sized f (m * n) a +concat = S.concat @Nat + +zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f) + => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) +zip = S.zip @Nat + +zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f) + => Sized f n a -> Sized f n b -> Sized f n (a, b) +zipSame = S.zipSame @Nat + +zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) + => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c +zipWith = S.zipWith @Nat + +zipWithSame + :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f) + => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c +zipWithSame = S.zipWithSame @Nat + +unzip + :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f) + => Sized f n (a, b) -> (Sized f n a, Sized f n b) +unzip = S.unzip @Nat + +unzipWith + :: (Dom f a, Dom f b, Dom f c, CUnzip f) + => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c) +unzipWith = S.unzipWith @Nat + +map + :: (Dom f a, Dom f b, CFreeMonoid f) + => (a -> b) -> Sized f n a -> Sized f n b +map = S.map @Nat + +reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a +reverse = S.reverse @Nat + +intersperse + :: (Dom f a, CFreeMonoid f) + => a -> Sized f n a -> Sized f ((Two * n) -. One) a +intersperse = S.intersperse @Nat + +nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a +nub = S.nub @Nat + +sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a +sort = S.sort @Nat + +sortBy + :: (Dom f a, CFreeMonoid f) + => (a -> a -> Ordering) + -> Sized f n a -> Sized f n a +sortBy = S.sortBy @Nat + +insert + :: (Dom f a, CFreeMonoid f, Ord a) + => a -> Sized f n a -> Sized f ('S n) a +insert = S.insert @Nat + +insertBy + :: (Dom f a, CFreeMonoid f) + => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f ('S n) a +insertBy = S.insertBy @Nat + +toList :: (Dom f a, CFoldable f) => Sized f n a -> [a] +toList = S.toList @Nat + +fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a) +fromList = S.fromList @Nat + +fromList' :: (Dom f a, CFreeMonoid f, SingI n) => [a] -> Maybe (Sized f n a) +fromList' = S.fromList' @Nat + +unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a +unsafeFromList = S.unsafeFromList @Nat + +unsafeFromList' :: (Dom f a, SingI n, CFreeMonoid f) => [a] -> Sized f n a +unsafeFromList' = S.unsafeFromList' @Nat + +fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a +fromListWithDefault = S.fromListWithDefault @Nat + +fromListWithDefault' :: (Dom f a, SingI n, CFreeMonoid f) + => a -> [a] -> Sized f n a +fromListWithDefault' = S.fromListWithDefault' @Nat + +unsized :: Sized f n a -> f a +unsized = S.unsized @Nat + +toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a) +toSized = S.toSized @Nat + +toSized' :: (Dom f a, CFreeMonoid f, SingI n) => f a -> Maybe (Sized f n a) +toSized' = S.toSized' @Nat + +unsafeToSized :: SNat n -> f a -> Sized f n a +unsafeToSized = S.unsafeToSized @Nat + +unsafeToSized' :: (Dom f a, SingI n) => f a -> Sized f n a +unsafeToSized' = S.unsafeToSized' @Nat + +toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a +toSizedWithDefault = S.toSizedWithDefault @Nat + +toSizedWithDefault' :: (Dom f a, SingI n, CFreeMonoid f) + => a -> f a -> Sized f n a +toSizedWithDefault' = S.toSizedWithDefault' @Nat + +type Partitioned f (n :: Nat) a = S.Partitioned f n a + +pattern Partitioned + :: forall (f :: Type -> Type) (n :: Nat) a. () + => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a) + => SNat n1 -> Sized f n1 a -> SNat m + -> Sized f m a -> Partitioned f n a +{-# COMPLETE Partitioned #-} +pattern Partitioned ls l rs r = S.Partitioned ls l rs r + +takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a +takeWhile = S.takeWhile @Nat + +dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a +dropWhile = S.dropWhile @Nat + +span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +span = S.span @Nat + +break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +break = S.break @Nat + +partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a +partition = S.partition @Nat + +elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool +elem = S.elem @Nat + +notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool +notElem = S.notElem @Nat + +find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a +find = S.find @Nat + +findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int +findIndex = S.findIndex @Nat + +sFindIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) +sFindIndex = S.sFindIndex @Nat + +findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] +findIndices = S.findIndices @Nat + +sFindIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n] +sFindIndices = S.sFindIndices @Nat + +elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int +elemIndex = S.findIndex @Nat + +sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n) +{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-} +sUnsafeElemIndex = S.sElemIndex @Nat + +sElemIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) +sElemIndex = S.sFindIndex @Nat + +elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int] +elemIndices = S.findIndices @Nat + +sElemIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n] +sElemIndices = S.sFindIndices @Nat + +type ConsView f (n :: Nat) a = S.ConsView f n a + +viewCons :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a +viewCons = S.viewCons @Nat + +type SnocView f (n :: Nat) a = S.SnocView f n a + +viewSnoc :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a +viewSnoc = S.viewCons @Nat + +pattern (:<) + :: forall (f :: Type -> Type) a (n :: Nat). + (Dom f a, SingI n, CFreeMonoid f) + => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) + => a -> Sized f n1 a -> Sized f n a +pattern a :< b = a S.:< b +infixr 5 :< + +pattern NilL :: forall f (n :: Nat) a. + (SingI n, CFreeMonoid f, Dom f a) + => n ~ 'Z => Sized f n a +pattern NilL = S.NilL + +pattern (:>) + :: forall (f :: Type -> Type) a (n :: Nat). + (Dom f a, SingI n, CFreeMonoid f) + => forall (n1 :: Nat). (n ~ (n1 + One), SingI n1) + => Sized f n1 a -> a -> Sized f n a +pattern a :> b = a S.:> b +infixl 5 :> + +pattern NilR :: forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a, SingI n) + => n ~ 'Z => Sized f n a +pattern NilR = S.NilR diff --git a/test/Shared.hs b/test/Shared.hs new file mode 100644 --- /dev/null +++ b/test/Shared.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds, TemplateHaskell #-} +{-# OPTIONS_GHC -O2 -fno-hpc #-} +{-# OPTIONS_GHC -dsuppress-idinfo -dsuppress-coercions + -dsuppress-type-applications + -dsuppress-module-prefixes -dsuppress-type-signatures + -dsuppress-uniques #-} +module Shared where +import Language.Haskell.TH +import Test.Hspec +import Test.Inspection + + +checkInspection + :: Result -> Expectation +checkInspection Success{} = pure () +checkInspection (Failure msg) = + fail msg + +inspecting :: String -> Obligation -> Q Exp +inspecting desc reg = + [|it desc $ checkInspection $(inspectTest reg)|] diff --git a/test/opt-test.hs b/test/opt-test.hs new file mode 100644 --- /dev/null +++ b/test/opt-test.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE DataKinds, RankNTypes, TemplateHaskell #-} +{-# OPTIONS_GHC -O2 -fno-hpc #-} +{-# OPTIONS_GHC -dsuppress-idinfo -dsuppress-coercions + -dsuppress-type-applications + -dsuppress-module-prefixes -dsuppress-type-signatures + -dsuppress-uniques #-} +module Main where +import Control.Subcategory +import qualified Data.Sequence as Seq +import Data.Singletons.Prelude +import Data.Sized.Builtin (Sized, zipWithSame) +import qualified Data.Sized.Builtin as SV +import qualified Data.Vector as V +import qualified Data.Vector.Generic as G +import Data.Vector.Storable (Storable) +import qualified Data.Vector.Storable as S +import Data.Vector.Unboxed (Unbox) +import qualified Data.Vector.Unboxed as U +import Shared +import Test.Hspec +import Test.Inspection + +type LSized = Sized [] +type VSized = Sized V.Vector +type USized = Sized U.Vector +type SSized = Sized S.Vector +type SeqSized = Sized Seq.Seq + +zipWith_subcat_List + :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int] +zipWith_subcat_List = czipWith + +zipWith_List + :: (Int -> Int -> Int) -> LSized n Int -> LSized m Int -> LSized (Min n m) Int +zipWith_List = SV.zipWith + +zipWithSame_List + :: (Int -> Int -> Int) -> LSized n Int -> LSized n Int -> LSized n Int +zipWithSame_List = zipWithSame + +zipWith_List_Prel :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int] +zipWith_List_Prel = zipWith + +zipWithSame_Boxed :: (a -> b -> c) -> VSized n a -> VSized n b -> VSized n c +zipWithSame_Boxed = zipWithSame + +zipWithSame_Boxed_mono + :: (Int -> (Integer -> Bool) -> [Int]) + -> VSized n Int -> VSized n (Integer -> Bool) -> VSized n [Int] +zipWithSame_Boxed_mono = zipWithSame + +zipWithSame_Unboxed + :: (Unbox a, Unbox b, Unbox c) + => (a -> b -> c) -> USized n a -> USized n b -> USized n c +zipWithSame_Unboxed = zipWithSame + +zipWithSame_Unboxed_monomorphic + :: (Int -> Char -> Bool) -> USized n Int -> USized n Char -> USized n Bool +zipWithSame_Unboxed_monomorphic = zipWithSame + +zipWith_Unboxed + :: (Unbox a, Unbox b, Unbox c) + => (a -> b -> c) -> U.Vector a -> U.Vector b -> U.Vector c +zipWith_Unboxed = U.zipWith + +zipWith_Unboxed_monomorphic + :: (Int -> Char -> Bool) -> U.Vector Int -> U.Vector Char -> U.Vector Bool +zipWith_Unboxed_monomorphic = U.zipWith + +zipWithSame_Storable + :: (Storable a, Storable b, Storable c) + => (a -> b -> c) -> SSized n a -> SSized n b -> SSized n c +zipWithSame_Storable = zipWithSame + +zipWithSame_Seq + :: (a -> b -> c) -> SeqSized n a -> SeqSized n b -> SeqSized n c +zipWithSame_Seq = zipWithSame + +zipWith_Boxed :: (a -> b -> c) -> V.Vector a -> V.Vector b -> V.Vector c +zipWith_Boxed = V.zipWith + +main :: IO () +main = hspec $ do + describe "czipWith" $ do + $(inspecting "doesn't contain type classes" + $ hasNoTypeClasses 'zipWith_subcat_List + ) + describe "zipWith" $ do + $(inspecting "doesn't contain type classes" + $ hasNoTypeClasses 'zipWith_List + ) + describe "zipWithSame" $ do + describe "list" $ do + it "doesn't contain type classes" $ + checkInspection + $(inspectTest + $ hasNoTypeClasses 'zipWithSame_List + ) + it "is almost the same as the original zipWith (list)" $ + checkInspection + $(inspectTest $ + 'zipWithSame_List ==- 'zipWith_List_Prel + ) + describe "Boxed Vector" $ do + it "doesn't contain type classes, except for G.Vector" $ + checkInspection + $(inspectTest + $ 'zipWithSame_Boxed `hasNoTypeClassesExcept` + [''G.Vector] + ) + it "doesn't contain type classes, if fully instantiated" $ + checkInspection + $(inspectTest + $ hasNoTypeClasses 'zipWithSame_Boxed_mono + ) + it "is almost the same as the original zipWith (Boxed)" $ + checkInspection + $(inspectTest $ + 'zipWithSame_Boxed ==- 'zipWith_Boxed + ) + describe "Unboxed Vector" $ do + it "doesn't contain type classes except for Unbox" $ + checkInspection + $(inspectTest + $ 'zipWithSame_Unboxed `hasNoTypeClassesExcept` + [''Unbox] + ) + it "doesn't contain type classes if fully instnatiated" $ + checkInspection + $(inspectTest + $ hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic + ) + it "is almost the same as the original zipWith, if fully instantiated" $ + checkInspection + $(inspectTest $ + 'zipWithSame_Unboxed_monomorphic + ==- 'zipWith_Unboxed_monomorphic + )