--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Finite
-- Copyright   :  (C) 2015-2022 mniip
-- License     :  BSD3
-- Maintainer  :  mniip <mniip@mniip.com>
-- Stability   :  experimental
-- Portability :  portable
--------------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Finite
    (
        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 GHC.TypeLits
import Data.Void

import qualified Data.Finite.Integral as I
import Data.Finite.Internal

-- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is
-- out of bounds.
packFinite :: forall n. KnownNat n => Integer -> Maybe (Finite n)
packFinite :: forall (n :: Nat). KnownNat n => Integer -> Maybe (Finite n)
packFinite = Integer -> Maybe (Finite Integer n)
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Maybe (Finite a n)
I.packFinite

-- | Same as 'packFinite' but with a proxy argument to avoid type signatures.
packFiniteProxy
    :: forall n proxy. KnownNat n
    => proxy n -> Integer -> Maybe (Finite n)
packFiniteProxy :: forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer -> Maybe (Finite n)
packFiniteProxy = proxy n -> Integer -> Maybe (Finite Integer n)
forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> a -> Maybe (Finite a n)
I.packFiniteProxy

-- | Same as 'finite' but with a proxy argument to avoid type signatures.
finiteProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n
finiteProxy :: forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer -> Finite n
finiteProxy = proxy n -> Integer -> Finite Integer n
forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> a -> Finite a n
I.finiteProxy

-- | Generate a list of length @n@ of all elements of @'Finite' n@.
finites :: forall n. KnownNat n => [Finite n]
finites :: forall (n :: Nat). KnownNat n => [Finite n]
finites = [Finite Integer n]
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
[Finite a n]
I.finites

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

-- | Produce the 'Finite' that is congruent to the given integer modulo @n@.
modulo :: forall n. KnownNat n => Integer -> Finite n
modulo :: forall (n :: Nat). KnownNat n => Integer -> Finite n
modulo = Integer -> Finite Integer n
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Finite a n
I.modulo

-- | Same as 'modulo' but with a proxy argument to avoid type signatures.
moduloProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n
moduloProxy :: forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer -> Finite n
moduloProxy = proxy n -> Integer -> Finite Integer n
forall (n :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy n -> a -> Finite a n
I.moduloProxy

-- | Test two different types of finite numbers for equality.
equals :: forall n m. Finite n -> Finite m -> Bool
equals :: forall (n :: Nat) (m :: Nat). Finite n -> Finite m -> Bool
equals = Finite Integer n -> Finite Integer m -> Bool
forall (n :: Nat) (m :: Nat) a.
Eq a =>
Finite a n -> Finite a m -> Bool
I.equals
infix 4 `equals`

-- | Compare two different types of finite numbers.
cmp :: forall n m. Finite n -> Finite m -> Ordering
cmp :: forall (n :: Nat) (m :: Nat). Finite n -> Finite m -> Ordering
cmp = Finite Integer n -> Finite Integer m -> Ordering
forall (n :: Nat) (m :: Nat) a.
Ord a =>
Finite a n -> Finite a m -> Ordering
I.cmp

-- | Convert a type-level literal into a 'Finite'.
natToFinite
    :: forall n m proxy. (KnownNat n, KnownNat m, n + 1 <= m)
    => proxy n -> Finite m
natToFinite :: forall (n :: Nat) (m :: Nat) (proxy :: Nat -> *).
(KnownNat n, KnownNat m, (n + 1) <= m) =>
proxy n -> Finite m
natToFinite = proxy n -> Finite Integer m
forall (n :: Nat) (m :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n, Limited a m, (n + 1) <= m) =>
proxy n -> Finite a m
I.natToFinite

-- | Add one inhabitant in the end.
weaken :: forall n. Finite n -> Finite (n + 1)
weaken :: forall (n :: Nat). Finite n -> Finite (n + 1)
weaken = Finite Integer n -> Finite Integer (n + 1)
forall (n :: Nat) a.
Limited a (n + 1) =>
Finite a n -> Finite a (n + 1)
I.weaken

-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the
-- removed inhabitant.
strengthen :: forall n. KnownNat n => Finite (n + 1) -> Maybe (Finite n)
strengthen :: forall (n :: Nat). KnownNat n => Finite (n + 1) -> Maybe (Finite n)
strengthen = Finite Integer (n + 1) -> Maybe (Finite Integer n)
forall (n :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
Finite a (n + 1) -> Maybe (Finite a n)
I.strengthen

-- | Add one inhabitant in the beginning, shifting everything up by one.
shift :: forall n. Finite n -> Finite (n + 1)
shift :: forall (n :: Nat). Finite n -> Finite (n + 1)
shift = Finite Integer n -> Finite Integer (n + 1)
forall (n :: Nat) a.
(SaneIntegral a, Limited a (n + 1)) =>
Finite a n -> Finite a (n + 1)
I.shift

-- | Remove one inhabitant from the beginning, shifting everything down by one.
-- Returns 'Nothing' if the input was the removed inhabitant.
unshift :: forall n. Finite (n + 1) -> Maybe (Finite n)
unshift :: forall (n :: Nat). Finite (n + 1) -> Maybe (Finite n)
unshift = Finite Integer (n + 1) -> Maybe (Finite Integer n)
forall (n :: Nat) a.
SaneIntegral a =>
Finite a (n + 1) -> Maybe (Finite a n)
I.unshift

-- | Add multiple inhabitants in the end.
weakenN :: forall n m. (n <= m) => Finite n -> Finite m
weakenN :: forall (n :: Nat) (m :: Nat). (n <= m) => Finite n -> Finite m
weakenN = Finite Integer n -> Finite Integer m
forall (n :: Nat) (m :: Nat) a.
(n <= m, Limited a m) =>
Finite a n -> Finite a m
I.weakenN

-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input
-- was one of the removed inhabitants.
strengthenN :: forall n m. KnownNat m => Finite n -> Maybe (Finite m)
strengthenN :: forall (n :: Nat) (m :: Nat).
KnownNat m =>
Finite n -> Maybe (Finite m)
strengthenN = Finite Integer n -> Maybe (Finite Integer m)
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a m, Limited a m) =>
Finite a n -> Maybe (Finite a m)
I.strengthenN

-- | Add multiple inhabitants in the beginning, shifting everything up by the
-- amount of inhabitants added.
shiftN :: forall n m. (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m
shiftN :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m, n <= m) =>
Finite n -> Finite m
shiftN = Finite Integer n -> Finite Integer m
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n, KnownIntegral a m, n <= m) =>
Finite a n -> Finite a m
I.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. (KnownNat n, KnownNat m) => Finite n -> Maybe (Finite m)
unshiftN :: forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Finite n -> Maybe (Finite m)
unshiftN = Finite Integer n -> Maybe (Finite Integer m)
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n, KnownIntegral a m,
 Limited a m) =>
