--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Finite.Integral
-- Copyright   :  (C) 2015-2022 mniip
-- License     :  BSD3
-- Maintainer  :  mniip <mniip@mniip.com>
-- Stability   :  experimental
-- Portability :  portable
--------------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Finite.Integral
    (
        SaneIntegral, Limited, KnownIntegral, intVal,
        withIntegral,
        Finite,
        packFinite, packFiniteProxy,
        finite, finiteProxy,
        getFinite, finites, finitesProxy,
        modulo, moduloProxy,
        equals, cmp,
        natToFinite,
        weaken, strengthen, shift, unshift,
        weakenN, strengthenN, shiftN, unshiftN,
        weakenProxy, strengthenProxy, shiftProxy, unshiftProxy,
        add, sub, multiply,
        combineSum, combineZero, combineProduct, combineOne, combineExponential,
        separateSum, separateZero, separateProduct, separateOne,
        separateExponential,
        isValidFinite
    )
    where

import Data.Coerce
import Data.List
import Data.Proxy
import Data.Void
import GHC.TypeLits

import Data.Finite.Internal.Integral

-- | Convert an @a@ into a @'Finite' a@, returning 'Nothing' if the input is
-- out of bounds.
packFinite
    :: forall n a. (SaneIntegral a, KnownIntegral a n)
    => a -> Maybe (Finite a n)
packFinite :: forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Maybe (Finite a n)
packFinite a
x
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = Finite a n -> Maybe (Finite a n)
forall a. a -> Maybe a
Just (Finite a n -> Maybe (Finite a n))
-> Finite a n -> Maybe (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite a
x
    | Bool
otherwise = Maybe (Finite a n)
forall a. Maybe a
Nothing
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE packFinite #-}

-- | Same as 'packFinite' but with a proxy argument to avoid type signatures.
packFiniteProxy
    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)
    => proxy n -> a -> Maybe (Finite a n)
packFiniteProxy :: forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> a -> Maybe (Finite a n)
packFiniteProxy proxy n
_ = a -> Maybe (Finite a n)
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Maybe (Finite a n)
packFinite
{-# INLINABLE packFiniteProxy #-}

-- | Same as 'finite' but with a proxy argument to avoid type signatures.
finiteProxy
    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)
    => proxy n -> a -> Finite a n
finiteProxy :: forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> a -> Finite a n
finiteProxy proxy n
_ = a -> Finite a n
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Finite a n
finite
{-# INLINABLE finiteProxy #-}

-- | Generate an ascending list of length @n@ of all elements of @'Finite' a n@.
finites :: forall n a. (SaneIntegral a, KnownIntegral a n) => [Finite a n]
finites :: forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
[Finite a n]
finites = a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a n) -> [a] -> [Finite a n]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n) [a
0..]
    -- [0 .. n - 1] does not work if n is 0 of an unsigned type
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE finites #-}

-- | Same as 'finites' but with a proxy argument to avoid type signatures.
finitesProxy
    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)
    => proxy n -> [Finite a n]
