sized 0.9.0.0 → 1.0.0.0
raw patch · 7 files changed
+2040/−3619 lines, 7 filesdep −singletonsdep −singletons-presburgerdep ~ghc-typelits-presburgerdep ~type-natural
Dependencies removed: singletons, singletons-presburger
Dependency ranges changed: ghc-typelits-presburger, type-natural
Files
- sized.cabal +4/−7
- src/Data/Sized.hs +1828/−1412
- src/Data/Sized/Builtin.hs +4/−1005
- src/Data/Sized/Flipped.hs +61/−42
- src/Data/Sized/Internal.hs +50/−77
- src/Data/Sized/Peano.hs +0/−1002
- test/opt-test.hs +93/−74
sized.cabal view
@@ -1,12 +1,12 @@ cabal-version: >=2.0 name: sized-version: 0.9.0.0+version: 1.0.0.0 license: BSD3 license-file: LICENSE maintainer: konn.jinro_at_gmail.com author: Hiromi ISHII tested-with:- ghc ==8.6.5, ghc ==8.8.3, ghc ==8.10.1+ ghc ==8.6.5, ghc ==8.8.4, ghc ==8.10.3 synopsis: Sized sequence data-types description:@@ -23,7 +23,6 @@ exposed-modules: Data.Sized Data.Sized.Builtin- Data.Sized.Peano Data.Sized.Flipped hs-source-dirs: src@@ -35,11 +34,9 @@ constraints, these, type-natural >=0.8.1.0,- ghc-typelits-presburger >=0.2.0.0,+ ghc-typelits-presburger >=0.4, ghc-typelits-knownnat,- singletons-presburger, mono-traversable >=0.10,- singletons >=2.0, subcategories, deepseq >=1.4, hashable >=1.2,@@ -61,9 +58,9 @@ hspec -any, inspection-testing ^>=0.4, mono-traversable -any,- singletons -any, sized -any, template-haskell -any,+ type-natural, th-lift -any, subcategories -any, vector -any
src/Data/Sized.hs view
@@ -1,1415 +1,1831 @@-{-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds #-}-{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable, DerivingStrategies, ExplicitNamespaces #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs #-}-{-# LANGUAGE GeneralizedNewtypeDeriving, InstanceSigs, KindSignatures #-}-{-# LANGUAGE LambdaCase, LiberalTypeSynonyms, MultiParamTypeClasses #-}-{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms #-}-{-# LANGUAGE PolyKinds, QuantifiedConstraints, RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeApplications #-}-{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-}-{-# LANGUAGE UndecidableSuperClasses, 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 '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 Data.Sized.Internal--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.Singletons.Prelude (SingI (..), SomeSing (..),- withSing, withSingI)-import Data.Singletons.Prelude.Bool (Sing)-import Data.Singletons.Prelude.Enum (PEnum (..), sPred, sSucc)-import Data.These (These (..))-import Data.Type.Equality (gcastWith, (:~:) (..))-import qualified Data.Type.Natural as Peano-import Data.Type.Natural.Class (IsPeano (..), One, PNum (..),- POrd (..), PeanoOrder (..), S,- SNum (..), Zero, ZeroOrSucc (..),- pattern Zero, sOne, sZero,- type (-.))-import Data.Type.Ordinal (HasOrdinal, Ordinal (..),- ordToNatural)-import Data.Typeable (Typeable)-import qualified Data.Vector as V-import qualified Data.Vector.Storable as SV-import qualified Data.Vector.Unboxed as UV-import qualified GHC.TypeLits as TL-import Prelude (Bool (..), Enum (..), Eq (..),- Functor, Int, Maybe (..),- Num (..), Ord (..), Ordering,- Show (..), const, flip, fmap,- fromIntegral, uncurry, ($), (.))-import qualified Prelude as P-import Proof.Propositional (IsTrue (..), withWitness)-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.7.0.0-data SomeSized' f nat a where- SomeSized' :: Sing n- -> Sized f (n :: nat) a- -> SomeSized' f nat a--deriving instance Typeable SomeSized'--instance Show (f a) => Show (SomeSized' f nat a) where- showsPrec d (SomeSized' _ s) = P.showParen (d > 9) $- P.showString "SomeSized' _ " . showsPrec 10 s-instance Eq (f a) => Eq (SomeSized' f nat a) where- (SomeSized' _ (Sized xs)) == (SomeSized' _ (Sized ys)) = xs == ys------------------------------------------------------------------------------------- Accessors----------------------------------------------------------------------------------------------------------------------------------------------------------------------- Length infromation------------------------------------------------------------------------------------- | Returns the length of wrapped containers.--- If you use @unsafeFromList@ or similar unsafe functions,--- this function may return different value from type-parameterized length.------ Since 0.8.0.0 (type changed)-length- :: forall nat f (n :: nat) a.- (IsPeano nat, Dom f a, SingI n)- => Sized f n a -> Int-length = const $ fromIntegral $ toNatural $ sing @n-{-# INLINE CONLIKE [1] length #-}--lengthTLZero :: Sized f 0 a -> Int-lengthTLZero = P.const 0-{-# INLINE lengthTLZero #-}--lengthPeanoZero :: Sized f 'Peano.Z a -> Int-lengthPeanoZero = P.const 0-{-# INLINE lengthPeanoZero #-}--{-# RULES-"length/0" [~1] length = lengthTLZero-"length/Z" [~1] length = lengthPeanoZero- #-}---- | @Sing@ version of 'length'.------ Since 0.8.0.0 (type changed)-sLength :: forall nat f (n :: nat) a.- (HasOrdinal nat, Dom f a, SingI n)- => Sized f n a -> Sing n-sLength _ = sing @n-{-# INLINE[2] sLength #-}---- | Test if the sequence is empty or not.------ Since 0.7.0.0-null- :: forall nat f (n :: nat) a. (CFoldable f, Dom f a)- => Sized f n a -> Bool-null = coerce $ cnull @f @a-{-# INLINE CONLIKE [2] null #-}--nullTL0 :: Sized f 0 a -> Bool-nullTL0 = P.const True-{-# INLINE nullTL0 #-}--nullPeano0 :: Sized f 'Peano.Z a -> Bool-nullPeano0 = P.const True-{-# INLINE nullPeano0 #-}--nullPeanoSucc :: Sized f (S n) a -> Bool-nullPeanoSucc = P.const False-{-# INLINE nullPeanoSucc #-}--nullTLSucc :: Sized f (n + 1) a -> Bool-nullTLSucc = P.const False-{-# INLINE nullTLSucc #-}--{-# RULES-"null/0" [~2] null = nullTL0-"null/0" [~2] null = nullTLSucc-"null/0" [~1] forall (vec :: 1 TL.<= n => Sized f n a).- null vec = False-"null/Z" [~2] null = nullPeano0-"null/Sn" [~2] null = nullPeanoSucc- #-}-------------------------------------------------------------------------------------- Indexing------------------------------------------------------------------------------------- | (Unsafe) indexing with @Int@s.--- If you want to check boundary statically, use '%!!' or 'sIndex'.------ Since 0.7.0.0-(!!)- :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True)- => Sized f m a -> Int -> a-(!!) = coerce $ cindex @f @a-{-# INLINE (!!) #-}---- | Safe indexing with 'Ordinal's.------ Since 0.7.0.0-(%!!)- :: forall nat f (n :: nat) c.- (HasOrdinal nat, CFoldable f, Dom f c)- => Sized f n c -> Ordinal n -> c-(%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c-{-# INLINE (%!!) #-}-{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-}-{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-}---- | Flipped version of '!!'.------ Since 0.7.0.0-index- :: forall nat f (m :: nat) a.- (CFoldable f, Dom f a, (One nat <= m) ~ 'True)- => Int -> Sized f m a -> a-index = flip (!!)-{-# INLINE index #-}---- | Flipped version of '%!!'.------ Since 0.7.0.0-sIndex- :: forall nat f (n :: nat) c. (HasOrdinal nat, CFoldable f, Dom f c)- => Ordinal n -> Sized f n c -> c-sIndex = flip $ (%!!) @nat @f @n @c-{-# INLINE sIndex #-}---- | Take the first element of non-empty sequence.--- If you want to make case-analysis for general sequence,--- see <#ViewsAndPatterns Views and Patterns> section.------ Since 0.7.0.0-head- :: forall nat f (n :: nat) a.- (HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True)- => Sized f n a -> a-head = coerce $ chead @f @a-{-# INLINE head #-}---- | Take the last element of non-empty sequence.--- If you want to make case-analysis for general sequence,--- see <#ViewsAndPatterns Views and Patterns> section.------ Since 0.7.0.0-last :: forall nat f (n :: nat) a.- (HasOrdinal nat, (Zero nat < n) ~ 'True, CFoldable f, Dom f a)- => Sized f n a -> a-last = coerce $ clast @f @a-{-# INLINE last #-}---- | Take the 'head' and 'tail' of non-empty sequence.--- If you want to make case-analysis for general sequence,--- see <#ViewsAndPatterns Views and Patterns> section.------ Since 0.7.0.0-uncons :: forall nat f (n :: nat) a.- (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True)- => Sized f n a -> Uncons f n a-uncons =- withSingI- (sPred $ sing @n)- $ gcastWith- (succAndPlusOneL $ sPred $ sing @n)- $ gcastWith- (lneqRightPredSucc sZero (sing @n) Witness- )- $ uncurry (Uncons @nat @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)---- | 'uncons' with explicit specified length @n@------ Since 0.7.0.0-uncons'- :: forall nat f (n :: nat) a proxy.- (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a)- => proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a-uncons' _ = withSingI (sSucc $ sing @n)- $ withWitness (lneqZero $ sing @n) uncons-{-# INLINE uncons' #-}--data Uncons f (n :: nat) a where- Uncons :: forall nat f (n :: nat) a. SingI n- => a -> Sized f n a -> Uncons f (One nat + n) a---- | Take the 'init' and 'last' of non-empty sequence.--- If you want to make case-analysis for general sequence,--- see <#ViewsAndPatterns Views and Patterns> section.------ Since 0.7.0.0-unsnoc- :: forall nat f (n :: nat) a.- (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True)- => Sized f n a -> Unsnoc f n a-unsnoc = withSingI- (sPred $ sing @n)- $ gcastWith- (lneqRightPredSucc sZero (sing @n) Witness- )- $ uncurry (Unsnoc @nat @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a)-{-# NOINLINE [1] unsnoc #-}--data Unsnoc f n a where- Unsnoc :: forall nat f n a. Sized f (n :: nat) a -> a -> Unsnoc f (Succ n) a---- | 'unsnoc'' with explicit specified length @n@------ Since 0.7.0.0-unsnoc'- :: forall nat f (n :: nat) a proxy.- (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a)- => proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a-unsnoc' _ =- withSingI (sSucc $ sing @n)- $ withWitness (lneqZero $ sing @n) unsnoc-{-# INLINE unsnoc' #-}--------------------------------------------------------------------------------------- Slicing------------------------------------------------------------------------------------- | Take the tail of non-empty sequence.--- If you want to make case-analysis for general sequence,--- see <#ViewsAndPatterns Views and Patterns> section.------ Since 0.7.0.0-tail- :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sized f (One nat + n) a -> Sized f n a-tail = coerce $ ctail @f @a-{-# INLINE tail #-}---- | Take the initial segment of non-empty sequence.--- If you want to make case-analysis for general sequence,--- see <#ViewsAndPatterns Views and Patterns> section.------ Since 0.7.0.0-init- :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sized f (n + One nat) a -> Sized f n a-init = coerce $ cinit @f @a-{-# INLINE init #-}---- | @take k xs@ takes first @k@ element of @xs@ where--- the length of @xs@ should be larger than @k@.------ Since 0.7.0.0-take- :: forall nat (n :: nat) f (m :: nat) a.- (CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat)- => Sing n -> Sized f m a -> Sized f n a-take = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n-{-# INLINE take #-}---- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.------ Since 0.7.0.0-takeAtMost- :: forall nat (n :: nat) f m a.- (CFreeMonoid f, Dom f a, HasOrdinal nat)- => Sing n -> Sized f m a -> Sized f (Min n m) a-takeAtMost = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n-{-# INLINE takeAtMost #-}---- | @drop k xs@ drops first @k@ element of @xs@ and returns--- the rest of sequence, where the length of @xs@ should be larger than @k@.------ Since 0.7.0.0-drop- :: forall nat (n :: nat) f (m :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True)- => Sing n -> Sized f m a -> Sized f (m - n) a-drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @nat @n-{-# INLINE drop #-}---- | @splitAt k xs@ split @xs@ at @k@, where--- the length of @xs@ should be less than or equal to @k@.------ Since 0.7.0.0-splitAt- :: forall nat (n :: nat) f m a.- (CFreeMonoid f, Dom f a , (n <= m) ~ 'True, HasOrdinal nat)- => Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)-splitAt =- coerce $ csplitAt @f @a . P.fromIntegral . toNatural @nat @n-{-# INLINE splitAt #-}---- | @splitAtMost k xs@ split @xs@ at @k@.--- If @k@ exceeds the length of @xs@, then the second result value become empty.------ Since 0.7.0.0-splitAtMost- :: forall nat (n :: nat) f (m :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)-splitAtMost =- coerce $ csplitAt @f @a . P.fromIntegral . toNatural @nat @n-{-# INLINE splitAtMost #-}-------------------------------------------------------------------------------------- Construction----------------------------------------------------------------------------------------------------------------------------------------------------------------------- Initialisation------------------------------------------------------------------------------------- | Empty sequence.------ Since 0.7.0.0 (type changed)-empty- :: forall nat f a. (Monoid (f a), HasOrdinal nat, Dom f a)- => Sized f (Zero nat) a-empty = coerce $ mempty @(f a)-{-# INLINE empty #-}---- | Sequence with one element.------ Since 0.7.0.0-singleton :: forall nat f a. (CPointed f, Dom f a) => a -> Sized f (One nat) a-singleton = coerce $ cpure @f @a-{-# INLINE singleton #-}---- | Consruct the 'Sized' sequence from base type, but--- the length parameter is dynamically determined and--- existentially quantified; see also 'SomeSized''.------ Since 0.7.0.0-toSomeSized- :: forall nat f a. (HasOrdinal nat, Dom f a, CFoldable f)- => f a -> SomeSized' f nat a-toSomeSized = \xs ->- case fromNatural $ P.fromIntegral $ clength xs of- SomeSing sn -> withSingI sn $ SomeSized' sn $ unsafeToSized sn xs---- | Replicates the same value.------ Since 0.7.0.0-replicate :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sing n -> a -> Sized f n a-replicate = coerce $ creplicate @f @a . P.fromIntegral . toNatural @nat @n-{-# INLINE replicate #-}---- | 'replicate' with the length inferred.------ Since 0.7.0.0-replicate'- :: forall nat f (n :: nat) a.- (HasOrdinal nat, SingI (n :: nat), CFreeMonoid f, Dom f a)- => a -> Sized f n a-replicate' = withSing replicate-{-# INLINE replicate' #-}---- | Construct a sequence of the given length by applying the function to each index.------ Since 0.7.0.0-generate- :: forall (nat :: Type) f (n :: nat) (a :: Type).- (CFreeMonoid f, Dom f a, HasOrdinal nat)- => Sing n -> (Ordinal n -> a) -> Sized f n a-generate = coerce $ \sn -> withSingI sn $- cgenerate @f @a (P.fromIntegral $ toNatural @nat @n sn)- . (. toEnum @(Ordinal n))-{-# INLINE [1] generate #-}---- | 'generate' with length inferred.------ Since 0.8.0.0-generate'- :: forall (nat :: Type) f (n :: nat) (a :: Type).- (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat)- => (Ordinal n -> a) -> Sized f n a-generate' = generate sing-{-# 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.8.0.0-cons- :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a)- => a -> Sized f n a -> Sized f (One nat + n) a-cons = coerce $ ccons @f @a-{-# INLINE cons #-}---- | Infix version of 'cons'.------ Since 0.8.0.0-(<|)- :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a)- => a -> Sized f n a -> Sized f (One nat + n) a-(<|) = cons-{-# INLINE (<|) #-}-infixr 5 <|---- | Append an element to the tail of sequence.------ Since 0.7.0.0-snoc- :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a)- => Sized f n a -> a -> Sized f (n + One nat) a-snoc (Sized xs) a = Sized $ csnoc xs a-{-# INLINE snoc #-}---- | Infix version of 'snoc'.------ Since 0.7.0.0-(|>) :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a-(|>) = snoc-{-# INLINE (|>) #-}-infixl 5 |>---- | Append two lists.------ Since 0.7.0.0-append- :: forall nat f (n :: nat) (m :: nat) a.- (CFreeMonoid f, Dom f a)- => Sized f n a -> Sized f m a -> Sized f (n + m) a-append = coerce $ mappend @(f a)-{-# INLINE append #-}---- | Infix version of 'append'.------ Since 0.7.0.0-(++)- :: forall nat f (n :: nat) (m :: nat) a.- (CFreeMonoid f, Dom f a)- => Sized f n a -> Sized f m a -> Sized f (n + m) a-(++) = append-infixr 5 ++---- | Concatenates multiple sequences into one.------ Since 0.7.0.0-concat :: forall nat f' (m :: nat) f (n :: nat) a.- (CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a),- Dom f' (Sized f n a)- )- => Sized f' m (Sized f n a) -> Sized f (m * n) a-concat = coerce $ cfoldMap @f' @(Sized f n a) runSized-{-# INLINE [2] concat #-}-------------------------------------------------------------------------------------- Zips------------------------------------------------------------------------------------- | Zipping two sequences. Length is adjusted to shorter one.------ Since 0.7.0.0-zip- :: forall nat f (n :: nat) a (m :: nat) b.- (Dom f a, CZip f, Dom f b, Dom f (a, b))- => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)-zip = coerce $ czip @f @a @b---- | 'zip' for the sequences of the same length.------ Since 0.7.0.0-zipSame- :: forall nat f (n :: nat) a b.- (Dom f a, CZip f, Dom f b, Dom f (a, b))- => Sized f n a -> Sized f n b -> Sized f n (a, b)-zipSame = coerce $ czip @f @a @b-{-# INLINE [1] zipSame #-}---- | Zipping two sequences with funtion. Length is adjusted to shorter one.------ Since 0.7.0.0-zipWith- :: forall nat f (n :: nat) a (m :: nat) b c.- (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c)- => (a -> b -> c)- -> Sized f n a- -> Sized f m b- -> Sized f (Min n m) c-zipWith = coerce $ czipWith @f @a @b @c-{-# INLINE [1] zipWith #-}---- | 'zipWith' for the sequences of the same length.------ Since 0.7.0.0-zipWithSame- :: forall nat f (n :: nat) a b c.- (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c)- => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c-zipWithSame = coerce $ czipWith @f @a @b @c-{-# INLINE [1] zipWithSame #-}---- | Unzipping the sequence of tuples.------ Since 0.7.0.0-unzip- :: forall nat f (n :: nat) a b.- (CUnzip f, Dom f a, Dom f b, Dom f (a, b))- => Sized f n (a, b) -> (Sized f n a, Sized f n b)-unzip = coerce $ cunzip @f @a @b-{-# INLINE unzip #-}---- | Unzipping the sequence of tuples.------ Since 0.7.0.0-unzipWith- :: forall nat f (n :: nat) a b c.- (CUnzip f, Dom f a, Dom f b, Dom f c)- => (a -> (b, c))- -> Sized f n a -> (Sized f n b, Sized f n c)-unzipWith = coerce $ cunzipWith @f @a @b @c-{-# INLINE unzipWith #-}------------------------------------------------------------------------------------- Transformation------------------------------------------------------------------------------------- | Map function.------ Since 0.7.0.0-map- :: forall nat f (n :: nat) a b.- (CFreeMonoid f, Dom f a, Dom f b)- => (a -> b) -> Sized f n a -> Sized f n b-map f = Sized . cmap f . runSized-{-# INLINE map #-}---- | Reverse function.------ Since 0.7.0.0-reverse- :: forall nat f (n :: nat) a.- (Dom f a, CFreeMonoid f)- => Sized f n a -> Sized f n a-reverse = coerce $ creverse @f @a-{-# INLINE reverse #-}---- | Intersperces.------ Since 0.7.0.0-intersperse- :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a)- => a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a-intersperse = coerce $ cintersperse @f @a-{-# INLINE intersperse #-}---- | Remove all duplicates.------ Since 0.7.0.0-nub- :: forall nat f (n :: nat) a.- (HasOrdinal nat, Dom f a, Eq a, CFreeMonoid f)- => Sized f n a -> SomeSized' f nat a-nub = toSomeSized . coerce (cnub @f @a)---- | Sorting sequence by ascending order.------ Since 0.7.0.0-sort :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a, Ord a)- => Sized f n a -> Sized f n a-sort = coerce $ csort @f @a---- | Generalized version of 'sort'.------ Since 0.7.0.0-sortBy- :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a)- => (a -> a -> Ordering) -> Sized f n a -> Sized f n a-sortBy = coerce $ csortBy @f @a---- | Insert new element into the presorted sequence.------ Since 0.7.0.0-insert- :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a, Ord a)- => a -> Sized f n a -> Sized f (Succ n) a-insert = coerce $ cinsert @f @a---- | Generalized version of 'insert'.------ Since 0.7.0.0-insertBy- :: forall nat f (n :: nat) a.- (CFreeMonoid f, Dom f a)- => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a-insertBy = coerce $ cinsertBy @f @a------------------------------------------------------------------------------------- Conversion----------------------------------------------------------------------------------------------------------------------------------------------------------------------- List------------------------------------------------------------------------------------- | Convert to list.------ Since 0.7.0.0-toList- :: forall nat f (n :: nat) a.- (CFoldable f, Dom f a)- => Sized f n a -> [a]-toList = coerce $ ctoList @f @a-{-# INLINE [2] toList #-}--{-# RULES-"toList/List"- Data.Sized.toList = runSized- #-}---- | If the given list is shorter than @n@, then returns @Nothing@--- Otherwise returns @Sized f n a@ consisting of initial @n@ element--- of given list.------ Since 0.7.0.0 (type changed)-fromList- :: forall nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sing n -> [a] -> Maybe (Sized f n a)-fromList Zero _ = Just $ Sized (mempty :: f a)-fromList sn xs =- let len = P.fromIntegral $ toNatural sn- in if P.length xs < len- then Nothing- else Just $ Sized $ ctake len $ cfromList xs-{-# INLINABLE [2] fromList #-}---- | 'fromList' with the result length inferred.------ Since 0.7.0.0-fromList'- :: forall nat f (n :: nat) a.- (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n)- => [a] -> Maybe (Sized f n a)-fromList' = withSing fromList-{-# INLINE fromList' #-}---- | Unsafe version of 'fromList'. If the length of the given list does not--- equal to @n@, then something unusual happens.------ Since 0.7.0.0-unsafeFromList- :: forall (nat :: Type) f (n :: nat) a.- (CFreeMonoid f, Dom f a)- => Sing n -> [a] -> Sized f n a-unsafeFromList = const $ coerce $ cfromList @f @a-{-# INLINE [1] unsafeFromList #-}---- | 'unsafeFromList' with the result length inferred.------ Since 0.7.0.0-unsafeFromList'- :: forall nat f (n :: nat) a.- (SingI n, CFreeMonoid f, Dom f a)- => [a] -> Sized f n a-unsafeFromList' = withSing unsafeFromList-{-# INLINE [1] unsafeFromList' #-}-{-# RULES-"unsafeFromList'/List" [~1]- unsafeFromList' = Sized-"unsafeFromList'/Vector" [~1]- unsafeFromList' = Sized . V.fromList-"unsafeFromList'/Seq" [~1]- unsafeFromList' = Sized . Seq.fromList-"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]).- unsafeFromList' xs = Sized (SV.fromList xs)-"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]).- unsafeFromList' xs = Sized (UV.fromList xs)- #-}---- | Construct a @Sized f n a@ by padding default value if the given list is short.------ Since 0.5.0.0 (type changed)-fromListWithDefault- :: forall nat f (n :: nat) a.- (HasOrdinal nat, Dom f a, CFreeMonoid f)- => Sing n -> a -> [a] -> Sized f n a-fromListWithDefault sn def xs =- let len = P.fromIntegral $ toNatural sn- in Sized $ cfromList (ctake len xs) <>- creplicate (len - clength xs) def-{-# INLINABLE fromListWithDefault #-}---- | 'fromListWithDefault' with the result length inferred.------ Since 0.7.0.0-fromListWithDefault'- :: forall nat f (n :: nat) a. (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a)- => a -> [a] -> Sized f n a-fromListWithDefault' = withSing fromListWithDefault-{-# INLINE fromListWithDefault' #-}-------------------------------------------------------------------------------------- Base containes------------------------------------------------------------------------------------- | Forget the length and obtain the wrapped base container.------ Since 0.7.0.0-unsized :: forall nat f (n :: nat) a. Sized f n a -> f a-unsized = runSized-{-# INLINE unsized #-}---- | If the length of the input is shorter than @n@, then returns @Nothing@.--- Otherwise returns @Sized f n a@ consisting of initial @n@ element--- of the input.------ Since 0.7.0.0-toSized- :: forall nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sing (n :: nat) -> f a -> Maybe (Sized f n a)-toSized sn xs =- let len = P.fromIntegral $ toNatural sn- in if clength xs < len- then Nothing- else Just $ unsafeToSized sn $ ctake len xs-{-# INLINABLE [2] toSized #-}---- | 'toSized' with the result length inferred.------ Since 0.7.0.0-toSized'- :: forall nat f (n :: nat) a.- (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n)- => f a -> Maybe (Sized f n a)-toSized' = withSing toSized-{-# INLINE toSized' #-}---- | Unsafe version of 'toSized'. If the length of the given list does not--- equal to @n@, then something unusual happens.------ Since 0.7.0.0-unsafeToSized :: forall nat f (n :: nat) a. Sing n -> f a -> Sized f n a-unsafeToSized _ = Sized-{-# INLINE [2] unsafeToSized #-}---- | 'unsafeToSized' with the result length inferred.------ Since 0.7.0.0-unsafeToSized'- :: forall nat f (n :: nat) a.- (SingI n, Dom f a)- => f a -> Sized f n a-unsafeToSized' = withSing unsafeToSized-{-# INLINE unsafeToSized' #-}---- | Construct a @Sized f n a@ by padding default value if the given list is short.------ Since 0.7.0.0-toSizedWithDefault- :: forall nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => Sing (n :: nat) -> a -> f a -> Sized f n a-toSizedWithDefault sn def xs =- let len = P.fromIntegral $ toNatural sn- in Sized $ ctake len xs <> creplicate (len - clength xs) def-{-# INLINABLE toSizedWithDefault #-}---- | 'toSizedWithDefault' with the result length inferred.------ Since 0.7.0.0-toSizedWithDefault'- :: forall nat f (n :: nat) a.- (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a)- => a -> f a -> Sized f n a-toSizedWithDefault' = withSing toSizedWithDefault-{-# INLINE toSizedWithDefault' #-}-------------------------------------------------------------------------------------- Querying----------------------------------------------------------------------------------------------------------------------------------------------------------------------- Partitioning------------------------------------------------------------------------------------- | The type @Partitioned f n a@ represents partitioned sequence of length @n@.--- Value @Partitioned lenL ls lenR rs@ stands for:------ * Entire sequence is divided into @ls@ and @rs@, and their length--- are @lenL@ and @lenR@ resp.------ * @lenL + lenR = n@------ Since 0.7.0.0-data Partitioned f n a where- Partitioned :: (Dom f a)- => Sing n- -> Sized f n a- -> Sing m- -> Sized f m a- -> Partitioned f (n + m) a---- | Take the initial segment as long as elements satisfys the predicate.------ Since 0.7.0.0-takeWhile- :: forall nat f (n :: nat) a.- (HasOrdinal nat, Dom f a, CFreeMonoid f)- => (a -> Bool) -> Sized f n a -> SomeSized' f nat a-takeWhile = (toSomeSized .) . coerce (ctakeWhile @f @a)-{-# INLINE takeWhile #-}---- | Drop the initial segment as long as elements satisfys the predicate.------ Since 0.7.0.0-dropWhile- :: forall nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => (a -> Bool) -> Sized f n a -> SomeSized' f nat a-dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a)-{-# INLINE dropWhile #-}---- | Split the sequence into the longest prefix--- of elements that satisfy the predicate--- and the rest.------ Since 0.7.0.0-span- :: forall nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => (a -> Bool) -> Sized f n a -> Partitioned f n a-span = (unsafePartitioned @nat @n .) . coerce (cspan @f @a)-{-# INLINE span #-}---- | 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 nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => (a -> Bool) -> Sized f n a -> Partitioned f n a-break = (unsafePartitioned @nat @n .) . coerce (cbreak @f @a)-{-# INLINE break #-}---- | 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 nat f (n :: nat) a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => (a -> Bool) -> Sized f n a -> Partitioned f n a-partition = (unsafePartitioned @nat @n .) . coerce (cpartition @f @a)-{-# INLINE partition #-}--unsafePartitioned- :: forall nat (n :: nat) f a.- (HasOrdinal nat, CFreeMonoid f, Dom f a)- => (f a, f a) -> Partitioned f n a-unsafePartitioned (l, r) =- case (toSomeSized @nat l, toSomeSized @nat r) of- ( SomeSized' (lenL :: Sing nl) ls,- SomeSized' (lenR :: Sing nr) rs- ) ->- gcastWith- (unsafeCoerce $ Refl @()- :: n :~: nl + nr- )- $ Partitioned lenL ls lenR rs-------------------------------------------------------------------------------------- Searching------------------------------------------------------------------------------------ | Membership test; see also 'notElem'.------ Since 0.7.0.0-elem- :: forall nat f (n :: nat) a.- (CFoldable f, Dom f a, Eq a)- => a -> Sized f n a -> Bool-elem = coerce $ celem @f @a-{-# INLINE elem #-}---- | Negation of 'elem'.------ Since 0.7.0.0-notElem- :: forall nat f (n :: nat) a.- (CFoldable f, Dom f a, Eq a)- => a -> Sized f n a -> Bool-notElem = coerce $ cnotElem @f @a-{-# INLINE notElem #-}---- | Find the element satisfying the predicate.------ Since 0.7.0.0-find- :: forall nat f (n :: nat) a.- (CFoldable f, Dom f a)- => (a -> Bool) -> Sized f n a -> Maybe a-find = coerce $ cfind @f @a-{-# INLINE[1] find #-}-{-# RULES-"find/List" [~1] forall p.- find p = L.find @[] p . runSized-"find/Vector" [~1] forall p.- find p = V.find p . runSized-"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool).- find p = SV.find p . runSized-"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool).- find p = UV.find p . runSized- #-}---- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.------ Since 0.7.0.0-findIndex- :: forall nat f (n :: nat) a .- (CFoldable f, Dom f a)- => (a -> Bool) -> Sized f n a -> Maybe Int-findIndex = coerce $ cfindIndex @f @a-{-# INLINE findIndex #-}---- | 'Ordinal' version of 'findIndex'.------ Since 0.7.0.0-sFindIndex- :: forall nat f (n :: nat) a .- (SingI (n :: nat), CFoldable f, Dom f a, HasOrdinal nat)- => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)-sFindIndex = (fmap toEnum .) . coerce (cfindIndex @f @a)-{-# INLINE sFindIndex #-}---- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.------ Since 0.7.0.0-findIndices- :: forall nat f (n :: nat) a .- (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> [Int]-findIndices = coerce $ cfindIndices @f @a-{-# INLINE findIndices #-}-{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}---- | 'Ordinal' version of 'findIndices'.------ Since 0.7.0.0-sFindIndices- :: forall nat f (n :: nat) a .- (HasOrdinal nat, CFoldable f, Dom f a, SingI (n :: nat))- => (a -> Bool) -> Sized f n a -> [Ordinal n]-sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p-{-# INLINE sFindIndices #-}---{-# RULES-"Foldable.sum/Vector"- F.sum = V.sum . runSized- #-}---- | Returns the index of the given element in the list, if exists.------ Since 0.7.0.0-elemIndex :: forall nat f (n :: nat) a .- (CFoldable f, Eq a, Dom f a) => a -> Sized f n a -> Maybe Int-elemIndex = coerce $ celemIndex @f @a-{-# INLINE elemIndex #-}---- | Ordinal version of 'elemIndex'.--- Since 0.7.0.0, we no longer do boundary check inside the definition.------ Since 0.7.0.0-sElemIndex, sUnsafeElemIndex :: forall nat f (n :: nat) a.- (SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat)- => a -> Sized f n a -> Maybe (Ordinal n)-sElemIndex = (fmap toEnum .) . coerce (celemIndex @f @a)-{-# INLINE sElemIndex #-}---- | Since 0.5.0.0 (type changed)-sUnsafeElemIndex = sElemIndex-{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-}---- | Returns all indices of the given element in the list.------ Since 0.7.0.0-elemIndices- :: forall nat f (n :: nat) a .- (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> [Int]-elemIndices = coerce $ celemIndices @f @a-{-# INLINE elemIndices #-}---- | Ordinal version of 'elemIndices'------ Since 0.7.0.0-sElemIndices- :: forall nat f (n :: nat) a .- (CFoldable f, HasOrdinal nat, SingI (n :: nat), Dom f a, Eq a)- => a -> Sized f n a -> [Ordinal n]-sElemIndices = (fmap toEnum .) . elemIndices-{-# INLINE sElemIndices #-}------------------------------------------------------------------------------------- Views and Patterns-----------------------------------------------------------------------------------{-$ViewsAndPatterns #ViewsAndPatterns#-- With GHC's @ViewPatterns@ and @PatternSynonym@ extensions,- we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor.- Curretnly, there are two direction view and patterns: Cons and Snoc.- Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead'- (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on- cons (resp. snoc) of @Sized f n a@ in O(1).--}--{-$views #views#-- With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:--@-slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n-slen ('viewCons' -> 'NilCV') = 'SZ'-slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)-slen _ = error "impossible"-@-- The constraint @('SingI' n, 'Dom f a' f)@ is needed for view function.- In the above, we have extra wildcard pattern (@_@) at the last.- Code compiles if we removed it, but current GHC warns for incomplete pattern,- although we know first two patterns exhausts all the case.-- Equivalently, we can use snoc-style pattern-matching:--@-slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n-slen ('viewSnoc' -> 'NilSV') = 'SZ'-slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as)-@--}---- | View of the left end of sequence (cons-side).------ Since 0.7.0.0-data ConsView f n a where- NilCV :: ConsView f (Zero nat) a- (:-)- :: (SingI n, SingI (One nat + n))- => a -> Sized f n a -> ConsView f (One nat + n) a--infixr 5 :----- | Case analysis for the cons-side of sequence.------ Since 0.5.0.0 (type changed)-viewCons :: forall nat f (n :: nat) a .- (HasOrdinal nat, SingI n, CFreeMonoid f,Dom f a)- => Sized f n a- -> ConsView f n a-viewCons sz = case zeroOrSucc $ sing @n of- IsZero -> NilCV- IsSucc n' ->- withSingI n'- $ withSingI (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 (Zero nat) a- (:-::) :: SingI (n :: nat) => Sized f n a -> a -> SnocView f (n + One nat) a-infixl 5 :-::---- | Case analysis for the snoc-side of sequence.------ Since 0.5.0.0 (type changed)-viewSnoc :: forall nat f (n :: nat) a.- (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a)- => Sized f n a- -> SnocView f n a-viewSnoc sz = case zeroOrSucc (sing @n) of- IsZero -> NilSV- IsSucc (n' :: Sing n') ->- withSingI n' $- gcastWith (succAndPlusOneR n') $- case unsnoc' n' sz of- Unsnoc (xs :: Sized f m a) a ->- gcastWith- (unsafeCoerce (Refl @()) :: n' :~: m)- $ xs :-:: a--{-$patterns #patterns#-- So we can pattern match on both end of sequence via views, but- it is rather clumsy to nest it. For example:--@-nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a-nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a-@-- In such a case, with @PatternSynonyms@ extension we can write as follows:--@-nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a-nextToHead (_ ':<' a ':<' _) = a-@-- Of course, we can also rewrite above @slen@ example using @PatternSynonyms@:--@-slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n-slen '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 nat (f :: Type -> Type) a (n :: nat).- (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)- => forall (n1 :: nat). (n ~ (One nat + n1), SingI n1)- => a -> Sized f n1 a -> Sized f n a-pattern a :< as <- (viewCons -> a :- as) where- a :< as = a <| as--chkNil- :: forall nat f (n :: nat) a.- (IsPeano nat, SingI n)- => Sized f n a -> ZeroOrSucc n-chkNil = const $ zeroOrSucc $ sing @n---- | Pattern synonym for a nil sequence.-pattern Nil :: forall nat f (n :: nat) a.- (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat)- => (n ~ Zero nat) => Sized f n a-pattern Nil <- (chkNil -> IsZero) where- Nil = empty--infixl 5 :>---- | Pattern synonym for snoc-side unsnoc.-pattern (:>)- :: forall nat (f :: Type -> Type) a (n :: nat).- (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)- => forall (n1 :: nat). (n ~ (n1 + One nat), SingI n1)- => Sized f n1 a -> a -> Sized f n a-pattern a :> b <- (viewSnoc -> a :-:: b) where- a :> b = a |> b--{-# 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,- HasOrdinal nat, SingI n, forall a. DomC f a)- => P.Applicative (Sized f (n :: nat)) where- {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-}- {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-}- {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.Nat)) #-}-- pure (x :: a) = withDict (Dict @(DomC f a))- $ replicate' x- {-# INLINE pure #-}-- (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) =- withDict (Dict @(DomC f b))- $ withDict (Dict @(DomC f a))- $ withDict (Dict @(DomC f (a -> b)))- $ zipWithSame ($) fs xs- {-# INLINE [1] (<*>) #-}-{-# RULES-"<*>/List" [~1] forall fs xs.- Sized fs <*> Sized xs = Sized (getZipList (ZipList fs <*> ZipList xs))-"<*>/Seq" [~1] forall fs xs.- Sized fs <*> Sized xs = Sized (Seq.zipWith ($) fs xs)-"<*>/Vector" [~1] forall fs xs.- Sized fs <*> Sized xs = Sized (V.zipWith ($) fs xs)- #-}--instance (CFreeMonoid f, PeanoOrder nat, SingI (n :: nat))- => CPointed (Sized f n) where- cpure = replicate'--instance (CFreeMonoid f, CZip f)- => CApplicative (Sized f n) where- pair = zipSame- (<.>) = zipWithSame ($)- (<.) = P.const- (.>) = P.flip P.const---- | __N.B.__ Since @calign@ is just zipping for fixed @n@,--- we require more strong 'CZip' constraint here.-instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where- calignWith = coerce (\f -> czipWith @f @a @b @c ((f .) . These))- :: forall a b c.- (Dom f a, Dom f b, Dom f c)- => (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c- {-# INLINE [1] calignWith #-}- calign = coerce $ czipWith @f @a @b These- :: forall a b.- (Dom f a, Dom f b, Dom f (These a b))- => Sized f n a -> Sized f n b -> Sized f n (These a b)- {-# INLINE [1] calign #-}--instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where- czipWith = coerce $ czipWith @f @a @b @c- :: forall a b c.- (Dom f a, Dom f b, Dom f c)- => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c- {-# INLINE [1] czipWith #-}- czip = coerce $ czip @f @a @b- :: forall a b.- (Dom f a, Dom f b, Dom f (a, b))- => Sized f n a -> Sized f n b -> Sized f n (a, b)- {-# INLINE [1] czip #-}--instance- (PeanoOrder nat, SingI (n :: nat), CZip f, CFreeMonoid f)- => CRepeat (Sized f n) where+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE LiberalTypeSynonyms #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# 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 GHC.TypeLits.Presburger #-}++{- | 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 $ toNatural $ 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 . toNatural @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 . toNatural @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 . toNatural @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 . toNatural @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 . toNatural @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 . toNatural @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 $ toNatural @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 $ toNatural 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 $ toNatural 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 $ toNatural 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 $ toNatural 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 $ toNatural 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 $ toNatural 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 $ toNatural 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 $ toNatural 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 #-}
src/Data/Sized/Builtin.hs view
@@ -1,1005 +1,4 @@-{-# LANGUAGE CPP, ConstraintKinds, DataKinds, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude #-}-{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, TypeApplications #-}-{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}--- | This module exports provides the functionality to make length-parametrized types--- from existing 'CFreeMonoid' sequential types,--- parametrised with GHC's built in 'Nat' kind.------ Most of the complexity of operations on @'Sized' f n a@ are the same as--- original operations on @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.Builtin- ( -- * Main Data-types- Sized(), SomeSized, pattern SomeSized, Ordinal,- DomC(),- -- * Accessors- -- ** Length information- length, sLength, null,- -- ** Indexing- (!!), (%!!), index, sIndex, head, last,- uncons, uncons', Uncons, pattern Uncons,- unsnoc, unsnoc', Unsnoc, pattern Unsnoc,- -- ** Slicing- tail, init, take, takeAtMost, drop, splitAt, splitAtMost,- -- * Construction- -- ** Initialisation- empty, singleton, toSomeSized, replicate, replicate', generate, generate',- -- ** Concatenation- cons, (<|), snoc, (|>), append, (++), concat,- -- ** Zips- zip, zipSame, zipWith, zipWithSame, unzip, unzipWith,- -- * Transformation- map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,- -- * Conversion- -- ** List- toList, fromList, fromList', unsafeFromList, unsafeFromList',- fromListWithDefault, fromListWithDefault',- -- ** Base container- unsized,- toSized, toSized', unsafeToSized, unsafeToSized',- toSizedWithDefault, toSizedWithDefault',- -- * Querying- -- ** Partitioning- Partitioned(), pattern Partitioned,- takeWhile, dropWhile, span, break, partition,- -- ** Searching- elem, notElem, find, findIndex, sFindIndex,- findIndices, sFindIndices,- elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,- -- * Views and Patterns- -- $ViewsAndPatterns-- -- ** Views- -- $views-- -- ** Patterns- -- $patterns-- -- ** Definitions- viewCons, ConsView,- pattern (:-), pattern NilCV,- viewSnoc, SnocView,- pattern (:-::), pattern NilSV,-- pattern Nil, pattern (:<), pattern (:>),- ) where-import Data.Sized (DomC)-import qualified Data.Sized as S--import Control.Subcategory-import Data.Coerce (coerce)-import Data.Kind (Type)-import Data.Maybe (fromJust)-import Data.Singletons.Prelude (SNum ((%+)), SingI (sing))-import Data.Singletons.Prelude.Enum (PEnum (..))-import Data.Singletons.TypeLits (SNat, withKnownNat)-import qualified Data.Sized.Internal as Internal-import Data.Type.Natural (IsPeano (toNatural, zeroOrSucc),- Min, PeanoOrder (plusMonotoneR))-import Data.Type.Natural.Class (ZeroOrSucc (IsSucc, IsZero),- type (-.))-import qualified Data.Type.Ordinal as O-import GHC.TypeNats (KnownNat, Nat, type (*),- type (+), type (-), type (<=))-import Prelude (Bool (..), Eq, Int, Maybe,- Monoid, Ord, Ordering, const,- uncurry, ($), (.))-import qualified Prelude as P-import Proof.Propositional (IsTrue (Witness), withWitness)--type Ordinal = (O.Ordinal :: Nat -> Type)-type a < b = a + 1 <= b---- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.------ Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@.------ Since 0.2.0.0-type Sized = (Internal.Sized :: (Type -> Type) -> Nat -> Type -> Type)---- | 'Sized' sequence 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-type SomeSized f a = S.SomeSized' f Nat a--pattern SomeSized- :: forall (f :: Type -> Type) a. ()- => forall (n :: Nat). SNat n- -> Sized f n a -> SomeSized f a-{-# COMPLETE SomeSized #-}-pattern SomeSized n s = S.SomeSized' n s---- | 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)-{-# INLINE length #-}-length :: (Dom f a, KnownNat n) => Sized f n a -> Int-length = S.length @Nat---- | @Sing@ version of 'length'.------ Since 0.8.0.0 (type changed)-sLength :: (Dom f a, KnownNat n) => Sized f n a -> SNat n-{-# INLINE sLength #-}-sLength = S.sLength @Nat---- | Test if the sequence is empty or not.------ Since 0.7.0.0-null :: (Dom f a, CFoldable f) => Sized f n a -> Bool-{-# INLINE null #-}-null = S.null @Nat-------------------------------------------------------------------------------------- Indexing------------------------------------------------------------------------------------- | (Unsafe) indexing with @Int@s.--- If you want to check boundary statically, use '%!!' or 'sIndex'.------ Since 0.7.0.0-(!!) :: forall f m a. (Dom f a, CFoldable f, (1 <= m)) => Sized f m a -> Int -> a-{-# INLINE (!!) #-}-(!!) = coerce $ cindex @f @a---- | Safe indexing with 'Ordinal's.------ Since 0.7.0.0-(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c-{-# INLINE (%!!) #-}-(%!!) = (S.%!!) @Nat---- | Flipped version of '!!'.------ Since 0.7.0.0-index- :: (Dom f a, CFoldable f, (1 <= m))- => Int -> Sized f m a -> a-{-# INLINE index #-}-index = P.flip (!!)---- | Flipped version of '%!!'.------ Since 0.7.0.0-sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c-{-# INLINE sIndex #-}-sIndex = S.sIndex @Nat---- | 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 a. (Dom f a, CFoldable f, (1 <= n)) => Sized f n a -> a-{-# INLINE head #-}-head = coerce $ chead @f @a---- | 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 a. (Dom f a, CFoldable f, (0 < n)) => Sized f n a -> a-{-# INLINE last #-}-last = coerce $ clast @f @a---- | 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 a.- (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))- => Sized f n a -> Uncons f n a-{-# INLINE uncons #-}-uncons =- uncurry (Uncons @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a)---- | 'uncons' with explicit specified length @n@------ Since 0.7.0.0-uncons'- :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))- => Sized f n a- -> Uncons f n a-{-# INLINE uncons' #-}-uncons' = 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.7.0.0-unsnoc- :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))- => Sized f n a -> Unsnoc f n a-{-# INLINE unsnoc #-}-unsnoc = P.undefined---- | 'unsnoc'' with explicit specified length @n@------ Since 0.7.0.0-unsnoc' :: (Dom f a, KnownNat n, CFreeMonoid f) => proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) a-{-# INLINE unsnoc' #-}-unsnoc' = S.unsnoc' @Nat--data Uncons f n a where- Uncons :: forall f n a. KnownNat n- => a -> Sized f n a -> Uncons f (1 + n) a---type Unsnoc f (n :: Nat) a = S.Unsnoc f n a--pattern Unsnoc- :: forall (f :: Type -> Type) (n :: Nat) a. ()- => forall (n1 :: Nat). (n ~ Succ n1)- => Sized f n1 a -> a -> Unsnoc f n a-pattern Unsnoc xs x = S.Unsnoc xs x---- | 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 :: (Dom f a, CFreeMonoid f) => Sized f (1 + n) a -> Sized f n a-{-# INLINE tail #-}-tail = S.tail @Nat---- | 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 :: (Dom f a, CFreeMonoid f) => Sized f (n + 1) a -> Sized f n a-{-# INLINE init #-}-init = S.init @Nat---- | @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 f m a. (Dom f a, CFreeMonoid f, (n <= m))- => SNat n -> Sized f m a -> Sized f n a-{-# INLINE take #-}-take = coerce $ ctake @f @a . P.fromIntegral . toNatural @Nat @n---- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.------ Since 0.7.0.0-takeAtMost- :: (Dom f a, CFreeMonoid f)- => SNat n -> Sized f m a -> Sized f (Min n m) a-{-# INLINE takeAtMost #-}-takeAtMost = S.takeAtMost @Nat---- | @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 f m a. (Dom f a, CFreeMonoid f, (n <= m))- => SNat n -> Sized f m a -> Sized f (m - n) a-{-# INLINE drop #-}-drop = coerce $ cdrop @f @a . P.fromIntegral . toNatural @Nat @n---- | @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 f m a. (Dom f a, CFreeMonoid f, (n <= m))- => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)-{-# INLINE splitAt #-}-splitAt = coerce $ csplitAt @f @a . P.fromIntegral . toNatural @Nat---- | @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- :: (Dom f a, CFreeMonoid f)- => SNat n -> Sized f m a- -> (Sized f (Min n m) a, Sized f (m -. n) a)-{-# INLINE splitAtMost #-}-splitAtMost = S.splitAtMost @Nat------------------------------------------------------------------------------------- Construction----------------------------------------------------------------------------------------------------------------------------------------------------------------------- Initialisation------------------------------------------------------------------------------------- | Empty sequence.------ Since 0.7.0.0 (type changed)-empty :: (Dom f a, Monoid (f a)) => Sized f 0 a-{-# INLINE empty #-}-empty = S.empty @Nat---- | Sequence with one element.------ Since 0.7.0.0-singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f 1 a-{-# INLINE singleton #-}-singleton = S.singleton @Nat----- | 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 :: (Dom f a, CFoldable f) => f a -> SomeSized f a-{-# INLINE toSomeSized #-}-toSomeSized = S.toSomeSized @Nat---- | Replicates the same value.------ Since 0.7.0.0-replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a-{-# INLINE replicate #-}-replicate = S.replicate @Nat---- | 'replicate' with the length inferred.------ Since 0.7.0.0-replicate' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> Sized f n a-{-# INLINE replicate' #-}-replicate' = S.replicate' @Nat---- | Construct a sequence of the given length by applying the function to each index.------ Since 0.7.0.0-generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a-{-# INLINE generate #-}-generate = S.generate @Nat---- | 'generate' with length inferred.------ Since 0.8.0.0-generate'- :: forall f n a. (KnownNat n, Dom f a, CFreeMonoid f) => (Ordinal n -> a) -> Sized f n a-{-# INLINE generate' #-}-generate' = S.generate' @Nat-------------------------------------------------------------------------------------- Concatenation------------------------------------------------------------------------------------- | Append an element to the head of sequence.------ Since 0.7.0.0-cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a-{-# INLINE cons #-}-cons = S.cons @Nat---- | Append an element to the tail of sequence.------ Since 0.7.0.0-snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a-{-# INLINE snoc #-}-snoc = S.snoc @Nat---- | Infix version of 'snoc'.------ Since 0.7.0.0-(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a-{-# INLINE (<|) #-}-(<|) = (S.<|) @Nat---- | Append an element to the tail of sequence.------ Since 0.7.0.0-(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a-{-# INLINE (|>) #-}-(|>) = (S.|>) @Nat---- | Infix version of 'append'.------ Since 0.7.0.0-(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a-{-# INLINE (++) #-}-(++) = (S.++) @Nat---- | Append two lists.------ Since 0.7.0.0-append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a-{-# INLINE append #-}-append = S.append @Nat---- | Concatenates multiple sequences into one.------ Since 0.7.0.0-concat- :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a),- CFreeMonoid f, CFunctor f', CFoldable f'- ) => Sized f' m (Sized f n a) -> Sized f (m * n) a-{-# INLINE concat #-}-concat = S.concat @Nat--------------------------------------------------------------------------------------- Zips------------------------------------------------------------------------------------- | Zipping two sequences. Length is adjusted to shorter one.------ Since 0.7.0.0-zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f)- => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)-{-# INLINE zip #-}-zip = S.zip @Nat---- | 'zip' for the sequences of the same length.------ Since 0.7.0.0-zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f)- => Sized f n a -> Sized f n b -> Sized f n (a, b)-{-# INLINE zipSame #-}-zipSame = S.zipSame @Nat---- | Zipping two sequences with funtion. Length is adjusted to shorter one.------ Since 0.7.0.0-zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)- => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c-{-# INLINE zipWith #-}-zipWith = S.zipWith @Nat---- | 'zipWith' for the sequences of the same length.------ Since 0.7.0.0-zipWithSame- :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)- => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c-{-# INLINE zipWithSame #-}-zipWithSame = S.zipWithSame @Nat---- | Unzipping the sequence of tuples.------ Since 0.7.0.0-unzip- :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f)- => Sized f n (a, b) -> (Sized f n a, Sized f n b)-{-# INLINE unzip #-}-unzip = S.unzip @Nat---- | Unzipping the sequence of tuples.------ Since 0.7.0.0-unzipWith- :: (Dom f a, Dom f b, Dom f c, CUnzip f)- => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)-{-# INLINE unzipWith #-}-unzipWith = S.unzipWith @Nat------------------------------------------------------------------------------------- Transformation------------------------------------------------------------------------------------- | Map function.------ Since 0.7.0.0-map- :: (Dom f a, Dom f b, CFreeMonoid f)- => (a -> b) -> Sized f n a -> Sized f n b-{-# INLINE map #-}-map = S.map @Nat---- | Reverse function.------ Since 0.7.0.0-reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a-{-# INLINE reverse #-}-reverse = S.reverse @Nat---- | Intersperces.------ Since 0.7.0.0-intersperse- :: (Dom f a, CFreeMonoid f)- => a -> Sized f n a -> Sized f ((2 * n) -. 1) a-{-# INLINE intersperse #-}-intersperse = S.intersperse @Nat---- | Remove all duplicates.------ Since 0.7.0.0-nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a-{-# INLINE nub #-}-nub = S.nub @Nat---- | Sorting sequence by ascending order.------ Since 0.7.0.0-sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a-{-# INLINE sort #-}-sort = S.sort @Nat---- | Generalized version of 'sort'.------ Since 0.7.0.0-sortBy- :: (Dom f a, CFreeMonoid f)- => (a -> a -> Ordering)- -> Sized f n a -> Sized f n a-{-# INLINE sortBy #-}-sortBy = S.sortBy @Nat---- | Insert new element into the presorted sequence.------ Since 0.7.0.0-insert- :: (Dom f a, CFreeMonoid f, Ord a)- => a -> Sized f n a -> Sized f (n + 1) a-{-# INLINE insert #-}-insert = S.insert @Nat---- | Generalized version of 'insert'.------ Since 0.7.0.0-{-# INLINE insertBy #-}-insertBy- :: (Dom f a, CFreeMonoid f)- => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (n + 1) a-insertBy = S.insertBy @Nat------------------------------------------------------------------------------------- Conversion----------------------------------------------------------------------------------------------------------------------------------------------------------------------- List------------------------------------------------------------------------------------- | Convert to list.------ Since 0.7.0.0-{-# INLINE toList #-}-toList :: (Dom f a, CFoldable f) => Sized f n a -> [a]-toList = S.toList @Nat---- | 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)-{-# INLINE fromList #-}-fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a)-fromList = S.fromList @Nat---- | 'fromList' with the result length inferred.------ Since 0.7.0.0-{-# INLINE fromList' #-}-fromList' :: (Dom f a, CFreeMonoid f, KnownNat n) => [a] -> Maybe (Sized f n a)-fromList' = S.fromList' @Nat---- | 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-{-# INLINE unsafeFromList #-}-unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a-unsafeFromList = S.unsafeFromList @Nat---- | 'unsafeFromList' with the result length inferred.------ Since 0.7.0.0-{-# INLINE unsafeFromList' #-}-unsafeFromList' :: (Dom f a, KnownNat n, CFreeMonoid f) => [a] -> Sized f n a-unsafeFromList' = S.unsafeFromList' @Nat---- | Construct a @Sized f n a@ by padding default value if the given list is short.------ Since 0.5.0.0 (type changed)-{-# INLINE fromListWithDefault #-}-fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a-fromListWithDefault = S.fromListWithDefault @Nat---- | 'fromListWithDefault' with the result length inferred.------ Since 0.7.0.0-{-# INLINE fromListWithDefault' #-}-fromListWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f)- => a -> [a] -> Sized f n a-fromListWithDefault' = S.fromListWithDefault' @Nat-------------------------------------------------------------------------------------- Base containes------------------------------------------------------------------------------------- | Forget the length and obtain the wrapped base container.------ Since 0.7.0.0-{-# INLINE unsized #-}-unsized :: Sized f n a -> f a-unsized = S.unsized @Nat---- | 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-{-# INLINE toSized #-}-toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a)-toSized = S.toSized @Nat---- | 'toSized' with the result length inferred.------ Since 0.7.0.0-{-# INLINE toSized' #-}-toSized' :: (Dom f a, CFreeMonoid f, KnownNat n) => f a -> Maybe (Sized f n a)-toSized' = S.toSized' @Nat---- | 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-{-# INLINE unsafeToSized #-}-unsafeToSized :: SNat n -> f a -> Sized f n a-unsafeToSized = S.unsafeToSized @Nat---- | 'unsafeToSized' with the result length inferred.------ Since 0.7.0.0-{-# INLINE unsafeToSized' #-}-unsafeToSized' :: (Dom f a, KnownNat n) => f a -> Sized f n a-unsafeToSized' = S.unsafeToSized' @Nat---- | Construct a @Sized f n a@ by padding default value if the given list is short.------ Since 0.7.0.0-{-# INLINE toSizedWithDefault #-}-toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a-toSizedWithDefault = S.toSizedWithDefault @Nat---- | 'toSizedWithDefault' with the result length inferred.------ Since 0.7.0.0-{-# INLINE toSizedWithDefault' #-}-toSizedWithDefault' :: (Dom f a, KnownNat n, CFreeMonoid f)- => a -> f a -> Sized f n a-toSizedWithDefault' = S.toSizedWithDefault' @Nat------------------------------------------------------------------------------------- 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-type Partitioned f (n :: Nat) a = S.Partitioned f n a--pattern Partitioned- :: forall (f :: Type -> Type) (n :: Nat) a. ()- => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a)- => SNat n1 -> Sized f n1 a -> SNat m- -> Sized f m a -> Partitioned f n a-{-# COMPLETE Partitioned #-}-pattern Partitioned ls l rs r = S.Partitioned ls l rs r---- | Take the initial segment as long as elements satisfys the predicate.------ Since 0.7.0.0-{-# INLINE takeWhile #-}-takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a-takeWhile = S.takeWhile @Nat---- | Drop the initial segment as long as elements satisfys the predicate.------ Since 0.7.0.0-{-# INLINE dropWhile #-}-dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a-dropWhile = S.dropWhile @Nat---- | Split the sequence into the longest prefix--- of elements that satisfy the predicate--- and the rest.------ Since 0.7.0.0-span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a-{-# INLINE span #-}-span = S.span @Nat---- | Split the sequence into the longest prefix--- of elements that do not satisfy the--- predicate and the rest.------ Since 0.7.0.0-{-# INLINE break #-}-break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a-break = S.break @Nat---- | 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-{-# INLINE partition #-}-partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a-partition = S.partition @Nat-------------------------------------------------------------------------------------- Searching------------------------------------------------------------------------------------ | Membership test; see also 'notElem'.------ Since 0.7.0.0-{-# INLINE elem #-}-elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool-elem = S.elem @Nat---- | Negation of 'elem'.------ Since 0.7.0.0-{-# INLINE notElem #-}-notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool-notElem = S.notElem @Nat---- | Find the element satisfying the predicate.------ Since 0.7.0.0-{-# INLINE find #-}-find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a-find = S.find @Nat---- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.------ Since 0.7.0.0-{-# INLINE findIndex #-}-findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int-findIndex = S.findIndex @Nat---- | 'Ordinal' version of 'findIndex'.------ Since 0.7.0.0-{-# INLINE sFindIndex #-}-sFindIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)-sFindIndex = S.sFindIndex @Nat---- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.------ Since 0.7.0.0-{-# INLINE findIndices #-}-findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]-findIndices = S.findIndices @Nat---- | 'Ordinal' version of 'findIndices'.------ Since 0.7.0.0-{-# INLINE sFindIndices #-}-sFindIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n]-sFindIndices = S.sFindIndices @Nat---- | Returns the index of the given element in the list, if exists.------ Since 0.8.0.0-{-# INLINE elemIndex #-}-elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int-elemIndex = S.elemIndex @Nat--sElemIndex, sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)-{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}---- | Ordinal version of 'elemIndex'.--- Since 0.7.0.0, we no longer do boundary check inside the definition.------ Since 0.7.0.0-sUnsafeElemIndex = S.sElemIndex @Nat---- | Ordinal version of 'elemIndex'.--- Since 0.7.0.0, we no longer do boundary check inside the definition.------ Since 0.7.0.0-sElemIndex = S.sElemIndex @Nat---- | Returns all indices of the given element in the list.------ Since 0.8.0.0-{-# INLINE elemIndices #-}-elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int]-elemIndices = S.elemIndices @Nat---- | Ordinal version of 'elemIndices'------ Since 0.8.0.0-{-# INLINE sElemIndices #-}-sElemIndices- :: (Dom f a, CFoldable f, KnownNat n, Eq a)- => a -> Sized f n a -> [Ordinal n]-sElemIndices = S.sElemIndices @Nat------------------------------------------------------------------------------------- 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 -> 'Sing' 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 -> 'Sing' n-slen ('viewSnoc' -> 'NilSV') = 'SZ'-slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as)-@--}----- | View of the left end of sequence (cons-side).------ Since 0.9.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 9 :----- | Case analysis for the cons-side of sequence.------ Since 0.5.0.0 (type changed)-viewCons :: forall f n a. (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a-viewCons sz = case zeroOrSucc $ sing @n of- IsZero -> NilCV- IsSucc n' ->- withWitness (plusMonotoneR (sing @1) (sing @0) n' Witness) $- withKnownNat n'- $ withKnownNat (sing @1 %+ n')- $ case uncons' sz of- Uncons a xs -> a :- xs---- | View of the left end of sequence (snoc-side).------ Since 0.7.0.0-type SnocView =- (S.SnocView :: (Type -> Type) -> Nat -> Type -> Type)---- | Since 0.8.0.0-pattern NilSV- :: forall (f :: Type -> Type) n a. ()- => (n ~ 0)- => SnocView f n a-pattern NilSV = S.NilSV---infixl 9 :-::--- | Since 0.8.0.0-pattern (:-::)- :: forall (f :: Type -> Type) n a. ()- => forall n1. (n ~ (n1 + 1), SingI n1)- => Sized f n1 a -> a -> SnocView f n a-pattern ls :-:: l = ls S.:-:: l-{-# COMPLETE NilSV, (:-::) #-}----- | Case analysis for the snoc-side of sequence.------ Since 0.8.0.0 (type changed)-viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> SnocView f n a-viewSnoc = S.viewSnoc @Nat--{-$patterns #patterns#-- So we can pattern match on both end of sequence via views, but- it is rather clumsy to nest it. For example:--@-nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a-nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a-@-- In such a case, with @PatternSynonyms@ extension we can write as follows:--@-nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a-nextToHead (_ ':<' a ':<' _) = a-@-- Of course, we can also rewrite above @slen@ example using @PatternSynonyms@:--@-slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n-slen '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>.--}---- | 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, KnownNat n)- => a -> Sized f n1 a -> Sized f n a-pattern a :< as <- (viewCons -> a :- as) where- a :< as = a <| as-infixr 5 :<--chkNil- :: forall f n a.- (KnownNat n)- => Sized f n a -> ZeroOrSucc n-chkNil = const $ zeroOrSucc $ sing @n---- | Pattern synonym for a nil sequence.-pattern Nil- :: forall (f :: Type -> Type) n a.- (Dom f a, KnownNat n, CFreeMonoid f)- => (n ~ 0) => Sized f n a-pattern Nil <- (chkNil -> IsZero) where- Nil = empty---- | 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), SingI n1)- => Sized f n1 a -> a -> Sized f n a-pattern a :> b = a S.:> b-infixl 5 :>--{-# COMPLETE (:<), Nil #-}-{-# COMPLETE (:>), Nil #-}+module Data.Sized.Builtin+ {-# DEPRECATED "Use Data.Sized instead" #-}+ ( module Data.Sized ) where+import Data.Sized
src/Data/Sized/Flipped.hs view
@@ -1,47 +1,64 @@-{-# LANGUAGE CPP, ConstraintKinds, DataKinds, DeriveDataTypeable #-}-{-# LANGUAGE DeriveFunctor, DeriveTraversable, EmptyDataDecls #-}-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-}-{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms #-}-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LiberalTypeSynonyms #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+ #if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-} #endif-module Data.Sized.Flipped (Flipped(..)) where-import Data.Sized.Internal+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 (..))-import Data.MonoTraversable (MonoFunctor (..))-import Data.MonoTraversable (MonoTraversable (..))-import qualified Data.Sequence as Seq-import qualified Data.Type.Natural as PN-import Data.Type.Ordinal (HasOrdinal, Ordinal (..))-import Data.Typeable (Typeable)-import qualified Data.Vector as V+import 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+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)+{- | 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 #-}@@ -49,17 +66,19 @@ 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)) #-}+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
@@ -10,34 +10,31 @@ #endif {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.Sized.Internal (Sized(..)) where-import Control.DeepSeq (NFData (..))-import Control.Lens.At (Index, IxValue, Ixed (..))-import Control.Lens.Indexed (FoldableWithIndex (..),- FunctorWithIndex (..),- TraversableWithIndex (..))-import Control.Subcategory (CFoldable, CFunctor, Constrained)-import Data.Hashable (Hashable (..))-import Data.Kind (Type)-import Data.MonoTraversable (Element, MonoFoldable (..),- MonoFunctor (..),- MonoTraversable (..))-import qualified Data.Sequence as Seq-import Data.Singletons.Prelude (SingI)-import qualified Data.Type.Natural as PN-import Data.Type.Ordinal (HasOrdinal, Ordinal (..),- ordToNatural, unsafeNaturalToOrd)-import Data.Typeable (Typeable)-import qualified Data.Vector as V-import qualified Data.Vector.Storable as SV-import qualified Data.Vector.Unboxed as UV-import qualified GHC.TypeLits as TL+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 =+newtype Sized (f :: Type -> Type) (n :: Nat) a = Sized { runSized :: f a } deriving (Eq, Ord, Typeable, Functor, Foldable, Traversable)@@ -86,42 +83,31 @@ -- | 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) #-}+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, HasOrdinal nat, SingI n)- => FunctorWithIndex (Ordinal (n :: nat)) (Sized f n) where+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 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)) #-}+ {-# 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, HasOrdinal nat, SingI n)- => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where+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 #-} @@ -137,34 +123,21 @@ 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)) #-}-+ {-# 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, HasOrdinal nat, SingI n)- => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where+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 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)) #-}+ {-# 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)) #-}
− src/Data/Sized/Peano.hs
@@ -1,1002 +0,0 @@-{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}-{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction, NoStarIsType #-}-{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeApplications #-}-{-# LANGUAGE TypeInType, TypeOperators, ViewPatterns #-}--- | This module exports provides the functionality to make length-parametrized types--- from existing 'CFreeMonoid' sequential types,--- parametrised with peano numeral 'PN.Nat' kind.------ Most of the complexity of operations on @'Sized' f n a@ are the same as--- original operations on @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.Peano {-# DEPRECATED "Removed in future release" #-}- ( -- * Main Data-types- Sized(), SomeSized, pattern SomeSized, Ordinal,- DomC(),- -- * Accessors- -- ** Length information- length, sLength, null,- -- ** Indexing- (!!), (%!!), index, sIndex, head, last,- uncons, uncons', Uncons, pattern Uncons,- unsnoc, unsnoc', Unsnoc, pattern Unsnoc,- -- ** Slicing- tail, init, take, takeAtMost, drop, splitAt, splitAtMost,- -- * Construction- -- ** Initialisation- empty, singleton, toSomeSized, replicate, replicate', generate, generate',- -- ** Concatenation- cons, (<|), snoc, (|>), append, (++), concat,- -- ** Zips- zip, zipSame, zipWith, zipWithSame, unzip, unzipWith,- -- * Transformation- map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,- -- * Conversion- -- ** List- toList, fromList, fromList', unsafeFromList, unsafeFromList',- fromListWithDefault, fromListWithDefault',- -- ** Base container- unsized,- toSized, toSized', unsafeToSized, unsafeToSized',- toSizedWithDefault, toSizedWithDefault',- -- * Querying- -- ** Partitioning- Partitioned(), pattern Partitioned,- takeWhile, dropWhile, span, break, partition,- -- ** Searching- elem, notElem, find, findIndex, sFindIndex,- findIndices, sFindIndices,- elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,- -- * Views and Patterns- -- $ViewsAndPatterns-- -- ** Views- -- $views-- -- ** Patterns- -- $patterns-- -- ** Definitions- viewCons, ConsView,- pattern (:-), pattern NilCV,- viewSnoc, SnocView,- pattern (:-::), pattern NilSV,-- pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR,- ) where-import Data.Sized (DomC)-import qualified Data.Sized as S--import Control.Subcategory-import Data.Kind (Type)-import Data.Singletons.Prelude (POrd ((<=)), SingI)-import Data.Singletons.Prelude.Enum (PEnum (..))-import Data.Type.Natural (Min, Nat (..), One, SNat, Two,- type (*), type (+), type (-))-import Data.Type.Natural.Class (type (-.), type (<))-import qualified Data.Type.Ordinal as O-import Prelude (Bool (..), Eq, Int, Maybe,- Monoid, Ord, Ordering)--type Ordinal = (O.Ordinal :: Nat -> Type)---- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.------ Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@.------ Since 0.2.0.0-type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type)----- | 'Sized' sequence 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-type SomeSized f a = S.SomeSized' f Nat a--pattern SomeSized- :: forall (f :: Type -> Type) a. ()- => forall (n :: Nat). SNat n- -> Sized f n a -> SomeSized f a-{-# COMPLETE SomeSized #-}-pattern SomeSized n s = S.SomeSized' n s---- | 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)-{-# INLINE length #-}-length :: (Dom f a, SingI n) => Sized f n a -> Int-length = S.length @Nat---- | @Sing@ version of 'length'.------ Since 0.8.0.0 (type changed)-{-# INLINE sLength #-}-sLength :: (Dom f a, SingI n) => Sized f n a -> SNat n-sLength = S.sLength @Nat---- | Test if the sequence is empty or not.------ Since 0.7.0.0-{-# INLINE null #-}-null :: (Dom f a, CFoldable f) => Sized f n a -> Bool-null = S.null @Nat-------------------------------------------------------------------------------------- Indexing------------------------------------------------------------------------------------- | (Unsafe) indexing with @Int@s.--- If you want to check boundary statically, use '%!!' or 'sIndex'.------ Since 0.7.0.0-{-# INLINE (!!) #-}-(!!) :: (Dom f a, CFoldable f, (One <= m) ~ 'True) => Sized f m a -> Int -> a-(!!) = (S.!!) @Nat---- | Safe indexing with 'Ordinal's.------ Since 0.7.0.0-{-# INLINE (%!!) #-}-(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c-(%!!) = (S.%!!) @Nat---- | Flipped version of '!!'.------ Since 0.7.0.0-{-# INLINE index #-}-index- :: (Dom f a, CFoldable f, (One <= m) ~ 'True)- => Int -> Sized f m a -> a-index = S.index @Nat---- | Flipped version of '%!!'.------ Since 0.7.0.0-{-# INLINE sIndex #-}-sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c-sIndex = S.sIndex @Nat---- | 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-{-# INLINE head #-}-head :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a-head = S.head @Nat---- | 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-{-# INLINE last #-}-last :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a-last = S.last @Nat---- | 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-{-# INLINE uncons #-}-uncons- :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)- => Sized f n a -> Uncons f n a-uncons = S.uncons @Nat---- | 'uncons' with explicit specified length @n@------ Since 0.7.0.0-{-# INLINE uncons' #-}-uncons'- :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)- => Sized f n a- -> Uncons f n a-uncons' = S.uncons @Nat---- | 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-{-# INLINE unsnoc #-}-unsnoc- :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)- => Sized f n a -> Unsnoc f n a-unsnoc = S.unsnoc @Nat---- | 'unsnoc'' with explicit specified length @n@------ Since 0.7.0.0-{-# INLINE unsnoc' #-}-unsnoc' :: (Dom f a, SingI n, CFreeMonoid f) => proxy n -> Sized f ('S n) a -> Unsnoc f ('S n) a-unsnoc' = S.unsnoc' @Nat--type Uncons f (n :: Nat) a = S.Uncons f n a-pattern Uncons- :: forall (f :: Type -> Type) (n :: Nat) a. ()- => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)- => a -> Sized f n1 a -> Uncons f n a-pattern Uncons a as = S.Uncons a as--type Unsnoc f (n :: Nat) a = S.Unsnoc f n a--pattern Unsnoc- :: forall (f :: Type -> Type) (n :: Nat) a. ()- => forall (n1 :: Nat). (n ~ Succ n1)- => Sized f n1 a -> a -> Unsnoc f n a-pattern Unsnoc xs x = S.Unsnoc xs x---- | 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-{-# INLINE tail #-}-tail :: (Dom f a, CFreeMonoid f) => Sized f (One + n) a -> Sized f n a-tail = S.tail @Nat----- | 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-{-# INLINE init #-}-init :: (Dom f a, CFreeMonoid f) => Sized f (n + One) a -> Sized f n a-init = S.init @Nat---- | @take k xs@ takes first @k@ element of @xs@ where--- the length of @xs@ should be larger than @k@.------ Since 0.7.0.0-{-# INLINE take #-}-take- :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)- => SNat n -> Sized f m a -> Sized f n a-take = S.take @Nat---- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.------ Since 0.7.0.0-{-# INLINE takeAtMost #-}-takeAtMost- :: (Dom f a, CFreeMonoid f)- => SNat n -> Sized f m a -> Sized f (Min n m) a-takeAtMost = S.takeAtMost @Nat---- | @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-{-# INLINE drop #-}-drop- :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)- => SNat n -> Sized f m a -> Sized f (m - n) a-drop = S.drop @Nat---- | @splitAt k xs@ split @xs@ at @k@, where--- the length of @xs@ should be less than or equal to @k@.------ Since 0.7.0.0-{-# INLINE splitAt #-}-splitAt- :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)- => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)-splitAt = S.splitAt @Nat---- | @splitAtMost 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-{-# INLINE splitAtMost #-}-splitAtMost- :: (Dom f a, CFreeMonoid f)- => SNat n -> Sized f m a- -> (Sized f (Min n m) a, Sized f (m -. n) a)-splitAtMost = S.splitAtMost @Nat------------------------------------------------------------------------------------- Construction----------------------------------------------------------------------------------------------------------------------------------------------------------------------- Initialisation------------------------------------------------------------------------------------- | Empty sequence.------ Since 0.7.0.0 (type changed)-{-# INLINE empty #-}-empty :: (Dom f a, Monoid (f a)) => Sized f 'Z a-empty = S.empty @Nat---- | Sequence with one element.------ Since 0.7.0.0-{-# INLINE singleton #-}-singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f One a-singleton = S.singleton @Nat---- | 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-{-# INLINE toSomeSized #-}-toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a-toSomeSized = S.toSomeSized @Nat---- | Replicates the same value.------ Since 0.7.0.0-{-# INLINE replicate #-}-replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a-replicate = S.replicate @Nat---- | 'replicate' with the length inferred.------ Since 0.7.0.0-{-# INLINE replicate' #-}-replicate' :: (Dom f a, CFreeMonoid f, SingI n) => a -> Sized f n a-replicate' = S.replicate' @Nat---- | Construct a sequence of the given length by applying the function to each index.------ Since 0.7.0.0-{-# INLINE generate #-}-generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a-generate = S.generate @Nat---- | 'generate' with length inferred.------ Since 0.8.0.0-{-# INLINE generate' #-}-generate' :: forall f n a.- (SingI n, Dom f a, CFreeMonoid f)- => (Ordinal n -> a) -> Sized f n a-generate' = S.generate' @Nat-------------------------------------------------------------------------------------- Concatenation------------------------------------------------------------------------------------- | Append an element to the head of sequence.------ Since 0.7.0.0-{-# INLINE cons #-}-cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a-cons = S.cons @Nat---- | Append an element to the tail of sequence.------ Since 0.7.0.0-{-# INLINE snoc #-}-snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a-snoc = S.snoc @Nat---- | Infix version of 'snoc'.------ Since 0.7.0.0-{-# INLINE (<|) #-}-(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a-(<|) = (S.<|) @Nat---- | Append an element to the tail of sequence.------ Since 0.7.0.0-{-# INLINE (|>) #-}-(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a-(|>) = (S.|>) @Nat---- | Infix version of 'append'.------ Since 0.7.0.0-{-# INLINE (++) #-}-(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a-(++) = (S.++) @Nat---- | Append two lists.------ Since 0.7.0.0-{-# INLINE append #-}-append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a-append = S.append @Nat---- | Concatenates multiple sequences into one.------ Since 0.7.0.0-{-# INLINE concat #-}-concat- :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a),- CFreeMonoid f, CFunctor f', CFoldable f'- ) => Sized f' m (Sized f n a) -> Sized f (m * n) a-concat = S.concat @Nat-------------------------------------------------------------------------------------- Zips------------------------------------------------------------------------------------- | Zipping two sequences. Length is adjusted to shorter one.------ Since 0.7.0.0-{-# INLINE zip #-}-zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f)- => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)-zip = S.zip @Nat---- | 'zip' for the sequences of the same length.------ Since 0.7.0.0-{-# INLINE zipSame #-}-zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f)- => Sized f n a -> Sized f n b -> Sized f n (a, b)-zipSame = S.zipSame @Nat---- | Zipping two sequences with funtion. Length is adjusted to shorter one.------ Since 0.7.0.0-{-# INLINE zipWith #-}-zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)- => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c-zipWith = S.zipWith @Nat---- | 'zipWith' for the sequences of the same length.------ Since 0.7.0.0-{-# INLINE zipWithSame #-}-zipWithSame- :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)- => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c-zipWithSame = S.zipWithSame @Nat---- | Unzipping the sequence of tuples.------ Since 0.7.0.0-{-# INLINE unzip #-}-unzip- :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f)- => Sized f n (a, b) -> (Sized f n a, Sized f n b)-unzip = S.unzip @Nat---- | Unzipping the sequence of tuples.------ Since 0.7.0.0-{-# INLINE unzipWith #-}-unzipWith- :: (Dom f a, Dom f b, Dom f c, CUnzip f)- => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)-unzipWith = S.unzipWith @Nat------------------------------------------------------------------------------------- Transformation------------------------------------------------------------------------------------- | Map function.------ Since 0.7.0.0-{-# INLINE map #-}-map- :: (Dom f a, Dom f b, CFreeMonoid f)- => (a -> b) -> Sized f n a -> Sized f n b-map = S.map @Nat---- | Reverse function.------ Since 0.7.0.0-{-# INLINE reverse #-}-reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a-reverse = S.reverse @Nat---- | Intersperces.------ Since 0.7.0.0-{-# INLINE intersperse #-}-intersperse- :: (Dom f a, CFreeMonoid f)- => a -> Sized f n a -> Sized f ((Two * n) -. One) a-intersperse = S.intersperse @Nat---- | Remove all duplicates.------ Since 0.7.0.0-{-# INLINE nub #-}-nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a-nub = S.nub @Nat---- | Sorting sequence by ascending order.------ Since 0.7.0.0-{-# INLINE sort #-}-sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a-sort = S.sort @Nat---- | Generalized version of 'sort'.------ Since 0.7.0.0-{-# INLINE sortBy #-}-sortBy- :: (Dom f a, CFreeMonoid f)- => (a -> a -> Ordering)- -> Sized f n a -> Sized f n a-sortBy = S.sortBy @Nat---- | Insert new element into the presorted sequence.------ Since 0.7.0.0-{-# INLINE insert #-}-insert- :: (Dom f a, CFreeMonoid f, Ord a)- => a -> Sized f n a -> Sized f ('S n) a-insert = S.insert @Nat---- | Generalized version of 'insert'.------ Since 0.7.0.0-{-# INLINE insertBy #-}-insertBy- :: (Dom f a, CFreeMonoid f)- => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f ('S n) a-insertBy = S.insertBy @Nat------------------------------------------------------------------------------------- Conversion----------------------------------------------------------------------------------------------------------------------------------------------------------------------- List------------------------------------------------------------------------------------- | Convert to list.------ Since 0.7.0.0-{-# INLINE toList #-}-toList :: (Dom f a, CFoldable f) => Sized f n a -> [a]-toList = S.toList @Nat---- | 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)-{-# INLINE fromList #-}-fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a)-fromList = S.fromList @Nat---- | 'fromList' with the result length inferred.------ Since 0.7.0.0-{-# INLINE fromList' #-}-fromList' :: (Dom f a, CFreeMonoid f, SingI n) => [a] -> Maybe (Sized f n a)-fromList' = S.fromList' @Nat---- | 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-{-# INLINE unsafeFromList #-}-unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a-unsafeFromList = S.unsafeFromList @Nat---- | 'unsafeFromList' with the result length inferred.------ Since 0.7.0.0-{-# INLINE unsafeFromList' #-}-unsafeFromList' :: (Dom f a, SingI n, CFreeMonoid f) => [a] -> Sized f n a-unsafeFromList' = S.unsafeFromList' @Nat---- | Construct a @Sized f n a@ by padding default value if the given list is short.------ Since 0.5.0.0 (type changed)-{-# INLINE fromListWithDefault #-}-fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a-fromListWithDefault = S.fromListWithDefault @Nat---- | 'fromListWithDefault' with the result length inferred.------ Since 0.7.0.0-{-# INLINE fromListWithDefault' #-}-fromListWithDefault' :: (Dom f a, SingI n, CFreeMonoid f)- => a -> [a] -> Sized f n a-fromListWithDefault' = S.fromListWithDefault' @Nat-------------------------------------------------------------------------------------- Base containes------------------------------------------------------------------------------------- | Forget the length and obtain the wrapped base container.------ Since 0.7.0.0-{-# INLINE unsized #-}-unsized :: Sized f n a -> f a-unsized = S.unsized @Nat---- | 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-{-# INLINE toSized #-}-toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a)-toSized = S.toSized @Nat---- | 'toSized' with the result length inferred.------ Since 0.7.0.0-{-# INLINE toSized' #-}-toSized' :: (Dom f a, CFreeMonoid f, SingI n) => f a -> Maybe (Sized f n a)-toSized' = S.toSized' @Nat---- | 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-{-# INLINE unsafeToSized #-}-unsafeToSized :: SNat n -> f a -> Sized f n a-unsafeToSized = S.unsafeToSized @Nat---- | 'unsafeToSized' with the result length inferred.------ Since 0.7.0.0-{-# INLINE unsafeToSized' #-}-unsafeToSized' :: (Dom f a, SingI n) => f a -> Sized f n a-unsafeToSized' = S.unsafeToSized' @Nat---- | Construct a @Sized f n a@ by padding default value if the given list is short.------ Since 0.7.0.0-{-# INLINE toSizedWithDefault #-}-toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a-toSizedWithDefault = S.toSizedWithDefault @Nat---- | 'toSizedWithDefault' with the result length inferred.------ Since 0.7.0.0-{-# INLINE toSizedWithDefault' #-}-toSizedWithDefault' :: (Dom f a, SingI n, CFreeMonoid f)- => a -> f a -> Sized f n a-toSizedWithDefault' = S.toSizedWithDefault' @Nat------------------------------------------------------------------------------------- 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-type Partitioned f (n :: Nat) a = S.Partitioned f n a--pattern Partitioned- :: forall (f :: Type -> Type) (n :: Nat) a. ()- => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a)- => SNat n1 -> Sized f n1 a -> SNat m- -> Sized f m a -> Partitioned f n a-{-# COMPLETE Partitioned #-}-pattern Partitioned ls l rs r = S.Partitioned ls l rs r---- | Take the initial segment as long as elements satisfys the predicate.------ Since 0.7.0.0-{-# INLINE takeWhile #-}-takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a-takeWhile = S.takeWhile @Nat---- | Drop the initial segment as long as elements satisfys the predicate.------ Since 0.7.0.0-{-# INLINE dropWhile #-}-dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a-dropWhile = S.dropWhile @Nat---- | Split the sequence into the longest prefix--- of elements that satisfy the predicate--- and the rest.------ Since 0.7.0.0-{-# INLINE span #-}-span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a-span = S.span @Nat----- | Split the sequence into the longest prefix--- of elements that do not satisfy the--- predicate and the rest.------ Since 0.7.0.0-{-# INLINE break #-}-break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a-break = S.break @Nat---- | 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-{-# INLINE partition #-}-partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a-partition = S.partition @Nat-------------------------------------------------------------------------------------- Searching------------------------------------------------------------------------------------ | Membership test; see also 'notElem'.------ Since 0.7.0.0-{-# INLINE elem #-}-elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool-elem = S.elem @Nat---- | Negation of 'elem'.------ Since 0.7.0.0-{-# INLINE notElem #-}-notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool-notElem = S.notElem @Nat---- | Find the element satisfying the predicate.------ Since 0.7.0.0-{-# INLINE find #-}-find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a-find = S.find @Nat---- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.------ Since 0.7.0.0-{-# INLINE findIndex #-}-findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int-findIndex = S.findIndex @Nat---- | 'Ordinal' version of 'findIndex'.------ Since 0.7.0.0-{-# INLINE sFindIndex #-}-sFindIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)-sFindIndex = S.sFindIndex @Nat---- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.------ Since 0.7.0.0-{-# INLINE findIndices #-}-findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]-findIndices = S.findIndices @Nat---- | 'Ordinal' version of 'findIndices'.------ Since 0.7.0.0-{-# INLINE sFindIndices #-}-sFindIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n]-sFindIndices = S.sFindIndices @Nat---- | Returns the index of the given element in the list, if exists.------ Since 0.7.0.0-{-# INLINE elemIndex #-}-elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int-elemIndex = S.elemIndex @Nat--sElemIndex, sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)-{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}---- | Ordinal version of 'elemIndex'.--- Since 0.7.0.0, we no longer do boundary check inside the definition.------ Since 0.7.0.0-sUnsafeElemIndex = S.sElemIndex @Nat---- | Ordinal version of 'elemIndex'.--- Since 0.7.0.0, we no longer do boundary check inside the definition.------ Since 0.7.0.0-sElemIndex = S.sElemIndex @Nat---- | Returns all indices of the given element in the list.------ Since 0.8.0.0-{-# INLINE elemIndices #-}-elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int]-elemIndices = S.elemIndices @Nat---- | Ordinal version of 'elemIndices'------ Since 0.8.0.0-{-# INLINE sElemIndices #-}-sElemIndices- :: (Dom f a, CFoldable f, SingI n, Eq a)- => a -> Sized f n a -> [Ordinal n]-sElemIndices = S.sElemIndices @Nat-------------------------------------------------------------------------------------- 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 -> 'Sing' 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 -> 'Sing' n-slen ('viewSnoc' -> 'NilSV') = 'SZ'-slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as)-@--}----- | View of the left end of sequence (cons-side).------ Since 0.7.0.0-type ConsView f (n :: Nat) a = S.ConsView f n a---- | Since 0.8.0.0-pattern NilCV- :: forall (f :: Type -> Type) n a. ()- => (n ~ 'Z)- => ConsView f n a-pattern NilCV = S.NilCV---- | Since 0.8.0.0-pattern (:-)- :: forall (f :: Type -> Type) n a. ()- => forall n1. (n ~ (One + n1), SingI n1)- => a -> Sized f n1 a -> ConsView f n a-pattern l :- ls = l S.:- ls--infixr 9 :--{-# COMPLETE NilCV, (:-) #-}---- | Case analysis for the cons-side of sequence.------ Since 0.5.0.0 (type changed)-viewCons :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a-viewCons = S.viewCons @Nat---- | View of the left end of sequence (snoc-side).------ Since 0.7.0.0-type SnocView f (n :: Nat) a = S.SnocView f n a---- | Since 0.8.0.0-pattern NilSV- :: forall (f :: Type -> Type) n a. ()- => (n ~ 'Z)- => SnocView f n a-pattern NilSV = S.NilSV--infixl 9 :-::--- | Since 0.8.0.0-pattern (:-::)- :: forall (f :: Type -> Type) n a. ()- => forall n1. (n ~ (n1 + One), SingI n1)- => Sized f n1 a -> a -> SnocView f n a-pattern ls :-:: l = ls S.:-:: l-{-# COMPLETE NilSV, (:-::) #-}---- | Case analysis for the snoc-side of sequence.------ Since 0.8.0.0 (type changed)-viewSnoc :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a-viewSnoc = S.viewCons @Nat---{-$patterns #patterns#-- So we can pattern match on both end of sequence via views, but- it is rather clumsy to nest it. For example:--@-nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a-nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a-@-- In such a case, with @PatternSynonyms@ extension we can write as follows:--@-nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a-nextToHead (_ ':<' a ':<' _) = a-@-- Of course, we can also rewrite above @slen@ example using @PatternSynonyms@:--@-slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n-slen 'Nil' = 'SZ'-slen (_ ':<' as) = 'SS' (slen as)-slen _ = error "impossible"-@-- 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>.--}---- | Pattern synonym for cons-side uncons.-pattern (:<)- :: forall (f :: Type -> Type) a (n :: Nat).- (Dom f a, SingI n, CFreeMonoid f)- => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)- => a -> Sized f n1 a -> Sized f n a-pattern a :< b = a S.:< b-infixr 5 :<---- | Pattern synonym for a nil sequence.-pattern Nil- :: forall (f :: Type -> Type) a n.- (Dom f a, SingI n, CFreeMonoid f)- => (n ~ 'Z) => Sized f n a-pattern Nil = S.Nil---- | Pattern synonym for cons-side nil.-pattern NilL :: forall f (n :: Nat) a.- (SingI n, CFreeMonoid f, Dom f a)- => n ~ 'Z => Sized f n a-pattern NilL = Nil---- | Pattern synonym for snoc-side unsnoc.-pattern (:>)- :: forall (f :: Type -> Type) a (n :: Nat).- (Dom f a, SingI n, CFreeMonoid f)- => forall (n1 :: Nat). (n ~ (n1 + One), SingI n1)- => Sized f n1 a -> a -> Sized f n a-pattern a :> b = a S.:> b-infixl 5 :>---- | Pattern synonym for snoc-side nil.-pattern NilR :: forall f (n :: Nat) a.- (CFreeMonoid f, Dom f a, SingI n)- => n ~ 'Z => Sized f n a-pattern NilR = Nil-{-# COMPLETE (:<), NilL #-}-{-# COMPLETE (:<), NilR #-}-{-# COMPLETE (:<), Nil #-}-{-# COMPLETE (:>), NilL #-}-{-# COMPLETE (:>), NilR #-}-{-# COMPLETE (:>), Nil #-}
test/opt-test.hs view
@@ -1,42 +1,50 @@-{-# LANGUAGE DataKinds, RankNTypes, TemplateHaskell #-}+{-# 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.Singletons.Prelude-import Data.Sized.Builtin (Sized, zipWithSame)-import qualified Data.Sized.Builtin as SV-import qualified Data.Vector as V-import qualified Data.Vector.Generic as G-import Data.Vector.Storable (Storable)-import qualified Data.Vector.Storable as S-import Data.Vector.Unboxed (Unbox)-import qualified Data.Vector.Unboxed as U-import Numeric.Natural (Natural)-import Shared-import Test.Hspec-import Test.Inspection +import Control.Subcategory+import qualified Data.Sequence as Seq+import Data.Sized.Builtin (Sized, zipWithSame)+import qualified Data.Sized.Builtin 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.Hspec+import Test.Inspection+ type LSized = Sized []+ type VSized = Sized V.Vector+ type USized = Sized U.Vector+ type SSized = Sized S.Vector+ type SeqSized = Sized Seq.Seq -zipWith_subcat_List- :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]+zipWith_subcat_List ::+ (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 ::+ (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 ::+ (Int -> Int -> Int) -> LSized n Int -> LSized n Int -> LSized n Int zipWithSame_List = zipWithSame zipWith_List_Prel :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int]@@ -45,36 +53,47 @@ 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 ::+ (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 ::+ (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 ::+ (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 ::+ (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 ::+ (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 ::+ (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 ::+ (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@@ -89,66 +108,66 @@ main :: IO () main = hspec $ do describe "czipWith" $ do- $(inspecting "doesn't contain type classes"- $ hasNoTypeClasses 'zipWith_subcat_List- )+ $( inspecting "doesn't contain type classes" $+ hasNoTypeClasses 'zipWith_subcat_List+ ) describe "zipWith" $ do- $(inspecting "doesn't contain type classes"- $ hasNoTypeClasses 'zipWith_List- )+ $( inspecting "doesn't contain type classes" $+ hasNoTypeClasses 'zipWith_List+ ) describe "zipWithSame" $ do describe "list" $ do it "doesn't contain type classes" $ checkInspection- $(inspectTest- $ hasNoTypeClasses 'zipWithSame_List- )+ $( inspectTest $+ hasNoTypeClasses 'zipWithSame_List+ ) it "is almost the same as the original zipWith (list)" $ checkInspection- $(inspectTest $+ $( inspectTest $ 'zipWithSame_List ==- 'zipWith_List_Prel- )+ ) describe "Boxed Vector" $ do it "doesn't contain type classes, except for G.Vector" $ checkInspection- $(inspectTest- $ 'zipWithSame_Boxed `hasNoTypeClassesExcept`- [''G.Vector]- )+ $( inspectTest $+ 'zipWithSame_Boxed+ `hasNoTypeClassesExcept` [''G.Vector]+ ) it "is almost the same as the original zipWith (Boxed)" $ checkInspection- $(inspectTest $+ $( inspectTest $ 'zipWithSame_Boxed ==- 'zipWith_Boxed- )+ ) describe "Unboxed Vector" $ do it "doesn't contain type classes except for Unbox" $ checkInspection- $(inspectTest- $ 'zipWithSame_Unboxed `hasNoTypeClassesExcept`- [''Unbox]- )+ $( inspectTest $+ 'zipWithSame_Unboxed+ `hasNoTypeClassesExcept` [''Unbox]+ ) it "doesn't contain type classes if fully instnatiated" $ checkInspection- $(inspectTest- $ hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic- )+ $( inspectTest $+ hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic+ ) it "is almost the same as the original zipWith, if fully instantiated" $ checkInspection- $(inspectTest $+ $( inspectTest $ 'zipWithSame_Unboxed_monomorphic- ==- 'zipWith_Unboxed_monomorphic- )+ ==- 'zipWith_Unboxed_monomorphic+ ) describe "length" $ do it "is a constant function when length is concrete (with Dom dictionary)" $ checkInspection- $(inspectTest $- 'length_two ==- 'const_two_dom- )+ $( inspectTest $+ 'length_two ==- 'const_two_dom+ ) it "doesn't contain Integer when the length is concrete" $ checkInspection- $(inspectTest $ hasNoType 'length_two ''Integer- )+ $( inspectTest $ hasNoType 'length_two ''Integer+ ) it "doesn't contain Natural when the length is concrete" $ checkInspection- $(inspectTest $ hasNoType 'length_two ''Natural- )+ $( inspectTest $ hasNoType 'length_two ''Natural+ )