sized 0.6.0.0 → 0.7.0.0
raw patch · 13 files changed
+2717/−1800 lines, 13 filesdep +ghc-typelits-knownnatdep +hspecdep +inspection-testingdep −ListLikedep ~basedep ~constraintsdep ~containers
Dependencies added: ghc-typelits-knownnat, hspec, inspection-testing, sized, subcategories, template-haskell, th-lift, these
Dependencies removed: ListLike
Dependency ranges changed: base, constraints, containers, mono-traversable, singletons, vector
Files
- Data/Sized.hs +0/−1309
- Data/Sized/Builtin.hs +0/−48
- Data/Sized/Flipped.hs +0/−96
- Data/Sized/Internal.hs +0/−261
- Data/Sized/Peano.hs +0/−45
- sized.cabal +63/−41
- src/Data/Sized.hs +1397/−0
- src/Data/Sized/Builtin.hs +432/−0
- src/Data/Sized/Flipped.hs +65/−0
- src/Data/Sized/Internal.hs +170/−0
- src/Data/Sized/Peano.hs +431/−0
- test/Shared.hs +21/−0
- test/opt-test.hs +138/−0
− Data/Sized.hs
@@ -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- <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>- and- <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.--}--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)- #-}
− Data/Sized/Builtin.hs
@@ -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
− Data/Sized/Flipped.hs
@@ -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
− Data/Sized/Internal.hs
@@ -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
− Data/Sized/Peano.hs
@@ -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
sized.cabal view
@@ -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
+ src/Data/Sized.hs view
@@ -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+ <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>+ and+ <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.+-}++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 #-}
+ src/Data/Sized/Builtin.hs view
@@ -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
+ src/Data/Sized/Flipped.hs view
@@ -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 #-}
+ src/Data/Sized/Internal.hs view
@@ -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)) #-}
+ src/Data/Sized/Peano.hs view
@@ -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
@@ -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)|]
+ test/opt-test.hs view
@@ -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+ )