sized 0.3.0.1 → 1.1.0.2
raw patch · 14 files changed
Files
- Changelog.md +51/−0
- Data/Sized.hs +0/−1304
- Data/Sized/Builtin.hs +0/−45
- Data/Sized/Flipped.hs +0/−93
- Data/Sized/Internal.hs +0/−257
- Data/Sized/Peano.hs +0/−45
- README.md +7/−0
- sized.cabal +73/−40
- src/Data/Sized.hs +1834/−0
- src/Data/Sized/Builtin.hs +4/−0
- src/Data/Sized/Flipped.hs +81/−0
- src/Data/Sized/Internal.hs +141/−0
- test/Shared.hs +35/−0
- test/opt-test.hs +182/−0
+ Changelog.md view
@@ -0,0 +1,51 @@+# Changelog++## 1.1.0.2++* Supports GHC 9.10++## 1.1.0.1++* Supports GHC 9.8+* Drops Support for GHC <9++## 1.1.0.0++* Supports GHC 9.6+* Migrates to recent toolchains++## 1.0.0.1++* Minor refactoring of test-suite to support inspection-testiong 0.5++## 1.0.0.0++* Drops Peano-numerals+* Obsolete kind-generic classes+* Now all types are kinded with GHC's builtin type-level naturals, and no type parameters for naturals.+* Drops dependency for `singletons` package and their relatives.++## 0.9.0.0++* This is transitional change: preparation for future rework of `type-natural`+ - Types and constraints in `Data.Sized.Builtin` is now incompatible with `Data.Sized` and `Data.Sized.Peano`+ - The latter two modules will be removed in future release.+* Removes `NilL` and `NilR`+* Compolete overhaul on `Data.Sized.Builtin`+ - Stop using orders from `Data.Singletons`+ - Types of nested pattern synonyms can now be inferred correctly++## 0.8.0.0++* Makes `sLength` using `KnownNat` instance to get O(1) always.+* Introduces `Nil` pattern and deprecates `NilL` and `NilR`.+* Previously, in sepcialised modules for `Builtin` and `Peano`,+ `elemIndex`, `elemIndices` and their Ordinal version were misimplemented;+ they are now correctly uses their counterparts in `Data.Sized`.+* Adds documentation for specialised modules.++## 0.7.0.0++* Stop using `ListLike` package and switched to [`subcategories`] package for the abstraction of sequential types.+* Complete overhaul on type signatures.+* Both `Data.Sized.Builtin` and `Data.Sized.Peano` exports specialised functions instead of reexporting functions from `Data.Sized`.
− Data/Sized.hs
@@ -1,1304 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes, 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 #-}-{-# 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.2.0.0-sLength :: forall f (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.1.0.0-empty :: forall f 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 (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.1.0.0-fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a)- => Sing (n :: nat) -> [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.1.0.0-fromListWithDefault :: forall f (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.1.0.0-sElemIndex :: forall (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 #-}--sUnsafeElemIndex :: forall (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.1.0.0-viewCons :: forall f a (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.1.0.0-viewSnoc :: forall f (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,45 +0,0 @@-{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}-{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-}-{-# LANGUAGE ViewPatterns #-}--- | 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,93 +0,0 @@-{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-}-{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-}-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,257 +0,0 @@-{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, KindSignatures #-}-{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-}-{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}-{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-}-{-# 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.2.0.0-instance {-# OVERLAPS #-} 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.2.0.0-instance {-# OVERLAPS #-} 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
+ README.md view
@@ -0,0 +1,7 @@+sized - Sized sequence data-types+=================================+ [](https://hackage.haskell.org/package/sized)++A wrapper to make length-parametrized data-type from endofunctors from [subcategories].++[subcategories]: http://hackage.haskell.org/package/subcategories
sized.cabal view
@@ -1,45 +1,78 @@--- Initial sized-sequences.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/+cabal-version: 3.0+name: sized+version: 1.1.0.2+license: BSD-3-Clause+license-file: LICENSE+maintainer: konn.jinro_at_gmail.com+author: Hiromi ISHII+copyright: (c) Hiromi ISHII+tested-with: ghc ==9.0.2 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 || ==9.10.1+extra-doc-files:+ Changelog.md+ README.md -name: sized-version: 0.3.0.1-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.2+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.Flipped++ hs-source-dirs: src+ other-modules: Data.Sized.Internal+ default-language: Haskell2010+ ghc-options:+ -Wall+ -Wno-redundant-constraints++ build-depends:+ base >=4 && <5,+ constraints,+ containers >=0.5,+ deepseq >=1.4,+ equational-reasoning >=0.5,+ ghc-typelits-knownnat,+ ghc-typelits-presburger >=0.7.2,+ hashable >=1.2,+ lens >=0.14,+ mono-traversable >=0.10,+ subcategories >=0.2,+ these,+ type-natural >=1.3,+ vector >=0.12,++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:+ -Wall+ -Wno-redundant-constraints+ -fno-hpc++ build-depends:+ base,+ containers,+ inspection-testing >=0.4 && <0.6,+ mono-traversable,+ primitive,+ sized,+ subcategories,+ tasty,+ tasty-inspection-testing,+ template-haskell,+ th-lift,+ type-natural,+ vector,
+ src/Data/Sized.hs view
@@ -0,0 +1,1834 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LiberalTypeSynonyms #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE NoStarIsType #-}+{-# OPTIONS_GHC -fenable-rewrite-rules #-}+{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}+{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}++{- | 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,+ 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 Nil,+ pattern (:<),+ pattern (:>),+ )+where++import Control.Applicative (ZipList (..), (<*>))+import Control.Subcategory+ ( CApplicative (..),+ CFoldable (..),+ CFreeMonoid (..),+ CFunctor (..),+ CPointed (..),+ CRepeat (..),+ CSemialign (..),+ CTraversable (..),+ CUnzip (..),+ CZip (..),+ Constrained (Dom),+ cfromList,+ ctoList,+ )+import Data.Coerce (coerce)+import Data.Constraint (Dict (..), withDict)+import qualified Data.Foldable as F+import Data.Kind (Type)+import qualified Data.List as L+import Data.Maybe (fromJust)+import Data.Monoid (Monoid (..), (<>))+import qualified Data.Sequence as Seq+import Data.Sized.Internal+import Data.These (These (..))+import Data.Type.Equality (gcastWith, (:~:) (..))+import Data.Type.Natural+import Data.Type.Ordinal (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 Unsafe.Coerce (unsafeCoerce)+import Prelude+ ( Bool (..),+ Enum (..),+ Eq (..),+ Functor,+ Int,+ Maybe (..),+ Num (..),+ Ord (..),+ Ordering,+ Show (..),+ const,+ flip,+ fmap,+ fromIntegral,+ uncurry,+ ($),+ (.),+ )+import qualified Prelude as P++--------------------------------------------------------------------------------+-- 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 a where+ SomeSized ::+ SNat n ->+ Sized f n a ->+ SomeSized f a++deriving instance Typeable SomeSized++instance Show (f a) => Show (SomeSized f a) where+ showsPrec d (SomeSized _ s) =+ P.showParen (d > 9) $+ P.showString "SomeSized _ " . showsPrec 10 s++instance Eq (f a) => Eq (SomeSized f 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.8.0.0 (type changed)+-}+length ::+ forall f (n :: Nat) a.+ (Dom f a, KnownNat n) =>+ Sized f n a ->+ Int+length = const $ fromIntegral $ fromSNat $ sNat @n+{-# INLINE CONLIKE [1] length #-}++lengthTLZero :: Sized f 0 a -> Int+lengthTLZero = P.const 0+{-# INLINE lengthTLZero #-}++{-# RULES+"length/0" [~1] length = lengthTLZero+ #-}++{- | @SNat@ version of 'length'.++ Since 0.8.0.0 (type changed)+-}+sLength ::+ forall f (n :: Nat) a.+ (Dom f a, KnownNat n) =>+ Sized f n a ->+ SNat n+sLength _ = sNat @n+{-# INLINE [2] sLength #-}++{- | Test if the sequence is empty or not.++ Since 0.7.0.0+-}+null ::+ forall 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 #-}++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" [~2] null = nullTLSucc+"null/0" [~1] forall (vec :: 1 <= n => Sized f n a).+ null vec =+ False+"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 f (m :: Nat) a.+ (CFoldable f, Dom f a, (1 <= m)) =>+ Sized f m a ->+ Int ->+ a+(!!) = coerce $ cindex @f @a+{-# INLINE (!!) #-}++{- | Safe indexing with 'Ordinal's.++ Since 0.7.0.0+-}+(%!!) ::+ forall f (n :: Nat) c.+ (CFoldable f, Dom f c) =>+ Sized f n c ->+ Ordinal n ->+ c+(%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c+{-# INLINE (%!!) #-}+{-# SPECIALIZE (%!!) :: Sized [] (n :: Nat) a -> Ordinal n -> a #-}+{-# SPECIALIZE (%!!) :: Sized V.Vector (n :: Nat) a -> Ordinal n -> a #-}+{-# SPECIALIZE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Nat) a -> Ordinal n -> a #-}+{-# SPECIALIZE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Nat) a -> Ordinal n -> a #-}+{-# SPECIALIZE (%!!) :: Sized Seq.Seq (n :: Nat) a -> Ordinal n -> a #-}++{- | Flipped version of '!!'.++ Since 0.7.0.0+-}+index ::+ forall f (m :: Nat) a.+ (CFoldable f, Dom f a, (1 <= m)) =>+ Int ->+ Sized f m a ->+ a+index = flip (!!)+{-# INLINE index #-}++{- | Flipped version of '%!!'.++ Since 0.7.0.0+-}+sIndex ::+ forall f (n :: Nat) c.+ (CFoldable f, Dom f c) =>+ Ordinal n ->+ Sized f n c ->+ c+sIndex = flip $ (%!!) @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 f (n :: Nat) a.+ (CFoldable f, Dom f a, (0 < n)) =>+ 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 f (n :: Nat) a.+ ((0 < n), 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 f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a, (1 <= n)) =>+ Sized f n a ->+ Uncons f n a+uncons =+ withKnownNat+ (sPred $ sNat @n)+ $ uncurry (Uncons @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)++{- | 'uncons' with explicit specified length @n@++ Since 0.7.0.0+-}+uncons' ::+ forall f (n :: Nat) a proxy.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ proxy n ->+ Sized f (Succ n) a ->+ Uncons f (Succ n) a+uncons' _ =+ withKnownNat (sSucc $ sNat @n) uncons+{-# INLINE uncons' #-}++data Uncons f (n :: Nat) a where+ Uncons ::+ forall f (n :: Nat) a.+ KnownNat n =>+ a ->+ Sized f n a ->+ Uncons f (1 + 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 f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a, (0 < n)) =>+ Sized f n a ->+ Unsnoc f n a+unsnoc =+ withKnownNat+ (sPred $ sNat @n)+ $ uncurry (Unsnoc @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a)+{-# NOINLINE [1] unsnoc #-}++data Unsnoc f n a where+ Unsnoc :: forall f n a. Sized f (n :: Nat) a -> a -> Unsnoc f (Succ n) a++{- | 'unsnoc'' with explicit specified length @n@++ Since 0.7.0.0+-}+unsnoc' ::+ forall f (n :: Nat) a proxy.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ proxy n ->+ Sized f (Succ n) a ->+ Unsnoc f (Succ n) a+unsnoc' _ =+ withKnownNat (sSucc $ sNat @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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ Sized f (1 + 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ Sized f (n + 1) 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 (n :: Nat) f (m :: Nat) a.+ (CFreeMonoid f, Dom f a, (n <= m)) =>+ SNat n ->+ Sized f m a ->+ Sized f n a+take = coerce $ ctake @f @a . P.fromIntegral . fromSNat @n+{-# INLINE take #-}++{- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.++ Since 0.7.0.0+-}+takeAtMost ::+ forall (n :: Nat) f m a.+ (CFreeMonoid f, Dom f a) =>+ SNat n ->+ Sized f m a ->+ Sized f (Min n m) a+takeAtMost = coerce $ ctake @f @a . P.fromIntegral . fromSNat @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 (n :: Nat) f (m :: Nat) a.+ (CFreeMonoid f, Dom f a, (n <= m)) =>+ SNat n ->+ Sized f m a ->+ Sized f (m - n) a+drop = coerce $ cdrop @f @a . P.fromIntegral . fromSNat @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 (n :: Nat) f m a.+ (CFreeMonoid f, Dom f a, (n <= m)) =>+ SNat n ->+ Sized f m a ->+ (Sized f n a, Sized f (m -. n) a)+splitAt =+ coerce $ csplitAt @f @a . P.fromIntegral . fromSNat @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 (n :: Nat) f (m :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ SNat n ->+ Sized f m a ->+ (Sized f (Min n m) a, Sized f (m -. n) a)+splitAtMost =+ coerce $ csplitAt @f @a . P.fromIntegral . fromSNat @n+{-# INLINE splitAtMost #-}++--------------------------------------------------------------------------------+-- Construction+--------------------------------------------------------------------------------++--------------------------------------------------------------------------------+--- Initialisation+--------------------------------------------------------------------------------++{- | Empty sequence.++ Since 0.7.0.0 (type changed)+-}+empty ::+ forall f a.+ (Monoid (f a), Dom f a) =>+ Sized f (0) a+empty = coerce $ mempty @(f a)+{-# INLINE empty #-}++{- | Sequence with one element.++ Since 0.7.0.0+-}+singleton :: forall f a. (CPointed f, Dom f a) => a -> Sized f (1) 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 f a.+ (Dom f a, CFoldable f) =>+ f a ->+ SomeSized f a+{-# INLINE toSomeSized #-}+toSomeSized = \xs ->+ case toSomeSNat $ P.fromIntegral $ clength xs of+ SomeSNat sn -> withKnownNat sn $ SomeSized sn $ unsafeToSized sn xs++{- | Replicates the same value.++ Since 0.7.0.0+-}+replicate ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ SNat n ->+ a ->+ Sized f n a+replicate = coerce $ creplicate @f @a . P.fromIntegral . fromSNat @n+{-# INLINE replicate #-}++{- | 'replicate' with the length inferred.++ Since 0.7.0.0+-}+replicate' ::+ forall f (n :: Nat) a.+ (KnownNat (n :: Nat), CFreeMonoid f, Dom f a) =>+ a ->+ Sized f n a+replicate' = replicate (sNat @n)+{-# INLINE replicate' #-}++{- | Construct a sequence of the given length by applying the function to each index.++ Since 0.7.0.0+-}+generate ::+ forall f (n :: Nat) (a :: Type).+ (CFreeMonoid f, Dom f a) =>+ SNat n ->+ (Ordinal n -> a) ->+ Sized f n a+generate = coerce $ \sn ->+ withKnownNat sn $+ cgenerate @f @a (P.fromIntegral $ fromSNat @n sn)+ . (. toEnum @(Ordinal n))+{-# INLINE [1] generate #-}++{- | 'generate' with length inferred.++ Since 0.8.0.0+-}+generate' ::+ forall f (n :: Nat) (a :: Type).+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ (Ordinal n -> a) ->+ Sized f n a+generate' = generate sNat+{-# INLINE [1] generate' #-}++genVector ::+ forall (n :: Nat) a.+ SNat n ->+ (Ordinal n -> a) ->+ Sized V.Vector n a+genVector n f = withKnownNat n $ Sized $ V.generate (P.fromIntegral $ fromSNat n) (f . toEnum)+{-# INLINE genVector #-}++genSVector ::+ forall (n :: Nat) a.+ (SV.Storable a) =>+ SNat n ->+ (Ordinal n -> a) ->+ Sized SV.Vector n a+genSVector n f = withKnownNat n $ Sized $ SV.generate (P.fromIntegral $ fromSNat n) (f . toEnum)+{-# INLINE genSVector #-}++genSeq ::+ forall (n :: Nat) a.+ SNat n ->+ (Ordinal n -> a) ->+ Sized Seq.Seq n a+genSeq n f = withKnownNat n $ Sized $ Seq.fromFunction (P.fromIntegral $ fromSNat n) (f . toEnum)+{-# INLINE genSeq #-}++{-# RULES+"generate/Vector" [~1] generate = genVector+"generate/SVector" [~1] forall+ (n :: SNat (n :: Nat))+ (f :: SV.Storable a => Ordinal n -> a).+ generate n f =+ genSVector n f+"generate/UVector" [~1] forall+ (n :: SNat (n :: Nat))+ (f :: UV.Unbox a => Ordinal n -> a).+ generate n f =+ withKnownNat n $ Sized (UV.generate (P.fromIntegral $ fromSNat n) (f . toEnum))+"generate/Seq" [~1] generate = genSeq+ #-}++--------------------------------------------------------------------------------+--- Concatenation+--------------------------------------------------------------------------------++{- | Append an element to the head of sequence.++ Since 0.8.0.0+-}+cons ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ a ->+ Sized f n a ->+ Sized f (1 + n) a+cons = coerce $ ccons @f @a+{-# INLINE cons #-}++{- | Infix version of 'cons'.++ Since 0.8.0.0+-}+(<|) ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ a ->+ Sized f n a ->+ Sized f (1 + n) a+(<|) = cons+{-# INLINE (<|) #-}++infixr 5 <|++{- | Append an element to the tail of sequence.++ Since 0.7.0.0+-}+snoc ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ Sized f n a ->+ a ->+ Sized f (n + 1) a+snoc (Sized xs) a = Sized $ csnoc xs a+{-# INLINE snoc #-}++{- | Infix version of 'snoc'.++ Since 0.7.0.0+-}+(|>) ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ Sized f n a ->+ a ->+ Sized f (n + 1) a+(|>) = snoc+{-# INLINE (|>) #-}++infixl 5 |>++{- | Append two lists.++ Since 0.7.0.0+-}+append ::+ forall 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 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 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 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 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 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 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+zipWithSame = coerce $ czipWith @f @a @b @c+{-# INLINE [1] zipWithSame #-}++{- | Unzipping the sequence of tuples.++ Since 0.7.0.0+-}+unzip ::+ forall 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 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 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 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ a ->+ Sized f n a ->+ Sized f ((2 * n) -. 1) a+intersperse = coerce $ cintersperse @f @a+{-# INLINE intersperse #-}++{- | Remove all duplicates.++ Since 0.7.0.0+-}+nub ::+ forall f (n :: Nat) a.+ (Dom f a, Eq a, CFreeMonoid f) =>+ Sized f n a ->+ SomeSized f a+nub = toSomeSized . coerce (cnub @f @a)++{- | Sorting sequence by ascending order.++ Since 0.7.0.0+-}+sort ::+ forall 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 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 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 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 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ SNat n ->+ [a] ->+ Maybe (Sized f n a)+fromList Zero _ = Just $ Sized (mempty :: f a)+fromList sn xs =+ let len = P.fromIntegral $ fromSNat sn+ in if P.length xs < len+ then Nothing+ else Just $ Sized $ ctake len $ cfromList xs+{-# INLINEABLE [2] fromList #-}++{- | 'fromList' with the result length inferred.++ Since 0.7.0.0+-}+fromList' ::+ forall f (n :: Nat) a.+ (Dom f a, CFreeMonoid f, KnownNat n) =>+ [a] ->+ Maybe (Sized f n a)+fromList' = fromList sNat+{-# 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ SNat 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 f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ [a] ->+ Sized f n a+unsafeFromList' = unsafeFromList sNat+{-# 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 (n :: Nat) a.+ (Dom f a, CFreeMonoid f) =>+ SNat n ->+ a ->+ [a] ->+ Sized f n a+fromListWithDefault sn def xs =+ let len = P.fromIntegral $ fromSNat sn+ in Sized $+ cfromList (ctake len xs)+ <> creplicate (len - clength xs) def+{-# INLINEABLE fromListWithDefault #-}++{- | 'fromListWithDefault' with the result length inferred.++ Since 0.7.0.0+-}+fromListWithDefault' ::+ forall f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ a ->+ [a] ->+ Sized f n a+fromListWithDefault' = fromListWithDefault sNat+{-# INLINE fromListWithDefault' #-}++--------------------------------------------------------------------------------+--- Base containes+--------------------------------------------------------------------------------++{- | Forget the length and obtain the wrapped base container.++ Since 0.7.0.0+-}+unsized :: forall 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ SNat (n :: Nat) ->+ f a ->+ Maybe (Sized f n a)+toSized sn xs =+ let len = P.fromIntegral $ fromSNat sn+ in if clength xs < len+ then Nothing+ else Just $ unsafeToSized sn $ ctake len xs+{-# INLINEABLE [2] toSized #-}++{- | 'toSized' with the result length inferred.++ Since 0.7.0.0+-}+toSized' ::+ forall f (n :: Nat) a.+ (Dom f a, CFreeMonoid f, KnownNat n) =>+ f a ->+ Maybe (Sized f n a)+toSized' = toSized sNat+{-# 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 f (n :: Nat) a. SNat 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 f (n :: Nat) a.+ (KnownNat n, Dom f a) =>+ f a ->+ Sized f n a+unsafeToSized' = unsafeToSized sNat+{-# 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ SNat (n :: Nat) ->+ a ->+ f a ->+ Sized f n a+toSizedWithDefault sn def xs =+ let len = P.fromIntegral $ fromSNat sn+ in Sized $ ctake len xs <> creplicate (len - clength xs) def+{-# INLINEABLE toSizedWithDefault #-}++{- | 'toSizedWithDefault' with the result length inferred.++ Since 0.7.0.0+-}+toSizedWithDefault' ::+ forall f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ a ->+ f a ->+ Sized f n a+toSizedWithDefault' = toSizedWithDefault sNat+{-# 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) =>+ SNat n ->+ Sized f n a ->+ SNat 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 f (n :: Nat) a.+ (Dom f a, CFreeMonoid f) =>+ (a -> Bool) ->+ Sized f n a ->+ SomeSized f 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 f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ (a -> Bool) ->+ Sized f n a ->+ SomeSized f a+dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a)+{-# INLINE dropWhile #-}++{- | Split the sequence into the longest prefix+ of elements that satisfy the predicate+ and the rest.++ Since 0.7.0.0+-}+span ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ (a -> Bool) ->+ Sized f n a ->+ Partitioned f n a+span = (unsafePartitioned @n .) . coerce (cspan @f @a)+{-# INLINE span #-}++{- | Split the sequence into the longest prefix+ of elements that do not satisfy the+ predicate and the rest.++ Since 0.7.0.0+-}+break ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ (a -> Bool) ->+ Sized f n a ->+ Partitioned f n a+break = (unsafePartitioned @n .) . coerce (cbreak @f @a)+{-# INLINE break #-}++{- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.++ Since 0.7.0.0+-}+partition ::+ forall f (n :: Nat) a.+ (CFreeMonoid f, Dom f a) =>+ (a -> Bool) ->+ Sized f n a ->+ Partitioned f n a+partition = (unsafePartitioned @n .) . coerce (cpartition @f @a)+{-# INLINE partition #-}++unsafePartitioned ::+ forall (n :: Nat) f a.+ (CFreeMonoid f, Dom f a) =>+ (f a, f a) ->+ Partitioned f n a+unsafePartitioned (l, r) =+ case (toSomeSized l, toSomeSized r) of+ ( SomeSized (lenL :: SNat nl) ls+ , SomeSized (lenR :: SNat 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 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 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 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 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 f (n :: Nat) a.+ (KnownNat (n :: Nat), CFoldable f, Dom f a) =>+ (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 f (n :: Nat) a.+ (CFoldable f, Dom f a) =>+ (a -> Bool) ->+ Sized f n a ->+ [Int]+findIndices = coerce $ cfindIndices @f @a+{-# INLINE findIndices #-}+{-# SPECIALIZE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}++{- | 'Ordinal' version of 'findIndices'.++ Since 0.7.0.0+-}+sFindIndices ::+ forall f (n :: Nat) a.+ (CFoldable f, Dom f a, KnownNat (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 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 f (n :: Nat) a.+ (KnownNat n, CFoldable f, Dom f a, Eq a) =>+ 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 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 f (n :: Nat) a.+ (CFoldable f, KnownNat (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 :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n+slen ('viewCons' -> 'NilCV') = 'SZ'+slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)+slen _ = error "impossible"+@++ The constraint @('KnownNat' 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 :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' 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 (0) a+ (:-) ::+ (KnownNat n, KnownNat (1 + n)) =>+ a ->+ Sized f n a ->+ ConsView f (1 + n) a++infixr 5 :-++{- | Case analysis for the cons-side of sequence.++ Since 0.5.0.0 (type changed)+-}+viewCons ::+ forall f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ Sized f n a ->+ ConsView f n a+viewCons sz = case zeroOrSucc $ sNat @n of+ IsZero -> NilCV+ IsSucc n' ->+ withKnownNat n' $+ withKnownNat (sOne %+ 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 (0) a+ (:-::) :: KnownNat (n :: Nat) => Sized f n a -> a -> SnocView f (n + 1) a++infixl 5 :-::++{- | Case analysis for the snoc-side of sequence.++ Since 0.5.0.0 (type changed)+-}+viewSnoc ::+ forall f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ Sized f n a ->+ SnocView f n a+viewSnoc sz = case zeroOrSucc (sNat @n) of+ IsZero -> NilSV+ IsSucc (n' :: SNat n') ->+ withKnownNat 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, 'KnownNat' 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, 'KnownNat' n) => 'Sized' f ('S' ('S' n)) a -> a+nextToHead (_ ':<' a ':<' _) = a+@++ Of course, we can also rewrite above @slen@ example usNat @PatternSynonyms@:++@+slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n+slen 'Nil' = 'SZ'+slen (_ ':<' as) = 'SS' (slen as)+@++ So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to+ pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.+ @'Nil'@, @':<'@, and @':>'@ 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 (f :: Type -> Type) a (n :: Nat).+ (Dom f a, KnownNat n, CFreeMonoid f) =>+ forall (n1 :: Nat).+ (n ~ (1 + n1), KnownNat n1) =>+ a ->+ Sized f n1 a ->+ Sized f n a+pattern a :< as <-+ (viewCons -> a :- as)+ where+ a :< as = a <| as++chkNil ::+ forall f (n :: Nat) a.+ (KnownNat n) =>+ Sized f n a ->+ ZeroOrSucc n+chkNil = const $ zeroOrSucc $ sNat @n++-- | Pattern synonym for a nil sequence.+pattern Nil ::+ forall f (n :: Nat) a.+ (KnownNat n, CFreeMonoid f, Dom f a) =>+ (n ~ 0) =>+ Sized f n a+pattern Nil <-+ (chkNil -> IsZero)+ where+ Nil = empty++infixl 5 :>++-- | Pattern synonym for snoc-side unsnoc.+pattern (:>) ::+ forall (f :: Type -> Type) a (n :: Nat).+ (Dom f a, KnownNat n, CFreeMonoid f) =>+ forall (n1 :: Nat).+ (n ~ (n1 + 1), KnownNat n1) =>+ Sized f n1 a ->+ a ->+ Sized f n a+pattern a :> b <-+ (viewSnoc -> a :-:: b)+ where+ a :> b = a |> b++{-# COMPLETE (:<), Nil #-}++{-# COMPLETE (:>), Nil #-}++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+ , KnownNat n+ , forall a. DomC f a+ ) =>+ P.Applicative (Sized f (n :: Nat))+ where+ {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized [] (n :: Nat)) #-}+ {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized Seq.Seq (n :: Nat)) #-}+ {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized V.Vector (n :: 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, KnownNat (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+ (KnownNat (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,4 @@+module Data.Sized.Builtin+ {-# DEPRECATED "Use Data.Sized instead" #-}+ ( module Data.Sized ) where+import Data.Sized
+ src/Data/Sized/Flipped.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LiberalTypeSynonyms #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoStarIsType #-}+module Data.Sized.Flipped (Flipped (..)) where++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 (..), MonoFunctor (..), MonoTraversable (..))+import qualified Data.Sequence as Seq+import Data.Sized.Internal+import qualified Data.Type.Natural as PN+import Data.Type.Ordinal (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)) =>+ Ixed (Flipped f a n)+ where+ {-# SPECIALIZE instance Ixed (Flipped [] a (n :: TL.Nat)) #-}+ {-# SPECIALIZE instance Ixed (Flipped [] a (n :: PN.Nat)) #-}+ {-# SPECIALIZE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-}+ {-# SPECIALIZE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-}+ {-# SPECIALIZE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-}+ {-# SPECIALIZE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-}+ {-# SPECIALIZE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-}+ {-# SPECIALIZE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-}+ {-# SPECIALIZE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-}+ {-# SPECIALIZE 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,141 @@+{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable #-}+{-# LANGUAGE DeriveFunctor, DeriveTraversable, DerivingStrategies #-}+{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-}+{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators, UndecidableInstances #-}+{-# LANGUAGE NoStarIsType #-}+{-# 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.Type.Ordinal (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 GHC.TypeNats++-- | @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))+ => Ixed (Sized f (n :: Nat) a) where+ {-# SPECIALISE instance Ixed (Sized [] (n :: Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized V.Vector (n :: Nat) a) #-}+ {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: Nat) a) #-}+ {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: Nat) a) #-}+ {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: 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, KnownNat n)+ => FunctorWithIndex (Ordinal n) (Sized f n) where+ imap f = Sized . imap (f . unsafeNaturalToOrd . fromIntegral) . runSized+ {-# INLINE imap #-}+ {-# SPECIALISE instance KnownNat n+ => FunctorWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-}+ {-# SPECIALISE instance KnownNat n+ => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-}+ {-# SPECIALISE instance KnownNat n+ => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-}++-- | Since 0.4.0.0+instance {-# OVERLAPPABLE #-} (Integral i, FoldableWithIndex i f, KnownNat n)+ => FoldableWithIndex (Ordinal n) (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 KnownNat n+ => FoldableWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-}+ {-# SPECIALISE instance KnownNat n+ => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-}+ {-# SPECIALISE instance KnownNat n+ => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-}+-- | Since 0.2.0.0+instance (Integral i, TraversableWithIndex i f, KnownNat n)+ => TraversableWithIndex (Ordinal n) (Sized f n) where+ itraverse f = fmap Sized . itraverse (f . unsafeNaturalToOrd . fromIntegral) . runSized+ {-# INLINE itraverse #-}++ {-# SPECIALISE instance KnownNat n+ => TraversableWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-}+ {-# SPECIALISE instance KnownNat n+ => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-}+ {-# SPECIALISE instance KnownNat n+ => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-}
@@ -0,0 +1,35 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -O2 -fno-hpc #-}++module Shared where++import Language.Haskell.TH (ExpQ)+import Test.Tasty.Inspection++inspecting :: String -> Obligation -> ExpQ+inspecting title obl = inspectTest $ obl {testName = Just title}++data GHCVer = GHC8_8 | GHC8_10 | GHC9_0 | GHC9_2 | GHC9_4 | GHC9_6 | GHC9_8 | GHC9_10+ deriving (Show, Eq, Ord)++ghcVer :: GHCVer+#if __GLASGOW_HASKELL__ == 910+ghcVer = GHC9_10+#elif __GLASGOW_HASKELL__ == 908+ghcVer = GHC9_8+#elif __GLASGOW_HASKELL__ == 906+ghcVer = GHC9_6+#elif __GLASGOW_HASKELL__ == 904+ghcVer = GHC9_4+#elif __GLASGOW_HASKELL__ == 902+ghcVer = GHC9_2+#elif __GLASGOW_HASKELL__ == 900+ghcVer = GHC9_0+#elif __GLASGOW_HASKELL__ == 810+ghcVer = GHC8_10+#elif __GLASGOW_HASKELL__ == 808+ghcVer = GHC8_8+#else+ghcVer = error "Coudld not determine GHC Version: __GLASGOW_HASKELL__"+#endif
+ test/opt-test.hs view
@@ -0,0 +1,182 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE 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.Sized (Sized, zipWithSame)+import qualified Data.Sized as SV+import Data.Type.Natural+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 Numeric.Natural (Natural)+import Shared+import Test.Tasty+import Test.Tasty.Inspection+import qualified Data.Vector.Generic.Mutable as MV+import Control.Monad.Primitive (PrimMonad)++type LSized = Sized []++type VSized = Sized V.Vector++type USized = Sized U.Vector++type SSized = Sized S.Vector++type SeqSized = Sized Seq.Seq++{-# ANN module "HLINT: ignore Use camelCase" #-}++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++length_two :: Dom f a => Sized f 2 a -> Int+length_two = SV.length++const_two_dom :: Dom f a => Sized f 2 a -> Int+const_two_dom = const 2++main :: IO ()+main =+ defaultMain $+ testGroup+ "Optimisation test"+ [ testGroup+ "czipWith"+ [ $( inspecting "doesn't contain type classes" $+ hasNoTypeClasses 'zipWith_subcat_List+ )+ ]+ , testGroup+ "zipWith"+ [ $( inspecting "doesn't contain type classes" $+ hasNoTypeClasses 'zipWith_List+ )+ ]+ , testGroup+ "zipWithSame"+ [ testGroup+ "list"+ [ $( inspecting "doesn't contain type classes" $+ hasNoTypeClasses 'zipWithSame_List+ )+ , $( inspecting "is almost the same as the original zipWith (list)" $+ 'zipWithSame_List ==- 'zipWith_List_Prel+ )+ ]+ , testGroup+ "Boxed Vector"+ [ $( inspecting "doesn't contain type classes, except for G.Vector" $+ 'zipWithSame_Boxed+ `hasNoTypeClassesExcept` [''G.Vector]+ )+ , $( inspecting "is almost the same as the original zipWith (Boxed)" $+ 'zipWithSame_Boxed ==- 'zipWith_Boxed+ )+ ]+ , testGroup+ "Unboxed Vector"+ [ $( inspecting "doesn't contain type classes except for Unbox, and Vector, MVector (>= GHC 9)" $+ 'zipWithSame_Unboxed+ `hasNoTypeClassesExcept`+ if ghcVer >= GHC9_0 + then + if ghcVer >= GHC9_6+ then [''Unbox, ''G.Vector, ''MV.MVector]+ else [''Unbox, ''G.Vector, ''MV.MVector, ''Monad, ''PrimMonad]+ else [''Unbox]+ )+ + , $( inspecting "doesn't contain type classes if fully instnatiated" $+ hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic+ )+ , $( inspecting "is almost the same as the original zipWith, if fully instantiated" $+ 'zipWithSame_Unboxed_monomorphic+ ==- 'zipWith_Unboxed_monomorphic+ )+ ]+ ]+ , testGroup+ "length"+ [ $( inspecting "is a constant function when length is concrete (with Dom dictionary)" $+ 'length_two ==- 'const_two_dom+ )+ , $( inspecting "doesn't contain Integer when the length is concrete" $ hasNoType 'length_two ''Integer+ )+ , $( inspecting "doesn't contain Natural when the length is concrete" $ hasNoType 'length_two ''Natural+ )+ ]+ ]