{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# 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,
castFinite,
isValidFinite
)
where
import Data.Coerce
#if __GLASGOW_HASKELL__ < 910
import Data.List (foldl')
#endif
import Data.Proxy
import Data.Void
import GHC.TypeLits
import Data.Finite.Internal.Integral
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 #-}
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 #-}
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 #-}
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..]
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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
:: 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 #-}
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
:: 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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
castFinite
:: forall b a n. (SaneIntegral a, SaneIntegral b, Limited b n)
=> Finite a n -> Finite b n
castFinite :: forall b a (n :: Nat).
(SaneIntegral a, SaneIntegral b, Limited b n) =>
Finite a n -> Finite b n
castFinite (Finite a
x) = b -> Finite b n
forall a (n :: Nat). a -> Finite a n
Finite (b -> Finite b n) -> b -> Finite b n
forall a b. (a -> b) -> a -> b
$ a -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x
{-# INLINABLE castFinite #-}
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 #-}