{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- |
-- Module        : Data.Sized
-- Copyright     : Gautier DI FOLCO
-- License       : BSD2
--
-- Maintainer    : Gautier DI FOLCO <gautier.difolco@gmail.com>
-- Stability     : Unstable
-- Portability   : GHC
--
-- Create Sized version of any container.
module Data.Sized
  ( -- * Base type
    Sized,
    getSized,
    trustedSized,
    unknownSized,
    Unknown,
    Between,
    Exactly,
    AtLeast,
    AtMost,

    -- * Singleton constructor
    SizedSingleton (..),
    singleton,
    MkSizedSingletonApplicative (..),

    -- * From container
    Size (..),
    SizedFromContainer (..),
    MkSizedFromContainerFoldable (..),

    -- * Operations
    overSized,
    overSized2,
    overSized3,
    overSized4,
    overSized5,
    trustedChangeOverSized,
    trustedChangeOverSized2,
    trustedChangeOverSized3,
    trustedChangeOverSized4,
    trustedChangeOverSized5,
    fmapSized,
    withSized,
    precise,
    approximate,
    (<<>>),
    withSizedAppend,
    withSizedRetract,
    withSizedSubtract,
    withSizedProduct,

    -- * Type-level
    IsMoreGeneral,
    IsNotEmpty,
    type (<+>),
    RestrictAtMost,
    type (<->),
    type (<*>),
    Includes,
  )
where

import Data.Foldable (toList)
import Data.Ix (inRange)
import Data.Kind
import Data.Maybe (fromJust)
import Data.Proxy
import GHC.TypeLits as TypeLits

-- | Sized proofed value.
newtype Sized s a = Sized
  { -- | Extract the Sized proven value
    Sized s a -> a
getSized :: a
  }
  deriving stock (Sized s a -> Sized s a -> Bool
(Sized s a -> Sized s a -> Bool)
-> (Sized s a -> Sized s a -> Bool) -> Eq (Sized s a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s a. Eq a => Sized s a -> Sized s a -> Bool
/= :: Sized s a -> Sized s a -> Bool
$c/= :: forall s a. Eq a => Sized s a -> Sized s a -> Bool
== :: Sized s a -> Sized s a -> Bool
$c== :: forall s a. Eq a => Sized s a -> Sized s a -> Bool
Eq, Eq (Sized s a)
Eq (Sized s a)
-> (Sized s a -> Sized s a -> Ordering)
-> (Sized s a -> Sized s a -> Bool)
-> (Sized s a -> Sized s a -> Bool)
-> (Sized s a -> Sized s a -> Bool)
-> (Sized s a -> Sized s a -> Bool)
-> (Sized s a -> Sized s a -> Sized s a)
-> (Sized s a -> Sized s a -> Sized s a)
-> Ord (Sized s a)
Sized s a -> Sized s a -> Bool
Sized s a -> Sized s a -> Ordering
Sized s a -> Sized s a -> Sized s a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s a. Ord a => Eq (Sized s a)
forall s a. Ord a => Sized s a -> Sized s a -> Bool
forall s a. Ord a => Sized s a -> Sized s a -> Ordering
forall s a. Ord a => Sized s a -> Sized s a -> Sized s a
min :: Sized s a -> Sized s a -> Sized s a
$cmin :: forall s a. Ord a => Sized s a -> Sized s a -> Sized s a
max :: Sized s a -> Sized s a -> Sized s a
$cmax :: forall s a. Ord a => Sized s a -> Sized s a -> Sized s a
>= :: Sized s a -> Sized s a -> Bool
$c>= :: forall s a. Ord a => Sized s a -> Sized s a -> Bool
> :: Sized s a -> Sized s a -> Bool
$c> :: forall s a. Ord a => Sized s a -> Sized s a -> Bool
<= :: Sized s a -> Sized s a -> Bool
$c<= :: forall s a. Ord a => Sized s a -> Sized s a -> Bool
< :: Sized s a -> Sized s a -> Bool
$c< :: forall s a. Ord a => Sized s a -> Sized s a -> Bool
compare :: Sized s a -> Sized s a -> Ordering
$ccompare :: forall s a. Ord a => Sized s a -> Sized s a -> Ordering
$cp1Ord :: forall s a. Ord a => Eq (Sized s a)
Ord, Int -> Sized s a -> ShowS
[Sized s a] -> ShowS
Sized s a -> String
(Int -> Sized s a -> ShowS)
-> (Sized s a -> String)
-> ([Sized s a] -> ShowS)
-> Show (Sized s a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s a. Show a => Int -> Sized s a -> ShowS
forall s a. Show a => [Sized s a] -> ShowS
forall s a. Show a => Sized s a -> String
showList :: [Sized s a] -> ShowS
$cshowList :: forall s a. Show a => [Sized s a] -> ShowS
show :: Sized s a -> String
$cshow :: forall s a. Show a => Sized s a -> String
showsPrec :: Int -> Sized s a -> ShowS
$cshowsPrec :: forall s a. Show a => Int -> Sized s a -> ShowS
Show)

-- * Different kind of sizes

-- | Unknown/any size
data Unknown

-- | Exactly 'n'
data Exactly (n :: Nat)

-- | At least 'n'
data AtLeast (n :: Nat)

-- | At most 'n'
data AtMost (n :: Nat)

-- | Between (included) '(n..m)'
data Between (n :: Nat) (m :: Nat)

-- * Operations

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is size-conservative)
overSized :: (a -> b) -> Sized s a -> Sized s b
overSized :: (a -> b) -> Sized s a -> Sized s b
overSized a -> b
f = b -> Sized s b
forall a s. a -> Sized s a
trustedSized (b -> Sized s b) -> (Sized s a -> b) -> Sized s a -> Sized s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> (Sized s a -> a) -> Sized s a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s a -> a
forall s a. Sized s a -> a
getSized
{-# INLINE overSized #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is size-conservative)
overSized2 :: (a -> b -> c) -> Sized s a -> Sized s b -> Sized s c
overSized2 :: (a -> b -> c) -> Sized s a -> Sized s b -> Sized s c
overSized2 a -> b -> c
f Sized s a
a = c -> Sized s c
forall a s. a -> Sized s a
trustedSized (c -> Sized s c) -> (Sized s b -> c) -> Sized s b -> Sized s c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
a) (b -> c) -> (Sized s b -> b) -> Sized s b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s b -> b
forall s a. Sized s a -> a
getSized
{-# INLINE overSized2 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is size-conservative)
overSized3 :: (a -> b -> c -> d) -> Sized s a -> Sized s b -> Sized s c -> Sized s d
overSized3 :: (a -> b -> c -> d)
-> Sized s a -> Sized s b -> Sized s c -> Sized s d
overSized3 a -> b -> c -> d
f Sized s a
a Sized s b
b = d -> Sized s d
forall a s. a -> Sized s a
trustedSized (d -> Sized s d) -> (Sized s c -> d) -> Sized s c -> Sized s d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c -> d
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
a) (Sized s b -> b
forall s a. Sized s a -> a
getSized Sized s b
b) (c -> d) -> (Sized s c -> c) -> Sized s c -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s c -> c
forall s a. Sized s a -> a
getSized
{-# INLINE overSized3 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is size-conservative)
overSized4 :: (a -> b -> c -> d -> e) -> Sized s a -> Sized s b -> Sized s c -> Sized s d -> Sized s e
overSized4 :: (a -> b -> c -> d -> e)
-> Sized s a -> Sized s b -> Sized s c -> Sized s d -> Sized s e
overSized4 a -> b -> c -> d -> e
f Sized s a
a Sized s b
b Sized s c
c = e -> Sized s e
forall a s. a -> Sized s a
trustedSized (e -> Sized s e) -> (Sized s d -> e) -> Sized s d -> Sized s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c -> d -> e
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
a) (Sized s b -> b
forall s a. Sized s a -> a
getSized Sized s b
b) (Sized s c -> c
forall s a. Sized s a -> a
getSized Sized s c
c) (d -> e) -> (Sized s d -> d) -> Sized s d -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s d -> d
forall s a. Sized s a -> a
getSized
{-# INLINE overSized4 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is size-conservative)
overSized5 :: (a -> b -> c -> d -> e -> f) -> Sized s a -> Sized s b -> Sized s c -> Sized s d -> Sized s e -> Sized s f
overSized5 :: (a -> b -> c -> d -> e -> f)
-> Sized s a
-> Sized s b
-> Sized s c
-> Sized s d
-> Sized s e
-> Sized s f
overSized5 a -> b -> c -> d -> e -> f
f Sized s a
a Sized s b
b Sized s c
c Sized s d
d = f -> Sized s f
forall a s. a -> Sized s a
trustedSized (f -> Sized s f) -> (Sized s e -> f) -> Sized s e -> Sized s f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c -> d -> e -> f
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
a) (Sized s b -> b
forall s a. Sized s a -> a
getSized Sized s b
b) (Sized s c -> c
forall s a. Sized s a -> a
getSized Sized s c
c) (Sized s d -> d
forall s a. Sized s a -> a
getSized Sized s d
d) (e -> f) -> (Sized s e -> e) -> Sized s e -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s e -> e
forall s a. Sized s a -> a
getSized
{-# INLINE overSized5 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is respects output size)
trustedChangeOverSized :: (a -> b) -> Sized s0 a -> Sized s1 b
trustedChangeOverSized :: (a -> b) -> Sized s0 a -> Sized s1 b
trustedChangeOverSized a -> b
f = b -> Sized s1 b
forall a s. a -> Sized s a
trustedSized (b -> Sized s1 b) -> (Sized s0 a -> b) -> Sized s0 a -> Sized s1 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> (Sized s0 a -> a) -> Sized s0 a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s0 a -> a
forall s a. Sized s a -> a
getSized
{-# INLINE trustedChangeOverSized #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is respects output size)
trustedChangeOverSized2 :: (a -> b -> c) -> Sized s0 a -> Sized s1 b -> Sized s2 c
trustedChangeOverSized2 :: (a -> b -> c) -> Sized s0 a -> Sized s1 b -> Sized s2 c
trustedChangeOverSized2 a -> b -> c
f Sized s0 a
a = c -> Sized s2 c
forall a s. a -> Sized s a
trustedSized (c -> Sized s2 c) -> (Sized s1 b -> c) -> Sized s1 b -> Sized s2 c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c
f (Sized s0 a -> a
forall s a. Sized s a -> a
getSized Sized s0 a
a) (b -> c) -> (Sized s1 b -> b) -> Sized s1 b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s1 b -> b
forall s a. Sized s a -> a
getSized
{-# INLINE trustedChangeOverSized2 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is respects output size)
trustedChangeOverSized3 :: (a -> b -> c -> d) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d
trustedChangeOverSized3 :: (a -> b -> c -> d)
-> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d
trustedChangeOverSized3 a -> b -> c -> d
f Sized s0 a
a Sized s1 b
b = d -> Sized s3 d
forall a s. a -> Sized s a
trustedSized (d -> Sized s3 d) -> (Sized s2 c -> d) -> Sized s2 c -> Sized s3 d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c -> d
f (Sized s0 a -> a
forall s a. Sized s a -> a
getSized Sized s0 a
a) (Sized s1 b -> b
forall s a. Sized s a -> a
getSized Sized s1 b
b) (c -> d) -> (Sized s2 c -> c) -> Sized s2 c -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s2 c -> c
forall s a. Sized s a -> a
getSized
{-# INLINE trustedChangeOverSized3 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is respects output size)
trustedChangeOverSized4 :: (a -> b -> c -> d -> e) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d -> Sized s4 e
trustedChangeOverSized4 :: (a -> b -> c -> d -> e)
-> Sized s0 a
-> Sized s1 b
-> Sized s2 c
-> Sized s3 d
-> Sized s4 e
trustedChangeOverSized4 a -> b -> c -> d -> e
f Sized s0 a
a Sized s1 b
b Sized s2 c
c = e -> Sized s4 e
forall a s. a -> Sized s a
trustedSized (e -> Sized s4 e) -> (Sized s3 d -> e) -> Sized s3 d -> Sized s4 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c -> d -> e
f (Sized s0 a -> a
forall s a. Sized s a -> a
getSized Sized s0 a
a) (Sized s1 b -> b
forall s a. Sized s a -> a
getSized Sized s1 b
b) (Sized s2 c -> c
forall s a. Sized s a -> a
getSized Sized s2 c
c) (d -> e) -> (Sized s3 d -> d) -> Sized s3 d -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s3 d -> d
forall s a. Sized s a -> a
getSized
{-# INLINE trustedChangeOverSized4 #-}

-- | Wrap and unwrap 'Sized' (unsafe, be sure 'f' is respects output size)
trustedChangeOverSized5 :: (a -> b -> c -> d -> e -> f) -> Sized s0 a -> Sized s1 b -> Sized s2 c -> Sized s3 d -> Sized s4 e -> Sized s5 f
trustedChangeOverSized5 :: (a -> b -> c -> d -> e -> f)
-> Sized s0 a
-> Sized s1 b
-> Sized s2 c
-> Sized s3 d
-> Sized s4 e
-> Sized s5 f
trustedChangeOverSized5 a -> b -> c -> d -> e -> f
f Sized s0 a
a Sized s1 b
b Sized s2 c
c Sized s3 d
d = f -> Sized s5 f
forall a s. a -> Sized s a
trustedSized (f -> Sized s5 f) -> (Sized s4 e -> f) -> Sized s4 e -> Sized s5 f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c -> d -> e -> f
f (Sized s0 a -> a
forall s a. Sized s a -> a
getSized Sized s0 a
a) (Sized s1 b -> b
forall s a. Sized s a -> a
getSized Sized s1 b
b) (Sized s2 c -> c
forall s a. Sized s a -> a
getSized Sized s2 c
c) (Sized s3 d -> d
forall s a. Sized s a -> a
getSized Sized s3 d
d) (e -> f) -> (Sized s4 e -> e) -> Sized s4 e -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s4 e -> e
forall s a. Sized s a -> a
getSized
{-# INLINE trustedChangeOverSized5 #-}

-- | 'fmap' over a 'Sized' container
fmapSized :: Functor f => (a -> b) -> Sized s (f a) -> Sized s (f b)
fmapSized :: (a -> b) -> Sized s (f a) -> Sized s (f b)
fmapSized a -> b
f = (f a -> f b) -> Sized s (f a) -> Sized s (f b)
forall a b s. (a -> b) -> Sized s a -> Sized s b
overSized ((a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)
{-# INLINE fmapSized #-}

-- | Apply an unsafe function over empty, which is safe over 'Sized'
withSized :: (a -> Maybe b) -> Sized s a -> b
withSized :: (a -> Maybe b) -> Sized s a -> b
withSized a -> Maybe b
f = Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe b -> b) -> (Sized s a -> Maybe b) -> Sized s a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
f (a -> Maybe b) -> (Sized s a -> a) -> Sized s a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s a -> a
forall s a. Sized s a -> a
getSized
{-# INLINE withSized #-}

-- | Trusted value
trustedSized :: a -> Sized s a
trustedSized :: a -> Sized s a
trustedSized = a -> Sized s a
forall s a. a -> Sized s a
Sized
{-# INLINE trustedSized #-}

-- | Unknown value
unknownSized :: a -> Sized Unknown a
unknownSized :: a -> Sized Unknown a
unknownSized = a -> Sized Unknown a
forall s a. a -> Sized s a
Sized
{-# INLINE unknownSized #-}

-- | Singleton constructible value
class SizedSingleton a where
  type SizedSingletonElement a :: Type
  sizedSingleton :: Proxy a -> SizedSingletonElement a -> a

-- | Build a 'Sized' value from a singleton value
singleton :: SizedSingleton a => Proxy a -> SizedSingletonElement a -> Sized (Exactly 1) a
singleton :: Proxy a -> SizedSingletonElement a -> Sized (Exactly 1) a
singleton Proxy a
p = a -> Sized (Exactly 1) a
forall a s. a -> Sized s a
trustedSized (a -> Sized (Exactly 1) a)
-> (SizedSingletonElement a -> a)
-> SizedSingletonElement a
-> Sized (Exactly 1) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> SizedSingletonElement a -> a
forall a.
SizedSingleton a =>
Proxy a -> SizedSingletonElement a -> a
sizedSingleton Proxy a
p
{-# INLINE singleton #-}

-- | Build 'SizedSingleton' for 'Applicative' defined types
--   to be used with 'DerivingVia':
--
--   > deriving instance SizedSingleton [a] via (MkSizedSingletonApplicative [a])
newtype MkSizedSingletonApplicative a
  = MkSizedSingletonApplicative a

instance Applicative f => SizedSingleton (f a) where
  type SizedSingletonElement (f a) = a
  sizedSingleton :: Proxy (f a) -> SizedSingletonElement (f a) -> f a
sizedSingleton Proxy (f a)
_ = SizedSingletonElement (f a) -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- * From container

-- | Used to attempt conversion from possibly any size to 'Sized'.
class SizedFromContainer a where
  calculateSize :: a -> Int
  isAtLeast :: Int -> a -> Bool
  isAtLeast Int
n = (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n) (Int -> Bool) -> (a -> Int) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a. SizedFromContainer a => a -> Int
calculateSize
  isAtMost :: Int -> a -> Bool
  isAtMost Int
n = (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n) (Int -> Bool) -> (a -> Int) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a. SizedFromContainer a => a -> Int
calculateSize
  isExactly :: Int -> a -> Bool
  isExactly Int
n = (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) (Int -> Bool) -> (a -> Int) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a. SizedFromContainer a => a -> Int
calculateSize
  isBetween :: Int -> Int -> a -> Bool
  isBetween Int
n Int
m = (Int, Int) -> Int -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange (Int
n, Int
m) (Int -> Bool) -> (a -> Int) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall a. SizedFromContainer a => a -> Int
calculateSize

-- | Convert a container from possibly any size to 'Sized'.
class Size s where
  sized :: SizedFromContainer a => a -> Maybe (Sized s a)

instance Size Unknown where
  sized :: a -> Maybe (Sized Unknown a)
sized = Sized Unknown a -> Maybe (Sized Unknown a)
forall a. a -> Maybe a
Just (Sized Unknown a -> Maybe (Sized Unknown a))
-> (a -> Sized Unknown a) -> a -> Maybe (Sized Unknown a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Sized Unknown a
forall a s. a -> Sized s a
trustedSized

instance KnownNat n => Size (Exactly n) where
  sized :: a -> Maybe (Sized (Exactly n) a)
sized = (a -> Bool) -> a -> Maybe (Sized (Exactly n) a)
forall a s. (a -> Bool) -> a -> Maybe (Sized s a)
mkSized ((a -> Bool) -> a -> Maybe (Sized (Exactly n) a))
-> (a -> Bool) -> a -> Maybe (Sized (Exactly n) a)
forall a b. (a -> b) -> a -> b
$ Int -> a -> Bool
forall a. SizedFromContainer a => Int -> a -> Bool
isExactly (Int -> a -> Bool) -> Int -> a -> Bool
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> Proxy n -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n
forall k (t :: k). Proxy t
Proxy @n

instance KnownNat n => Size (AtLeast n) where
  sized :: a -> Maybe (Sized (AtLeast n) a)
sized = (a -> Bool) -> a -> Maybe (Sized (AtLeast n) a)
forall a s. (a -> Bool) -> a -> Maybe (Sized s a)
mkSized ((a -> Bool) -> a -> Maybe (Sized (AtLeast n) a))
-> (a -> Bool) -> a -> Maybe (Sized (AtLeast n) a)
forall a b. (a -> b) -> a -> b
$ Int -> a -> Bool
forall a. SizedFromContainer a => Int -> a -> Bool
isAtLeast (Int -> a -> Bool) -> Int -> a -> Bool
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> Proxy n -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n
forall k (t :: k). Proxy t
Proxy @n

instance KnownNat n => Size (AtMost n) where
  sized :: a -> Maybe (Sized (AtMost n) a)
sized = (a -> Bool) -> a -> Maybe (Sized (AtMost n) a)
forall a s. (a -> Bool) -> a -> Maybe (Sized s a)
mkSized ((a -> Bool) -> a -> Maybe (Sized (AtMost n) a))
-> (a -> Bool) -> a -> Maybe (Sized (AtMost n) a)
forall a b. (a -> b) -> a -> b
$ Int -> a -> Bool
forall a. SizedFromContainer a => Int -> a -> Bool
isAtMost (Int -> a -> Bool) -> Int -> a -> Bool
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> Proxy n -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n
forall k (t :: k). Proxy t
Proxy @n

instance (KnownNat n, KnownNat m, n <= m) => Size (Between n m) where
  sized :: a -> Maybe (Sized (Between n m) a)
sized = (a -> Bool) -> a -> Maybe (Sized (Between n m) a)
forall a s. (a -> Bool) -> a -> Maybe (Sized s a)
mkSized ((a -> Bool) -> a -> Maybe (Sized (Between n m) a))
-> (a -> Bool) -> a -> Maybe (Sized (Between n m) a)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> a -> Bool
forall a. SizedFromContainer a => Int -> Int -> a -> Bool
isBetween (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> Proxy n -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n
forall k (t :: k). Proxy t
Proxy @n) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m -> Integer) -> Proxy m -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy m
forall k (t :: k). Proxy t
Proxy @m)

mkSized :: (a -> Bool) -> a -> Maybe (Sized s a)
mkSized :: (a -> Bool) -> a -> Maybe (Sized s a)
mkSized a -> Bool
p a
x =
  if a -> Bool
p a
x
    then Sized s a -> Maybe (Sized s a)
forall a. a -> Maybe a
Just (Sized s a -> Maybe (Sized s a)) -> Sized s a -> Maybe (Sized s a)
forall a b. (a -> b) -> a -> b
$ a -> Sized s a
forall a s. a -> Sized s a
trustedSized a
x
    else Maybe (Sized s a)
forall a. Maybe a
Nothing

-- | Build 'MkSizedFromContainerFoldable' for 'Foldable' defined types
--   to be used with 'DerivingVia':
--
--   > deriving instance SizedFromContainer [a] via (MkSizedFromContainerFoldable [a])
newtype MkSizedFromContainerFoldable a
  = MkSizedFromContainerFoldable a

instance Foldable f => SizedFromContainer (f a) where
  calculateSize :: f a -> Int
calculateSize = f a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
  isExactly :: Int -> f a -> Bool
isExactly Int
n = ([Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int
Item [Int]
n]) ([Int] -> Bool) -> (f a -> [Int]) -> f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop Int
n ([Int] -> [Int]) -> (f a -> [Int]) -> f a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> [Int]
forall (f :: * -> *) a. Foldable f => f a -> [Int]
index
  isAtLeast :: Int -> f a -> Bool
isAtLeast Int
n = Bool -> Bool
not (Bool -> Bool) -> (f a -> Bool) -> f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int] -> Bool) -> (f a -> [Int]) -> f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
drop Int
n ([Int] -> [Int]) -> (f a -> [Int]) -> f a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> [Int]
forall (f :: * -> *) a. Foldable f => f a -> [Int]
index
  isAtMost :: Int -> f a -> Bool
isAtMost Int
n = [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> (f a -> [a]) -> f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
n ([a] -> [a]) -> (f a -> [a]) -> f a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
  isBetween :: Int -> Int -> f a -> Bool
isBetween Int
n Int
m f a
x =
    let indexed :: [Int]
indexed = f a -> [Int]
forall (f :: * -> *) a. Foldable f => f a -> [Int]
index f a
x
     in Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
n [Int]
indexed Bool -> Bool -> Bool
&& Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (Int -> Int
forall a. Enum a => a -> a
succ Int
m) [Int]
indexed

index :: Foldable f => f a -> [Int]
index :: f a -> [Int]
index = (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:) ([Int] -> [Int]) -> (f a -> [Int]) -> f a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> a -> Int) -> [Int] -> [a] -> [Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> a -> Int
forall a b. a -> b -> a
const [Item [Int]
1 ..] ([a] -> [Int]) -> (f a -> [a]) -> f a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

-- | Give a more precise sizing
precise :: (SizedFromContainer a, Size s) => Sized s' a -> Maybe (Sized s a)
precise :: Sized s' a -> Maybe (Sized s a)
precise = a -> Maybe (Sized s a)
forall s a.
(Size s, SizedFromContainer a) =>
a -> Maybe (Sized s a)
sized (a -> Maybe (Sized s a))
-> (Sized s' a -> a) -> Sized s' a -> Maybe (Sized s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s' a -> a
forall s a. Sized s a -> a
getSized
{-# INLINE precise #-}

type family IsMoreGeneral general restrictive :: Constraint where
  IsMoreGeneral (AtLeast n) (AtLeast m) = (n <= m)
  IsMoreGeneral (AtMost n) (AtMost m) = (m <= n)
  IsMoreGeneral (AtLeast n) (Exactly m) = (n <= m)
  IsMoreGeneral (AtMost n) (Exactly m) = (m <= n)
  IsMoreGeneral (AtLeast n) (Between m o) = (n <= m)
  IsMoreGeneral (AtMost n) (Between m o) = (o <= n)
  IsMoreGeneral (Between n m) (Between o p) = (n <= o, p <= m)
  IsMoreGeneral (Between n m) (Exactly o) = (n <= o, o <= m)
  IsMoreGeneral Unknown a = ()

type IsNotEmpty s = IsMoreGeneral s (Exactly 1)

-- | Give a more general sizing
approximate :: IsMoreGeneral s s' => Sized s' a -> Sized s a
approximate :: Sized s' a -> Sized s a
approximate = a -> Sized s a
forall a s. a -> Sized s a
trustedSized (a -> Sized s a) -> (Sized s' a -> a) -> Sized s' a -> Sized s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s' a -> a
forall s a. Sized s a -> a
getSized
{-# INLINE approximate #-}

-- | Concatenative operation of 'Sized'
withSizedAppend :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <+> s') c
withSizedAppend :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <+> s') c
withSizedAppend a -> b -> c
f Sized s a
x Sized s' b
y = c -> Sized (s <+> s') c
forall a s. a -> Sized s a
trustedSized (c -> Sized (s <+> s') c) -> c -> Sized (s <+> s') c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
x) (Sized s' b -> b
forall s a. Sized s a -> a
getSized Sized s' b
y)

type family (<+>) a b where
  (<+>) Unknown b = Unknown
  (<+>) a Unknown = Unknown
  (<+>) (AtMost n) (AtMost m) = AtMost (n + m)
  (<+>) (AtMost n) (Exactly m) = AtMost (n + m)
  (<+>) (Exactly n) (Exactly m) = Exactly (n + m)
  (<+>) (Exactly n) (AtMost m) = AtMost (n + m)
  (<+>) (Exactly n) (AtLeast m) = AtLeast (n + m)
  (<+>) (AtLeast n) (Exactly m) = AtLeast (n + m)
  (<+>) (AtLeast n) (AtLeast m) = AtLeast (n + m)
  (<+>) (AtLeast n) (AtMost m) = Between n (n + m)
  (<+>) (AtMost n) (AtLeast m) = Between m (n + m)
  (<+>) (AtLeast n) (Between m o) = Between (n + m) (n + o)
  (<+>) (AtMost n) (Between m o) = Between m (n + o)
  (<+>) (Between n m) (Exactly o) = Between (n + o) (m + o)
  (<+>) (Exactly o) (Between n m) = Between (n + o) (m + o)
  (<+>) (Between m o) (AtLeast n) = Between (n + m) (n + o)
  (<+>) (Between m o) (AtMost n) = Between m (n + o)
  (<+>) (Between n m) (Between o p) = Between (n + o) (m + p)

-- | Semigroup append
(<<>>) :: Semigroup a => Sized s a -> Sized s' a -> Sized (s <+> s') a
<<>> :: Sized s a -> Sized s' a -> Sized (s <+> s') a
(<<>>) = (a -> a -> a) -> Sized s a -> Sized s' a -> Sized (s <+> s') a
forall a b c s s'.
(a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <+> s') c
withSizedAppend a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)
{-# INLINE (<<>>) #-}

infixr 6 <<>>

type family RestrictAtMost a where
  RestrictAtMost Unknown = Unknown
  RestrictAtMost (AtMost n) = AtMost n
  RestrictAtMost (AtLeast n) = AtLeast 0
  RestrictAtMost (Between n m) = AtMost m
  RestrictAtMost (Exactly n) = AtMost n

withSizedRetract :: (a -> b) -> Sized s a -> Sized (RestrictAtMost s) b
withSizedRetract :: (a -> b) -> Sized s a -> Sized (RestrictAtMost s) b
withSizedRetract a -> b
f = b -> Sized (RestrictAtMost s) b
forall a s. a -> Sized s a
trustedSized (b -> Sized (RestrictAtMost s) b)
-> (Sized s a -> b) -> Sized s a -> Sized (RestrictAtMost s) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> (Sized s a -> a) -> Sized s a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized s a -> a
forall s a. Sized s a -> a
getSized

type family (<->) a b where
  (<->) Unknown b = Unknown
  (<->) a Unknown = Unknown
  (<->) (AtMost n) (AtMost m) = AtMost (n - m)
  (<->) (Exactly n) (AtMost m) = AtMost (n - m)
  (<->) (AtMost n) (Exactly m) = AtMost (n - m)
  (<->) (Exactly n) (Exactly m) = Exactly (n - m)
  (<->) (Exactly n) (AtLeast m) = AtLeast (n - m)
  (<->) (AtLeast n) (Exactly m) = AtLeast (n - m)
  (<->) (AtLeast n) (AtLeast m) = AtLeast (n - m)
  (<->) (AtLeast n) (AtMost m) = AtLeast (n - m)
  (<->) (AtMost n) (AtLeast m) = AtLeast 0
  (<->) (AtLeast n) (Between m o) = AtLeast (m - n)
  (<->) (AtMost n) (Between m o) = Between (m - n) o
  (<->) (Between n m) (Exactly o) = Between (n - o) (m - o)
  (<->) (Exactly o) (Between n m) = Between (o - n) (o - m)
  (<->) (Between m o) (AtLeast n) = AtLeast 0
  (<->) (Between m o) (AtMost n) = Between m (o - n)
  (<->) (Between n m) (Between o p) = Between (n - o) (m - p)

withSizedSubtract :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <-> s') c
withSizedSubtract :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <-> s') c
withSizedSubtract a -> b -> c
f Sized s a
a Sized s' b
b = c -> Sized (s <-> s') c
forall a s. a -> Sized s a
trustedSized (c -> Sized (s <-> s') c) -> c -> Sized (s <-> s') c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
a) (Sized s' b -> b
forall s a. Sized s a -> a
getSized Sized s' b
b)

type family (<*>) a b where
  (<*>) Unknown b = Unknown
  (<*>) a Unknown = Unknown
  (<*>) (AtMost n) (AtMost m) = AtMost (n TypeLits.* m)
  (<*>) (Exactly n) (AtMost m) = AtMost (n TypeLits.* m)
  (<*>) (AtMost n) (Exactly m) = AtMost (n TypeLits.* m)
  (<*>) (Exactly n) (Exactly m) = Exactly (n TypeLits.* m)
  (<*>) (AtLeast n) (Exactly m) = AtLeast (n TypeLits.* m)
  (<*>) (Exactly n) (AtLeast m) = AtLeast (n TypeLits.* m)
  (<*>) (AtLeast n) (AtLeast m) = AtLeast (n TypeLits.* m)
  (<*>) (AtLeast n) (AtMost m) = AtLeast 0
  (<*>) (AtMost n) (AtLeast m) = AtLeast 0
  (<*>) (AtLeast n) (Between m o) = AtLeast (m TypeLits.* n)
  (<*>) (AtMost n) (Between m o) = AtLeast 0
  (<*>) (Between n m) (Exactly o) = Between (n TypeLits.* o) (m TypeLits.* o)
  (<*>) (Exactly o) (Between n m) = Between (n TypeLits.* o) (m TypeLits.* o)
  (<*>) (Between m o) (AtLeast n) = AtLeast (m TypeLits.* n)
  (<*>) (Between m o) (AtMost n) = AtLeast 0
  (<*>) (Between n m) (Between o p) = Between (n TypeLits.* o) (m TypeLits.* p)

withSizedProduct :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <*> s') c
withSizedProduct :: (a -> b -> c) -> Sized s a -> Sized s' b -> Sized (s <*> s') c
withSizedProduct a -> b -> c
f Sized s a
a Sized s' b
b = c -> Sized (s <*> s') c
forall a s. a -> Sized s a
trustedSized (c -> Sized (s <*> s') c) -> c -> Sized (s <*> s') c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f (Sized s a -> a
forall s a. Sized s a -> a
getSized Sized s a
a) (Sized s' b -> b
forall s a. Sized s a -> a
getSized Sized s' b
b)

type family Includes (sized :: Type) (size :: Nat) :: Constraint where
  Includes (AtLeast n) m = (n <= m)
  Includes (AtMost n) m = (m <= n)
  Includes (Between n m) o = (n <= o, o <= m)
  Includes Unknown a = ()