--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Finite
-- Copyright   :  (C) 2015-2022 mniip
-- License     :  BSD3
-- Maintainer  :  mniip <mniip@mniip.com>
-- Stability   :  experimental
-- Portability :  portable
--------------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# 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, combineProduct,
        separateSum, separateProduct,
        isValidFinite
    )
    where

import Data.Maybe
import GHC.TypeLits

import Data.Finite.Internal

-- | Convert an 'Integer' into a 'Finite', returning 'Nothing' if the input is
-- out of bounds.
packFinite :: KnownNat n => Integer -> Maybe (Finite n)
packFinite :: Integer -> Maybe (Finite n)
packFinite Integer
x = Maybe (Finite n)
result
    where
        result :: Maybe (Finite n)
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Maybe (Finite n) -> Finite n
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Finite n)
result) Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
            then Finite n -> Maybe (Finite n)
forall a. a -> Maybe a
Just (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
            else Maybe (Finite n)
forall a. Maybe a
Nothing

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

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

-- | Generate a list of length @n@ of all elements of @'Finite' n@.
finites :: KnownNat n => [Finite n]
finites :: [Finite n]
finites = [Finite n]
results
  where
    results :: [Finite n]
results = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> [Integer] -> [Finite n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` [Integer
0 .. (Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal ([Finite n] -> Finite n
forall a. [a] -> a
head [Finite n]
results) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)]

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

-- | Produce the 'Finite' that is congruent to the given integer modulo @n@.
modulo :: KnownNat n => Integer -> Finite n
modulo :: Integer -> Finite n
modulo Integer
x = Finite n
result
    where
        result :: Finite n
result = if Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
            then [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error [Char]
"modulo: division by zero"
            else Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result)

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

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

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

-- | Convert a type-level literal into a 'Finite'.
natToFinite :: (KnownNat n, KnownNat m, n + 1 <= m) => proxy n -> Finite m
natToFinite :: proxy n -> Finite m
natToFinite proxy n
p = Integer -> Finite m
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite m) -> Integer -> Finite m
forall a b. (a -> b) -> a -> b
$ proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
p

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

-- | Remove one inhabitant from the end. Returns 'Nothing' if the input was the
-- removed inhabitant.
strengthen :: KnownNat n => Finite (n + 1) -> Maybe (Finite n)
strengthen :: Finite (n + 1) -> Maybe (Finite n)
strengthen (Finite Integer
x) = Maybe (Finite n)
result
    where
        result :: Maybe (Finite n)
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Maybe (Finite n) -> Finite n
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Finite n)
result)
            then Finite n -> Maybe (Finite n)
forall a. a -> Maybe a
Just (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
            else Maybe (Finite n)
forall a. Maybe a
Nothing

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

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

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

-- | Remove multiple inhabitants from the end. Returns 'Nothing' if the input
-- was one of the removed inhabitants.
strengthenN :: KnownNat n => Finite m -> Maybe (Finite n)
strengthenN :: Finite m -> Maybe (Finite n)
strengthenN (Finite Integer
x) = Maybe (Finite n)
result
    where
        result :: Maybe (Finite n)
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Maybe (Finite n) -> Finite n
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Finite n)
result)
            then Finite n -> Maybe (Finite n)
forall a. a -> Maybe a
Just (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
            else Maybe (Finite n)
forall a. Maybe a
Nothing

-- | Add multiple inhabitants in the beginning, shifting everything up by the
-- amount of inhabitants added.
shiftN :: (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m
shiftN :: Finite n -> Finite m
shiftN fx :: Finite n
fx@(Finite Integer
x) = Finite m
result
    where
        result :: Finite m
result = Integer -> Finite m
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite m) -> Integer -> Finite m
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Finite m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite m
result Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx

-- | 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 :: (KnownNat n, KnownNat m) => Finite m -> Maybe (Finite n)
unshiftN :: Finite m -> Maybe (Finite n)
unshiftN fx :: Finite m
fx@(Finite Integer
x) = Maybe (Finite n)
result
    where
        result :: Maybe (Finite n)
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite m
fx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Maybe (Finite n) -> Finite n
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Finite n)
result)
            then Maybe (Finite n)
forall a. Maybe a
Nothing
            else Finite n -> Maybe (Finite n)
forall a. a -> Maybe a
Just (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Finite m -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite m
fx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Maybe (Finite n) -> Finite n
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Finite n)
result)

weakenProxy :: proxy k -> Finite n -> Finite (n + k)
weakenProxy :: proxy k -> Finite n -> Finite (n + k)
weakenProxy proxy k
_ (Finite Integer
x) = Integer -> Finite (n + k)
forall (n :: Nat). Integer -> Finite n
Finite Integer
x

strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)
strengthenProxy :: proxy k -> Finite (n + k) -> Maybe (Finite n)
strengthenProxy proxy k
_ (Finite Integer
x) = Maybe (Finite n)
result
    where
        result :: Maybe (Finite n)
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Maybe (Finite n) -> Finite n
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Finite n)
result)
            then Finite n -> Maybe (Finite n)
forall a. a -> Maybe a
Just (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
            else Maybe (Finite n)
forall a. Maybe a
Nothing

shiftProxy :: KnownNat k => proxy k -> Finite n -> Finite (n + k)
shiftProxy :: proxy k -> Finite n -> Finite (n + k)
shiftProxy proxy k
p (Finite Integer
x) = Integer -> Finite (n + k)
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite (n + k)) -> Integer -> Finite (n + k)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy k
p

unshiftProxy :: KnownNat k => proxy k -> Finite (n + k) -> Maybe (Finite n)
unshiftProxy :: proxy k -> Finite (n + k) -> Maybe (Finite n)
unshiftProxy proxy k
p (Finite Integer
x) = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy k
p
    then Maybe (Finite n)
forall a. Maybe a
Nothing
    else Finite n -> Maybe (Finite n)
forall a. a -> Maybe a
Just (Finite n -> Maybe (Finite n)) -> Finite n -> Maybe (Finite n)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy k
p

-- | Add two 'Finite's.
add :: Finite n -> Finite m -> Finite (n + m)
add :: Finite n -> Finite m -> Finite (n + m)
add (Finite Integer
x) (Finite Integer
y) = Integer -> Finite (n + m)
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite (n + m)) -> Integer -> Finite (n + m)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y

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

-- | Multiply two 'Finite's.
multiply :: Finite n -> Finite m -> Finite (n GHC.TypeLits.* m)
multiply :: Finite n -> Finite m -> Finite (n * m)
multiply (Finite Integer
x) (Finite Integer
y) = Integer -> Finite (n * m)
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite (n * m)) -> Integer -> Finite (n * m)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y

getLeftType :: Either a b -> a
getLeftType :: Either a b -> a
getLeftType = [Char] -> Either a b -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"getLeftType"

-- | 'Left'-biased (left values come first) disjoint union of finite sets.
combineSum :: KnownNat n => Either (Finite n) (Finite m) -> Finite (n + m)
combineSum :: Either (Finite n) (Finite m) -> Finite (n + m)
combineSum (Left (Finite Integer
x)) = Integer -> Finite (n + m)
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
combineSum efx :: Either (Finite n) (Finite m)
efx@(Right (Finite Integer
x)) = Integer -> Finite (n + m)
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite (n + m)) -> Integer -> Finite (n + m)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Either (Finite n) (Finite m) -> Finite n
forall a b. Either a b -> a
getLeftType Either (Finite n) (Finite m)
efx)

-- | 'fst'-biased (fst is the inner, and snd is the outer iteratee) product of
-- finite sets.
combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n GHC.TypeLits.* m)
combineProduct :: (Finite n, Finite m) -> Finite (n * m)
combineProduct (fx :: Finite n
fx@(Finite Integer
x), Finite Integer
y) = Integer -> Finite (n * m)
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite (n * m)) -> Integer -> Finite (n * m)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx

-- | Take a 'Left'-biased disjoint union apart.
separateSum :: KnownNat n => Finite (n + m) -> Either (Finite n) (Finite m)
separateSum :: Finite (n + m) -> Either (Finite n) (Finite m)
separateSum (Finite Integer
x) = Either (Finite n) (Finite m)
result
    where
        result :: Either (Finite n) (Finite m)
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Either (Finite n) (Finite m) -> Finite n
forall a b. Either a b -> a
getLeftType Either (Finite n) (Finite m)
result)
            then Finite m -> Either (Finite n) (Finite m)
forall a b. b -> Either a b
Right (Finite m -> Either (Finite n) (Finite m))
-> Finite m -> Either (Finite n) (Finite m)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite m
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite m) -> Integer -> Finite m
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (Either (Finite n) (Finite m) -> Finite n
forall a b. Either a b -> a
getLeftType Either (Finite n) (Finite m)
result)
            else Finite n -> Either (Finite n) (Finite m)
forall a b. a -> Either a b
Left (Finite n -> Either (Finite n) (Finite m))
-> Finite n -> Either (Finite n) (Finite m)
forall a b. (a -> b) -> a -> b
$ Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x

-- | Take a 'fst'-biased product apart.
separateProduct :: KnownNat n => Finite (n GHC.TypeLits.* m) -> (Finite n, Finite m)
separateProduct :: Finite (n * m) -> (Finite n, Finite m)
separateProduct (Finite Integer
x) = (Finite n, Finite m)
result
    where
        result :: (Finite n, Finite m)
result = (Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal ((Finite n, Finite m) -> Finite n
forall a b. (a, b) -> a
fst (Finite n, Finite m)
result), Integer -> Finite m
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite m) -> Integer -> Finite m
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal ((Finite n, Finite m) -> Finite n
forall a b. (a, b) -> a
fst (Finite n, Finite m)
result))

-- | 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 :: KnownNat n => Finite n -> Bool
isValidFinite :: Finite n -> Bool
isValidFinite fx :: Finite n
fx@(Finite Integer
x) = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0