{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
module Numeric.Peano where
import Data.List (unfoldr)
import Control.DeepSeq (NFData (rnf))
import Data.Data (Data, Typeable)
import GHC.Generics (Generic)
import Numeric.Natural
import Data.Ix
import Data.Function
import Text.Read
data Nat
= Z
| S Nat
deriving (Nat -> Nat -> Bool
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c== :: Nat -> Nat -> Bool
Eq,(forall x. Nat -> Rep Nat x)
-> (forall x. Rep Nat x -> Nat) -> Generic Nat
forall x. Rep Nat x -> Nat
forall x. Nat -> Rep Nat x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Nat x -> Nat
$cfrom :: forall x. Nat -> Rep Nat x
Generic,Typeable Nat
DataType
Constr
Typeable Nat =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat)
-> (Nat -> Constr)
-> (Nat -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat))
-> ((forall b. Data b => b -> b) -> Nat -> Nat)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r)
-> (forall u. (forall d. Data d => d -> u) -> Nat -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat)
-> Data Nat
Nat -> DataType
Nat -> Constr
(forall b. Data b => b -> b) -> Nat -> Nat
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
forall u. (forall d. Data d => d -> u) -> Nat -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cS :: Constr
$cZ :: Constr
$tNat :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapMp :: (forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapM :: (forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
$cgmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Nat)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
dataTypeOf :: Nat -> DataType
$cdataTypeOf :: Nat -> DataType
toConstr :: Nat -> Constr
$ctoConstr :: Nat -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
$cp1Data :: Typeable Nat
Data,Typeable)
foldrNat :: (a -> a) -> a -> Nat -> a
foldrNat :: (a -> a) -> a -> Nat -> a
foldrNat f :: a -> a
f k :: a
k = Nat -> a
go
where
go :: Nat -> a
go Z = a
k
go (S n :: Nat
n) = a -> a
f (Nat -> a
go Nat
n)
{-# INLINE foldrNat #-}
foldlNat' :: (a -> a) -> a -> Nat -> a
foldlNat' :: (a -> a) -> a -> Nat -> a
foldlNat' f :: a -> a
f = a -> Nat -> a
go
where
go :: a -> Nat -> a
go !a
b Z = a
b
go !a
b (S n :: Nat
n) = a -> Nat -> a
go (a -> a
f a
b) Nat
n
{-# INLINE foldlNat' #-}
instance Ord Nat where
compare :: Nat -> Nat -> Ordering
compare Z Z = Ordering
EQ
compare (S n :: Nat
n) (S m :: Nat
m) = Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Nat
n Nat
m
compare Z (S _) = Ordering
LT
compare (S _) Z = Ordering
GT
Z <= :: Nat -> Nat -> Bool
<= _ = Bool
True
S _ <= Z = Bool
False
S n :: Nat
n <= S m :: Nat
m = Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
m
_ < :: Nat -> Nat -> Bool
< Z = Bool
False
n :: Nat
n < S m :: Nat
m = Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
m
>= :: Nat -> Nat -> Bool
(>=) = (Nat -> Nat -> Bool) -> Nat -> Nat -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
> :: Nat -> Nat -> Bool
(>) = (Nat -> Nat -> Bool) -> Nat -> Nat -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
(<)
min :: Nat -> Nat -> Nat
min Z _ = Nat
Z
min _ Z = Nat
Z
min (S n :: Nat
n) (S m :: Nat
m) = Nat -> Nat
S (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
min Nat
n Nat
m)
max :: Nat -> Nat -> Nat
max Z m :: Nat
m = Nat
m
max n :: Nat
n Z = Nat
n
max (S n :: Nat
n) (S m :: Nat
m) = Nat -> Nat
S (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
n Nat
m)
instance Num Nat where
n :: Nat
n + :: Nat -> Nat -> Nat
+ m :: Nat
m = (Nat -> Nat) -> Nat -> Nat -> Nat
forall a. (a -> a) -> a -> Nat -> a
foldrNat Nat -> Nat
S Nat
m Nat
n
n :: Nat
n * :: Nat -> Nat -> Nat
* m :: Nat
m = (Nat -> Nat) -> Nat -> Nat -> Nat
forall a. (a -> a) -> a -> Nat -> a
foldrNat (Nat
mNat -> Nat -> Nat
forall a. Num a => a -> a -> a
+) Nat
Z Nat
n
abs :: Nat -> Nat
abs = Nat -> Nat
forall a. a -> a
id
signum :: Nat -> Nat
signum Z = Nat
Z
signum (S _) = Nat -> Nat
S Nat
Z
fromInteger :: Integer -> Nat
fromInteger n :: Integer
n
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = [Char] -> Nat
forall a. HasCallStack => [Char] -> a
error "cannot convert negative integers to Peano numbers"
| Bool
otherwise = Integer -> Nat
forall t. (Eq t, Num t) => t -> Nat
go Integer
n where
go :: t -> Nat
go 0 = Nat
Z
go m :: t
m = Nat -> Nat
S (t -> Nat
go (t
mt -> t -> t
forall a. Num a => a -> a -> a
-1))
Z - :: Nat -> Nat -> Nat
- _ = Nat
Z
n :: Nat
n - Z = Nat
n
S n :: Nat
n - S m :: Nat
m = Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
m
instance Bounded Nat where
minBound :: Nat
minBound = Nat
Z
maxBound :: Nat
maxBound = (Nat -> Nat) -> Nat
forall a. (a -> a) -> a
fix Nat -> Nat
S
instance Show Nat where
showsPrec :: Int -> Nat -> ShowS
showsPrec n :: Int
n = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
n (Integer -> ShowS) -> (Nat -> Integer) -> Nat -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger
instance Read Nat where
readPrec :: ReadPrec Nat
readPrec = (Natural -> Nat) -> ReadPrec Natural -> ReadPrec Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Natural -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Natural -> Nat) ReadPrec Natural
forall a. Read a => ReadPrec a
readPrec
instance NFData Nat where
rnf :: Nat -> ()
rnf Z = ()
rnf (S n :: Nat
n) = Nat -> ()
forall a. NFData a => a -> ()
rnf Nat
n
instance Real Nat where
toRational :: Nat -> Rational
toRational = Integer -> Rational
forall a. Real a => a -> Rational
toRational (Integer -> Rational) -> (Nat -> Integer) -> Nat -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger
instance Enum Nat where
succ :: Nat -> Nat
succ = Nat -> Nat
S
pred :: Nat -> Nat
pred (S n :: Nat
n) = Nat
n
pred Z = [Char] -> Nat
forall a. HasCallStack => [Char] -> a
error "pred called on zero nat"
fromEnum :: Nat -> Int
fromEnum = (Int -> Int) -> Int -> Nat -> Int
forall a. (a -> a) -> a -> Nat -> a
foldlNat' Int -> Int
forall a. Enum a => a -> a
succ 0
toEnum :: Int -> Nat
toEnum m :: Int
m
| Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = [Char] -> Nat
forall a. HasCallStack => [Char] -> a
error "cannot convert negative number to Peano"
| Bool
otherwise = Int -> Nat
forall t. (Eq t, Num t) => t -> Nat
go Int
m
where
go :: t -> Nat
go 0 = Nat
Z
go n :: t
n = Nat -> Nat
S (t -> Nat
go (t
n t -> t -> t
forall a. Num a => a -> a -> a
- 1))
enumFrom :: Nat -> [Nat]
enumFrom = (Nat -> Nat) -> Nat -> [Nat]
forall a. (a -> a) -> a -> [a]
iterate Nat -> Nat
S
enumFromTo :: Nat -> Nat -> [Nat]
enumFromTo n :: Nat
n m :: Nat
m = ((Nat, Nat) -> Maybe (Nat, (Nat, Nat))) -> (Nat, Nat) -> [Nat]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (Nat, Nat) -> Maybe (Nat, (Nat, Nat))
f (Nat
n, Nat -> Nat
S Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n)
where
f :: (Nat, Nat) -> Maybe (Nat, (Nat, Nat))
f (_,Z) = Maybe (Nat, (Nat, Nat))
forall a. Maybe a
Nothing
f (e :: Nat
e,S l :: Nat
l) = (Nat, (Nat, Nat)) -> Maybe (Nat, (Nat, Nat))
forall a. a -> Maybe a
Just (Nat
e, (Nat -> Nat
S Nat
e, Nat
l))
enumFromThen :: Nat -> Nat -> [Nat]
enumFromThen n :: Nat
n m :: Nat
m = (Nat -> Nat) -> Nat -> [Nat]
forall a. (a -> a) -> a -> [a]
iterate Nat -> Nat
t Nat
n
where
ts :: Nat -> Nat -> Nat -> Nat
ts Z mm :: Nat
mm = Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
(+) Nat
mm
ts (S nn :: Nat
nn) (S mm :: Nat
mm) = Nat -> Nat -> Nat -> Nat
ts Nat
nn Nat
mm
ts nn :: Nat
nn Z = Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
subtract Nat
nn
t :: Nat -> Nat
t = Nat -> Nat -> Nat -> Nat
ts Nat
n Nat
m
enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
enumFromThenTo n :: Nat
n m :: Nat
m t :: Nat
t = ((Nat, Nat) -> Maybe (Nat, (Nat, Nat))) -> (Nat, Nat) -> [Nat]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (Nat, Nat) -> Maybe (Nat, (Nat, Nat))
f (Nat
n, Nat
jm)
where
ts :: Nat -> Nat -> (Nat, Nat -> Nat, Nat)
ts (S nn :: Nat
nn) (S mm :: Nat
mm) = Nat -> Nat -> (Nat, Nat -> Nat, Nat)
ts Nat
nn Nat
mm
ts Z mm :: Nat
mm = (Nat -> Nat
S Nat
t Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n, Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
(+) Nat
mm, Nat
mm)
ts nn :: Nat
nn Z = (Nat -> Nat
S Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
t, Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
subtract Nat
nn, Nat
nn)
(jm :: Nat
jm,tf :: Nat -> Nat
tf,tt :: Nat
tt) = Nat -> Nat -> (Nat, Nat -> Nat, Nat)
ts Nat
n Nat
m
td :: Nat -> Nat
td = Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
subtract Nat
tt
f :: (Nat, Nat) -> Maybe (Nat, (Nat, Nat))
f (_,Z) = Maybe (Nat, (Nat, Nat))
forall a. Maybe a
Nothing
f (e :: Nat
e,l :: Nat
l@(S _)) = (Nat, (Nat, Nat)) -> Maybe (Nat, (Nat, Nat))
forall a. a -> Maybe a
Just (Nat
e, (Nat -> Nat
tf Nat
e, Nat -> Nat
td Nat
l))
instance Integral Nat where
toInteger :: Nat -> Integer
toInteger = (Integer -> Integer) -> Integer -> Nat -> Integer
forall a. (a -> a) -> a -> Nat -> a
foldlNat' Integer -> Integer
forall a. Enum a => a -> a
succ 0
quotRem :: Nat -> Nat -> (Nat, Nat)
quotRem _ Z = (Nat
forall a. Bounded a => a
maxBound, [Char] -> Nat
forall a. HasCallStack => [Char] -> a
error "divide by zero")
quotRem x :: Nat
x y :: Nat
y = Nat -> Nat -> Nat -> (Nat, Nat)
qr Nat
Z Nat
x Nat
y
where
qr :: Nat -> Nat -> Nat -> (Nat, Nat)
qr q :: Nat
q n :: Nat
n m :: Nat
m = Nat -> Nat -> (Nat, Nat)
go Nat
n Nat
m
where
go :: Nat -> Nat -> (Nat, Nat)
go nn :: Nat
nn Z = Nat -> Nat -> Nat -> (Nat, Nat)
qr (Nat -> Nat
S Nat
q) Nat
nn Nat
m
go (S nn :: Nat
nn) (S mm :: Nat
mm) = Nat -> Nat -> (Nat, Nat)
go Nat
nn Nat
mm
go Z (S _) = (Nat
q, Nat
n)
quot :: Nat -> Nat -> Nat
quot n :: Nat
n m :: Nat
m = Nat -> Nat
go Nat
n where
go :: Nat -> Nat
go = Nat -> Nat -> Nat
subt Nat
m where
subt :: Nat -> Nat -> Nat
subt Z nn :: Nat
nn = Nat -> Nat
S (Nat -> Nat
go Nat
nn)
subt (S mm :: Nat
mm) (S nn :: Nat
nn) = Nat -> Nat -> Nat
subt Nat
mm Nat
nn
subt (S _) Z = Nat
Z
rem :: Nat -> Nat -> Nat
rem _ Z = [Char] -> Nat
forall a. HasCallStack => [Char] -> a
error "divide by zero"
rem nn :: Nat
nn mm :: Nat
mm = Nat -> Nat -> Nat
r Nat
nn Nat
mm where
r :: Nat -> Nat -> Nat
r n :: Nat
n m :: Nat
m = Nat -> Nat -> Nat
go Nat
n Nat
m where
go :: Nat -> Nat -> Nat
go nnn :: Nat
nnn Z = Nat -> Nat -> Nat
r Nat
nnn Nat
m
go (S nnn :: Nat
nnn) (S mmm :: Nat
mmm) = Nat -> Nat -> Nat
go Nat
nnn Nat
mmm
go Z (S _) = Nat
n
div :: Nat -> Nat -> Nat
div = Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
quot
mod :: Nat -> Nat -> Nat
mod = Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
rem
divMod :: Nat -> Nat -> (Nat, Nat)
divMod = Nat -> Nat -> (Nat, Nat)
forall a. Integral a => a -> a -> (a, a)
quotRem
instance Ix Nat where
range :: (Nat, Nat) -> [Nat]
range = (Nat -> Nat -> [Nat]) -> (Nat, Nat) -> [Nat]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Nat -> Nat -> [Nat]
forall a. Enum a => a -> a -> [a]
enumFromTo
inRange :: (Nat, Nat) -> Nat -> Bool
inRange = (Nat -> Nat -> Nat -> Bool) -> (Nat, Nat) -> Nat -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Nat -> Nat -> Nat -> Bool
go where
go :: Nat -> Nat -> Nat -> Bool
go (S _) _ Z = Bool
False
go Z y :: Nat
y x :: Nat
x = Nat
x Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
y
go (S x :: Nat
x) (S y :: Nat
y) (S z :: Nat
z) = Nat -> Nat -> Nat -> Bool
go Nat
x Nat
y Nat
z
go (S _) Z (S _) = Bool
False
index :: (Nat, Nat) -> Nat -> Int
index = (Nat -> Nat -> Nat -> Int) -> (Nat, Nat) -> Nat -> Int
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Nat -> Nat -> Nat -> Int
forall p. Num p => Nat -> Nat -> Nat -> p
go where
go :: Nat -> Nat -> Nat -> p
go Z h :: Nat
h i :: Nat
i = p -> Nat -> Nat -> p
forall p. Num p => p -> Nat -> Nat -> p
lim 0 Nat
h Nat
i
go (S _) _ Z = [Char] -> p
forall a. HasCallStack => [Char] -> a
error "out of range"
go (S l :: Nat
l) (S h :: Nat
h) (S i :: Nat
i) = Nat -> Nat -> Nat -> p
go Nat
l Nat
h Nat
i
go (S _) Z (S _) = [Char] -> p
forall a. HasCallStack => [Char] -> a
error "out of range"
lim :: p -> Nat -> Nat -> p
lim _ Z (S _) = [Char] -> p
forall a. HasCallStack => [Char] -> a
error "out of range"
lim !p
a (S n :: Nat
n) (S m :: Nat
m) = p -> Nat -> Nat -> p
lim (p
a p -> p -> p
forall a. Num a => a -> a -> a
+ 1) Nat
n Nat
m
lim !p
a _ Z = p
a