--------------------------------------------------------------------------------
-- |
-- 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 = 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 = 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 = I.finiteProxy

-- | Generate a list of length @n@ of all elements of @'Finite' n@.
finites :: forall n. KnownNat n => [Finite n]
finites = 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 = I.finitesProxy

-- | Produce the 'Finite' that is congruent to the given integer modulo @n@.
modulo :: forall n. KnownNat n => Integer -> Finite n
modulo = 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 = I.moduloProxy

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

-- | Compare two different types of finite numbers.
cmp :: forall n m. Finite n -> Finite m -> Ordering
cmp = 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 = I.natToFinite

-- | Add one inhabitant in the end.
weaken :: forall n. Finite n -> Finite (n + 1)
weaken = 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 = I.strengthen

-- | Add one inhabitant in the beginning, shifting everything up by one.
shift :: forall n. Finite n -> Finite (n + 1)
shift = 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 = I.unshift

-- | Add multiple inhabitants in the end.
weakenN :: forall n m. (n <= m) => Finite n -> Finite m
weakenN = 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 = 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 = 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 = I.unshiftN

weakenProxy :: forall n k proxy. proxy k -> Finite n -> Finite (n + k)
weakenProxy = I.weakenProxy

strengthenProxy
    :: forall n k proxy. KnownNat n
    => proxy k -> Finite (n + k) -> Maybe (Finite n)
strengthenProxy = I.strengthenProxy

shiftProxy
    :: forall n k proxy. KnownNat k
    => proxy k -> Finite n -> Finite (n + k)
shiftProxy = I.shiftProxy

unshiftProxy
    :: forall n k proxy. KnownNat k
    => proxy k -> Finite (n + k) -> Maybe (Finite n)
unshiftProxy = I.unshiftProxy

-- | Add two 'Finite's.
add :: forall n m. Finite n -> Finite m -> Finite (n + m)
add = 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 = I.sub

-- | Multiply two 'Finite's.
multiply :: forall n m. Finite n -> Finite m -> Finite (n GHC.TypeLits.* m)
multiply = 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 = 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 = 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 = I.combineProduct

-- | Witness that 'combineProduct' preserves units: @1@ is the unit of
-- 'GHC.TypeLits.*', and '()' is the unit of '(,)'.
combineOne :: () -> Finite 1
combineOne = 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 = I.combineExponential

-- | Take a 'Left'-biased disjoint union apart.
separateSum
    :: forall n m. KnownNat n
    => Finite (n + m) -> Either (Finite n) (Finite m)
separateSum = 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 = I.separateZero

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

separateOne :: Finite 1 -> ()
separateOne = 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 = 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 = I.isValidFinite