diff --git a/Changelog.md b/Changelog.md new file mode 100644 --- /dev/null +++ b/Changelog.md @@ -0,0 +1,51 @@ +# Changelog + +## 1.1.0.2 + +* Supports GHC 9.10 + +## 1.1.0.1 + +* Supports GHC 9.8 +* Drops Support for GHC <9 + +## 1.1.0.0 + +* Supports GHC 9.6 +* Migrates to recent toolchains + +## 1.0.0.1 + +* Minor refactoring of test-suite to support inspection-testiong 0.5 + +## 1.0.0.0 + +* Drops Peano-numerals +* Obsolete kind-generic classes +* Now all types are kinded with GHC's builtin type-level naturals, and no type parameters for naturals. +* Drops dependency for `singletons` package and their relatives. + +## 0.9.0.0 + +* This is transitional change: preparation for future rework of `type-natural` + - Types and constraints in `Data.Sized.Builtin` is now incompatible with `Data.Sized` and `Data.Sized.Peano` + - The latter two modules will be removed in future release. +* Removes `NilL` and `NilR` +* Compolete overhaul on `Data.Sized.Builtin` + - Stop using orders from `Data.Singletons` + - Types of nested pattern synonyms can now be inferred correctly + +## 0.8.0.0 + +* Makes `sLength` using `KnownNat` instance to get O(1) always. +* Introduces `Nil` pattern and deprecates `NilL` and `NilR`. +* Previously, in sepcialised modules for `Builtin` and `Peano`, + `elemIndex`, `elemIndices` and their Ordinal version were misimplemented; + they are now correctly uses their counterparts in `Data.Sized`. +* Adds documentation for specialised modules. + +## 0.7.0.0 + +* Stop using `ListLike` package and switched to [`subcategories`] package for the abstraction of sequential types. +* Complete overhaul on type signatures. +* Both `Data.Sized.Builtin` and `Data.Sized.Peano` exports specialised functions instead of reexporting functions from `Data.Sized`. diff --git a/Data/Sized.hs b/Data/Sized.hs deleted file mode 100644 --- a/Data/Sized.hs +++ /dev/null @@ -1,1275 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, DataKinds #-} -{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable, ExplicitNamespaces, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, GADTs, GeneralizedNewtypeDeriving #-} -{-# LANGUAGE KindSignatures, LambdaCase, LiberalTypeSynonyms #-} -{-# LANGUAGE MultiParamTypeClasses, NoMonomorphismRestriction #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables, RankNTypes #-} -{-# LANGUAGE StandaloneDeriving, TypeApplications, TypeFamilies #-} -{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-} -{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-} -{-# OPTIONS_GHC -fenable-rewrite-rules #-} --- | This module provides the functionality to make length-parametrized types --- from existing 'ListLike' and 'Functor' sequential types. --- --- Most of the complexity of operations for @Sized f n a@ are the same as --- original operations for @f@. For example, '!!' is O(1) for --- @Sized Vector n a@ but O(i) for @Sized [] n a@. --- --- This module also provides powerful view types and pattern synonyms to --- inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail. -module Data.Sized - ( -- * Main Data-types - Sized(), SomeSized(..), - instLL, instFunctor, ListLikeF, - withListLikeF, withListLikeF', - -- * Accessors - -- ** Length information - length, sLength, null, - -- ** Indexing - (!!), (%!!), index, sIndex, head, last, - uncons, uncons', unsnoc, unsnoc', - -- ** Slicing - tail, init, take, takeAtMost, drop, splitAt, splitAtMost, - -- * Construction - -- ** Initialisation - empty, singleton, toSomeSized, replicate, replicate', generate, - -- ** Concatenation - cons, (<|), snoc, (|>), append, (++), concat, - -- ** Zips - zip, zipSame, zipWith, zipWithSame, unzip, - -- * Transformation - map, fmap, reverse, intersperse, nub, sort, sortBy, insert, insertBy, - -- * Conversion - -- ** List - toList, fromList, fromList', unsafeFromList, unsafeFromList', - fromListWithDefault, fromListWithDefault', - -- ** Base container - unsized, - toSized, toSized', unsafeToSized, unsafeToSized', - toSizedWithDefault, toSizedWithDefault', - -- * Querying - -- ** Partitioning - Partitioned(..), - takeWhile, dropWhile, span, break, partition, - -- ** Searching - elem, notElem, find, findF, findIndex, findIndexIF, - sFindIndex, sFindIndexIF, - findIndices, findIndicesIF, sFindIndices, sFindIndicesIF, - elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices, - -- * Views and Patterns - -- $ViewsAndPatterns - - -- ** Views - -- $views - - -- ** Patterns - -- $patterns - - -- ** Definitions - viewCons, ConsView (..), viewSnoc, SnocView(..), - - pattern (:<), pattern NilL , pattern (:>), pattern NilR, - ) where - -import Data.Sized.Internal - -import Control.Applicative ((<$>), (<*>), ZipList(..)) -import Control.Lens.Indexed (FoldableWithIndex (..), ifind) -import Data.Foldable (Foldable) -import qualified Data.Foldable as F -import Data.Kind (Type) -import qualified Data.List as L -import Data.ListLike (ListLike) -import qualified Data.ListLike as LL -import qualified Data.MonoTraversable as MT -import Data.Monoid (Endo (..), First (..)) -import qualified Data.Sequence as Seq -import Data.Singletons.TypeLits (withKnownNat) -import Data.Singletons.Prelude (PNum (..), POrd (..), SOrd (..)) -import Data.Singletons.Prelude (Sing (..), SingI (..)) -import Data.Singletons.Prelude (withSing, withSingI) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import Data.Type.Monomorphic (Monomorphic (..)) -import Data.Type.Monomorphic (Monomorphicable (..)) -import qualified Data.Type.Natural as Peano -import Data.Type.Natural.Class -import Data.Type.Ordinal (HasOrdinal, Ordinal (..), enumOrdinal) -import Data.Type.Ordinal (ordToInt, unsafeFromInt) -import Data.Typeable (Typeable) -import qualified Data.Vector as V -import qualified Data.Vector.Storable as SV -import qualified Data.Vector.Unboxed as UV -import qualified GHC.TypeLits as TL -import Prelude (Bool (..), Enum (..), Eq (..)) -import Prelude (Functor, Int, Maybe (..)) -import Prelude (Num (..), Ord (..), Ordering) -import Prelude (Show (..), flip, fst, ($), (.)) -import qualified Prelude as P -import Unsafe.Coerce (unsafeCoerce) - --------------------------------------------------------------------------------- --- Main data-types --------------------------------------------------------------------------------- - --- | 'Sized' vector with the length is existentially quantified. --- This type is used mostly when the return type's length cannot --- be statically determined beforehand. --- --- @SomeSized sn xs :: SomeSized f a@ stands for the 'Sized' sequence --- @xs@ of element type @a@ and length @sn@. --- --- Since 0.1.0.0 -data SomeSized f nat a where - SomeSized :: (ListLike (f a) a) - => Sing n - -> Sized f (n :: nat) a - -> SomeSized f nat a - -deriving instance Typeable SomeSized - -instance Show (f a) => Show (SomeSized f nat a) where - showsPrec d (SomeSized _ s) = P.showParen (d > 9) $ - P.showString "SomeSized _ " . showsPrec 10 s -instance Eq (f a) => Eq (SomeSized f nat a) where - (SomeSized _ (Sized xs)) == (SomeSized _ (Sized ys)) = xs == ys - -demote' :: HasOrdinal nat => Sing (n :: nat) -> MonomorphicRep (Sing :: nat -> Type) -demote' = demote . Monomorphic -{-# SPECIALISE demote' :: Sing (n :: TL.Nat) -> P.Integer #-} -{-# SPECIALISE demote' :: Sing (n :: Peano.Nat) -> P.Integer #-} - --------------------------------------------------------------------------------- --- Accessors --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- Length infromation --------------------------------------------------------------------------------- - --- | Returns the length of wrapped containers. --- If you use @unsafeFromList@ or similar unsafe functions, --- this function may return different value from type-parameterized length. --- --- Since 0.1.0.0 -length :: ListLike (f a) a => Sized f n a -> Int -length = LL.length . runSized -{-# INLINE [1] length #-} -{-# RULES -"length/0" [~1] forall (xs :: Sized f 0 a). - length xs = 0 -"length/Z" [~1] forall (xs :: Sized f 'Peano.Z a). - length xs = 0 - #-} - --- | @Sing@ version of 'length'. --- --- Since 0.2.0.0 -sLength :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sized f n a -> Sing n -sLength (Sized xs) = - case promote (P.fromIntegral $ LL.length xs) of - Monomorphic (n :: Sing (k :: nat)) -> unsafeCoerce n -{-# INLINE[2] sLength #-} -{-# RULES -"sLength/KnownNat" [~1] forall (xs :: TL.KnownNat n => Sized f n a). - sLength xs = sing :: Sing n -"sLength/SingI" [~2] forall (xs :: SingI n => Sized f n a). - sLength xs = sing :: Sing n - #-} - --- | Test if the sequence is empty or not. --- --- Since 0.1.0.0 -null :: ListLike (f a) a => Sized f n a -> Bool -null = LL.null . runSized -{-# INLINE CONLIKE [1] null #-} -{-# RULES -"null/0" [~1] forall (xs :: Sized f 0 a). - null xs = True - -"null/Z" [~1] forall (xs :: Sized f 'Peano.Z a). - null xs = True -#-} - --------------------------------------------------------------------------------- ---- Indexing --------------------------------------------------------------------------------- - --- | (Unsafe) indexing with @Int@s. --- If you want to check boundary statically, use '%!!' or 'sIndex'. --- --- Since 0.1.0.0 -(!!) :: (ListLike (f a) a) => Sized f (Succ m) a -> Int -> a -Sized xs !! n = LL.index xs n -{-# INLINE (!!) #-} - --- | Safe indexing with 'Ordinal's. --- --- Since 0.1.0.0 -(%!!) :: (HasOrdinal nat, LL.ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c -Sized xs %!! n = LL.index xs $ P.fromIntegral $ ordToInt n -{-# INLINE (%!!) #-} -{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-} -{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-} - --- | Flipped version of '!!'. --- --- Since 0.1.0.0 -index :: (ListLike (f a) a) => Int -> Sized f (Succ m) a -> a -index n (Sized xs) = LL.index xs n -{-# INLINE index #-} - --- | Flipped version of '%!!'. --- --- Since 0.1.0.0 -sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c -sIndex = flip (%!!) -{-# INLINE sIndex #-} - --- | Take the first element of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ 'True) => Sized f n a -> b -head = LL.head . runSized -{-# INLINE head #-} - --- | Take the last element of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -last :: (HasOrdinal nat, (Zero nat :< n) ~ 'True, ListLike (f a) b) => Sized f n a -> b -last = LL.last . runSized -{-# INLINE last #-} - --- | Take the 'head' and 'tail' of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a) -uncons = ((,) <$> LL.head <*> Sized . LL.tail) . runSized -{-# INLINE [1] uncons #-} -{-# RULES -"uncons/[]" [~1] forall (x :: a) (xs:: [a]). - uncons (Sized (x : xs)) = (x, Sized xs) -"uncons/Seq" [~1] forall (xs:: Seq.Seq a). - uncons (Sized xs) = - case Seq.viewl xs of { (x Seq.:< ys) -> (x, Sized ys) - ; _ -> P.error "Empty seq with non-zero index!" - } - #-} - -uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a) -uncons' _ = uncons -{-# INLINE uncons' #-} - --- | Take the 'init' and 'last' of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b) -unsnoc = ((,) <$> Sized . LL.init <*> LL.last) . runSized -{-# NOINLINE [1] unsnoc #-} -{-# RULES -"unsnoc/Seq" [~1] forall (xs:: Seq.Seq a). - unsnoc (Sized xs) = - case Seq.viewr xs of { (ys Seq.:> x) -> (Sized ys, x) - ; _ -> P.error "Empty seq with non-zero index!" - } - #-} - -unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b) -unsnoc' _ = unsnoc -{-# INLINE unsnoc' #-} - - --------------------------------------------------------------------------------- ---- Slicing --------------------------------------------------------------------------------- - --- | Take the tail of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -tail :: (HasOrdinal nat, ListLike (f a) a)=> Sized f (Succ n) a -> Sized f (n :: nat) a -tail = Sized . LL.tail . runSized -{-# INLINE tail #-} - --- | Take the initial segment of non-empty sequence. --- If you want to make case-analysis for general sequence, --- see <#ViewsAndPatterns Views and Patterns> section. --- --- Since 0.1.0.0 -init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a -init = Sized . LL.init . runSized -{-# INLINE init #-} - --- | @take k xs@ takes first @k@ element of @xs@ where --- the length of @xs@ should be larger than @k@. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -take :: (ListLike (f a) a, (n :<= m) ~ 'True, HasOrdinal nat) - => Sing (n :: nat) -> Sized f m a -> Sized f n a -take sn = Sized . LL.genericTake (demote' sn) . runSized -{-# INLINE take #-} - --- | @take k xs@ takes first @k@ element of @xs@ at most. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -takeAtMost :: (ListLike (f a) a, HasOrdinal nat) - => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a -takeAtMost sn = Sized . LL.genericTake (demote $ Monomorphic sn) . runSized -{-# INLINE takeAtMost #-} - --- | @drop k xs@ drops first @k@ element of @xs@ and returns --- the rest of sequence, where the length of @xs@ should be larger than @k@. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -drop :: (HasOrdinal nat, ListLike (f a) a, (n :<= m) ~ 'True) - => Sing (n :: nat) -> Sized f m a -> Sized f (m :- n) a -drop sn = Sized . LL.genericDrop (demote' sn) . runSized -{-# INLINE drop #-} - --- | @splitAt k xs@ split @xs@ at @k@, where --- the length of @xs@ should be less than or equal to @k@. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -splitAt :: (ListLike (f a) a , (n :<= m) ~ 'True, HasOrdinal nat) - => Sing (n :: nat) -> Sized f m a -> (Sized f n a, Sized f (m :-. n) a) -splitAt n (Sized xs) = - let (as, bs) = LL.genericSplitAt (demote' n) xs - in (Sized as, Sized bs) -{-# INLINE splitAt #-} - --- | @splitAtMost k xs@ split @xs@ at @k@. --- If @k@ exceeds the length of @xs@, then the second result value become empty. --- It is really sad, that this function --- takes at least O(k) regardless of base container. --- --- Since 0.1.0.0 -splitAtMost :: (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> Sized f m a -> (Sized f (Min n m) a, Sized f (m :-. n) a) -splitAtMost n (Sized xs) = - let (as, bs) = LL.genericSplitAt (demote' n) xs - in (Sized as, Sized bs) -{-# INLINE splitAtMost #-} - - --------------------------------------------------------------------------------- --- Construction --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- Initialisation --------------------------------------------------------------------------------- - --- | Empty sequence. --- --- Since 0.1.0.0 -empty :: forall f a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a -empty = Sized LL.empty -{-# INLINE empty #-} - --- | Sequence with one element. --- --- Since 0.1.0.0 -singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a -singleton = Sized . LL.singleton -{-# INLINE singleton #-} - --- | Consruct the 'Sized' sequence from base type, but --- the length parameter is dynamically determined and --- existentially quantified; see also 'SomeSized'. --- --- Since 0.1.0.0 -toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a) - => f a -> SomeSized f nat a -toSomeSized = \xs -> - case promote $ LL.genericLength xs of - Monomorphic sn -> withSingI sn $ SomeSized sn $ unsafeToSized sn xs - --- | Replicates the same value. --- --- Since 0.1.0.0 -replicate :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sing n -> a -> Sized f n a -replicate sn a = Sized $ LL.genericReplicate (demote $ Monomorphic sn) a -{-# INLINE replicate #-} - --- | 'replicate' with the length inferred. --- --- Since 0.1.0.0 -replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a -replicate' = withSing replicate -{-# INLINE replicate' #-} - -generate :: forall (nat :: Type) (n :: nat) (a :: Type) f. - (ListLike (f a) a, HasOrdinal nat) - => Sing n -> (Ordinal n -> a) -> Sized f n a -generate n f = unsafeFromList n [f i | i <- enumOrdinal n ] -{-# INLINE [1] generate #-} -{-# RULES -"generate/Vector" [~1] forall (n :: (HasOrdinal nat) => Sing (n :: nat)) (f :: Ordinal n -> a). - generate (n :: Sing (n :: (nat :: Type))) f = withSingI n $ Sized (V.generate (fromSing' n) (f . toEnum)) -"generate/SVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) - (f :: SV.Storable a => Ordinal n -> a). - generate n f = withSingI n $ Sized (SV.generate (fromSing' n) (f . toEnum)) -"generate/SVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) - (f :: UV.Unbox a => Ordinal n -> a). - generate n f = withSingI n $ Sized (UV.generate (fromSing' n) (f . toEnum)) -"generate/Seq" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat)) - (f :: Ordinal n -> a). - generate n f = withSingI n $ Sized (Seq.fromFunction (fromSing' n) (f . toEnum)) -#-} - -fromSing' :: HasOrdinal nat => Sing (n :: nat) -> Int -fromSing' = P.fromIntegral . demote . Monomorphic - --------------------------------------------------------------------------------- ---- Concatenation --------------------------------------------------------------------------------- - --- | Append an element to the head of sequence. --- --- Since 0.1.0.0 -cons :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a -cons a = Sized . LL.cons a . runSized -{-# INLINE cons #-} - --- | Infix version of 'cons'. --- --- Since 0.1.0.0 -(<|) :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a -(<|) = cons -{-# INLINE (<|) #-} -infixr 5 <| - --- | Append an element to the tail of sequence. --- --- Since 0.1.0.0 -snoc :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a -snoc (Sized xs) a = Sized $ LL.snoc xs a -{-# INLINE snoc #-} - --- | Infix version of 'snoc'. --- --- Since 0.1.0.0 -(|>) :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a -(|>) = snoc -{-# INLINE (|>) #-} -infixl 5 |> - --- | Append two lists. --- --- Since 0.1.0.0 -append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a -append (Sized xs) (Sized ys) = Sized $ LL.append xs ys -{-# INLINE append #-} - --- | Infix version of 'append'. --- --- Since 0.1.0.0 -(++) :: (ListLike (f a) a) => Sized f n a -> Sized f m a -> Sized f (n :+ m) a -(++) = append -infixr 5 ++ - --- | Concatenates multiple sequences into one. --- --- Since 0.1.0.0 -concat :: forall f f' m n a. (Functor f', Foldable f', ListLike (f a) a) - => Sized f' m (Sized f n a) -> Sized f (m :* n) a -concat = Sized . F.foldr LL.append LL.empty . P.fmap runSized -{-# INLINE [2] concat #-} - -{-# RULES -"concat/list-list" [~1] forall (xss :: [Sized [] n a]). - concat (Sized xss) = Sized (L.concatMap runSized xss) -"concat/list-list" [~2] forall (xss :: (ListLike (f a) a, ListLike (f (Sized f n a)) (Sized f n a)) - => f (Sized f n a)). - concat (Sized xss) = Sized (LL.concatMap runSized xss) - #-} - --------------------------------------------------------------------------------- ---- Zips --------------------------------------------------------------------------------- - --- | Zipping two sequences. Length is adjusted to shorter one. --- --- Since 0.1.0.0 -zip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) - => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) -zip (Sized xs) (Sized ys) = Sized $ LL.zip xs ys -{-# INLINE [1] zip #-} -{-# RULES -"zip/Seq" [~1] forall xs ys. - zip (Sized xs) (Sized ys) = Sized (Seq.zip xs ys) -"zip/List" [~1] forall xs ys. - zip (Sized xs) (Sized ys) = Sized (P.zip xs ys) -"zip/Vector" [~1] forall xs ys. - zip (Sized xs) (Sized ys) = Sized (V.zip xs ys) -"zip/UVector" [~1] - forall (xs :: UV.Unbox a => UV.Vector a) (ys :: UV.Unbox b => UV.Vector b). - zip (Sized xs) (Sized ys) = Sized (UV.zip xs ys) - #-} - --- | 'zip' for the sequences of the same length. --- --- Since 0.1.0.0 -zipSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) - => Sized f n a -> Sized f n b -> Sized f n (a, b) -zipSame (Sized xs) (Sized ys) = Sized $ LL.zip xs ys -{-# INLINE [1] zipSame #-} -{-# RULES -"zipSame/Seq" [~1] forall xs ys. - zipSame (Sized xs) (Sized ys) = Sized (Seq.zip xs ys) -"zipSame/List" [~1] forall xs ys. - zipSame (Sized xs) (Sized ys) = Sized (P.zip xs ys) -"zipSame/Vector" [~1] forall xs ys. - zipSame (Sized xs) (Sized ys) = Sized (V.zip xs ys) -"zipSame/UVector" [~1] - forall (xs :: UV.Unbox a => UV.Vector a) (ys :: UV.Unbox b => UV.Vector b). - zipSame (Sized xs) (Sized ys) = Sized (UV.zip xs ys) - #-} - --- | Zipping two sequences with funtion. Length is adjusted to shorter one. --- --- Since 0.1.0.0 -zipWith :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) - => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c -zipWith f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys -{-# INLINE [1] zipWith #-} - -{-# RULES -"zipWith/Seq" [~1] forall f xs ys. - zipWith f (Sized xs) (Sized ys) = Sized (Seq.zipWith f xs ys) -"zipWith/List" [~1] forall f xs ys. - zipWith f (Sized xs) (Sized ys) = Sized (P.zipWith f xs ys) -"zipWith/Vector" [~1] forall f xs ys. - zipWith f (Sized xs) (Sized ys) = Sized (V.zipWith f xs ys) -"zipWith/UVector" [~1] - forall (f :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) => a -> b -> c) - xs ys. - zipWith f (Sized xs) (Sized ys) = Sized (UV.zipWith f xs ys) -"zipWith/MVector" [~1] - forall (f :: (SV.Storable a, SV.Storable b, SV.Storable c) => a -> b -> c) - xs ys. - zipWith f (Sized xs) (Sized ys) = Sized (SV.zipWith f xs ys) - #-} - --- | 'zipWith' for the sequences of the same length. --- --- Since 0.1.0.0 -zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) - => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c -zipWithSame f (Sized xs) (Sized ys) = Sized $ LL.zipWith f xs ys -{-# INLINE [1] zipWithSame #-} - -{-# RULES -"zipWithSame/Seq" [~1] forall f xs ys. - zipWithSame f (Sized xs) (Sized ys) = Sized (Seq.zipWith f xs ys) -"zipWithSame/List" [~1] forall f xs ys. - zipWithSame f (Sized xs) (Sized ys) = Sized (P.zipWith f xs ys) -"zipWithSame/Vector" [~1] forall f xs ys. - zipWithSame f (Sized xs) (Sized ys) = Sized (V.zipWith f xs ys) -"zipWithSame/UVector" [~1] - forall (f :: (UV.Unbox a, UV.Unbox b, UV.Unbox c) => a -> b -> c) - xs ys. - zipWithSame f (Sized xs) (Sized ys) = Sized (UV.zipWith f xs ys) -"zipWithSame/MVector" [~1] - forall (f :: (SV.Storable a, SV.Storable b, SV.Storable c) => a -> b -> c) - xs ys. - zipWithSame f (Sized xs) (Sized ys) = Sized (SV.zipWith f xs ys) - #-} - --- | Unzipping the sequence of tuples. --- --- Since 0.1.0.0 -unzip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a,b)) - => Sized f n (a, b) -> (Sized f n a, Sized f n b) -unzip (Sized xys) = - let (xs, ys) = LL.unzip xys - in (Sized xs, Sized ys) -{-# INLINE unzip #-} - - --------------------------------------------------------------------------------- --- Transformation --------------------------------------------------------------------------------- - --- | Map function. --- --- Since 0.1.0.0 -map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b -map f = Sized . LL.map f . runSized -{-# INLINE map #-} - -fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b -fmap f = Sized . P.fmap f . runSized -{-# INLINE fmap #-} - --- | Reverse function. --- --- Since 0.1.0.0 -reverse :: ListLike (f a) a => Sized f n a -> Sized f n a -reverse = Sized . LL.reverse . runSized -{-# INLINE reverse #-} - --- | Intersperces. --- --- Since 0.1.0.0 -intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a -intersperse a = Sized . LL.intersperse a . runSized -{-# INLINE intersperse #-} - --- | Remove all duplicates. --- --- Since 0.1.0.0 -nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a -nub = toSomeSized . LL.nub . runSized - --- | Sorting sequence by ascending order. --- --- Since 0.1.0.0 -sort :: (ListLike (f a) a, Ord a) - => Sized f n a -> Sized f n a -sort = Sized . LL.sort . runSized - --- | Generalized version of 'sort'. --- --- Since 0.1.0.0 -sortBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a -sortBy cmp = Sized . LL.sortBy cmp . runSized - --- | Insert new element into the presorted sequence. --- --- Since 0.1.0.0 -insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a -insert a = Sized . LL.insert a . runSized - --- | Generalized version of 'insert'. --- --- Since 0.1.0.0 -insertBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a -insertBy cmp a = Sized . LL.insertBy cmp a . runSized - - --------------------------------------------------------------------------------- --- Conversion --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- List --------------------------------------------------------------------------------- - --- | Convert to list. --- --- Since 0.1.0.0 -toList :: ListLike (f a) a => Sized f n a -> [a] -toList = LL.toList . runSized -{-# INLINE [2] toList #-} - -{-# RULES -"toList/" forall (xs :: Sized [] a n). - Data.Sized.toList xs = runSized xs - #-} - --- | If the given list is shorter than @n@, then returns @Nothing@ --- Otherwise returns @Sized f n a@ consisting of initial @n@ element --- of given list. --- --- Since 0.1.0.0 -fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> [a] -> Maybe (Sized f n a) -fromList Zero _ = Just $ Sized (LL.empty :: f a) -fromList sn xs = - let len = P.fromIntegral $ demote $ Monomorphic sn - in if P.length xs < len - then Nothing - else Just $ unsafeFromList sn $ P.take len xs -{-# INLINABLE [2] fromList #-} - --- | 'fromList' with the result length inferred. --- --- Since 0.1.0.0 -fromList' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => [a] -> Maybe (Sized f n a) -fromList' = withSing fromList -{-# INLINE fromList' #-} - --- | Unsafe version of 'fromList'. If the length of the given list does not --- equal to @n@, then something unusual happens. --- --- Since 0.1.0.0 -unsafeFromList :: forall (nat :: Type) f (n :: nat) a. ListLike (f a) a => Sing n -> [a] -> Sized f n a -unsafeFromList _ xs = Sized $ LL.fromList xs -{-# INLINE [1] unsafeFromList #-} -{-# RULES -"unsafeFromList/List" [~1] forall s xs. - unsafeFromList s xs = Sized xs -"unsafeFromList/Vector" [~1] forall s (xs :: [a]). - unsafeFromList s xs = Sized (V.fromList xs) -"unsafeFromList/Seq" [~1] forall s (xs :: [a]). - unsafeFromList s xs = Sized (Seq.fromList xs) -"unsafeFromList/SVector" [~1] forall s (xs :: SV.Storable a => [a]). - unsafeFromList s xs = Sized (SV.fromList xs) -"unsafeFromList/UVector" [~1] forall s (xs :: UV.Unbox a => [a]). - unsafeFromList s xs = Sized (UV.fromList xs) - #-} - --- | 'unsafeFromList' with the result length inferred. --- --- Since 0.1.0.0 -unsafeFromList' :: (SingI (n :: TL.Nat), ListLike (f a) a) => [a] -> Sized f n a -unsafeFromList' = withSing unsafeFromList -{-# INLINE [1] unsafeFromList' #-} -{-# RULES -"unsafeFromList'/List" [~1] forall xs. - unsafeFromList' xs = Sized xs -"unsafeFromList'/Vector" [~1] forall (xs :: [a]). - unsafeFromList' xs = Sized (V.fromList xs) -"unsafeFromList'/Seq" [~1] forall (xs :: [a]). - unsafeFromList' xs = Sized (Seq.fromList xs) -"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]). - unsafeFromList' xs = Sized (SV.fromList xs) -"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]). - unsafeFromList' xs = Sized (UV.fromList xs) - #-} - - --- | Construct a @Sized f n a@ by padding default value if the given list is short. --- --- Since 0.1.0.0 -fromListWithDefault :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sing n -> a -> [a] -> Sized f n a -fromListWithDefault sn def xs = - let len = demote' sn - in Sized $ LL.fromList (L.genericTake len xs) `LL.append` LL.genericReplicate (len - L.genericLength xs) def -{-# INLINABLE fromListWithDefault #-} - --- | 'fromListWithDefault' with the result length inferred. --- --- Since 0.1.0.0 -fromListWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> [a] -> Sized f n a -fromListWithDefault' = withSing fromListWithDefault -{-# INLINE fromListWithDefault' #-} - --------------------------------------------------------------------------------- ---- Base containes --------------------------------------------------------------------------------- - --- | Forget the length and obtain the wrapped base container. --- --- Since 0.1.0.0 -unsized :: Sized f n a -> f a -unsized = runSized -{-# INLINE unsized #-} - --- | If the length of the input is shorter than @n@, then returns @Nothing@. --- Otherwise returns @Sized f n a@ consisting of initial @n@ element --- of the input. --- --- Since 0.1.0.0 -toSized :: (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> f a -> Maybe (Sized f n a) -toSized sn xs = - let len = demote' sn - in if LL.genericLength xs < len - then Nothing - else Just $ unsafeToSized sn $ LL.genericTake len xs -{-# INLINABLE [2] toSized #-} - --- | 'toSized' with the result length inferred. --- --- Since 0.1.0.0 -toSized' :: (ListLike (f a) a, SingI (n :: TL.Nat)) => f a -> Maybe (Sized f n a) -toSized' = withSing toSized -{-# INLINE toSized' #-} - --- | Unsafe version of 'toSized'. If the length of the given list does not --- equal to @n@, then something unusual happens. --- --- Since 0.1.0.0 -unsafeToSized :: Sing n -> f a -> Sized f n a -unsafeToSized _ = Sized -{-# INLINE [2] unsafeToSized #-} - --- | 'unsafeToSized' with the result length inferred. --- --- Since 0.1.0.0 -unsafeToSized' :: (SingI (n :: TL.Nat), ListLike (f a) a) => f a -> Sized f n a -unsafeToSized' = withSing unsafeToSized -{-# INLINE unsafeToSized' #-} - --- | Construct a @Sized f n a@ by padding default value if the given list is short. --- --- Since 0.1.0.0 -toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a) - => Sing (n :: nat) -> a -> f a -> Sized f n a -toSizedWithDefault sn def xs = - let len = P.fromIntegral $ demote (Monomorphic sn) - in Sized $ LL.take len xs `LL.append` LL.replicate (len - LL.length xs) def -{-# INLINABLE toSizedWithDefault #-} - --- | 'toSizedWithDefault' with the result length inferred. --- --- Since 0.1.0.0 -toSizedWithDefault' :: (SingI (n :: TL.Nat), ListLike (f a) a) => a -> f a -> Sized f n a -toSizedWithDefault' = withSing toSizedWithDefault -{-# INLINE toSizedWithDefault' #-} - - --------------------------------------------------------------------------------- --- Querying --------------------------------------------------------------------------------- - --------------------------------------------------------------------------------- ---- Partitioning --------------------------------------------------------------------------------- - --- | The type @Partitioned f n a@ represents partitioned sequence of length @n@. --- Value @Partitioned lenL ls lenR rs@ stands for: --- --- * Entire sequence is divided into @ls@ and @rs@, and their length --- are @lenL@ and @lenR@ resp. --- --- * @lenL + lenR = n@ --- --- Since 0.1.0.0 -data Partitioned f n a where - Partitioned :: (ListLike (f a) a) - => Sing n - -> Sized f (n :: TL.Nat) a - -> Sing m - -> Sized f (m :: TL.Nat) a - -> Partitioned f (n :+ m) a - --- | Take the initial segment as long as elements satisfys the predicate. --- --- Since 0.1.0.0 -takeWhile :: (HasOrdinal nat, ListLike (f a) a) - => (a -> Bool) -> Sized f n a -> SomeSized f nat a -takeWhile p = toSomeSized . LL.takeWhile p . runSized -{-# INLINE takeWhile #-} - --- | Drop the initial segment as long as elements satisfys the predicate. --- --- Since 0.1.0.0 -dropWhile :: (HasOrdinal nat, ListLike (f a) a) - => (a -> Bool) -> Sized f n a -> SomeSized f nat a -dropWhile p = toSomeSized . LL.dropWhile p . runSized -{-# INLINE dropWhile #-} - --- | Invariant: @'ListLike' (f a) a@ instance must be implemented --- to satisfy the following property: --- @length (fst (span p xs)) + length (snd (span p xs)) == length xs@ --- Otherwise, this function introduces severe contradiction. --- --- Since 0.1.0.0 -span :: ListLike (f a) a - => (a -> Bool) -> Sized f n a -> Partitioned f n a -span p xs = - let (as, bs) = LL.span p $ runSized xs - in case (toSomeSized as, toSomeSized bs) of - (SomeSized lenL ls, SomeSized lenR rs) -> - unsafeCoerce $ Partitioned lenL ls lenR rs -{-# INLINE span #-} - --- | Invariant: @'ListLike' (f a) a@ instance must be implemented --- to satisfy the following property: --- @length (fst (break p xs)) + length (snd (break p xs)) == length xs@ --- Otherwise, this function introduces severe contradiction. --- --- Since 0.1.0.0 -break :: ListLike (f a) a - => (a -> Bool) -> Sized f n a -> Partitioned f n a -break p (Sized xs) = - let (as, bs) = LL.break p xs - in case (toSomeSized as, toSomeSized bs) of - (SomeSized lenL ls, SomeSized lenR rs) -> - unsafeCoerce $ Partitioned lenL ls lenR rs -{-# INLINE break #-} - --- | Invariant: @'ListLike' (f a) a@ instance must be implemented --- to satisfy the following property: --- @length (fst (partition p xs)) + length (snd (partition p xs)) == length xs@ --- Otherwise, this function introduces severe contradiction. --- --- Since 0.1.0.0 -partition :: ListLike (f a) a - => (a -> Bool) -> Sized f n a -> Partitioned f n a -partition p (Sized xs) = - let (as, bs) = LL.partition p xs - in case (toSomeSized as, toSomeSized bs) of - (SomeSized lenL ls, SomeSized lenR rs) -> - unsafeCoerce $ Partitioned lenL ls lenR rs -{-# INLINE partition #-} - --------------------------------------------------------------------------------- ---- Searching --------------------------------------------------------------------------------- --- | Membership test; see also 'notElem'. --- --- Since 0.1.0.0 -elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool -elem a = LL.elem a . runSized -{-# INLINE elem #-} - --- | Negation of 'elem'. --- --- Since 0.1.0.0 -notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool -notElem a = LL.notElem a . runSized -{-# INLINE notElem #-} - --- | Find the element satisfying the predicate. --- --- Since 0.1.0.0 -find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a -find p = F.find p -{-# INLINE[1] find #-} -{-# RULES -"find/List" [~1] forall p (xs :: [a]). - find p (Sized xs) = L.find p xs -"find/Vector" [~1] forall p xs. - find p (Sized xs) = V.find p xs -"find/Storable Vector" [~1] forall p (xs :: SV.Storable a => SV.Vector a). - find p (Sized xs) = SV.find p xs -"find/Unboxed Vector" [~1] forall p (xs :: UV.Unbox a => UV.Vector a). - find p (Sized xs) = UV.find p xs - #-} - --- | @'Foldable'@ version of @'find'@. -findF :: (Foldable f) => (a -> Bool) -> Sized f n a -> Maybe a -findF p = getFirst. F.foldMap (\a -> if p a then First (Just a) else First Nothing) . runSized -{-# INLINE [1] findF #-} -{-# SPECIALISE [0] findF :: (a -> Bool) -> Sized Seq.Seq n a -> Maybe a #-} -{-# RULES -"findF/list" [~1] forall p. - findF p = L.find p - #-} - --- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists. --- --- Since 0.1.0.0 -findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int -findIndex p = LL.findIndex p . runSized -{-# INLINE findIndex #-} - --- | 'Ordinal' version of 'findIndex'. --- --- Since 0.1.0.0 -sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) - => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) -sFindIndex p = P.fmap toEnum . findIndex p -{-# INLINE sFindIndex #-} - --- | @'findIndex'@ implemented in terms of @'FoldableWithIndex'@ -findIndexIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> Maybe i -findIndexIF p = P.fmap fst . ifind (P.const p) . runSized -{-# INLINE [1] findIndexIF #-} -{-# RULES -"findIndexIF/list" [~1] forall p. - findIndexIF p = L.findIndex p . runSized -"findIndexIF/vector" [~1] forall p. - findIndexIF p = V.findIndex p . runSized - #-} - --- | @'sFindIndex'@ implemented in terms of @'FoldableWithIndex'@ -sFindIndexIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n) - => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n) -sFindIndexIF p = P.fmap fst . ifind (P.const p) -{-# INLINE [1] sFindIndexIF #-} --- {-# RULES --- "sFindIndexIF/list" [~1] forall p . --- sFindIndexIF p = P.fmap toEnum . L.findIndex p . runSized --- "sFindIndexIF/vector" [~1] forall p. --- sFindIndexIF p = P.fmap toEnum . V.findIndex p . runSized --- #-} - --- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. --- --- Since 0.1.0.0 -findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int] -findIndices p = LL.findIndices p . runSized -{-# INLINE findIndices #-} -{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-} - --- | @'findIndices'@ implemented in terms of @'FoldableWithIndex'@ -findIndicesIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> [i] -findIndicesIF p = flip appEndo [] . ifoldMap (\i x -> if p x then Endo (i:) else Endo P.id) . runSized -{-# INLINE [1] findIndicesIF #-} -{-# RULES -"findIndicesIF/list" [~1] forall p. - findIndicesIF p = L.findIndices p . runSized -"findIndicesIF/vector" [~1] forall p. - findIndicesIF p = V.toList . V.findIndices p . runSized - #-} - - --- | 'Ordinal' version of 'findIndices'. --- --- Since 0.1.0.0 -sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) - => (a -> Bool) -> Sized f n a -> [Ordinal n] -sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p -{-# INLINE sFindIndices #-} - -sFindIndicesIF :: (FoldableWithIndex i f, P.Integral i, HasOrdinal nat, SingI n) - => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n] -sFindIndicesIF p = flip appEndo [] . - ifoldMap (\i x -> if p x then Endo (P.toEnum (P.fromIntegral i):) else Endo P.id) . - runSized -{-# INLINE [1] sFindIndicesIF #-} --- {-# RULES --- "sFindIndicesIF/list" [~1] forall p. --- sFindIndicesIF p = P.map toEnum . L.findIndices p . runSized --- "sFindIndicesIF/vector" [~1] forall p. --- sFindIndicesIF p = V.toList . V.map toEnum . V.findIndices p . runSized --- #-} - -{-# RULES -"Foldable.sum/Vector" - F.sum = V.sum . runSized -"MonoTraversable.sum/Vector" - MT.osum = V.sum . runSized - #-} - --- | Returns the index of the given element in the list, if exists. --- --- Since 0.1.0.0 -elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int -elemIndex a (Sized xs) = LL.elemIndex a xs -{-# INLINE elemIndex #-} - --- | Ordinal version of 'elemIndex' --- It statically checks boundary invariants. --- If you don't internal structure on @'Sized'@, --- then @'sUnsafeElemIndex'@ is much faster and --- also safe for most cases. --- --- Since 0.1.0.0 -sElemIndex :: forall (n :: nat) f a. - (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) - => a -> Sized f n a -> Maybe (Ordinal n) -sElemIndex a (Sized xs) = do - i <- LL.elemIndex a xs - case promote (P.fromIntegral i) of - Monomorphic sn -> - case sn %:< (sing :: Sing n) of - STrue -> Just (OLt sn) - SFalse -> Nothing -{-# INLINE sElemIndex #-} - -sUnsafeElemIndex :: forall (n :: nat) f a. - (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) - => a -> Sized f n a -> Maybe (Ordinal n) -sUnsafeElemIndex a (Sized xs) = - unsafeFromInt . P.fromIntegral <$> LL.elemIndex a xs - --- | Returns all indices of the given element in the list. --- --- Since 0.1.0.0 -elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int] -elemIndices a = LL.elemIndices a . runSized -{-# INLINE elemIndices #-} - --- | Ordinal version of 'elemIndices' --- --- Since 0.1.0.0 -sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a) - => a -> Sized f n a -> [Ordinal n] -sElemIndices p = P.fmap (unsafeFromInt . P.fromIntegral) . elemIndices p -{-# INLINE sElemIndices #-} - --------------------------------------------------------------------------------- --- Views and Patterns --------------------------------------------------------------------------------- - -{-$ViewsAndPatterns #ViewsAndPatterns# - - With GHC's @ViewPatterns@ and @PatternSynonym@ extensions, - we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor. - Curretnly, there are two direction view and patterns: Cons and Snoc. - Assuming underlying sequence type @f@ has O(1) implementation for 'LL.null', 'LL.head' - (resp. 'LL.last') and 'LL.tail' (resp. 'LL.init'), We can view and pattern-match on - cons (resp. snoc) of @Sized f n a@ in O(1). --} - -{-$views #views# - - With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows: - -@ -slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n -slen ('viewCons' -> 'NilCV') = 'SZ' -slen ('viewCons' -> _ '::-' as) = 'SS' (slen as) -slen _ = error "impossible" -@ - - The constraint @('SingI' n, 'ListLike (f a) a' f)@ is needed for view function. - In the above, we have extra wildcard pattern (@_@) at the last. - Code compiles if we removed it, but current GHC warns for incomplete pattern, - although we know first two patterns exhausts all the case. - - Equivalently, we can use snoc-style pattern-matching: - -@ -slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n -slen ('viewSnoc' -> 'NilSV') = 'SZ' -slen ('viewSnoc' -> as ':-::' _) = 'SS' (slen as) -@ --} - --- | View of the left end of sequence (cons-side). --- --- Since 0.1.0.0 -data ConsView f n a where - NilCV :: ConsView f (Zero nat) a - (::-) :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a - -infixr 5 ::- - --- | Case analysis for the cons-side of sequence. --- --- Since 0.1.0.0 -viewCons :: forall f a (n :: nat). (HasOrdinal nat, ListLike (f a) a) - => Sized f n a - -> ConsView f n a -viewCons sz = case zeroOrSucc (sLength sz) of - IsZero -> NilCV - IsSucc n' -> withSingI n' $ P.uncurry (::-) (uncons' n' sz) - --- | View of the left end of sequence (snoc-side). --- --- Since 0.1.0.0 -data SnocView f n a where - NilSV :: SnocView f (Zero nat) a - (:-::) :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a -infixl 5 :-:: - --- | Case analysis for the snoc-side of sequence. --- --- Since 0.1.0.0 -viewSnoc :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) - => Sized f n a - -> SnocView f n a -viewSnoc sz = case zeroOrSucc (sLength sz) of - IsZero -> NilSV - IsSucc n' -> - withSingI n' $ P.uncurry (:-::) (unsnoc' n' sz) - -{-$patterns #patterns# - - So we can pattern match on both end of sequence via views, but - it is rather clumsy to nest it. For example: - -@ -nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a -nextToHead ('viewCons' -> _ '::-' ('viewCons' -> a '::-' _)) = a -@ - - In such a case, with @PatternSynonyms@ extension we can write as follows: - -@ -nextToHead :: ('ListLike (f a) a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a -nextToHead (_ ':<' a ':<' _) = a -@ - - Of course, we can also rewrite above @slen@ example using @PatternSynonyms@: - -@ -slen :: ('SingI' n, 'ListLike (f a) a' f) => 'Sized' f n a -> 'Sing' n -slen 'NilL' = 'SZ' -slen (_ ':<' as) = 'SS' (slen as) -slen _ = error "impossible" -@ - - So, we can use @':<'@ and @'NilL'@ (resp. @':>'@ and @'NilR'@) to - pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. - @':<'@, @'NilL'@, @':>'@ and @'NilR'@ are neither functions nor data constructors, - but pattern synonyms so we cannot use them in expression contexts. - For more detail on pattern synonyms, see - - and - . --} - -infixr 5 :< --- | Pattern synonym for cons-side uncons. -pattern (:<) :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). - (n ~ Succ n1, SingI n1) - => a -> Sized f n1 a -> Sized f n a -pattern a :< as <- (viewCons -> a ::- as) where - a :< as = a <| as - -pattern NilL :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => (n ~ Zero nat) => Sized f n a -pattern NilL <- (viewCons -> NilCV) where - NilL = empty - -infixl 5 :> - -pattern (:>) :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). - (n ~ Succ n1, SingI n1) - => Sized f n1 a -> a -> Sized f n a -pattern a :> b <- (viewSnoc -> a :-:: b) where - a :> b = a |> b - -pattern NilR :: forall nat f (n :: nat) a. - (ListLike (f a) a, HasOrdinal nat) - => n ~ Zero nat => Sized f n a -pattern NilR <- (viewSnoc -> NilSV) where - NilR = empty - --- | Applicative instance, generalizing @'Data.Monoid.ZipList'@. -instance (Functor f, HasOrdinal nat, SingI n, ListLikeF f) - => P.Applicative (Sized f (n :: nat)) where - {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.Nat)) #-} - - pure (x :: a) = - withListLikeF (Nothing :: Maybe (f a)) $ - replicate' x - {-# INLINE pure #-} - - (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) = - withListLikeF (Nothing :: Maybe (f (a -> b))) $ - withListLikeF (Nothing :: Maybe (f a)) $ - withListLikeF (Nothing :: Maybe (f b)) $ - zipWithSame ($) fs xs - {-# INLINE [1] (<*>) #-} -{-# RULES -"<*>/List" [~1] forall fs xs. - Sized fs <*> Sized xs = Sized (getZipList (ZipList fs <*> ZipList xs)) -"<*>/Seq" [~1] forall fs xs. - Sized fs <*> Sized xs = Sized (Seq.zipWith ($) fs xs) -"<*>/Vector" [~1] forall fs xs. - Sized fs <*> Sized xs = Sized (V.zipWith ($) fs xs) - #-} diff --git a/Data/Sized/Builtin.hs b/Data/Sized/Builtin.hs deleted file mode 100644 --- a/Data/Sized/Builtin.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} -{-# LANGUAGE ViewPatterns #-} --- | This module exports @'S.Sized'@ type specialized to --- GHC's built-in type numeral @'TL.Nat'@. -module Data.Sized.Builtin - (Ordinal, Sized, module Data.Sized, - pattern (:<), pattern NilL, pattern (:>), pattern NilR) where -import Data.Sized hiding ((:<), (:>), NilL, NilR, Sized) -import qualified Data.Sized as S - -import Data.ListLike (ListLike) -import Data.Singletons.Prelude (SingI) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Ordinal as O -import qualified GHC.TypeLits as TL - -type Ordinal (n :: TL.Nat) = O.Ordinal n -type Sized f (n :: TL.Nat) = S.Sized f n - -pattern (:<) :: forall f (n :: TL.Nat) a. - (ListLike (f a) a) - => forall (n1 :: TL.Nat). - (n ~ Succ n1, SingI n1) - => a -> Sized f n1 a -> Sized f n a -pattern a :< b = a S.:< b -infixr 5 :< - -pattern NilL :: forall f (n :: TL.Nat) a. - (ListLike (f a) a) - => n ~ 0 => Sized f n a -pattern NilL = S.NilL - -pattern (:>) :: forall f (n :: TL.Nat) a. - (ListLike (f a) a) - => forall (n1 :: TL.Nat). - (n ~ Succ n1, SingI n1) - => Sized f n1 a -> a -> Sized f n a -pattern a :> b = a S.:> b -infixl 5 :> - -pattern NilR :: forall f (n :: TL.Nat) a. - (ListLike (f a) a, SingI n) - => n ~ 0 => Sized f n a -pattern NilR = S.NilR diff --git a/Data/Sized/Flipped.hs b/Data/Sized/Flipped.hs deleted file mode 100644 --- a/Data/Sized/Flipped.hs +++ /dev/null @@ -1,93 +0,0 @@ -{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} -{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PatternSynonyms #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies, TypeInType #-} -{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns #-} -module Data.Sized.Flipped (Flipped(..), - pattern (:<), pattern NilL, - pattern (:>), pattern NilR) where -import qualified Data.Sized as Orig -import Data.Sized.Internal - -import Control.DeepSeq (NFData(..)) -import Control.Lens.At (Index, IxValue, Ixed (..)) -import Control.Lens.TH (makeWrapped) -import Control.Lens.Wrapped (_Wrapped) -import Data.Hashable (Hashable (..)) -import Data.Kind (Type) -import qualified Data.ListLike as LL -import Data.MonoTraversable (Element, MonoFoldable (..)) -import Data.MonoTraversable (MonoFunctor (..)) -import Data.MonoTraversable (MonoTraversable (..)) -import qualified Data.Sequence as Seq -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Natural as PN -import Data.Type.Natural.Class (Zero) -import Data.Type.Ordinal (HasOrdinal, Ordinal (..)) -import Data.Typeable (Typeable) -import qualified Data.Vector as V -import qualified Data.Vector.Storable as SV -import qualified Data.Vector.Unboxed as UV -import qualified GHC.TypeLits as TL - --- | Wrapper for @'Sized'@ which takes length as its last element, instead of the second. --- --- Since 0.2.0.0 -newtype Flipped f a n = Flipped { runFlipped :: Sized f n a } - deriving (Show, Eq, Ord, Typeable, NFData, Hashable) - -makeWrapped ''Flipped - -type instance Index (Flipped f a n) = Ordinal n -type instance IxValue (Flipped f a n) = IxValue (f a) -type instance Element (Flipped f a n) = Element (Sized f n a) -deriving instance MonoFunctor (f a) => MonoFunctor (Flipped f a n) -deriving instance MonoFoldable (f a) => MonoFoldable (Flipped f a n) -instance (MonoTraversable (f a)) => MonoTraversable (Flipped f a n) where - otraverse = _Wrapped . otraverse - {-# INLINE otraverse #-} - - omapM = _Wrapped . omapM - {-# INLINE omapM #-} - -instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat) - => Ixed (Flipped f a (n :: nat)) where - {-# SPECIALISE instance Ixed (Flipped [] a (n :: TL.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped [] a (n :: PN.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-} - {-# SPECIALISE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-} - ix o = _Wrapped . ix o - {-# INLINE ix #-} - -pattern (:<) :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1) - => a -> Flipped f a n1 -> Flipped f a n -pattern a :< as <- Flipped (a Orig.:< (Flipped -> as)) where - a :< Flipped as = Flipped (a Orig.:< as) - -pattern NilL :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => n ~ Zero nat => Flipped f a n -pattern NilL = Flipped Orig.NilL - -pattern (:>) :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => forall (n1 :: nat). (n ~ Succ n1, PN.SingI n1) - => Flipped f a n1 -> a -> Flipped f a n -pattern as :> a <- Flipped ((Flipped -> as) Orig.:> a) where - Flipped as :> a = Flipped (as Orig.:> a) - -pattern NilR :: forall nat (f :: Type -> Type) (n :: nat) a. - (LL.ListLike (f a) a, HasOrdinal nat) - => n ~ Zero nat => Flipped f a n -pattern NilR = Flipped Orig.NilR diff --git a/Data/Sized/Internal.hs b/Data/Sized/Internal.hs deleted file mode 100644 --- a/Data/Sized/Internal.hs +++ /dev/null @@ -1,259 +0,0 @@ -{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable, DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable, EmptyDataDecls, ExplicitNamespaces #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} -{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-} -{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} -module Data.Sized.Internal - (Sized(..),instLL, instFunctor, ListLikeF, - withListLikeF, withListLikeF' - ) where -import Control.DeepSeq (NFData (..)) -import Control.Lens.At (Index, IxValue, Ixed (..)) -import Control.Lens.Indexed (FoldableWithIndex (..)) -import Control.Lens.Indexed (FunctorWithIndex (..)) -import Control.Lens.Indexed (TraversableWithIndex (..)) -import Data.Constraint ((:-) (..), (:=>) (..), Class (..)) -import Data.Constraint (Dict (..), trans, weaken1, weaken2) -import Data.Constraint ((&&&), (\\)) -import Data.Constraint.Forall (Forall, inst) -import Data.Foldable (Foldable) -import Data.Hashable (Hashable (..)) -import Data.Kind (Type) -import Data.ListLike (ListLike) -import Data.MonoTraversable (Element, MonoFoldable (..)) -import Data.MonoTraversable (MonoFunctor (..)) -import Data.MonoTraversable (MonoTraversable (..)) -import Data.Proxy (Proxy (..)) -import qualified Data.Sequence as Seq -import Data.Singletons.Prelude (SingI) -import Data.Traversable (Traversable) -import qualified Data.Type.Natural as PN -import Data.Type.Ordinal (HasOrdinal, Ordinal (..), ordToInt) -import Data.Type.Ordinal (unsafeFromInt) -import Data.Typeable (Typeable) -import qualified Data.Vector as V -import qualified Data.Vector.Storable as SV -import qualified Data.Vector.Unboxed as UV -import qualified GHC.TypeLits as TL - --- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version. --- --- Here, 'f' must be the instance of 'Functor' and @'ListLike' (f a) a@ for all @a@. --- This constraint is expressed by 'ListLikeF'. --- Folding and traversing function such as 'all' and 'foldl'' is available --- via 'Foldable' or 'Traversable' class, if 'f' is the instance of them. --- --- Since 0.2.0.0 -newtype Sized (f :: Type -> Type) (n :: nat) a = - Sized { runSized :: f a - } deriving (Eq, Ord, Typeable, - Functor, Foldable, Traversable) - -type instance Element (Sized f n a) = Element (f a) - --- | Since 0.2.0.0 -deriving instance MonoFoldable (f a) - => MonoFoldable (Sized f n a) - --- | Since 0.2.0.0 -deriving instance MonoFunctor (f a) - => MonoFunctor (Sized f n a) - --- | Since 0.2.0.0 -instance {-# OVERLAPPABLE #-} (MonoTraversable (f a)) - => MonoTraversable (Sized f n a) where - {-# SPECIALISE instance MonoTraversable (Sized [] n a) #-} - {-# SPECIALISE instance MonoTraversable (Sized V.Vector n a) #-} - {-# SPECIALISE instance MonoTraversable (Sized Seq.Seq n a) #-} - {-# SPECIALISE instance UV.Unbox a => MonoTraversable (Sized UV.Vector n a) #-} - {-# SPECIALISE instance SV.Storable a => MonoTraversable (Sized SV.Vector n a) #-} - otraverse f = fmap Sized . otraverse f . runSized - omapM f = fmap Sized . omapM f. runSized - --- | Since 0.2.0.0 -instance {-# OVERLAPS #-} SV.Storable a => MonoTraversable (Sized SV.Vector n a) where - otraverse f = fmap Sized . otraverse f . runSized - omapM f = fmap Sized . omapM f . runSized - --- | Since 0.2.0.0 -instance {-# OVERLAPS #-} UV.Unbox a => MonoTraversable (Sized UV.Vector n a) where - otraverse f = fmap Sized . otraverse f . runSized - omapM f = fmap Sized . omapM f . runSized - -deriving instance NFData (f a) => NFData (Sized f n a) -deriving instance Hashable (f a) => Hashable (Sized f n a) - -instance Show (f a) => Show (Sized f n a) where - showsPrec d (Sized x) = showsPrec d x - --- | Since 0.2.0.0 -type instance Index (Sized f n a) = Ordinal n - --- | Since 0.3.0.0 -type instance IxValue (Sized f n a) = IxValue (f a) -instance (Integral (Index (f a)), Ixed (f a), HasOrdinal nat) - => Ixed (Sized f (n :: nat) a) where - {-# SPECIALISE instance Ixed (Sized [] (n :: TL.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized [] (n :: PN.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized V.Vector (n :: TL.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized V.Vector (n :: PN.Nat) a) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: TL.Nat) a) #-} - {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: PN.Nat) a) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: TL.Nat) a) #-} - {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: PN.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: TL.Nat) a) #-} - {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: PN.Nat) a) #-} - {-# INLINE ix #-} - ix n f = fmap Sized . ix (fromIntegral $ ordToInt n) f . runSized - --- | Since 0.2.0.0 -instance (Integral i, FunctorWithIndex i f, HasOrdinal nat, SingI n) - => FunctorWithIndex (Ordinal (n :: nat)) (Sized f n) where - imap f = Sized . imap (f . unsafeFromInt . fromIntegral) . runSized - {-# INLINE imap #-} - {-# SPECIALISE instance TL.KnownNat n - => FunctorWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FunctorWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} - --- | Since 0.2.0.0 -instance (Integral i, FoldableWithIndex i f, HasOrdinal nat, SingI n) - => FoldableWithIndex (Ordinal (n :: nat)) (Sized f n) where - ifoldMap f = ifoldMap (f . unsafeFromInt . fromIntegral) . runSized - {-# INLINE ifoldMap #-} - - ifoldr f e = ifoldr (f . unsafeFromInt . fromIntegral) e . runSized - {-# INLINE ifoldr #-} - - ifoldl f e = ifoldl (f . unsafeFromInt . fromIntegral) e . runSized - {-# INLINE ifoldl #-} - - ifoldr' f e = ifoldr' (f . unsafeFromInt . fromIntegral) e . runSized - {-# INLINE ifoldr' #-} - - ifoldl' f e = ifoldl' (f . unsafeFromInt . fromIntegral) e . runSized - {-# INLINE ifoldl' #-} - - {-# SPECIALISE instance TL.KnownNat n - => FoldableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FoldableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} - --- | Since 0.2.0.0 -instance (Integral i, TraversableWithIndex i f, HasOrdinal nat, SingI n) - => TraversableWithIndex (Ordinal (n :: nat)) (Sized f n) where - itraverse f = fmap Sized . itraverse (f . unsafeFromInt . fromIntegral) . runSized - {-# INLINE itraverse #-} - - {-# SPECIALISE instance TL.KnownNat n - => TraversableWithIndex (Ordinal n) (Sized [] (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => TraversableWithIndex (Ordinal n) (Sized [] (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: PN.Nat)) #-} - {-# SPECIALISE instance TL.KnownNat n - => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: TL.Nat)) #-} - {-# SPECIALISE instance SingI n - => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: PN.Nat)) #-} - -class (ListLike (f a) a) => LLF f a -instance (ListLike (f a) a) => LLF f a - -instance Class (ListLike (f a) a) (LLF f a) where - cls = Sub Dict -instance (LLF f a) :=> (ListLike (f a) a) where - ins = Sub Dict - --- | Functor @f@ such that there is instance @ListLike (f a) a@ for any @a@. --- --- Since 0.1.0.0 -type ListLikeF f = (Functor f, Forall (LLF f)) - -instLLF :: forall f a. Forall (LLF f) :- ListLike (f a) a -instLLF = trans ins inst -{-# INLINE [1] instLLF #-} -{-# RULES -"instLLF/List" [~1] - instLLF = Sub Dict :: Forall (LLF []) :- ListLike [a] a -"instLLF/Seq" [~1] - instLLF = Sub Dict :: Forall (LLF Seq.Seq) :- ListLike (Seq.Seq a) a -"instLLF/Vector" [~1] - instLLF = Sub Dict :: Forall (LLF V.Vector) :- ListLike (V.Vector a) a - #-} - -instLL :: forall f a. ListLikeF f :- ListLike (f a) a -instLL = trans instLLF weaken2 -{-# INLINE [1] instLL #-} -{-# RULES -"instLL/List" [~1] - instLL = Sub Dict :: ListLikeF [] :- ListLike [a] a -"instLL/Seq" [~1] - instLL = Sub Dict :: ListLikeF Seq.Seq :- ListLike (Seq.Seq a) a -"instLL/Vector" [~1] - instLL = Sub Dict :: ListLikeF V.Vector :- ListLike (V.Vector a) a - #-} - - -instFunctor :: ListLikeF f :- Functor f -instFunctor = weaken1 -{-# INLINE [1] instFunctor #-} -{-# RULES -"instFunctor/List" [~1] - instFunctor = Sub Dict :: ListLikeF [] :- Functor [] -"instFunctor/Seq" [~1] - instFunctor = Sub Dict :: ListLikeF Seq.Seq :- Functor Seq.Seq -"instFunctor/Vector" [~1] - instFunctor = Sub Dict :: ListLikeF V.Vector :- Functor V.Vector - #-} - -withListLikeF :: forall pxy f a b. ListLikeF f - => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b -withListLikeF _ b = b \\ llDic &&& instFunctor - where - llDic = instLL :: ListLikeF f :- ListLike (f a) a -{-# RULES -"withListLikeF/List" [~1] forall (pxy :: proxy [a]). - withListLikeF pxy = id -"withListLikeF/Seq" [~1] forall (pxy :: proxy (Seq.Seq a)). - withListLikeF pxy = id -"withListLikeF/Vector" [~1] forall (pxy :: proxy (V.Vector a)). - withListLikeF pxy = id - #-} -{-# INLINE [1] withListLikeF #-} - -withListLikeF' :: ListLikeF f => f a -> ((Functor f, ListLike (f a) a) => b) -> b -withListLikeF' xs = withListLikeF (toProxy xs) -{-# RULES -"withListLikeF'/List" [~1] forall (pxy :: [a]). - withListLikeF' pxy = id -"withListLikeF'/Seq" [~1] forall (pxy :: (Seq.Seq a)). - withListLikeF' pxy = id -"withListLikeF'/Vector" [~1] forall (pxy ::(V.Vector a)). - withListLikeF' pxy = id - #-} -{-# INLINE [1] withListLikeF' #-} - -toProxy :: a -> Proxy a -toProxy _ = Proxy diff --git a/Data/Sized/Peano.hs b/Data/Sized/Peano.hs deleted file mode 100644 --- a/Data/Sized/Peano.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-} -{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeInType #-} -{-# LANGUAGE ViewPatterns #-} --- | This module exports @'S.Sized'@ type specialized to --- type-level Peano numeral @'PN.Nat'@. -module Data.Sized.Peano - (Ordinal, Sized, module Data.Sized, - pattern (:<), pattern NilL, pattern (:>), pattern NilR) where -import Data.Sized hiding ((:<), (:>), NilL, NilR, Sized) -import qualified Data.Sized as S - -import Data.ListLike (ListLike) -import Data.Singletons.Prelude (SingI) -import Data.Singletons.Prelude.Enum (PEnum (..)) -import qualified Data.Type.Ordinal as O -import qualified Data.Type.Natural as PN - -type Ordinal (n :: PN.Nat) = O.Ordinal n -type Sized f (n :: PN.Nat) = S.Sized f n - -pattern (:<) :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => forall (n1 :: PN.Nat). - (n ~ Succ n1, SingI n1) - => a -> Sized f n1 a -> Sized f n a -pattern a :< b = a S.:< b -infixr 5 :< - -pattern NilL :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => n ~ 'PN.Z => Sized f n a -pattern NilL = S.NilL - -pattern (:>) :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => forall (n1 :: PN.Nat). - (n ~ Succ n1, SingI n1) - => Sized f n1 a -> a -> Sized f n a -pattern a :> b = a S.:> b -infixl 5 :> - -pattern NilR :: forall f (n :: PN.Nat) a. - (ListLike (f a) a) - => n ~ 'PN.Z => Sized f n a -pattern NilR = S.NilR diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,7 @@ +sized - Sized sequence data-types +================================= +![Haskell CI](https://github.com/konn/sized/workflows/Haskell%20CI/badge.svg) [![Hackage](https://img.shields.io/hackage/v/sized.svg)](https://hackage.haskell.org/package/sized) + +A wrapper to make length-parametrized data-type from endofunctors from [subcategories]. + +[subcategories]: http://hackage.haskell.org/package/subcategories diff --git a/sized.cabal b/sized.cabal --- a/sized.cabal +++ b/sized.cabal @@ -1,42 +1,78 @@ +cabal-version: 3.0 name: sized -version: 0.2.1.1 -cabal-version: >=1.10 -build-type: Simple -license: BSD3 +version: 1.1.0.2 +license: BSD-3-Clause license-file: LICENSE maintainer: konn.jinro_at_gmail.com +author: Hiromi ISHII +copyright: (c) Hiromi ISHII +tested-with: ghc ==9.0.2 || ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 || ==9.10.1 +extra-doc-files: + Changelog.md + README.md + synopsis: Sized sequence data-types description: - A wrapper to make length-parametrized data-type from ListLike data-types. + A wrapper to make length-parametrized data-type from functorial data-types. + category: Data -author: Hiromi ISHII +build-type: Simple source-repository head - type: git - location: git://github.com/konn/sized.git + type: git + location: git://github.com/konn/sized.git library - exposed-modules: - Data.Sized - Data.Sized.Builtin - Data.Sized.Peano - Data.Sized.Flipped - build-depends: - base >=4.7 && <5, - type-natural >=0.7.1.2, - mono-traversable >=0.10 && <1.1, - ListLike >=4.5.1, - singletons >=2.0, - deepseq >=1.4.2.0, - hashable >=1.2.6.1, - vector >=0.12.0.1, - containers >=0.5.7.1, - constraints >=0.9.1, - equational-reasoning ==0.*, - monomorphic >=0.0.3.3, - lens >=0.14 - default-language: Haskell2010 - other-modules: - Data.Sized.Internal - ghc-options: -O2 -Wall -Wno-redundant-constraints + exposed-modules: + Data.Sized + Data.Sized.Builtin + Data.Sized.Flipped + hs-source-dirs: src + other-modules: Data.Sized.Internal + default-language: Haskell2010 + ghc-options: + -Wall + -Wno-redundant-constraints + + build-depends: + base >=4 && <5, + constraints, + containers >=0.5, + deepseq >=1.4, + equational-reasoning >=0.5, + ghc-typelits-knownnat, + ghc-typelits-presburger >=0.7.2, + hashable >=1.2, + lens >=0.14, + mono-traversable >=0.10, + subcategories >=0.2, + these, + type-natural >=1.3, + vector >=0.12, + +test-suite optimisaion-test + type: exitcode-stdio-1.0 + main-is: opt-test.hs + hs-source-dirs: test + other-modules: Shared + default-language: Haskell2010 + ghc-options: + -Wall + -Wno-redundant-constraints + -fno-hpc + + build-depends: + base, + containers, + inspection-testing >=0.4 && <0.6, + mono-traversable, + primitive, + sized, + subcategories, + tasty, + tasty-inspection-testing, + template-haskell, + th-lift, + type-natural, + vector, diff --git a/src/Data/Sized.hs b/src/Data/Sized.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized.hs @@ -0,0 +1,1834 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE LiberalTypeSynonyms #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE NoStarIsType #-} +{-# OPTIONS_GHC -fenable-rewrite-rules #-} +{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-} +{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-} + +{- | This module provides the functionality to make length-parametrized types + from existing 'CFreeMonoid' sequential types. + + Most of the complexity of operations for @Sized f n a@ are the same as + original operations for @f@. For example, '!!' is O(1) for + @Sized Vector n a@ but O(i) for @Sized [] n a@. + + This module also provides powerful view types and pattern synonyms to + inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail. +-} +module Data.Sized + ( -- * Main Data-types + Sized (), + SomeSized (..), + DomC (), + + -- * Accessors + + -- ** Length information + length, + sLength, + null, + + -- ** Indexing + (!!), + (%!!), + index, + sIndex, + head, + last, + uncons, + uncons', + Uncons (..), + unsnoc, + unsnoc', + Unsnoc (..), + + -- ** Slicing + tail, + init, + take, + takeAtMost, + drop, + splitAt, + splitAtMost, + + -- * Construction + + -- ** Initialisation + empty, + singleton, + toSomeSized, + replicate, + replicate', + generate, + generate', + + -- ** Concatenation + cons, + (<|), + snoc, + (|>), + append, + (++), + concat, + + -- ** Zips + zip, + zipSame, + zipWith, + zipWithSame, + unzip, + unzipWith, + + -- * Transformation + map, + reverse, + intersperse, + nub, + sort, + sortBy, + insert, + insertBy, + + -- * Conversion + + -- ** List + toList, + fromList, + fromList', + unsafeFromList, + unsafeFromList', + fromListWithDefault, + fromListWithDefault', + + -- ** Base container + unsized, + toSized, + toSized', + unsafeToSized, + unsafeToSized', + toSizedWithDefault, + toSizedWithDefault', + + -- * Querying + + -- ** Partitioning + Partitioned (..), + takeWhile, + dropWhile, + span, + break, + partition, + + -- ** Searching + elem, + notElem, + find, + findIndex, + sFindIndex, + findIndices, + sFindIndices, + elemIndex, + sElemIndex, + sUnsafeElemIndex, + elemIndices, + sElemIndices, + + -- * Views and Patterns + -- $ViewsAndPatterns + + -- ** Views + -- $views + + -- ** Patterns + -- $patterns + + -- ** Definitions + viewCons, + ConsView (..), + viewSnoc, + SnocView (..), + pattern Nil, + pattern (:<), + pattern (:>), + ) +where + +import Control.Applicative (ZipList (..), (<*>)) +import Control.Subcategory + ( CApplicative (..), + CFoldable (..), + CFreeMonoid (..), + CFunctor (..), + CPointed (..), + CRepeat (..), + CSemialign (..), + CTraversable (..), + CUnzip (..), + CZip (..), + Constrained (Dom), + cfromList, + ctoList, + ) +import Data.Coerce (coerce) +import Data.Constraint (Dict (..), withDict) +import qualified Data.Foldable as F +import Data.Kind (Type) +import qualified Data.List as L +import Data.Maybe (fromJust) +import Data.Monoid (Monoid (..), (<>)) +import qualified Data.Sequence as Seq +import Data.Sized.Internal +import Data.These (These (..)) +import Data.Type.Equality (gcastWith, (:~:) (..)) +import Data.Type.Natural +import Data.Type.Ordinal (Ordinal (..), ordToNatural) +import Data.Typeable (Typeable) +import qualified Data.Vector as V +import qualified Data.Vector.Storable as SV +import qualified Data.Vector.Unboxed as UV +import Unsafe.Coerce (unsafeCoerce) +import Prelude + ( Bool (..), + Enum (..), + Eq (..), + Functor, + Int, + Maybe (..), + Num (..), + Ord (..), + Ordering, + Show (..), + const, + flip, + fmap, + fromIntegral, + uncurry, + ($), + (.), + ) +import qualified Prelude as P + +-------------------------------------------------------------------------------- +-- Main data-types +-------------------------------------------------------------------------------- + +{- | 'Sized' vector with the length is existentially quantified. + This type is used mostly when the return type's length cannot + be statically determined beforehand. + + @SomeSized sn xs :: SomeSized f a@ stands for the 'Sized' sequence + @xs@ of element type @a@ and length @sn@. + + Since 0.7.0.0 +-} +data SomeSized f a where + SomeSized :: + SNat n -> + Sized f n a -> + SomeSized f a + +deriving instance Typeable SomeSized + +instance Show (f a) => Show (SomeSized f a) where + showsPrec d (SomeSized _ s) = + P.showParen (d > 9) $ + P.showString "SomeSized _ " . showsPrec 10 s + +instance Eq (f a) => Eq (SomeSized f a) where + (SomeSized _ (Sized xs)) == (SomeSized _ (Sized ys)) = xs == ys + +-------------------------------------------------------------------------------- +-- Accessors +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Length infromation +-------------------------------------------------------------------------------- + +{- | Returns the length of wrapped containers. + If you use @unsafeFromList@ or similar unsafe functions, + this function may return different value from type-parameterized length. + + Since 0.8.0.0 (type changed) +-} +length :: + forall f (n :: Nat) a. + (Dom f a, KnownNat n) => + Sized f n a -> + Int +length = const $ fromIntegral $ fromSNat $ sNat @n +{-# INLINE CONLIKE [1] length #-} + +lengthTLZero :: Sized f 0 a -> Int +lengthTLZero = P.const 0 +{-# INLINE lengthTLZero #-} + +{-# RULES +"length/0" [~1] length = lengthTLZero + #-} + +{- | @SNat@ version of 'length'. + + Since 0.8.0.0 (type changed) +-} +sLength :: + forall f (n :: Nat) a. + (Dom f a, KnownNat n) => + Sized f n a -> + SNat n +sLength _ = sNat @n +{-# INLINE [2] sLength #-} + +{- | Test if the sequence is empty or not. + + Since 0.7.0.0 +-} +null :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a) => + Sized f n a -> + Bool +null = coerce $ cnull @f @a +{-# INLINE CONLIKE [2] null #-} + +nullTL0 :: Sized f 0 a -> Bool +nullTL0 = P.const True +{-# INLINE nullTL0 #-} + +nullPeanoSucc :: Sized f (S n) a -> Bool +nullPeanoSucc = P.const False +{-# INLINE nullPeanoSucc #-} + +nullTLSucc :: Sized f (n + 1) a -> Bool +nullTLSucc = P.const False +{-# INLINE nullTLSucc #-} + +{-# RULES +"null/0" [~2] null = nullTL0 +"null/0" [~2] null = nullTLSucc +"null/0" [~1] forall (vec :: 1 <= n => Sized f n a). + null vec = + False +"null/Sn" [~2] null = nullPeanoSucc + #-} + +-------------------------------------------------------------------------------- +--- Indexing +-------------------------------------------------------------------------------- + +{- | (Unsafe) indexing with @Int@s. + If you want to check boundary statically, use '%!!' or 'sIndex'. + + Since 0.7.0.0 +-} +(!!) :: + forall f (m :: Nat) a. + (CFoldable f, Dom f a, (1 <= m)) => + Sized f m a -> + Int -> + a +(!!) = coerce $ cindex @f @a +{-# INLINE (!!) #-} + +{- | Safe indexing with 'Ordinal's. + + Since 0.7.0.0 +-} +(%!!) :: + forall f (n :: Nat) c. + (CFoldable f, Dom f c) => + Sized f n c -> + Ordinal n -> + c +(%!!) = coerce $ (. (P.fromIntegral . ordToNatural)) . cindex @f @c +{-# INLINE (%!!) #-} +{-# SPECIALIZE (%!!) :: Sized [] (n :: Nat) a -> Ordinal n -> a #-} +{-# SPECIALIZE (%!!) :: Sized V.Vector (n :: Nat) a -> Ordinal n -> a #-} +{-# SPECIALIZE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Nat) a -> Ordinal n -> a #-} +{-# SPECIALIZE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Nat) a -> Ordinal n -> a #-} +{-# SPECIALIZE (%!!) :: Sized Seq.Seq (n :: Nat) a -> Ordinal n -> a #-} + +{- | Flipped version of '!!'. + + Since 0.7.0.0 +-} +index :: + forall f (m :: Nat) a. + (CFoldable f, Dom f a, (1 <= m)) => + Int -> + Sized f m a -> + a +index = flip (!!) +{-# INLINE index #-} + +{- | Flipped version of '%!!'. + + Since 0.7.0.0 +-} +sIndex :: + forall f (n :: Nat) c. + (CFoldable f, Dom f c) => + Ordinal n -> + Sized f n c -> + c +sIndex = flip $ (%!!) @f @n @c +{-# INLINE sIndex #-} + +{- | Take the first element of non-empty sequence. + If you want to make case-analysis for general sequence, + see <#ViewsAndPatterns Views and Patterns> section. + + Since 0.7.0.0 +-} +head :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a, (0 < n)) => + Sized f n a -> + a +head = coerce $ chead @f @a +{-# INLINE head #-} + +{- | Take the last element of non-empty sequence. + If you want to make case-analysis for general sequence, + see <#ViewsAndPatterns Views and Patterns> section. + + Since 0.7.0.0 +-} +last :: + forall f (n :: Nat) a. + ((0 < n), CFoldable f, Dom f a) => + Sized f n a -> + a +last = coerce $ clast @f @a +{-# INLINE last #-} + +{- | Take the 'head' and 'tail' of non-empty sequence. + If you want to make case-analysis for general sequence, + see <#ViewsAndPatterns Views and Patterns> section. + + Since 0.7.0.0 +-} +uncons :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a, (1 <= n)) => + Sized f n a -> + Uncons f n a +uncons = + withKnownNat + (sPred $ sNat @n) + $ uncurry (Uncons @f @(Pred n) @a) . coerce (fromJust . cuncons @f @a) + +{- | 'uncons' with explicit specified length @n@ + + Since 0.7.0.0 +-} +uncons' :: + forall f (n :: Nat) a proxy. + (KnownNat n, CFreeMonoid f, Dom f a) => + proxy n -> + Sized f (Succ n) a -> + Uncons f (Succ n) a +uncons' _ = + withKnownNat (sSucc $ sNat @n) uncons +{-# INLINE uncons' #-} + +data Uncons f (n :: Nat) a where + Uncons :: + forall f (n :: Nat) a. + KnownNat n => + a -> + Sized f n a -> + Uncons f (1 + n) a + +{- | Take the 'init' and 'last' of non-empty sequence. + If you want to make case-analysis for general sequence, + see <#ViewsAndPatterns Views and Patterns> section. + + Since 0.7.0.0 +-} +unsnoc :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a, (0 < n)) => + Sized f n a -> + Unsnoc f n a +unsnoc = + withKnownNat + (sPred $ sNat @n) + $ uncurry (Unsnoc @f @(Pred n)) . coerce (fromJust . cunsnoc @f @a) +{-# NOINLINE [1] unsnoc #-} + +data Unsnoc f n a where + Unsnoc :: forall f n a. Sized f (n :: Nat) a -> a -> Unsnoc f (Succ n) a + +{- | 'unsnoc'' with explicit specified length @n@ + + Since 0.7.0.0 +-} +unsnoc' :: + forall f (n :: Nat) a proxy. + (KnownNat n, CFreeMonoid f, Dom f a) => + proxy n -> + Sized f (Succ n) a -> + Unsnoc f (Succ n) a +unsnoc' _ = + withKnownNat (sSucc $ sNat @n) unsnoc +{-# INLINE unsnoc' #-} + +-------------------------------------------------------------------------------- +--- Slicing +-------------------------------------------------------------------------------- + +{- | Take the tail of non-empty sequence. + If you want to make case-analysis for general sequence, + see <#ViewsAndPatterns Views and Patterns> section. + + Since 0.7.0.0 +-} +tail :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + Sized f (1 + n) a -> + Sized f n a +tail = coerce $ ctail @f @a +{-# INLINE tail #-} + +{- | Take the initial segment of non-empty sequence. + If you want to make case-analysis for general sequence, + see <#ViewsAndPatterns Views and Patterns> section. + + Since 0.7.0.0 +-} +init :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + Sized f (n + 1) a -> + Sized f n a +init = coerce $ cinit @f @a +{-# INLINE init #-} + +{- | @take k xs@ takes first @k@ element of @xs@ where + the length of @xs@ should be larger than @k@. + + Since 0.7.0.0 +-} +take :: + forall (n :: Nat) f (m :: Nat) a. + (CFreeMonoid f, Dom f a, (n <= m)) => + SNat n -> + Sized f m a -> + Sized f n a +take = coerce $ ctake @f @a . P.fromIntegral . fromSNat @n +{-# INLINE take #-} + +{- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@. + + Since 0.7.0.0 +-} +takeAtMost :: + forall (n :: Nat) f m a. + (CFreeMonoid f, Dom f a) => + SNat n -> + Sized f m a -> + Sized f (Min n m) a +takeAtMost = coerce $ ctake @f @a . P.fromIntegral . fromSNat @n +{-# INLINE takeAtMost #-} + +{- | @drop k xs@ drops first @k@ element of @xs@ and returns + the rest of sequence, where the length of @xs@ should be larger than @k@. + + Since 0.7.0.0 +-} +drop :: + forall (n :: Nat) f (m :: Nat) a. + (CFreeMonoid f, Dom f a, (n <= m)) => + SNat n -> + Sized f m a -> + Sized f (m - n) a +drop = coerce $ cdrop @f @a . P.fromIntegral . fromSNat @n +{-# INLINE drop #-} + +{- | @splitAt k xs@ split @xs@ at @k@, where + the length of @xs@ should be less than or equal to @k@. + + Since 0.7.0.0 +-} +splitAt :: + forall (n :: Nat) f m a. + (CFreeMonoid f, Dom f a, (n <= m)) => + SNat n -> + Sized f m a -> + (Sized f n a, Sized f (m -. n) a) +splitAt = + coerce $ csplitAt @f @a . P.fromIntegral . fromSNat @n +{-# INLINE splitAt #-} + +{- | @splitAtMost k xs@ split @xs@ at @k@. + If @k@ exceeds the length of @xs@, then the second result value become empty. + + Since 0.7.0.0 +-} +splitAtMost :: + forall (n :: Nat) f (m :: Nat) a. + (CFreeMonoid f, Dom f a) => + SNat n -> + Sized f m a -> + (Sized f (Min n m) a, Sized f (m -. n) a) +splitAtMost = + coerce $ csplitAt @f @a . P.fromIntegral . fromSNat @n +{-# INLINE splitAtMost #-} + +-------------------------------------------------------------------------------- +-- Construction +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Initialisation +-------------------------------------------------------------------------------- + +{- | Empty sequence. + + Since 0.7.0.0 (type changed) +-} +empty :: + forall f a. + (Monoid (f a), Dom f a) => + Sized f (0) a +empty = coerce $ mempty @(f a) +{-# INLINE empty #-} + +{- | Sequence with one element. + + Since 0.7.0.0 +-} +singleton :: forall f a. (CPointed f, Dom f a) => a -> Sized f (1) a +singleton = coerce $ cpure @f @a +{-# INLINE singleton #-} + +{- | Consruct the 'Sized' sequence from base type, but + the length parameter is dynamically determined and + existentially quantified; see also 'SomeSized'. + + Since 0.7.0.0 +-} +toSomeSized :: + forall f a. + (Dom f a, CFoldable f) => + f a -> + SomeSized f a +{-# INLINE toSomeSized #-} +toSomeSized = \xs -> + case toSomeSNat $ P.fromIntegral $ clength xs of + SomeSNat sn -> withKnownNat sn $ SomeSized sn $ unsafeToSized sn xs + +{- | Replicates the same value. + + Since 0.7.0.0 +-} +replicate :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + SNat n -> + a -> + Sized f n a +replicate = coerce $ creplicate @f @a . P.fromIntegral . fromSNat @n +{-# INLINE replicate #-} + +{- | 'replicate' with the length inferred. + + Since 0.7.0.0 +-} +replicate' :: + forall f (n :: Nat) a. + (KnownNat (n :: Nat), CFreeMonoid f, Dom f a) => + a -> + Sized f n a +replicate' = replicate (sNat @n) +{-# INLINE replicate' #-} + +{- | Construct a sequence of the given length by applying the function to each index. + + Since 0.7.0.0 +-} +generate :: + forall f (n :: Nat) (a :: Type). + (CFreeMonoid f, Dom f a) => + SNat n -> + (Ordinal n -> a) -> + Sized f n a +generate = coerce $ \sn -> + withKnownNat sn $ + cgenerate @f @a (P.fromIntegral $ fromSNat @n sn) + . (. toEnum @(Ordinal n)) +{-# INLINE [1] generate #-} + +{- | 'generate' with length inferred. + + Since 0.8.0.0 +-} +generate' :: + forall f (n :: Nat) (a :: Type). + (KnownNat n, CFreeMonoid f, Dom f a) => + (Ordinal n -> a) -> + Sized f n a +generate' = generate sNat +{-# INLINE [1] generate' #-} + +genVector :: + forall (n :: Nat) a. + SNat n -> + (Ordinal n -> a) -> + Sized V.Vector n a +genVector n f = withKnownNat n $ Sized $ V.generate (P.fromIntegral $ fromSNat n) (f . toEnum) +{-# INLINE genVector #-} + +genSVector :: + forall (n :: Nat) a. + (SV.Storable a) => + SNat n -> + (Ordinal n -> a) -> + Sized SV.Vector n a +genSVector n f = withKnownNat n $ Sized $ SV.generate (P.fromIntegral $ fromSNat n) (f . toEnum) +{-# INLINE genSVector #-} + +genSeq :: + forall (n :: Nat) a. + SNat n -> + (Ordinal n -> a) -> + Sized Seq.Seq n a +genSeq n f = withKnownNat n $ Sized $ Seq.fromFunction (P.fromIntegral $ fromSNat n) (f . toEnum) +{-# INLINE genSeq #-} + +{-# RULES +"generate/Vector" [~1] generate = genVector +"generate/SVector" [~1] forall + (n :: SNat (n :: Nat)) + (f :: SV.Storable a => Ordinal n -> a). + generate n f = + genSVector n f +"generate/UVector" [~1] forall + (n :: SNat (n :: Nat)) + (f :: UV.Unbox a => Ordinal n -> a). + generate n f = + withKnownNat n $ Sized (UV.generate (P.fromIntegral $ fromSNat n) (f . toEnum)) +"generate/Seq" [~1] generate = genSeq + #-} + +-------------------------------------------------------------------------------- +--- Concatenation +-------------------------------------------------------------------------------- + +{- | Append an element to the head of sequence. + + Since 0.8.0.0 +-} +cons :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + a -> + Sized f n a -> + Sized f (1 + n) a +cons = coerce $ ccons @f @a +{-# INLINE cons #-} + +{- | Infix version of 'cons'. + + Since 0.8.0.0 +-} +(<|) :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + a -> + Sized f n a -> + Sized f (1 + n) a +(<|) = cons +{-# INLINE (<|) #-} + +infixr 5 <| + +{- | Append an element to the tail of sequence. + + Since 0.7.0.0 +-} +snoc :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + Sized f n a -> + a -> + Sized f (n + 1) a +snoc (Sized xs) a = Sized $ csnoc xs a +{-# INLINE snoc #-} + +{- | Infix version of 'snoc'. + + Since 0.7.0.0 +-} +(|>) :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + Sized f n a -> + a -> + Sized f (n + 1) a +(|>) = snoc +{-# INLINE (|>) #-} + +infixl 5 |> + +{- | Append two lists. + + Since 0.7.0.0 +-} +append :: + forall f (n :: Nat) (m :: Nat) a. + (CFreeMonoid f, Dom f a) => + Sized f n a -> + Sized f m a -> + Sized f (n + m) a +append = coerce $ mappend @(f a) +{-# INLINE append #-} + +{- | Infix version of 'append'. + + Since 0.7.0.0 +-} +(++) :: + forall f (n :: Nat) (m :: Nat) a. + (CFreeMonoid f, Dom f a) => + Sized f n a -> + Sized f m a -> + Sized f (n + m) a +(++) = append + +infixr 5 ++ + +{- | Concatenates multiple sequences into one. + + Since 0.7.0.0 +-} +concat :: + forall f' (m :: Nat) f (n :: Nat) a. + ( CFreeMonoid f + , CFunctor f' + , CFoldable f' + , Dom f a + , Dom f' (f a) + , Dom f' (Sized f n a) + ) => + Sized f' m (Sized f n a) -> + Sized f (m * n) a +concat = coerce $ cfoldMap @f' @(Sized f n a) runSized +{-# INLINE [2] concat #-} + +-------------------------------------------------------------------------------- +--- Zips +-------------------------------------------------------------------------------- + +{- | Zipping two sequences. Length is adjusted to shorter one. + + Since 0.7.0.0 +-} +zip :: + forall f (n :: Nat) a (m :: Nat) b. + (Dom f a, CZip f, Dom f b, Dom f (a, b)) => + Sized f n a -> + Sized f m b -> + Sized f (Min n m) (a, b) +zip = coerce $ czip @f @a @b + +{- | 'zip' for the sequences of the same length. + + Since 0.7.0.0 +-} +zipSame :: + forall f (n :: Nat) a b. + (Dom f a, CZip f, Dom f b, Dom f (a, b)) => + Sized f n a -> + Sized f n b -> + Sized f n (a, b) +zipSame = coerce $ czip @f @a @b +{-# INLINE [1] zipSame #-} + +{- | Zipping two sequences with funtion. Length is adjusted to shorter one. + + Since 0.7.0.0 +-} +zipWith :: + forall f (n :: Nat) a (m :: Nat) b c. + (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => + (a -> b -> c) -> + Sized f n a -> + Sized f m b -> + Sized f (Min n m) c +zipWith = coerce $ czipWith @f @a @b @c +{-# INLINE [1] zipWith #-} + +{- | 'zipWith' for the sequences of the same length. + + Since 0.7.0.0 +-} +zipWithSame :: + forall f (n :: Nat) a b c. + (Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) => + (a -> b -> c) -> + Sized f n a -> + Sized f n b -> + Sized f n c +zipWithSame = coerce $ czipWith @f @a @b @c +{-# INLINE [1] zipWithSame #-} + +{- | Unzipping the sequence of tuples. + + Since 0.7.0.0 +-} +unzip :: + forall f (n :: Nat) a b. + (CUnzip f, Dom f a, Dom f b, Dom f (a, b)) => + Sized f n (a, b) -> + (Sized f n a, Sized f n b) +unzip = coerce $ cunzip @f @a @b +{-# INLINE unzip #-} + +{- | Unzipping the sequence of tuples. + + Since 0.7.0.0 +-} +unzipWith :: + forall f (n :: Nat) a b c. + (CUnzip f, Dom f a, Dom f b, Dom f c) => + (a -> (b, c)) -> + Sized f n a -> + (Sized f n b, Sized f n c) +unzipWith = coerce $ cunzipWith @f @a @b @c +{-# INLINE unzipWith #-} + +-------------------------------------------------------------------------------- +-- Transformation +-------------------------------------------------------------------------------- + +{- | Map function. + + Since 0.7.0.0 +-} +map :: + forall f (n :: Nat) a b. + (CFreeMonoid f, Dom f a, Dom f b) => + (a -> b) -> + Sized f n a -> + Sized f n b +map f = Sized . cmap f . runSized +{-# INLINE map #-} + +{- | Reverse function. + + Since 0.7.0.0 +-} +reverse :: + forall f (n :: Nat) a. + (Dom f a, CFreeMonoid f) => + Sized f n a -> + Sized f n a +reverse = coerce $ creverse @f @a +{-# INLINE reverse #-} + +{- | Intersperces. + + Since 0.7.0.0 +-} +intersperse :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + a -> + Sized f n a -> + Sized f ((2 * n) -. 1) a +intersperse = coerce $ cintersperse @f @a +{-# INLINE intersperse #-} + +{- | Remove all duplicates. + + Since 0.7.0.0 +-} +nub :: + forall f (n :: Nat) a. + (Dom f a, Eq a, CFreeMonoid f) => + Sized f n a -> + SomeSized f a +nub = toSomeSized . coerce (cnub @f @a) + +{- | Sorting sequence by ascending order. + + Since 0.7.0.0 +-} +sort :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a, Ord a) => + Sized f n a -> + Sized f n a +sort = coerce $ csort @f @a + +{- | Generalized version of 'sort'. + + Since 0.7.0.0 +-} +sortBy :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + (a -> a -> Ordering) -> + Sized f n a -> + Sized f n a +sortBy = coerce $ csortBy @f @a + +{- | Insert new element into the presorted sequence. + + Since 0.7.0.0 +-} +insert :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a, Ord a) => + a -> + Sized f n a -> + Sized f (Succ n) a +insert = coerce $ cinsert @f @a + +{- | Generalized version of 'insert'. + + Since 0.7.0.0 +-} +insertBy :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + (a -> a -> Ordering) -> + a -> + Sized f n a -> + Sized f (Succ n) a +insertBy = coerce $ cinsertBy @f @a + +-------------------------------------------------------------------------------- +-- Conversion +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- List +-------------------------------------------------------------------------------- + +{- | Convert to list. + + Since 0.7.0.0 +-} +toList :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a) => + Sized f n a -> + [a] +toList = coerce $ ctoList @f @a +{-# INLINE [2] toList #-} + +{-# RULES +"toList/List" + Data.Sized.toList = + runSized + #-} + +{- | If the given list is shorter than @n@, then returns @Nothing@ + Otherwise returns @Sized f n a@ consisting of initial @n@ element + of given list. + + Since 0.7.0.0 (type changed) +-} +fromList :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + SNat n -> + [a] -> + Maybe (Sized f n a) +fromList Zero _ = Just $ Sized (mempty :: f a) +fromList sn xs = + let len = P.fromIntegral $ fromSNat sn + in if P.length xs < len + then Nothing + else Just $ Sized $ ctake len $ cfromList xs +{-# INLINEABLE [2] fromList #-} + +{- | 'fromList' with the result length inferred. + + Since 0.7.0.0 +-} +fromList' :: + forall f (n :: Nat) a. + (Dom f a, CFreeMonoid f, KnownNat n) => + [a] -> + Maybe (Sized f n a) +fromList' = fromList sNat +{-# INLINE fromList' #-} + +{- | Unsafe version of 'fromList'. If the length of the given list does not + equal to @n@, then something unusual happens. + + Since 0.7.0.0 +-} +unsafeFromList :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + SNat n -> + [a] -> + Sized f n a +unsafeFromList = const $ coerce $ cfromList @f @a +{-# INLINE [1] unsafeFromList #-} + +{- | 'unsafeFromList' with the result length inferred. + + Since 0.7.0.0 +-} +unsafeFromList' :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) => + [a] -> + Sized f n a +unsafeFromList' = unsafeFromList sNat +{-# INLINE [1] unsafeFromList' #-} + +{-# RULES +"unsafeFromList'/List" [~1] + unsafeFromList' = + Sized +"unsafeFromList'/Vector" [~1] + unsafeFromList' = + Sized . V.fromList +"unsafeFromList'/Seq" [~1] + unsafeFromList' = + Sized . Seq.fromList +"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]). + unsafeFromList' xs = + Sized (SV.fromList xs) +"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]). + unsafeFromList' xs = + Sized (UV.fromList xs) + #-} + +{- | Construct a @Sized f n a@ by padding default value if the given list is short. + + Since 0.5.0.0 (type changed) +-} +fromListWithDefault :: + forall f (n :: Nat) a. + (Dom f a, CFreeMonoid f) => + SNat n -> + a -> + [a] -> + Sized f n a +fromListWithDefault sn def xs = + let len = P.fromIntegral $ fromSNat sn + in Sized $ + cfromList (ctake len xs) + <> creplicate (len - clength xs) def +{-# INLINEABLE fromListWithDefault #-} + +{- | 'fromListWithDefault' with the result length inferred. + + Since 0.7.0.0 +-} +fromListWithDefault' :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) => + a -> + [a] -> + Sized f n a +fromListWithDefault' = fromListWithDefault sNat +{-# INLINE fromListWithDefault' #-} + +-------------------------------------------------------------------------------- +--- Base containes +-------------------------------------------------------------------------------- + +{- | Forget the length and obtain the wrapped base container. + + Since 0.7.0.0 +-} +unsized :: forall f (n :: Nat) a. Sized f n a -> f a +unsized = runSized +{-# INLINE unsized #-} + +{- | If the length of the input is shorter than @n@, then returns @Nothing@. + Otherwise returns @Sized f n a@ consisting of initial @n@ element + of the input. + + Since 0.7.0.0 +-} +toSized :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + SNat (n :: Nat) -> + f a -> + Maybe (Sized f n a) +toSized sn xs = + let len = P.fromIntegral $ fromSNat sn + in if clength xs < len + then Nothing + else Just $ unsafeToSized sn $ ctake len xs +{-# INLINEABLE [2] toSized #-} + +{- | 'toSized' with the result length inferred. + + Since 0.7.0.0 +-} +toSized' :: + forall f (n :: Nat) a. + (Dom f a, CFreeMonoid f, KnownNat n) => + f a -> + Maybe (Sized f n a) +toSized' = toSized sNat +{-# INLINE toSized' #-} + +{- | Unsafe version of 'toSized'. If the length of the given list does not + equal to @n@, then something unusual happens. + + Since 0.7.0.0 +-} +unsafeToSized :: forall f (n :: Nat) a. SNat n -> f a -> Sized f n a +unsafeToSized _ = Sized +{-# INLINE [2] unsafeToSized #-} + +{- | 'unsafeToSized' with the result length inferred. + + Since 0.7.0.0 +-} +unsafeToSized' :: + forall f (n :: Nat) a. + (KnownNat n, Dom f a) => + f a -> + Sized f n a +unsafeToSized' = unsafeToSized sNat +{-# INLINE unsafeToSized' #-} + +{- | Construct a @Sized f n a@ by padding default value if the given list is short. + + Since 0.7.0.0 +-} +toSizedWithDefault :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + SNat (n :: Nat) -> + a -> + f a -> + Sized f n a +toSizedWithDefault sn def xs = + let len = P.fromIntegral $ fromSNat sn + in Sized $ ctake len xs <> creplicate (len - clength xs) def +{-# INLINEABLE toSizedWithDefault #-} + +{- | 'toSizedWithDefault' with the result length inferred. + + Since 0.7.0.0 +-} +toSizedWithDefault' :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) => + a -> + f a -> + Sized f n a +toSizedWithDefault' = toSizedWithDefault sNat +{-# INLINE toSizedWithDefault' #-} + +-------------------------------------------------------------------------------- +-- Querying +-------------------------------------------------------------------------------- + +-------------------------------------------------------------------------------- +--- Partitioning +-------------------------------------------------------------------------------- + +{- | The type @Partitioned f n a@ represents partitioned sequence of length @n@. + Value @Partitioned lenL ls lenR rs@ stands for: + + * Entire sequence is divided into @ls@ and @rs@, and their length + are @lenL@ and @lenR@ resp. + + * @lenL + lenR = n@ + + Since 0.7.0.0 +-} +data Partitioned f n a where + Partitioned :: + (Dom f a) => + SNat n -> + Sized f n a -> + SNat m -> + Sized f m a -> + Partitioned f (n + m) a + +{- | Take the initial segment as long as elements satisfys the predicate. + + Since 0.7.0.0 +-} +takeWhile :: + forall f (n :: Nat) a. + (Dom f a, CFreeMonoid f) => + (a -> Bool) -> + Sized f n a -> + SomeSized f a +takeWhile = (toSomeSized .) . coerce (ctakeWhile @f @a) +{-# INLINE takeWhile #-} + +{- | Drop the initial segment as long as elements satisfys the predicate. + + Since 0.7.0.0 +-} +dropWhile :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + SomeSized f a +dropWhile = (toSomeSized .) . coerce (cdropWhile @f @a) +{-# INLINE dropWhile #-} + +{- | Split the sequence into the longest prefix + of elements that satisfy the predicate + and the rest. + + Since 0.7.0.0 +-} +span :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + Partitioned f n a +span = (unsafePartitioned @n .) . coerce (cspan @f @a) +{-# INLINE span #-} + +{- | Split the sequence into the longest prefix + of elements that do not satisfy the + predicate and the rest. + + Since 0.7.0.0 +-} +break :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + Partitioned f n a +break = (unsafePartitioned @n .) . coerce (cbreak @f @a) +{-# INLINE break #-} + +{- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't. + + Since 0.7.0.0 +-} +partition :: + forall f (n :: Nat) a. + (CFreeMonoid f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + Partitioned f n a +partition = (unsafePartitioned @n .) . coerce (cpartition @f @a) +{-# INLINE partition #-} + +unsafePartitioned :: + forall (n :: Nat) f a. + (CFreeMonoid f, Dom f a) => + (f a, f a) -> + Partitioned f n a +unsafePartitioned (l, r) = + case (toSomeSized l, toSomeSized r) of + ( SomeSized (lenL :: SNat nl) ls + , SomeSized (lenR :: SNat nr) rs + ) -> + gcastWith + ( unsafeCoerce $ Refl @() :: + n :~: nl + nr + ) + $ Partitioned lenL ls lenR rs + +-------------------------------------------------------------------------------- +--- Searching +-------------------------------------------------------------------------------- + +{- | Membership test; see also 'notElem'. + + Since 0.7.0.0 +-} +elem :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a, Eq a) => + a -> + Sized f n a -> + Bool +elem = coerce $ celem @f @a +{-# INLINE elem #-} + +{- | Negation of 'elem'. + + Since 0.7.0.0 +-} +notElem :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a, Eq a) => + a -> + Sized f n a -> + Bool +notElem = coerce $ cnotElem @f @a +{-# INLINE notElem #-} + +{- | Find the element satisfying the predicate. + + Since 0.7.0.0 +-} +find :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + Maybe a +find = coerce $ cfind @f @a +{-# INLINE [1] find #-} + +{-# RULES +"find/List" [~1] forall p. + find p = + L.find @[] p . runSized +"find/Vector" [~1] forall p. + find p = + V.find p . runSized +"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool). + find p = + SV.find p . runSized +"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool). + find p = + UV.find p . runSized + #-} + +{- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists. + + Since 0.7.0.0 +-} +findIndex :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + Maybe Int +findIndex = coerce $ cfindIndex @f @a +{-# INLINE findIndex #-} + +{- | 'Ordinal' version of 'findIndex'. + + Since 0.7.0.0 +-} +sFindIndex :: + forall f (n :: Nat) a. + (KnownNat (n :: Nat), CFoldable f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + Maybe (Ordinal n) +sFindIndex = (fmap toEnum .) . coerce (cfindIndex @f @a) +{-# INLINE sFindIndex #-} + +{- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices. + + Since 0.7.0.0 +-} +findIndices :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a) => + (a -> Bool) -> + Sized f n a -> + [Int] +findIndices = coerce $ cfindIndices @f @a +{-# INLINE findIndices #-} +{-# SPECIALIZE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-} + +{- | 'Ordinal' version of 'findIndices'. + + Since 0.7.0.0 +-} +sFindIndices :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a, KnownNat (n :: Nat)) => + (a -> Bool) -> + Sized f n a -> + [Ordinal n] +sFindIndices p = P.fmap (toEnum . P.fromIntegral) . findIndices p +{-# INLINE sFindIndices #-} + +{-# RULES +"Foldable.sum/Vector" + F.sum = + V.sum . runSized + #-} + +{- | Returns the index of the given element in the list, if exists. + + Since 0.7.0.0 +-} +elemIndex :: + forall f (n :: Nat) a. + (CFoldable f, Eq a, Dom f a) => + a -> + Sized f n a -> + Maybe Int +elemIndex = coerce $ celemIndex @f @a +{-# INLINE elemIndex #-} + +{- | Ordinal version of 'elemIndex'. + Since 0.7.0.0, we no longer do boundary check inside the definition. + + Since 0.7.0.0 +-} +sElemIndex + , sUnsafeElemIndex :: + forall f (n :: Nat) a. + (KnownNat n, CFoldable f, Dom f a, Eq a) => + a -> + Sized f n a -> + Maybe (Ordinal n) +sElemIndex = (fmap toEnum .) . coerce (celemIndex @f @a) +{-# INLINE sElemIndex #-} + +-- | Since 0.5.0.0 (type changed) +sUnsafeElemIndex = sElemIndex +{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-} + +{- | Returns all indices of the given element in the list. + + Since 0.7.0.0 +-} +elemIndices :: + forall f (n :: Nat) a. + (CFoldable f, Dom f a, Eq a) => + a -> + Sized f n a -> + [Int] +elemIndices = coerce $ celemIndices @f @a +{-# INLINE elemIndices #-} + +{- | Ordinal version of 'elemIndices' + + Since 0.7.0.0 +-} +sElemIndices :: + forall f (n :: Nat) a. + (CFoldable f, KnownNat (n :: Nat), Dom f a, Eq a) => + a -> + Sized f n a -> + [Ordinal n] +sElemIndices = (fmap toEnum .) . elemIndices +{-# INLINE sElemIndices #-} + +-------------------------------------------------------------------------------- +-- Views and Patterns +-------------------------------------------------------------------------------- + +{- $ViewsAndPatterns #ViewsAndPatterns# + + With GHC's @ViewPatterns@ and @PatternSynonym@ extensions, + we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor. + Curretnly, there are two direction view and patterns: Cons and Snoc. + Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead' + (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on + cons (resp. snoc) of @Sized f n a@ in O(1). +-} + +{- $views #views# + + With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows: + +@ +slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n +slen ('viewCons' -> 'NilCV') = 'SZ' +slen ('viewCons' -> _ ':-' as) = 'SS' (slen as) +slen _ = error "impossible" +@ + + The constraint @('KnownNat' n, 'Dom f a' f)@ is needed for view function. + In the above, we have extra wildcard pattern (@_@) at the last. + Code compiles if we removed it, but current GHC warns for incomplete pattern, + although we know first two patterns exhausts all the case. + + Equivalently, we can use snoc-style pattern-matching: + +@ +slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n +slen ('viewSnoc' -> 'NilSV') = 'SZ' +slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as) +@ +-} + +{- | View of the left end of sequence (cons-side). + + Since 0.7.0.0 +-} +data ConsView f n a where + NilCV :: ConsView f (0) a + (:-) :: + (KnownNat n, KnownNat (1 + n)) => + a -> + Sized f n a -> + ConsView f (1 + n) a + +infixr 5 :- + +{- | Case analysis for the cons-side of sequence. + + Since 0.5.0.0 (type changed) +-} +viewCons :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) => + Sized f n a -> + ConsView f n a +viewCons sz = case zeroOrSucc $ sNat @n of + IsZero -> NilCV + IsSucc n' -> + withKnownNat n' $ + withKnownNat (sOne %+ n') $ + case uncons' n' sz of + Uncons a xs -> a :- xs + +{- | View of the left end of sequence (snoc-side). + + Since 0.7.0.0 +-} +data SnocView f n a where + NilSV :: SnocView f (0) a + (:-::) :: KnownNat (n :: Nat) => Sized f n a -> a -> SnocView f (n + 1) a + +infixl 5 :-:: + +{- | Case analysis for the snoc-side of sequence. + + Since 0.5.0.0 (type changed) +-} +viewSnoc :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) => + Sized f n a -> + SnocView f n a +viewSnoc sz = case zeroOrSucc (sNat @n) of + IsZero -> NilSV + IsSucc (n' :: SNat n') -> + withKnownNat n' $ + case unsnoc' n' sz of + Unsnoc (xs :: Sized f m a) a -> + gcastWith + (unsafeCoerce (Refl @()) :: n' :~: m) + $ xs :-:: a + +{- $patterns #patterns# + + So we can pattern match on both end of sequence via views, but + it is rather clumsy to nest it. For example: + +@ +nextToHead :: ('Dom f a' f, 'KnownNat' n) => 'Sized' f ('S' ('S' n)) a -> a +nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a +@ + + In such a case, with @PatternSynonyms@ extension we can write as follows: + +@ +nextToHead :: ('Dom f a' f, 'KnownNat' n) => 'Sized' f ('S' ('S' n)) a -> a +nextToHead (_ ':<' a ':<' _) = a +@ + + Of course, we can also rewrite above @slen@ example usNat @PatternSynonyms@: + +@ +slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' n +slen 'Nil' = 'SZ' +slen (_ ':<' as) = 'SS' (slen as) +@ + + So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to + pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists. + @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors, + but pattern synonyms so we cannot use them in expression contexts. + For more detail on pattern synonyms, see + + and + . +-} + +infixr 5 :< + +-- | Pattern synonym for cons-side uncons. +pattern (:<) :: + forall (f :: Type -> Type) a (n :: Nat). + (Dom f a, KnownNat n, CFreeMonoid f) => + forall (n1 :: Nat). + (n ~ (1 + n1), KnownNat n1) => + a -> + Sized f n1 a -> + Sized f n a +pattern a :< as <- + (viewCons -> a :- as) + where + a :< as = a <| as + +chkNil :: + forall f (n :: Nat) a. + (KnownNat n) => + Sized f n a -> + ZeroOrSucc n +chkNil = const $ zeroOrSucc $ sNat @n + +-- | Pattern synonym for a nil sequence. +pattern Nil :: + forall f (n :: Nat) a. + (KnownNat n, CFreeMonoid f, Dom f a) => + (n ~ 0) => + Sized f n a +pattern Nil <- + (chkNil -> IsZero) + where + Nil = empty + +infixl 5 :> + +-- | Pattern synonym for snoc-side unsnoc. +pattern (:>) :: + forall (f :: Type -> Type) a (n :: Nat). + (Dom f a, KnownNat n, CFreeMonoid f) => + forall (n1 :: Nat). + (n ~ (n1 + 1), KnownNat n1) => + Sized f n1 a -> + a -> + Sized f n a +pattern a :> b <- + (viewSnoc -> a :-:: b) + where + a :> b = a |> b + +{-# COMPLETE (:<), Nil #-} + +{-# COMPLETE (:>), Nil #-} + +class Dom f a => DomC f a + +instance Dom f a => DomC f a + +-- | Applicative instance, generalizing @'Data.Monoid.ZipList'@. +instance + ( Functor f + , CFreeMonoid f + , CZip f + , KnownNat n + , forall a. DomC f a + ) => + P.Applicative (Sized f (n :: Nat)) + where + {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized [] (n :: Nat)) #-} + {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized Seq.Seq (n :: Nat)) #-} + {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized V.Vector (n :: Nat)) #-} + + pure (x :: a) = + withDict (Dict @(DomC f a)) $ + replicate' x + {-# INLINE pure #-} + + (fs :: Sized f n (a -> b)) <*> (xs :: Sized f n a) = + withDict (Dict @(DomC f b)) $ + withDict (Dict @(DomC f a)) $ + withDict (Dict @(DomC f (a -> b))) $ + zipWithSame ($) fs xs + {-# INLINE [1] (<*>) #-} + +{-# RULES +"<*>/List" [~1] forall fs xs. + Sized fs <*> Sized xs = + Sized (getZipList (ZipList fs <*> ZipList xs)) +"<*>/Seq" [~1] forall fs xs. + Sized fs <*> Sized xs = + Sized (Seq.zipWith ($) fs xs) +"<*>/Vector" [~1] forall fs xs. + Sized fs <*> Sized xs = + Sized (V.zipWith ($) fs xs) + #-} + +instance + (CFreeMonoid f, KnownNat (n :: Nat)) => + CPointed (Sized f n) + where + cpure = replicate' + +instance + (CFreeMonoid f, CZip f) => + CApplicative (Sized f n) + where + pair = zipSame + (<.>) = zipWithSame ($) + (<.) = P.const + (.>) = P.flip P.const + +{- | __N.B.__ Since @calign@ is just zipping for fixed @n@, + we require more strong 'CZip' constraint here. +-} +instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where + calignWith = + coerce (\f -> czipWith @f @a @b @c ((f .) . These)) :: + forall a b c. + (Dom f a, Dom f b, Dom f c) => + (These a b -> c) -> + Sized f n a -> + Sized f n b -> + Sized f n c + {-# INLINE [1] calignWith #-} + calign = + coerce $ czipWith @f @a @b These :: + forall a b. + (Dom f a, Dom f b, Dom f (These a b)) => + Sized f n a -> + Sized f n b -> + Sized f n (These a b) + {-# INLINE [1] calign #-} + +instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where + czipWith = + coerce $ czipWith @f @a @b @c :: + forall a b c. + (Dom f a, Dom f b, Dom f c) => + (a -> b -> c) -> + Sized f n a -> + Sized f n b -> + Sized f n c + {-# INLINE [1] czipWith #-} + czip = + coerce $ czip @f @a @b :: + forall a b. + (Dom f a, Dom f b, Dom f (a, b)) => + Sized f n a -> + Sized f n b -> + Sized f n (a, b) + {-# INLINE [1] czip #-} + +instance + (KnownNat (n :: Nat), CZip f, CFreeMonoid f) => + CRepeat (Sized f n) + where + crepeat = replicate' + {-# INLINE [1] crepeat #-} + +instance CTraversable f => CTraversable (Sized f n) where + ctraverse = \f -> fmap coerce . ctraverse f . runSized + {-# INLINE ctraverse #-} diff --git a/src/Data/Sized/Builtin.hs b/src/Data/Sized/Builtin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Builtin.hs @@ -0,0 +1,4 @@ +module Data.Sized.Builtin + {-# DEPRECATED "Use Data.Sized instead" #-} + ( module Data.Sized ) where +import Data.Sized diff --git a/src/Data/Sized/Flipped.hs b/src/Data/Sized/Flipped.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Flipped.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LiberalTypeSynonyms #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoStarIsType #-} +module Data.Sized.Flipped (Flipped (..)) where + +import Control.DeepSeq (NFData (..)) +import Control.Lens.At (Index, IxValue, Ixed (..)) +import Control.Lens.TH (makeWrapped) +import Control.Lens.Wrapped (_Wrapped) +import Data.Hashable (Hashable (..)) +import Data.MonoTraversable (Element, MonoFoldable (..), MonoFunctor (..), MonoTraversable (..)) +import qualified Data.Sequence as Seq +import Data.Sized.Internal +import qualified Data.Type.Natural as PN +import Data.Type.Ordinal (Ordinal (..)) +import Data.Typeable (Typeable) +import qualified Data.Vector as V +import qualified Data.Vector.Storable as SV +import qualified Data.Vector.Unboxed as UV +import qualified GHC.TypeLits as TL + +{- | Wrapper for @'Sized'@ which takes length as its last element, instead of the second. + + Since 0.2.0.0 +-} +newtype Flipped f a n = Flipped {runFlipped :: Sized f n a} + deriving (Show, Eq, Ord, Typeable, NFData, Hashable) + +makeWrapped ''Flipped + +type instance Index (Flipped f a n) = Ordinal n + +type instance IxValue (Flipped f a n) = IxValue (f a) + +type instance Element (Flipped f a n) = Element (Sized f n a) + +deriving instance MonoFunctor (f a) => MonoFunctor (Flipped f a n) + +deriving instance MonoFoldable (f a) => MonoFoldable (Flipped f a n) + +instance (MonoTraversable (f a)) => MonoTraversable (Flipped f a n) where + otraverse = _Wrapped . otraverse + {-# INLINE otraverse #-} + + omapM = _Wrapped . omapM + {-# INLINE omapM #-} + +instance + (Integral (Index (f a)), Ixed (f a)) => + Ixed (Flipped f a n) + where + {-# SPECIALIZE instance Ixed (Flipped [] a (n :: TL.Nat)) #-} + {-# SPECIALIZE instance Ixed (Flipped [] a (n :: PN.Nat)) #-} + {-# SPECIALIZE instance Ixed (Flipped V.Vector a (n :: TL.Nat)) #-} + {-# SPECIALIZE instance Ixed (Flipped V.Vector a (n :: PN.Nat)) #-} + {-# SPECIALIZE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: TL.Nat)) #-} + {-# SPECIALIZE instance SV.Storable a => Ixed (Flipped SV.Vector a (n :: PN.Nat)) #-} + {-# SPECIALIZE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: TL.Nat)) #-} + {-# SPECIALIZE instance UV.Unbox a => Ixed (Flipped UV.Vector a (n :: PN.Nat)) #-} + {-# SPECIALIZE instance Ixed (Flipped Seq.Seq a (n :: TL.Nat)) #-} + {-# SPECIALIZE instance Ixed (Flipped Seq.Seq a (n :: PN.Nat)) #-} + ix o = _Wrapped . ix o + {-# INLINE ix #-} diff --git a/src/Data/Sized/Internal.hs b/src/Data/Sized/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sized/Internal.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE ConstraintKinds, DataKinds, DeriveDataTypeable #-} +{-# LANGUAGE DeriveFunctor, DeriveTraversable, DerivingStrategies #-} +{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving, KindSignatures #-} +{-# LANGUAGE LiberalTypeSynonyms, MultiParamTypeClasses, PolyKinds #-} +{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators, UndecidableInstances #-} +{-# LANGUAGE NoStarIsType #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Data.Sized.Internal (Sized(..)) where +import Control.DeepSeq (NFData (..)) +import Control.Lens.At (Index, IxValue, Ixed (..)) +import Control.Lens.Indexed (FoldableWithIndex (..), + FunctorWithIndex (..), + TraversableWithIndex (..)) +import Control.Subcategory (CFoldable, CFunctor, Constrained) +import Data.Hashable (Hashable (..)) +import Data.Kind (Type) +import Data.MonoTraversable (Element, MonoFoldable (..), + MonoFunctor (..), MonoTraversable (..)) +import qualified Data.Sequence as Seq +import Data.Type.Ordinal (Ordinal (..), ordToNatural, + unsafeNaturalToOrd) +import Data.Typeable (Typeable) +import qualified Data.Vector as V +import qualified Data.Vector.Storable as SV +import qualified Data.Vector.Unboxed as UV +import GHC.TypeNats + +-- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version. +-- +-- Here, 'f' must be the instance of 'CFreeMonoid' (f a) a@ for all @a@. +-- +-- Since 0.2.0.0 +newtype Sized (f :: Type -> Type) (n :: Nat) a = + Sized { runSized :: f a + } deriving (Eq, Ord, Typeable, + Functor, Foldable, Traversable) + deriving newtype + (Constrained, CFoldable, CFunctor) + +type instance Element (Sized f n a) = Element (f a) + +-- | Since 0.2.0.0 +deriving instance MonoFoldable (f a) + => MonoFoldable (Sized f n a) + +-- | Since 0.2.0.0 +deriving instance MonoFunctor (f a) + => MonoFunctor (Sized f n a) + +-- | Since 0.2.0.0 +instance {-# OVERLAPPABLE #-} (MonoTraversable (f a)) + => MonoTraversable (Sized f n a) where + {-# SPECIALISE instance MonoTraversable (Sized [] n a) #-} + {-# SPECIALISE instance MonoTraversable (Sized V.Vector n a) #-} + {-# SPECIALISE instance MonoTraversable (Sized Seq.Seq n a) #-} + {-# SPECIALISE instance UV.Unbox a => MonoTraversable (Sized UV.Vector n a) #-} + {-# SPECIALISE instance SV.Storable a => MonoTraversable (Sized SV.Vector n a) #-} + otraverse f = fmap Sized . otraverse f . runSized + omapM f = fmap Sized . omapM f. runSized + +-- | Since 0.6.0.0 +instance {-# OVERLAPPING #-} SV.Storable a => MonoTraversable (Sized SV.Vector n a) where + otraverse f = fmap Sized . otraverse f . runSized + omapM f = fmap Sized . omapM f . runSized + +-- | Since 0.6.0.0 +instance {-# OVERLAPPING #-} UV.Unbox a => MonoTraversable (Sized UV.Vector n a) where + otraverse f = fmap Sized . otraverse f . runSized + omapM f = fmap Sized . omapM f . runSized + +deriving instance NFData (f a) => NFData (Sized f n a) +deriving instance Hashable (f a) => Hashable (Sized f n a) + +instance Show (f a) => Show (Sized f n a) where + showsPrec d (Sized x) = showsPrec d x + +-- | Since 0.2.0.0 +type instance Index (Sized f n a) = Ordinal n + +-- | Since 0.3.0.0 +type instance IxValue (Sized f n a) = IxValue (f a) +instance (Integral (Index (f a)), Ixed (f a)) + => Ixed (Sized f (n :: Nat) a) where + {-# SPECIALISE instance Ixed (Sized [] (n :: Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized V.Vector (n :: Nat) a) #-} + {-# SPECIALISE instance SV.Storable a => Ixed (Sized SV.Vector (n :: Nat) a) #-} + {-# SPECIALISE instance UV.Unbox a => Ixed (Sized UV.Vector (n :: Nat) a) #-} + {-# SPECIALISE instance Ixed (Sized Seq.Seq (n :: Nat) a) #-} + {-# INLINE ix #-} + ix n f = fmap Sized . ix (fromIntegral $ ordToNatural n) f . runSized + +-- | Since 0.2.0.0 +instance (Integral i, FunctorWithIndex i f, KnownNat n) + => FunctorWithIndex (Ordinal n) (Sized f n) where + imap f = Sized . imap (f . unsafeNaturalToOrd . fromIntegral) . runSized + {-# INLINE imap #-} + {-# SPECIALISE instance KnownNat n + => FunctorWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-} + {-# SPECIALISE instance KnownNat n + => FunctorWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-} + {-# SPECIALISE instance KnownNat n + => FunctorWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-} + +-- | Since 0.4.0.0 +instance {-# OVERLAPPABLE #-} (Integral i, FoldableWithIndex i f, KnownNat n) + => FoldableWithIndex (Ordinal n) (Sized f n) where + ifoldMap f = ifoldMap (f . unsafeNaturalToOrd . fromIntegral) . runSized + {-# INLINE ifoldMap #-} + + ifoldr f e = ifoldr (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldr #-} + + ifoldl f e = ifoldl (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldl #-} + + ifoldr' f e = ifoldr' (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldr' #-} + + ifoldl' f e = ifoldl' (f . unsafeNaturalToOrd . fromIntegral) e . runSized + {-# INLINE ifoldl' #-} + + {-# SPECIALISE instance KnownNat n + => FoldableWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-} + {-# SPECIALISE instance KnownNat n + => FoldableWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-} + {-# SPECIALISE instance KnownNat n + => FoldableWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-} +-- | Since 0.2.0.0 +instance (Integral i, TraversableWithIndex i f, KnownNat n) + => TraversableWithIndex (Ordinal n) (Sized f n) where + itraverse f = fmap Sized . itraverse (f . unsafeNaturalToOrd . fromIntegral) . runSized + {-# INLINE itraverse #-} + + {-# SPECIALISE instance KnownNat n + => TraversableWithIndex (Ordinal n) (Sized [] (n :: Nat)) #-} + {-# SPECIALISE instance KnownNat n + => TraversableWithIndex (Ordinal n) (Sized V.Vector (n :: Nat)) #-} + {-# SPECIALISE instance KnownNat n + => TraversableWithIndex (Ordinal n) (Sized Seq.Seq (n :: Nat)) #-} diff --git a/test/Shared.hs b/test/Shared.hs new file mode 100644 --- /dev/null +++ b/test/Shared.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# OPTIONS_GHC -O2 -fno-hpc #-} + +module Shared where + +import Language.Haskell.TH (ExpQ) +import Test.Tasty.Inspection + +inspecting :: String -> Obligation -> ExpQ +inspecting title obl = inspectTest $ obl {testName = Just title} + +data GHCVer = GHC8_8 | GHC8_10 | GHC9_0 | GHC9_2 | GHC9_4 | GHC9_6 | GHC9_8 | GHC9_10 + deriving (Show, Eq, Ord) + +ghcVer :: GHCVer +#if __GLASGOW_HASKELL__ == 910 +ghcVer = GHC9_10 +#elif __GLASGOW_HASKELL__ == 908 +ghcVer = GHC9_8 +#elif __GLASGOW_HASKELL__ == 906 +ghcVer = GHC9_6 +#elif __GLASGOW_HASKELL__ == 904 +ghcVer = GHC9_4 +#elif __GLASGOW_HASKELL__ == 902 +ghcVer = GHC9_2 +#elif __GLASGOW_HASKELL__ == 900 +ghcVer = GHC9_0 +#elif __GLASGOW_HASKELL__ == 810 +ghcVer = GHC8_10 +#elif __GLASGOW_HASKELL__ == 808 +ghcVer = GHC8_8 +#else +ghcVer = error "Coudld not determine GHC Version: __GLASGOW_HASKELL__" +#endif diff --git a/test/opt-test.hs b/test/opt-test.hs new file mode 100644 --- /dev/null +++ b/test/opt-test.hs @@ -0,0 +1,182 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -O2 -fno-hpc #-} +{-# OPTIONS_GHC -dsuppress-idinfo -dsuppress-coercions + -dsuppress-type-applications + -dsuppress-module-prefixes -dsuppress-type-signatures + -dsuppress-uniques #-} + +module Main where + +import Control.Subcategory +import qualified Data.Sequence as Seq +import Data.Sized (Sized, zipWithSame) +import qualified Data.Sized as SV +import Data.Type.Natural +import qualified Data.Vector as V +import qualified Data.Vector.Generic as G +import Data.Vector.Storable (Storable) +import qualified Data.Vector.Storable as S +import Data.Vector.Unboxed (Unbox) +import qualified Data.Vector.Unboxed as U +import Numeric.Natural (Natural) +import Shared +import Test.Tasty +import Test.Tasty.Inspection +import qualified Data.Vector.Generic.Mutable as MV +import Control.Monad.Primitive (PrimMonad) + +type LSized = Sized [] + +type VSized = Sized V.Vector + +type USized = Sized U.Vector + +type SSized = Sized S.Vector + +type SeqSized = Sized Seq.Seq + +{-# ANN module "HLINT: ignore Use camelCase" #-} + +zipWith_subcat_List :: + (Int -> Int -> Int) -> [Int] -> [Int] -> [Int] +zipWith_subcat_List = czipWith + +zipWith_List :: + (Int -> Int -> Int) -> LSized n Int -> LSized m Int -> LSized (Min n m) Int +zipWith_List = SV.zipWith + +zipWithSame_List :: + (Int -> Int -> Int) -> LSized n Int -> LSized n Int -> LSized n Int +zipWithSame_List = zipWithSame + +zipWith_List_Prel :: (Int -> Int -> Int) -> [Int] -> [Int] -> [Int] +zipWith_List_Prel = zipWith + +zipWithSame_Boxed :: (a -> b -> c) -> VSized n a -> VSized n b -> VSized n c +zipWithSame_Boxed = zipWithSame + +zipWithSame_Boxed_mono :: + (Int -> (Integer -> Bool) -> [Int]) -> + VSized n Int -> + VSized n (Integer -> Bool) -> + VSized n [Int] +zipWithSame_Boxed_mono = zipWithSame + +zipWithSame_Unboxed :: + (Unbox a, Unbox b, Unbox c) => + (a -> b -> c) -> + USized n a -> + USized n b -> + USized n c +zipWithSame_Unboxed = zipWithSame + +zipWithSame_Unboxed_monomorphic :: + (Int -> Char -> Bool) -> USized n Int -> USized n Char -> USized n Bool +zipWithSame_Unboxed_monomorphic = zipWithSame + +zipWith_Unboxed :: + (Unbox a, Unbox b, Unbox c) => + (a -> b -> c) -> + U.Vector a -> + U.Vector b -> + U.Vector c +zipWith_Unboxed = U.zipWith + +zipWith_Unboxed_monomorphic :: + (Int -> Char -> Bool) -> U.Vector Int -> U.Vector Char -> U.Vector Bool +zipWith_Unboxed_monomorphic = U.zipWith + +zipWithSame_Storable :: + (Storable a, Storable b, Storable c) => + (a -> b -> c) -> + SSized n a -> + SSized n b -> + SSized n c +zipWithSame_Storable = zipWithSame + +zipWithSame_Seq :: + (a -> b -> c) -> SeqSized n a -> SeqSized n b -> SeqSized n c +zipWithSame_Seq = zipWithSame + +zipWith_Boxed :: (a -> b -> c) -> V.Vector a -> V.Vector b -> V.Vector c +zipWith_Boxed = V.zipWith + +length_two :: Dom f a => Sized f 2 a -> Int +length_two = SV.length + +const_two_dom :: Dom f a => Sized f 2 a -> Int +const_two_dom = const 2 + +main :: IO () +main = + defaultMain $ + testGroup + "Optimisation test" + [ testGroup + "czipWith" + [ $( inspecting "doesn't contain type classes" $ + hasNoTypeClasses 'zipWith_subcat_List + ) + ] + , testGroup + "zipWith" + [ $( inspecting "doesn't contain type classes" $ + hasNoTypeClasses 'zipWith_List + ) + ] + , testGroup + "zipWithSame" + [ testGroup + "list" + [ $( inspecting "doesn't contain type classes" $ + hasNoTypeClasses 'zipWithSame_List + ) + , $( inspecting "is almost the same as the original zipWith (list)" $ + 'zipWithSame_List ==- 'zipWith_List_Prel + ) + ] + , testGroup + "Boxed Vector" + [ $( inspecting "doesn't contain type classes, except for G.Vector" $ + 'zipWithSame_Boxed + `hasNoTypeClassesExcept` [''G.Vector] + ) + , $( inspecting "is almost the same as the original zipWith (Boxed)" $ + 'zipWithSame_Boxed ==- 'zipWith_Boxed + ) + ] + , testGroup + "Unboxed Vector" + [ $( inspecting "doesn't contain type classes except for Unbox, and Vector, MVector (>= GHC 9)" $ + 'zipWithSame_Unboxed + `hasNoTypeClassesExcept` + if ghcVer >= GHC9_0 + then + if ghcVer >= GHC9_6 + then [''Unbox, ''G.Vector, ''MV.MVector] + else [''Unbox, ''G.Vector, ''MV.MVector, ''Monad, ''PrimMonad] + else [''Unbox] + ) + + , $( inspecting "doesn't contain type classes if fully instnatiated" $ + hasNoTypeClasses 'zipWithSame_Unboxed_monomorphic + ) + , $( inspecting "is almost the same as the original zipWith, if fully instantiated" $ + 'zipWithSame_Unboxed_monomorphic + ==- 'zipWith_Unboxed_monomorphic + ) + ] + ] + , testGroup + "length" + [ $( inspecting "is a constant function when length is concrete (with Dom dictionary)" $ + 'length_two ==- 'const_two_dom + ) + , $( inspecting "doesn't contain Integer when the length is concrete" $ hasNoType 'length_two ''Integer + ) + , $( inspecting "doesn't contain Natural when the length is concrete" $ hasNoType 'length_two ''Natural + ) + ] + ]