finitesProxy :: forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> [Finite a n]
finitesProxy proxy n
_ = [Finite a n]
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
[Finite a n]
finites
{-# INLINABLE finitesProxy #-}

-- | Produce the 'Finite' that is congruent to the given integer modulo @n@.
modulo :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Finite a n
modulo :: forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Finite a n
modulo a
x
    | a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error [Char]
"modulo: division by zero"
    | Bool
otherwise = a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
n
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE modulo #-}

-- | Same as 'modulo' but with a proxy argument to avoid type signatures.
moduloProxy
    :: forall n a proxy. (SaneIntegral a, KnownIntegral a n)
    => proxy n -> a -> Finite a n
moduloProxy :: forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> a -> Finite a n
moduloProxy proxy n
_ = a -> Finite a n
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Finite a n
modulo
{-# INLINABLE moduloProxy #-}

-- | Test two different types of finite numbers for equality.
equals :: forall n m a. Eq a => Finite a n -> Finite a m -> Bool
equals :: forall (n :: Nat) (m :: Nat) a.
Eq a =>
Finite a n -> Finite a m -> Bool
equals = (a -> a -> Bool) -> Finite a n -> Finite a m -> Bool
forall a b. Coercible a b => a -> b
coerce (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: a -> a -> Bool)
infix 4 `equals`
{-# INLINABLE equals #-}

-- | Compare two different types of finite numbers.
cmp :: forall n m a. Ord a => Finite a n -> Finite a m -> Ordering
cmp :: forall (n :: Nat) (m :: Nat) a.
Ord a =>
Finite a n -> Finite a m -> Ordering
cmp = (a -> a -> Ordering) -> Finite a n -> Finite a m -> Ordering
forall a b. Coercible a b => a -> b
coerce (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare :: a -> a -> Ordering)
{-# INLINABLE cmp #-}

-- | Convert a type-level literal into a 'Finite'.
natToFinite
    :: forall n m a proxy.
        (SaneIntegral a, KnownIntegral a n, Limited a m, n + 1 <= m)
    => proxy n -> Finite a m
natToFinite :: forall (n :: Nat) (m :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n, Limited a m, (n + 1) <= m) =>
proxy n -> Finite a m
natToFinite proxy n
p = a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal proxy n
p
{-# INLINABLE natToFinite #-}

-- | Add one inhabitant in the end.
weaken :: forall n a. Limited a (n + 1) => Finite a n -> Finite a (n + 1)
weaken :: forall (n :: Nat) a.
Limited a (n + 1) =>
Finite a n -> Finite a (n + 1)
weaken = Finite a n -> Finite a (n + 1)
forall a b. Coercible a b => a -> b
coerce
{-# INLINABLE weaken #-}

-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the
-- removed inhabitant.
strengthen
    :: forall n a. (SaneIntegral a, KnownIntegral a n)
    => Finite a (n + 1) -> Maybe (Finite a n)
strengthen :: forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
Finite a (n + 1) -> Maybe (Finite a n)
strengthen (Finite a
x)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n = Finite a n -> Maybe (Finite a n)
forall a. a -> Maybe a
Just (Finite a n -> Maybe (Finite a n))
-> Finite a n -> Maybe (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite a
x
    | Bool
otherwise = Maybe (Finite a n)
forall a. Maybe a
Nothing
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE strengthen #-}

-- | Add one inhabitant in the beginning, shifting everything up by one.
shift
    :: forall n a. (SaneIntegral a, Limited a (n + 1))
    => Finite a n -> Finite a (n + 1)
shift :: forall (n :: Nat) a.
(SaneIntegral a, Limited a (n + 1)) =>
Finite a n -> Finite a (n + 1)
shift (Finite a
x) = a -> Finite a (n + 1)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (n + 1)) -> a -> Finite a (n + 1)
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
{-# INLINABLE shift #-}

-- | Remove one inhabitant from the beginning, shifting everything down by one.
-- Returns 'Nothing' if the input was the removed inhabitant.
unshift :: forall n a. SaneIntegral a => Finite a (n + 1) -> Maybe (Finite a n)
unshift :: forall (n :: Nat) a.
SaneIntegral a =>
Finite a (n + 1) -> Maybe (Finite a n)
unshift (Finite a
x)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
1 = Maybe (Finite a n)
forall a. Maybe a
Nothing
    | Bool
otherwise = Finite a n -> Maybe (Finite a n)
forall a. a -> Maybe a
Just (Finite a n -> Maybe (Finite a n))
-> Finite a n -> Maybe (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
1
{-# INLINABLE unshift #-}

-- | Add multiple inhabitants in the end.
weakenN :: forall n m a. (n <= m, Limited a m) => Finite a n -> Finite a m
weakenN :: forall (n :: Nat) (m :: Nat) a.
(n <= m, Limited a m) =>
Finite a n -> Finite a m
weakenN = Finite a n -> Finite a m
forall a b. Coercible a b => a -> b
coerce
{-# INLINABLE weakenN #-}

-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input
-- was one of the removed inhabitants.
strengthenN
    :: forall n m a. (SaneIntegral a, KnownIntegral a m, Limited a m)
    => Finite a n -> Maybe (Finite a m)
strengthenN :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a m, Limited a m) =>
Finite a n -> Maybe (Finite a m)
strengthenN (Finite a
x)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
m = Finite a m -> Maybe (Finite a m)
forall a. a -> Maybe a
Just (Finite a m -> Maybe (Finite a m))
-> Finite a m -> Maybe (Finite a m)
forall a b. (a -> b) -> a -> b
$ a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite a
x
    | Bool
otherwise = Maybe (Finite a m)
forall a. Maybe a
Nothing
    where m :: a
m = Proxy m -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
{-# INLINABLE strengthenN #-}

-- | Add multiple inhabitants in the beginning, shifting everything up by the
-- amount of inhabitants added.
shiftN
    :: forall n m a.
        ( SaneIntegral a
        , KnownIntegral a n
        , KnownIntegral a m
        , n <= m
        )
    => Finite a n -> Finite a m
shiftN :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n, KnownIntegral a m, n <= m) =>
Finite a n -> Finite a m
shiftN (Finite a
x) = a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ (a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
n)
    where
        n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
        m :: a
m = Proxy m -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
{-# INLINABLE shiftN #-}

-- | Remove multiple inhabitants from the beginning, shifting everything down by
-- the amount of inhabitants removed. Returns 'Nothing' if the input was one of
-- the removed inhabitants.
unshiftN
    :: forall n m a.
        (SaneIntegral a, KnownIntegral a n, KnownIntegral a m, Limited a m)
    => Finite a n -> Maybe (Finite a m)
unshiftN :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n, KnownIntegral a m,
 Limited a m) =>
Finite a n -> Maybe (Finite a m)
unshiftN (Finite a
x)
    | a
m a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
n = Finite a m -> Maybe (Finite a m)
forall a. a -> Maybe a
Just (Finite a m -> Maybe (Finite a m))
-> Finite a m -> Maybe (Finite a m)
forall a b. (a -> b) -> a -> b
$ a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ (a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
n)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
m = Maybe (Finite a m)
forall a. Maybe a
Nothing
    | Bool
otherwise = Finite a m -> Maybe (Finite a m)
forall a. a -> Maybe a
Just (Finite a m -> Maybe (Finite a m))
-> Finite a m -> Maybe (Finite a m)
forall a b. (a -> b) -> a -> b
$ a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
m)
    where
        n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
        m :: a
m = Proxy m -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
{-# INLINABLE unshiftN #-}

weakenProxy
    :: forall n k a proxy. (Limited a (n + k))
    => proxy k -> Finite a n -> Finite a (n + k)
weakenProxy :: forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
Limited a (n + k) =>
proxy k -> Finite a n -> Finite a (n + k)
weakenProxy proxy k
_ = Finite a n -> Finite a (n + k)
forall a b. Coercible a b => a -> b
coerce
{-# INLINABLE weakenProxy #-}

strengthenProxy
    :: forall n k a proxy. (SaneIntegral a, KnownIntegral a n)
    => proxy k -> Finite a (n + k) -> Maybe (Finite a n)
strengthenProxy :: forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy k -> Finite a (n + k) -> Maybe (Finite a n)
strengthenProxy proxy k
_ (Finite a
x)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n = Finite a n -> Maybe (Finite a n)
forall a. a -> Maybe a
Just (Finite a n -> Maybe (Finite a n))
-> Finite a n -> Maybe (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite a
x
    | Bool
otherwise = Maybe (Finite a n)
forall a. Maybe a
Nothing
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE strengthenProxy #-}

shiftProxy
    :: forall n k a proxy.
        (SaneIntegral a, KnownIntegral a k, Limited a (n + k))
    => proxy k -> Finite a n -> Finite a (n + k)
shiftProxy :: forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a k, Limited a (n + k)) =>
proxy k -> Finite a n -> Finite a (n + k)
shiftProxy proxy k
_ (Finite a
x) = a -> Finite a (n + k)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (n + k)) -> a -> Finite a (n + k)
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
k
    where k :: a
k = Proxy k -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy k
forall {k} (t :: k). Proxy t
Proxy :: Proxy k)
{-# INLINABLE shiftProxy #-}

unshiftProxy
    :: forall n k a proxy. (SaneIntegral a, KnownIntegral a k)
    => proxy k -> Finite a (n + k) -> Maybe (Finite a n)
unshiftProxy :: forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a k) =>
proxy k -> Finite a (n + k) -> Maybe (Finite a n)
unshiftProxy proxy k
_ (Finite a
x)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
k = Maybe (Finite a n)
forall a. Maybe a
Nothing
    | Bool
otherwise = Finite a n -> Maybe (Finite a n)
forall a. a -> Maybe a
Just (Finite a n -> Maybe (Finite a n))
-> Finite a n -> Maybe (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
k
    where k :: a
k = Proxy k -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy k
forall {k} (t :: k). Proxy t
Proxy :: Proxy k)
{-# INLINABLE unshiftProxy #-}

-- | Add two 'Finite's.
add
    :: forall n m a. (SaneIntegral a, Limited a (n + m))
    => Finite a n -> Finite a m -> Finite a (n + m)
add :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, Limited a (n + m)) =>
Finite a n -> Finite a m -> Finite a (n + m)
add (Finite a
x) (Finite a
y) = a -> Finite a (n + m)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (n + m)) -> a -> Finite a (n + m)
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y
{-# INLINABLE add #-}

-- | Subtract two 'Finite's. Returns 'Left' for negative results, and 'Right'
-- for positive results. Note that this function never returns @'Left' 0@.
sub
    :: forall n m a. SaneIntegral a
    => Finite a n -> Finite a m -> Either (Finite a m) (Finite a n)
sub :: forall (n :: Nat) (m :: Nat) a.
SaneIntegral a =>
Finite a n -> Finite a m -> Either (Finite a m) (Finite a n)
sub (Finite a
x) (Finite a
y)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y = Finite a n -> Either (Finite a m) (Finite a n)
forall a b. b -> Either a b
Right (Finite a n -> Either (Finite a m) (Finite a n))
-> Finite a n -> Either (Finite a m) (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y
    | Bool
otherwise = Finite a m -> Either (Finite a m) (Finite a n)
forall a b. a -> Either a b
Left (Finite a m -> Either (Finite a m) (Finite a n))
-> Finite a m -> Either (Finite a m) (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ a
y a -> a -> a
forall a. Num a => a -> a -> a
- a
x
{-# INLINABLE sub #-}

-- | Multiply two 'Finite's.
multiply
    :: forall n m a. (SaneIntegral a, Limited a (n GHC.TypeLits.* m))
    => Finite a n -> Finite a m -> Finite a (n GHC.TypeLits.* m)
multiply :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, Limited a (n * m)) =>
Finite a n -> Finite a m -> Finite a (n * m)
multiply (Finite a
x) (Finite a
y) = a -> Finite a (n * m)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (n * m)) -> a -> Finite a (n * m)
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
y
{-# INLINABLE multiply #-}

-- | 'Left'-biased (left values come first) disjoint union of finite sets.
combineSum
    :: forall n m a. (SaneIntegral a, KnownIntegral a n, Limited a (n + m))
    => Either (Finite a n) (Finite a m) -> Finite a (n + m)
combineSum :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n, Limited a (n + m)) =>
Either (Finite a n) (Finite a m) -> Finite a (n + m)
combineSum (Left (Finite a
x)) = a -> Finite a (n + m)
forall a (n :: Nat). a -> Finite a n
Finite a
x
combineSum (Right (Finite a
x)) = a -> Finite a (n + m)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (n + m)) -> a -> Finite a (n + m)
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
n
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE combineSum #-}

-- | Witness that 'combineSum' preserves units: @0@ is the unit of
-- 'GHC.TypeLits.+', and 'Void' is the unit of 'Either'.
combineZero :: forall a. Void -> Finite a 0
combineZero :: forall a. Void -> Finite a 0
combineZero = Void -> Finite a 0
forall a. Void -> a
absurd
{-# INLINABLE combineZero #-}

-- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of
-- finite sets.
combineProduct
    :: forall n m a.
        (SaneIntegral a, KnownIntegral a n, Limited a (n GHC.TypeLits.* m))
    => (Finite a n, Finite a m) -> Finite a (n GHC.TypeLits.* m)
combineProduct :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n, Limited a (n * m)) =>
(Finite a n, Finite a m) -> Finite a (n * m)
combineProduct (Finite a
x, Finite a
y) = a -> Finite a (n * m)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (n * m)) -> a -> Finite a (n * m)
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
y a -> a -> a
forall a. Num a => a -> a -> a
* a
n
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE combineProduct #-}

-- | Witness that 'combineProduct' preserves units: @1@ is the unit of
-- 'GHC.TypeLits.*', and '()' is the unit of '(,)'.
combineOne :: forall a. (SaneIntegral a, Limited a 1) => () -> Finite a 1
combineOne :: forall a. (SaneIntegral a, Limited a 1) => () -> Finite a 1
combineOne ()
_ = a -> Finite a 1
forall a (n :: Nat). a -> Finite a n
Finite a
0
{-# INLINABLE combineOne #-}

-- | Product of @n@ copies of a finite set of size @m@, biased towards the lower
-- values of the argument (colex order).
combineExponential
    :: forall n m a.
        (SaneIntegral a, KnownIntegral a m, KnownIntegral a n, Limited a (m ^ n))
    => (Finite a n -> Finite a m) -> Finite a (m ^ n)
combineExponential :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a m, KnownIntegral a n,
 Limited a (m ^ n)) =>
(Finite a n -> Finite a m) -> Finite a (m ^ n)
combineExponential Finite a n -> Finite a m
f
    = a -> Finite a (m ^ n)
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a (m ^ n)) -> a -> Finite a (m ^ n)
forall a b. (a -> b) -> a -> b
$ (a, a) -> a
forall a b. (a, b) -> a
fst ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
$ ((a, a) -> Finite a n -> (a, a))
-> (a, a) -> [Finite a n] -> (a, a)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (a, a) -> Finite a n -> (a, a)
next (a
0, a
1) ([Finite a n]
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
[Finite a n]
finites :: [Finite a n])
    where
        next :: (a, a) -> Finite a n -> (a, a)
next (a
acc, a
power) Finite a n
x = a
acc' a -> (a, a) -> (a, a)
forall a b. a -> b -> b
`seq` (a
acc', a
m a -> a -> a
forall a. Num a => a -> a -> a
* a
power)
            where acc' :: a
acc' = a
acc a -> a -> a
forall a. Num a => a -> a -> a
+ Finite a m -> a
forall (n :: Nat) a. Finite a n -> a
getFinite (Finite a n -> Finite a m
f Finite a n
x) a -> a -> a
forall a. Num a => a -> a -> a
* a
power
        m :: a
m = Proxy m -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
{-# INLINABLE combineExponential #-}

-- | Take a 'Left'-biased disjoint union apart.
separateSum
    :: forall n m a. (SaneIntegral a, KnownIntegral a n)
    => Finite a (n + m) -> Either (Finite a n) (Finite a m)
separateSum :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
Finite a (n + m) -> Either (Finite a n) (Finite a m)
separateSum (Finite a
x)
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
n = Finite a m -> Either (Finite a n) (Finite a m)
forall a b. b -> Either a b
Right (Finite a m -> Either (Finite a n) (Finite a m))
-> Finite a m -> Either (Finite a n) (Finite a m)
forall a b. (a -> b) -> a -> b
$ a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
n
    | Bool
otherwise = Finite a n -> Either (Finite a n) (Finite a m)
forall a b. a -> Either a b
Left (Finite a n -> Either (Finite a n) (Finite a m))
-> Finite a n -> Either (Finite a n) (Finite a m)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite a
x
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE separateSum #-}

-- | Witness that 'separateSum' preserves units: @0@ is the unit of
-- 'GHC.TypeLits.+', and 'Void' is the unit of 'Either'.
--
-- Also witness that a @'Finite' a 0@ is uninhabited.
separateZero :: forall a. SaneIntegral a => Finite a 0 -> Void
separateZero :: forall a. SaneIntegral a => Finite a 0 -> Void
separateZero (Finite a
n) = a
n a -> Void -> Void
forall a b. a -> b -> b
`seq` [Char] -> Void
forall a. HasCallStack => [Char] -> a
error
    ([Char]
"separateZero: got Finite " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n))
{-# INLINABLE separateZero #-}

-- | Take a 'fst'-biased product apart.
separateProduct
    :: forall n m a. (SaneIntegral a, KnownIntegral a n)
    => Finite a (n GHC.TypeLits.* m) -> (Finite a n, Finite a m)
separateProduct :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
Finite a (n * m) -> (Finite a n, Finite a m)
separateProduct (Finite a
x) = case a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
x a
n of
    (a
d, a
m) -> (a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite a
m, a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite a
d)
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE separateProduct #-}

separateOne :: forall a. Finite a 1 -> ()
separateOne :: forall a. Finite a 1 -> ()
separateOne Finite a 1
_ = ()
{-# INLINABLE separateOne #-}

-- | Take a product of @n@ copies of a finite set of size @m@ apart, biased
-- towards the lower values of the argument (colex order).
separateExponential
    :: forall n m a. (SaneIntegral a, KnownIntegral a m)
    => Finite a (m ^ n) -> Finite a n -> Finite a m
separateExponential :: forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a m) =>
Finite a (m ^ n) -> Finite a n -> Finite a m
separateExponential = Finite a (m ^ n) -> Finite a n -> Finite a m
go
    where
        go :: Finite a (m ^ n) -> Finite a n -> Finite a m
go (Finite a
n) (Finite a
0) = a -> Finite a m
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a m) -> a -> Finite a m
forall a b. (a -> b) -> a -> b
$ a
n a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
m
        go (Finite a
n) (Finite a
x) = a
n' a -> Finite a m -> Finite a m
forall a b. a -> b -> b
`seq` Finite a (m ^ n) -> Finite a n -> Finite a m
go (a -> Finite a (m ^ n)
forall a (n :: Nat). a -> Finite a n
Finite a
n') (a -> Finite a n
forall a (n :: Nat). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
1)
            where n' :: a
n' = a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
m
        m :: a
m = Proxy m -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)
{-# INLINABLE separateExponential #-}

-- | Verifies that a given 'Finite' is valid. Should always return 'True' unless
-- you bring the @Data.Finite.Internal.Finite@ constructor into the scope, or
-- use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks.
isValidFinite
    :: forall n a. (Ord a, Num a, KnownIntegral a n)
    => Finite a n -> Bool
isValidFinite :: forall (n :: Nat) a.
(Ord a, Num a, KnownIntegral a n) =>
Finite a n -> Bool
isValidFinite (Finite a
x) = a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0
    where n :: a
n = Proxy n -> a
forall (n :: Nat) a (proxy :: Nat -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE isValidFinite #-}