Finite a n -> Maybe (Finite a m)
I.unshiftN

weakenProxy :: forall n k proxy. proxy k -> Finite n -> Finite (n + k)
weakenProxy :: forall (n :: Nat) (k :: Nat) (proxy :: Nat -> *).
proxy k -> Finite n -> Finite (n + k)
weakenProxy = proxy k -> Finite Integer n -> Finite Integer (n + k)
forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
Limited a (n + k) =>
proxy k -> Finite a n -> Finite a (n + k)
I.weakenProxy

strengthenProxy
    :: forall n k proxy. KnownNat n
    => proxy k -> Finite (n + k) -> Maybe (Finite n)
strengthenProxy :: forall (n :: Nat) (k :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy k -> Finite (n + k) -> Maybe (Finite n)
strengthenProxy = proxy k -> Finite Integer (n + k) -> Maybe (Finite Integer n)
forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy k -> Finite a (n + k) -> Maybe (Finite a n)
I.strengthenProxy

shiftProxy
    :: forall n k proxy. KnownNat k
    => proxy k -> Finite n -> Finite (n + k)
shiftProxy :: forall (n :: Nat) (k :: Nat) (proxy :: Nat -> *).
KnownNat k =>
proxy k -> Finite n -> Finite (n + k)
shiftProxy = proxy k -> Finite Integer n -> Finite Integer (n + k)
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)
I.shiftProxy

unshiftProxy
    :: forall n k proxy. KnownNat k
    => proxy k -> Finite (n + k) -> Maybe (Finite n)
unshiftProxy :: forall (n :: Nat) (k :: Nat) (proxy :: Nat -> *).
KnownNat k =>
proxy k -> Finite (n + k) -> Maybe (Finite n)
unshiftProxy = proxy k -> Finite Integer (n + k) -> Maybe (Finite Integer n)
forall (n :: Nat) (k :: Nat) a (proxy :: Nat -> *).
(SaneIntegral a, KnownIntegral a k) =>
proxy k -> Finite a (n + k) -> Maybe (Finite a n)
I.unshiftProxy

-- | Add two 'Finite's.
add :: forall n m. Finite n -> Finite m -> Finite (n + m)
add :: forall (n :: Nat) (m :: Nat).
Finite n -> Finite m -> Finite (n + m)
add = Finite Integer n -> Finite Integer m -> Finite Integer (n + m)
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, Limited a (n + m)) =>
Finite a n -> Finite a m -> Finite a (n + m)
I.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. Finite n -> Finite m -> Either (Finite m) (Finite n)
sub :: forall (n :: Nat) (m :: Nat).
Finite n -> Finite m -> Either (Finite m) (Finite n)
sub = Finite Integer n
-> Finite Integer m -> Either (Finite Integer m) (Finite Integer n)
forall (n :: Nat) (m :: Nat) a.
SaneIntegral a =>
Finite a n -> Finite a m -> Either (Finite a m) (Finite a n)
I.sub

