sized 0.7.0.0 → 0.8.0.0
raw patch · 5 files changed
+1399/−196 lines, 5 files
Files
- sized.cabal +1/−1
- src/Data/Sized.hs +174/−138
- src/Data/Sized/Builtin.hs +608/−32
- src/Data/Sized/Peano.hs +595/−20
- test/opt-test.hs +21/−5
sized.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=2.0 name: sized-version: 0.7.0.0+version: 0.8.0.0 license: BSD3 license-file: LICENSE maintainer: konn.jinro_at_gmail.com
src/Data/Sized.hs view
@@ -1,19 +1,14 @@-{-# LANGUAGE DerivingStrategies #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE UndecidableSuperClasses #-}-{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds #-} {-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-}-{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-}-{-# LANGUAGE PatternSynonyms, PolyKinds, QuantifiedConstraints, ScopedTypeVariables, RankNTypes #-}-{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies #-}-{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-}-#if __GLASGOW_HASKELL__ && __GLASGOW_HASKELL__ >= 806-{-# LANGUAGE NoStarIsType #-}-#endif+{-# 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 #-}@@ -35,13 +30,13 @@ length, sLength, null, -- ** Indexing (!!), (%!!), index, sIndex, head, last,- uncons, uncons', Uncons(..), + uncons, uncons', Uncons(..), unsnoc, unsnoc', Unsnoc(..), -- ** Slicing tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction -- ** Initialisation- empty, singleton, toSomeSized, replicate, replicate', generate,+ empty, singleton, toSomeSized, replicate, replicate', generate, generate', -- ** Concatenation cons, (<|), snoc, (|>), append, (++), concat, -- ** Zips@@ -61,7 +56,7 @@ Partitioned(..), takeWhile, dropWhile, span, break, partition, -- ** Searching- elem, notElem, find, findIndex, sFindIndex, + elem, notElem, find, findIndex, sFindIndex, findIndices, sFindIndices, elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, -- * Views and Patterns@@ -76,45 +71,54 @@ -- ** Definitions viewCons, ConsView (..), viewSnoc, SnocView(..), - pattern (:<), pattern NilL , pattern (:>), pattern NilR,+ pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR, ) 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 Data.Monoid-import Control.Applicative ((<*>), ZipList(..)) import qualified Data.List as L+import Data.Maybe (fromJust)+import Data.Monoid (Monoid (..), (<>)) import qualified Data.Sequence as Seq-import Data.Singletons.Prelude.Bool -import Data.Constraint-import Data.Singletons.Prelude (SomeSing(..))-import Data.Singletons.Prelude (SingI (..))-import Data.Singletons.Prelude (withSing, withSingI)-import Control.Subcategory-import Data.Singletons.Prelude.Enum (sSucc, sPred, PEnum (..))+import 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-import Data.Type.Ordinal (HasOrdinal, Ordinal (..))-import Data.Type.Ordinal (ordToNatural)+import Data.Type.Natural.Class (type (-.), IsPeano (..), One,+ PNum (..), POrd (..),+ PeanoOrder (..), S, SNum (..),+ Zero, pattern Zero,+ ZeroOrSucc (..), sOne, sZero)+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 (fmap, uncurry, fromIntegral, const, Bool (..), Enum (..), Eq (..))-import Prelude (Functor, Int, Maybe (..))-import Prelude (Num (..), Ord (..), Ordering)-import Prelude (Show (..), flip, ($), (.))+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)-import Data.Coerce (coerce)-import Data.Maybe (fromJust)-import Data.These (These(..))-import Data.Type.Equality (gcastWith)-import Proof.Propositional (withWitness, IsTrue(Witness))-import Data.Type.Equality ((:~:)(..)) -------------------------------------------------------------------------------- -- Main data-types@@ -153,10 +157,10 @@ -- If you use @unsafeFromList@ or similar unsafe functions, -- this function may return different value from type-parameterized length. ----- Since 0.7.0.0+-- Since 0.8.0.0 (type changed) length- :: forall nat f (n :: nat) a. - (IsPeano nat, CFoldable f, Dom f a, SingI n)+ :: 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 #-}@@ -176,12 +180,11 @@ -- | @Sing@ version of 'length'. ----- Since 0.7.0.0 (type changed)-sLength :: forall nat f (n :: nat) a. (HasOrdinal nat, CFoldable f, Dom f a)+-- 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 (Sized xs) =- case fromNatural (P.fromIntegral $ clength xs) of- SomeSing (n :: Sing (k :: nat)) -> unsafeCoerce n+sLength _ = sing @n {-# INLINE[2] sLength #-} -- | Test if the sequence is empty or not.@@ -211,12 +214,12 @@ {-# RULES "null/0" [~2] null = nullTL0-"null/0" [~1] forall (vec :: (1 TL.<= n) => Sized f n a).- null vec = False "null/0" [~2] null = nullTLSucc+"null/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@@ -236,7 +239,7 @@ -- -- Since 0.7.0.0 (%!!)- :: forall nat f (n :: nat) c. + :: 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@@ -256,7 +259,7 @@ -- -- Since 0.7.0.0 index- :: forall nat f (m :: nat) a. + :: forall nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True) => Int -> Sized f m a -> a index = flip (!!)@@ -277,7 +280,7 @@ -- -- Since 0.7.0.0 head- :: forall nat f (n :: nat) a. + :: 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@@ -288,7 +291,7 @@ -- see <#ViewsAndPatterns Views and Patterns> section. -- -- Since 0.7.0.0-last :: forall nat f (n :: nat) a. +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@@ -299,17 +302,22 @@ -- see <#ViewsAndPatterns Views and Patterns> section. -- -- Since 0.7.0.0-uncons :: forall nat f (n :: nat) a. +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 + $ 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)@@ -320,7 +328,7 @@ data Uncons f (n :: nat) a where Uncons :: forall nat f (n :: nat) a. SingI n- => a -> Sized f n a -> Uncons f (Succ n) a+ => 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,@@ -333,7 +341,7 @@ => Sized f n a -> Unsnoc f n a unsnoc = withSingI (sPred $ sing @n)- $ gcastWith + $ gcastWith (lneqRightPredSucc sZero (sing @n) Witness ) $ uncurry (Unsnoc @nat @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a)@@ -342,11 +350,14 @@ 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. + :: 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' _ = +unsnoc' _ = withSingI (sSucc $ sing @n) $ withWitness (lneqZero $ sing @n) unsnoc {-# INLINE unsnoc' #-}@@ -389,7 +400,7 @@ take = coerce $ ctake @f @a . P.fromIntegral . toNatural @nat @n {-# INLINE take #-} --- | @take k xs@ takes first @k@ element of @xs@ at most.+-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@. -- -- Since 0.7.0.0 takeAtMost@@ -489,7 +500,9 @@ replicate' = withSing replicate {-# INLINE replicate' #-} --- | Since 0.7.0.0+-- | 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)@@ -499,6 +512,16 @@ . (. 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@@ -526,7 +549,7 @@ (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@@ -534,20 +557,20 @@ -- | Append an element to the head of sequence. ----- Since 0.7.0.0+-- Since 0.8.0.0 cons- :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a)- => a -> Sized f n a -> Sized f (Succ n) 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.7.0.0+-- Since 0.8.0.0 (<|) :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a)- => a -> Sized f n a -> Sized f (Succ n) a+ => a -> Sized f n a -> Sized f (One nat + n) a (<|) = cons {-# INLINE (<|) #-} infixr 5 <|@@ -556,7 +579,7 @@ -- -- Since 0.7.0.0 snoc- :: forall nat f (n :: nat) a. + :: 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@@ -565,7 +588,7 @@ -- | Infix version of 'snoc'. -- -- Since 0.7.0.0-(|>) :: forall nat f (n :: nat) a. +(|>) :: forall nat f (n :: nat) a. (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a (|>) = snoc {-# INLINE (|>) #-}@@ -575,7 +598,7 @@ -- -- Since 0.7.0.0 append- :: forall nat f (n :: nat) (m :: nat) a. + :: 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)@@ -585,7 +608,7 @@ -- -- Since 0.7.0.0 (++)- :: forall nat f (n :: nat) (m :: nat) a. + :: 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@@ -594,7 +617,7 @@ -- | Concatenates multiple sequences into one. -- -- Since 0.7.0.0-concat :: forall nat f' (m :: nat) f (n :: nat) a. +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) )@@ -619,7 +642,7 @@ -- -- Since 0.7.0.0 zipSame- :: forall nat f (n :: nat) a b. + :: 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@@ -629,7 +652,7 @@ -- -- Since 0.7.0.0 zipWith- :: forall nat f (n :: nat) a (m :: nat) b c. + :: 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@@ -642,26 +665,9 @@ -- -- Since 0.7.0.0 zipWithSame- :: forall nat f (n :: nat) a b c. + :: forall nat f (n :: nat) a b c. (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c-{-# SPECIALISE INLINE [1] zipWithSame- :: (a -> b -> c) -> Sized [] n a -> Sized [] n b -> Sized [] n c- #-}-{-# SPECIALISE INLINE [1] zipWithSame- :: (a -> b -> c)- -> Sized V.Vector n a -> Sized V.Vector n b -> Sized V.Vector n c- #-}-{-# SPECIALISE INLINE [1] zipWithSame- :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) - => (a -> b -> c)- -> Sized UV.Vector n a -> Sized UV.Vector n b -> Sized UV.Vector n c- #-}-{-# SPECIALISE INLINE [1] zipWithSame- :: (SV.Storable a, SV.Storable b, SV.Storable c) - => (a -> b -> c)- -> Sized SV.Vector n a -> Sized SV.Vector n b -> Sized SV.Vector n c- #-} zipWithSame = coerce $ czipWith @f @a @b @c {-# INLINE [1] zipWithSame #-} @@ -694,7 +700,7 @@ -- -- Since 0.7.0.0 map- :: forall nat f (n :: nat) a b. + :: 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@@ -732,7 +738,7 @@ -- | Sorting sequence by ascending order. -- -- Since 0.7.0.0-sort :: forall nat f (n :: nat) a. +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@@ -792,7 +798,7 @@ -- -- Since 0.7.0.0 (type changed) fromList- :: forall nat f (n :: nat) a. + :: 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)@@ -850,12 +856,12 @@ -- -- Since 0.5.0.0 (type changed) fromListWithDefault- :: forall nat f (n :: nat) a. + :: 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) <> + in Sized $ cfromList (ctake len xs) <> creplicate (len - clength xs) def {-# INLINABLE fromListWithDefault #-} @@ -991,7 +997,11 @@ dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a) {-# INLINE dropWhile #-} --- | Since 0.7.0.0+-- | 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)@@ -999,7 +1009,11 @@ span = (unsafePartitioned @nat @n .) . coerce (cspan @f @a) {-# INLINE span #-} --- | Since 0.7.0.0+-- | 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)@@ -1007,16 +1021,18 @@ break = (unsafePartitioned @nat @n .) . coerce (cbreak @f @a) {-# INLINE break #-} --- | Since 0.7.0.0+-- | 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. + :: 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. + :: forall nat (n :: nat) f a. (HasOrdinal nat, CFreeMonoid f, Dom f a) => (f a, f a) -> Partitioned f n a unsafePartitioned (l, r) =@@ -1025,7 +1041,7 @@ SomeSized' (lenR :: Sing nr) rs ) -> gcastWith- (unsafeCoerce $ Refl @() + (unsafeCoerce $ Refl @() :: n :~: nl + nr ) $ Partitioned lenL ls lenR rs@@ -1037,7 +1053,7 @@ -- -- Since 0.7.0.0 elem- :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> Bool elem = coerce $ celem @f @a@@ -1047,7 +1063,7 @@ -- -- Since 0.7.0.0 notElem- :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a, Eq a) => a -> Sized f n a -> Bool notElem = coerce $ cnotElem @f @a@@ -1057,7 +1073,7 @@ -- -- Since 0.7.0.0 find- :: forall nat f (n :: nat) a. + :: forall nat f (n :: nat) a. (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> Maybe a find = coerce $ cfind @f @a@@ -1077,7 +1093,7 @@ -- -- Since 0.7.0.0 findIndex- :: forall nat f (n :: nat) a . + :: forall nat f (n :: nat) a . (CFoldable f, Dom f a) => (a -> Bool) -> Sized f n a -> Maybe Int findIndex = coerce $ cfindIndex @f @a@@ -1087,13 +1103,12 @@ -- -- Since 0.7.0.0 sFindIndex- :: forall nat f (n :: nat) a . + :: 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@@ -1123,13 +1138,13 @@ -- | Returns the index of the given element in the list, if exists. -- -- Since 0.7.0.0-elemIndex :: forall nat f (n :: nat) a . +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, we no longer do boundary check inside the definition. -- -- Since 0.7.0.0 sElemIndex, sUnsafeElemIndex :: forall nat f (n :: nat) a.@@ -1155,7 +1170,7 @@ -- -- Since 0.7.0.0 sElemIndices- :: forall nat f (n :: nat) a . + :: 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@@ -1205,14 +1220,14 @@ -- Since 0.7.0.0 data ConsView f n a where NilCV :: ConsView f (Zero nat) a- (:-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a+ (:-) :: SingI 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 . +viewCons :: forall nat f (n :: nat) a . (HasOrdinal nat, SingI n, CFreeMonoid f,Dom f a) => Sized f n a -> ConsView f n a@@ -1220,9 +1235,9 @@ IsZero -> NilCV IsSucc n' -> withSingI n'- $ withSingI (sSucc n')+ $ withSingI (sOne %+ n') $ case uncons' n' sz of- Uncons a xs -> (a :- xs)+ Uncons a xs -> a :- xs -- | View of the left end of sequence (snoc-side). --@@ -1235,14 +1250,14 @@ -- | Case analysis for the snoc-side of sequence. -- -- Since 0.5.0.0 (type changed)-viewSnoc :: forall nat f (n :: nat) a. +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' $ + withSingI n' $ gcastWith (succAndPlusOneR n') $ case unsnoc' n' sz of Unsnoc (xs :: Sized f m a) a ->@@ -1271,14 +1286,13 @@ @ slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n-slen 'NilL' = 'SZ'+slen 'Nil' = 'SZ' slen (_ ':<' as) = 'SS' (slen as)-slen _ = error "impossible" @ - So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to+ 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.- @':<'@, @'NilL'@, @':>'@ and @'NilR'@ are neither functions nor data constructors,+ @'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>@@ -1289,40 +1303,62 @@ infixr 5 :< -- | Pattern synonym for cons-side uncons. pattern (:<)- :: forall nat (f :: Type -> Type) a (n :: nat). + :: forall nat (f :: Type -> Type) a (n :: nat). (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)- => forall (n1 :: nat). (n ~ Succ n1, SingI n1)+ => 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++-- | Pattern synonym for cons-side nil.+{-# DEPRECATED NilL "Use Nil instead" #-} pattern NilL :: forall nat f (n :: nat) a. (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) => (n ~ Zero nat) => Sized f n a-pattern NilL <- (viewCons -> NilCV) where- NilL = empty+pattern NilL = Nil infixl 5 :> +-- | Pattern synonym for snoc-side unsnoc. pattern (:>)- :: forall nat (f :: Type -> Type) a (n :: nat). + :: 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 +{-# DEPRECATED NilR "Use Nil instead" #-} pattern NilR :: forall nat f (n :: nat) a. (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) => n ~ Zero nat => Sized f n a-pattern NilR <- (viewSnoc -> NilSV) where- NilR = empty+pattern NilR = Nil +{-# COMPLETE (:<), Nil #-}+{-# COMPLETE (:<), NilL #-}+{-# COMPLETE (:<), NilR #-}+{-# COMPLETE (:>), Nil #-}+{-# COMPLETE (:>), NilL #-}+{-# COMPLETE (:>), NilR #-}+ class Dom f a => DomC f a instance Dom f a => DomC f a -- | Applicative instance, generalizing @'Data.Monoid.ZipList'@.-instance +instance ( Functor f, CFreeMonoid f, CZip f, HasOrdinal nat, SingI n, forall a. DomC f a) => P.Applicative (Sized f (n :: nat)) where@@ -1364,7 +1400,7 @@ -- 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. + :: 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 #-}@@ -1372,11 +1408,11 @@ :: 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 #-} + {-# INLINE [1] calign #-} instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where czipWith = coerce $ czipWith @f @a @b @c- :: forall 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 #-}@@ -1384,13 +1420,13 @@ :: 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 #-} + {-# INLINE [1] czip #-} -instance +instance (PeanoOrder nat, SingI (n :: nat), CZip f, CFreeMonoid f) => CRepeat (Sized f n) where crepeat = replicate'- {-# INLINE [1] crepeat #-} + {-# INLINE [1] crepeat #-} instance CTraversable f => CTraversable (Sized f n) where ctraverse = \f -> fmap coerce . ctraverse f . runSized
src/Data/Sized/Builtin.hs view
@@ -4,12 +4,20 @@ {-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE NoStarIsType #-}--- | This module exports @'S.Sized'@ type and--- functions specialized to--- GHC's built-in type numeral @'Nat'@.+-- | 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+ ( -- * Main Data-types Sized(), SomeSized, pattern SomeSized, Ordinal, DomC(), -- * Accessors@@ -23,7 +31,7 @@ tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction -- ** Initialisation- empty, singleton, toSomeSized, replicate, replicate', generate,+ empty, singleton, toSomeSized, replicate, replicate', generate, generate', -- ** Concatenation cons, (<|), snoc, (|>), append, (++), concat, -- ** Zips@@ -57,11 +65,11 @@ -- ** Definitions viewCons, ConsView,- pattern (S.:-), pattern S.NilCV,+ pattern (:-), pattern NilCV, viewSnoc, SnocView,- pattern (S.:-::), pattern S.NilSV,+ pattern (:-::), pattern NilSV, - pattern (:<), pattern NilL , pattern (:>), pattern NilR,+ pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR, ) where import qualified Data.Sized as S import Data.Sized (DomC)@@ -79,8 +87,22 @@ import Data.Type.Natural (Min, type (-), type (+), type (*)) 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@@ -90,58 +112,125 @@ {-# COMPLETE SomeSized #-} pattern SomeSized n s = S.SomeSized' n s -length :: (Dom f a, CFoldable f, KnownNat n) => Sized f n a -> Int+-- | 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 -sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n+-- | @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 (!!) :: (Dom f a, CFoldable f, (1 <= m) ~ 'True) => Sized f m a -> Int -> a+{-# INLINE (!!) #-} (!!) = (S.!!) @Nat +-- | 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) ~ 'True) => Int -> Sized f m a -> a+{-# INLINE index #-} index = S.index @Nat +-- | 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 :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a+{-# INLINE head #-} 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 last :: (Dom f a, CFoldable f, (0 < n) ~ 'True) => Sized f n a -> a+{-# INLINE last #-} 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 uncons :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) => Sized f n a -> Uncons f n a+{-# INLINE uncons #-} uncons = S.uncons @Nat +-- | 'uncons' with explicit specified length @n@+--+-- Since 0.7.0.0 uncons' :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) => Sized f n a -> Uncons f n a+{-# INLINE uncons' #-} 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 unsnoc :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n) ~ 'True) => Sized f n a -> Unsnoc f n a+{-# INLINE unsnoc #-} unsnoc = S.unsnoc @Nat +-- | '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 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)+ => forall (n1 :: Nat). (n ~ (1 + n1), SingI n1) => a -> Sized f n1 a -> Uncons f n a pattern Uncons a as = S.Uncons a as @@ -153,186 +242,453 @@ => 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 :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> Sized f n a+{-# INLINE take #-} take = S.take @Nat +-- | @'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 :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> Sized f (m - n) a+{-# INLINE drop #-} 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 splitAt :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True) => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)+{-# INLINE splitAt #-} 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 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 -cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a+-- | '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 -(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (n + 1) a+-- | 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@@ -343,90 +699,310 @@ {-# 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 -elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int-elemIndex = S.findIndex @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 -sUnsafeElemIndex :: (Dom f a, KnownNat n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)+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 -sElemIndex :: (Dom f a, KnownNat n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)-sElemIndex = S.sFindIndex @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 -elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]-elemIndices = S.findIndices @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 -sElemIndices :: (Dom f a, CFoldable f, KnownNat n) => (a -> Bool) -> Sized f n a -> [Ordinal n]-sElemIndices = S.sFindIndices @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 -type ConsView f (n :: Nat) a = S.ConsView f n a+--------------------------------------------------------------------------------+-- 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 = + (S.ConsView :: (Type -> Type) -> Nat -> Type -> Type)++-- | Since 0.8.0.0+pattern NilCV+ :: forall (f :: Type -> Type) n a. ()+ => (n ~ 0)+ => ConsView f n a+pattern NilCV = S.NilCV++-- | Since 0.8.0.0+pattern (:-)+ :: forall (f :: Type -> Type) n a. ()+ => forall n1. (n ~ (1 + 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, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a viewCons = S.viewCons @Nat -type SnocView f (n :: Nat) a = S.SnocView f n a+-- | View of the left end of sequence (snoc-side).+--+-- Since 0.7.0.0+type SnocView = + (S.SnocView :: (Type -> Type) -> Nat -> Type -> Type) -viewSnoc :: (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a-viewSnoc = S.viewCons @Nat+-- | 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, SingI n, CFreeMonoid f)- => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)+ (Dom f a, KnownNat n, CFreeMonoid f)+ => forall (n1 :: Nat). (n ~ (1 + 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, KnownNat n, CFreeMonoid f)+ => (n ~ 0) => Sized f n a+pattern Nil = S.Nil++{-# DEPRECATED NilL "Use Nil instead" #-}+-- | Pattern synonym for cons-side nil. pattern NilL :: forall f (n :: Nat) a. (KnownNat n, CFreeMonoid f, Dom f a) => n ~ 0 => Sized f n a-pattern NilL = S.NilL+pattern NilL = Nil +-- | Pattern synonym for snoc-side unsnoc. pattern (:>) :: forall (f :: Type -> Type) a (n :: Nat). - (Dom f a, SingI n, CFreeMonoid f)+ (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 :> +{-# DEPRECATED NilR "Use Nil instead" #-}+-- | Pattern synonym for snoc-side nil. pattern NilR :: forall f (n :: Nat) a.- (CFreeMonoid f, Dom f a, SingI n)+ (CFreeMonoid f, Dom f a, KnownNat n) => n ~ 0 => Sized f n a-pattern NilR = S.NilR+pattern NilR = Nil+{-# COMPLETE (:<), NilL #-}+{-# COMPLETE (:<), NilR #-}+{-# COMPLETE (:<), Nil #-}+{-# COMPLETE (:>), NilL #-}+{-# COMPLETE (:>), NilR #-}+{-# COMPLETE (:>), Nil #-}
src/Data/Sized/Peano.hs view
@@ -5,10 +5,18 @@ {-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE NoStarIsType #-}--- | This module exports @'S.Sized'@ type specialized to--- type-level Peano numeral @'PN.Nat'@.+-- | 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- ( -- * Main Data-types+ ( -- * Main Data-types Sized(), SomeSized, pattern SomeSized, Ordinal, DomC(), -- * Accessors@@ -22,7 +30,7 @@ tail, init, take, takeAtMost, drop, splitAt, splitAtMost, -- * Construction -- ** Initialisation- empty, singleton, toSomeSized, replicate, replicate', generate,+ empty, singleton, toSomeSized, replicate, replicate', generate, generate', -- ** Concatenation cons, (<|), snoc, (|>), append, (++), concat, -- ** Zips@@ -56,11 +64,11 @@ -- ** Definitions viewCons, ConsView,- pattern (S.:-), pattern S.NilCV,+ pattern (:-), pattern NilCV, viewSnoc, SnocView,- pattern (S.:-::), pattern S.NilSV,+ pattern (:-::), pattern NilSV, - pattern (:<), pattern NilL , pattern (:>), pattern NilR,+ pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR, ) where import qualified Data.Sized as S import Data.Sized (DomC)@@ -78,8 +86,23 @@ import Data.Type.Natural (One) 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@@ -89,51 +112,118 @@ {-# COMPLETE SomeSized #-} pattern SomeSized n s = S.SomeSized' n s -length :: (Dom f a, CFoldable f, SingI n) => Sized f n a -> Int+-- | 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 -sLength :: (Dom f a, CFoldable f) => Sized f n a -> SNat n+-- | @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 @@ -152,186 +242,453 @@ => 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@@ -342,68 +699,270 @@ {-# 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 -elemIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int-elemIndex = S.findIndex @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 -sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)+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 -sElemIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)-sElemIndex = S.sFindIndex @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 -elemIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]-elemIndices = S.findIndices @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 -sElemIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n]-sElemIndices = S.sFindIndices @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)@@ -412,11 +971,20 @@ 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 = S.NilL+pattern NilL = Nil +-- | Pattern synonym for snoc-side unsnoc. pattern (:>) :: forall (f :: Type -> Type) a (n :: Nat). (Dom f a, SingI n, CFreeMonoid f)@@ -425,7 +993,14 @@ 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 = S.NilR+pattern NilR = Nil+{-# COMPLETE (:<), NilL #-}+{-# COMPLETE (:<), NilR #-}+{-# COMPLETE (:<), Nil #-}+{-# COMPLETE (:>), NilL #-}+{-# COMPLETE (:>), NilR #-}+{-# COMPLETE (:>), Nil #-}
test/opt-test.hs view
@@ -16,6 +16,7 @@ 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@@ -79,6 +80,12 @@ zipWith_Boxed :: (a -> b -> c) -> V.Vector a -> V.Vector b -> V.Vector c zipWith_Boxed = V.zipWith +length_two :: Dom f a => Sized f 2 a -> Int+length_two = SV.length++const_two_dom :: Dom f a => Sized f 2 a -> Int+const_two_dom = const 2+ main :: IO () main = hspec $ do describe "czipWith" $ do@@ -108,11 +115,6 @@ $ 'zipWithSame_Boxed `hasNoTypeClassesExcept` [''G.Vector] )- it "doesn't contain type classes, if fully instantiated" $- checkInspection- $(inspectTest- $ hasNoTypeClasses 'zipWithSame_Boxed_mono- ) it "is almost the same as the original zipWith (Boxed)" $ checkInspection $(inspectTest $@@ -136,3 +138,17 @@ 'zipWithSame_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+ )+ it "doesn't contain Integer when the length is concrete" $+ checkInspection+ $(inspectTest $ hasNoType 'length_two ''Integer+ )+ it "doesn't contain Natural when the length is concrete" $+ checkInspection+ $(inspectTest $ hasNoType 'length_two ''Natural+ )