{-# LANGUAGE BangPatterns         #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE DeriveGeneric        #-}

-- | Peano numerals. Effort is made to make them as efficient as
-- possible, and as lazy as possible, but they are many orders of
-- magnitude less efficient than machine integers. They are primarily
-- used for type-level programming, and occasionally for calculations
-- which can be short-circuited.
--
-- For instance, to check if two lists are the same length, you could
-- write:
--
-- @
-- 'length' xs == 'length' ys
-- @
--
-- But this unnecessarily traverses both lists. The more efficient
-- version, on the other hand, is less clear:
--
-- @
-- sameLength [] [] = True
-- sameLength (_:xs) (_:ys) = sameLength xs ys
-- sameLength _ _ = False
-- @
--
-- Using @'Data.List.genericLength'@, on the other hand, the laziness of
-- @'Nat'@ will indeed short-circuit:
--
-- >>> genericLength [1,2,3] == genericLength [1..]
-- False
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

-- $setup
-- >>> import Test.QuickCheck
-- >>> import Data.List (genericLength)
-- >>> default (Nat)
-- >>> :{
-- instance Arbitrary Nat where
--     arbitrary = fmap (fromInteger . getNonNegative) arbitrary
-- :}

-- | Peano numbers. Care is taken to make operations as lazy as
-- possible:
--
-- >>> 1 > S (S undefined)
-- False
-- >>> Z > undefined
-- False
-- >>> 3 + undefined >= 3
-- True
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)

-- | A right fold over the naturals.
-- Alternatively, a function which converts a natural into
-- a Church natural.
--
-- prop> foldrNat S Z n === n
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 #-}

-- | A strict left fold over the naturals.
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' #-}

-- | As lazy as possible
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)

-- | Subtraction stops at zero.
--
-- prop> n >= m ==> m - n == Z
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

-- | The maximum bound here is infinity.
--
-- prop> maxBound > (n :: Nat)
instance Bounded Nat where
    minBound :: Nat
minBound = Nat
Z
    maxBound :: Nat
maxBound = (Nat -> Nat) -> Nat
forall a. (a -> a) -> a
fix Nat -> Nat
S

-- | Shows integer representation.
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

-- | Reads the integer representation.
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

-- | Will obviously diverge for values like `maxBound`.
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

-- | Uses custom 'enumFrom', 'enumFromThen', 'enumFromThenTo' to avoid
-- expensive conversions to and from 'Int'.
--
-- >>> [1..3]
-- [1,2,3]
-- >>> [1..1]
-- [1]
-- >>> [2..1]
-- []
-- >>> take 3 [1,2..]
-- [1,2,3]
-- >>> take 3 [5,4..]
-- [5,4,3]
-- >>> [1,3..7]
-- [1,3,5,7]
-- >>> [5,4..1]
-- [5,4,3,2,1]
-- >>> [5,3..1]
-- [5,3,1]
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))


-- | Errors on zero.
--
-- >>> 5 `div` 2
-- 2
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