-- | Multiply two 'Finite's.
multiply :: forall n m. Finite n -> Finite m -> Finite (n GHC.TypeLits.* m)
multiply :: forall (n :: Nat) (m :: Nat).
Finite n -> Finite m -> Finite (n * m)
multiply = Finite Integer n -> Finite Integer m -> Finite Integer (n * m)
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, Limited a (n * m)) =>
Finite a n -> Finite a m -> Finite a (n * m)
I.multiply

-- | 'Left'-biased (left values come first) disjoint union of finite sets.
combineSum
    :: forall n m. KnownNat n
    => Either (Finite n) (Finite m) -> Finite (n + m)
combineSum :: forall (n :: Nat) (m :: Nat).
KnownNat n =>
Either (Finite n) (Finite m) -> Finite (n + m)
combineSum = Either (Finite Integer n) (Finite Integer m)
-> Finite Integer (n + m)
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)
I.combineSum

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

-- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of
-- finite sets.
combineProduct
    :: forall n m. KnownNat n
    => (Finite n, Finite m) -> Finite (n GHC.TypeLits.* m)
combineProduct :: forall (n :: Nat) (m :: Nat).
KnownNat n =>
(Finite n, Finite m) -> Finite (n * m)
combineProduct = (Finite Integer n, Finite Integer m) -> Finite Integer (n * m)
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)
I.combineProduct

-- | Witness that 'combineProduct' preserves units: @1@ is the unit of
-- 'GHC.TypeLits.*', and '()' is the unit of '(,)'.
combineOne :: () -> Finite 1
combineOne :: () -> Finite 1
combineOne = () -> Finite 1
forall a. (SaneIntegral a, Limited a 1) => () -> Finite a 1
I.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. (KnownNat m, KnownNat n)
    => (Finite n -> Finite m) -> Finite (m ^ n)
combineExponential :: forall (n :: Nat) (m :: Nat).
(KnownNat m, KnownNat n) =>
(Finite n -> Finite m) -> Finite (m ^ n)
combineExponential = (Finite Integer n -> Finite Integer m) -> Finite Integer (m ^ n)
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)
I.combineExponential

-- | Take a 'Left'-biased disjoint union apart.
separateSum
    :: forall n m. KnownNat n
    => Finite (n + m) -> Either (Finite n) (Finite m)
separateSum :: forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n + m) -> Either (Finite n) (Finite m)
separateSum = Finite Integer (n + m)
-> Either (Finite Integer n) (Finite Integer m)
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
Finite a (n + m) -> Either (Finite a n) (Finite a m)
I.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' 0@ is uninhabited.
separateZero :: Finite 0 -> Void
separateZero :: Finite 0 -> Void
separateZero = Finite 0 -> Void
forall a. SaneIntegral a => Finite a 0 -> Void
I.separateZero

-- | Take a 'fst'-biased product apart.
separateProduct
    :: forall n m. KnownNat n
    => Finite (n GHC.TypeLits.* m) -> (Finite n, Finite m)
separateProduct :: forall (n :: Nat) (m :: Nat).
KnownNat n =>
Finite (n * m) -> (Finite n, Finite m)
separateProduct = Finite Integer (n * m) -> (Finite Integer n, Finite Integer m)
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a n) =>
Finite a (n * m) -> (Finite a n, Finite a m)
I.separateProduct

separateOne :: Finite 1 -> ()
separateOne :: Finite 1 -> ()
separateOne = Finite 1 -> ()
forall a. Finite a 1 -> ()
I.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. KnownNat m
    => Finite (m ^ n) -> Finite n -> Finite m
separateExponential :: forall (n :: Nat) (m :: Nat).
KnownNat m =>
Finite (m ^ n) -> Finite n -> Finite m
separateExponential = Finite Integer (m ^ n) -> Finite Integer n -> Finite Integer m
forall (n :: Nat) (m :: Nat) a.
(SaneIntegral a, KnownIntegral a m) =>
Finite a (m ^ n) -> Finite a n -> Finite a m
I.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. KnownNat n => Finite n -> Bool
isValidFinite :: forall (n :: Nat). KnownNat n => Finite n -> Bool
isValidFinite = Finite Integer n -> Bool
forall (n :: Nat) a.
(Ord a, Num a, KnownIntegral a n) =>
Finite a n -> Bool
I.isValidFinite