    {-# LANGUAGE DeriveDataTypeable #-}

    -- |
    -- Module      :  Test.ChasingBottoms.Nat
    -- Copyright   :  (c) Nils Anders Danielsson 2004-2022, 2024-2025
    -- License     :  See the file LICENCE.
    --
    -- Maintainer  :  http://www.cse.chalmers.se/~nad/
    -- Stability   :  experimental
    -- Portability :  non-portable (GHC-specific)
    --
    -- A simple implementation of natural numbers on top of 'Integer's.
    -- Note that since 'Integer's are used there is no infinite natural
    -- number; in other words, 'succ' is strict.

    module Test.ChasingBottoms.Nat(Nat, isSucc, fromSucc, natrec, foldN) where

    import Test.QuickCheck
    import Test.QuickCheck.Arbitrary (CoArbitrary(..))
    import qualified Data.Generics as G
    import Data.Ratio ((%))
    import Data.Typeable

    default ()

    -- | Natural numbers.
    --
    -- No 'G.Data' instance is provided, because the implementation should
    -- be abstract.

    -- Could add 'G.Data' instance based on unary representation of
    -- natural numbers, but that would lead to inefficiencies.
    newtype Nat = Nat { Nat -> Integer
    nat2int :: Integer } deriving (Nat -> Nat -> Bool
    (Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Nat -> Nat -> Bool
    == :: Nat -> Nat -> Bool
    $c/= :: Nat -> Nat -> Bool
    /= :: Nat -> Nat -> Bool
    Eq, Eq Nat
    Eq Nat =>
    (Nat -> Nat -> Ordering)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Bool)
    -> (Nat -> Nat -> Nat)
    -> (Nat -> Nat -> Nat)
    -> Ord Nat
    Nat -> Nat -> Bool
    Nat -> Nat -> Ordering
    Nat -> Nat -> Nat
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Nat -> Nat -> Ordering
    compare :: Nat -> Nat -> Ordering
    $c< :: Nat -> Nat -> Bool
    < :: Nat -> Nat -> Bool
    $c<= :: Nat -> Nat -> Bool
    <= :: Nat -> Nat -> Bool
    $c> :: Nat -> Nat -> Bool
    > :: Nat -> Nat -> Bool
    $c>= :: Nat -> Nat -> Bool
    >= :: Nat -> Nat -> Bool
    $cmax :: Nat -> Nat -> Nat
    max :: Nat -> Nat -> Nat
    $cmin :: Nat -> Nat -> Nat
    min :: Nat -> Nat -> Nat
    Ord, Typeable)

    -- | @'isSucc' 0 == 'False'@, for other total natural numbers it is 'True'.
    isSucc :: Nat -> Bool
    isSucc :: Nat -> Bool
    isSucc (Nat Integer
    0) = Bool
    False
    isSucc Nat
    _       = Bool
    True

    -- | @'fromSucc' 0 == 'Nothing'@, @'fromSucc' (n+1) == 'Just' n@ for a
    -- total natural number @n@.
    fromSucc :: Nat -> Maybe Nat
    fromSucc :: Nat -> Maybe Nat
    fromSucc (Nat Integer
    0) = Maybe Nat
    forall a. Maybe a
    Nothing
    fromSucc Nat
    n       = Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just (Nat -> Maybe Nat) -> Nat -> Maybe Nat
    forall a b. (a -> b) -> a -> b
    $ Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n

    -- | 'natrec' performs primitive recursion on natural numbers.
    natrec :: a -> (Nat -> a -> a) -> Nat -> a
    natrec :: forall a. a -> (Nat -> a -> a) -> Nat -> a
    natrec a
    g Nat -> a -> a
    _ (Nat Integer
    0) = a
    g
    natrec a
    g Nat -> a -> a
    h Nat
    n       = let p :: Nat
    p = Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n in Nat -> a -> a
    h Nat
    p (a -> (Nat -> a -> a) -> Nat -> a
    forall a. a -> (Nat -> a -> a) -> Nat -> a
    natrec a
    g Nat -> a -> a
    h Nat
    p)

    -- | 'foldN' is a fold on natural numbers:
    --
    -- @
    --  'foldN' g h = 'natrec' g ('curry' '$' h . 'snd')
    -- @
    foldN :: a -> (a -> a) -> Nat -> a
    foldN :: forall a. a -> (a -> a) -> Nat -> a
    foldN a
    g a -> a
    h = a -> (Nat -> a -> a) -> Nat -> a
    forall a. a -> (Nat -> a -> a) -> Nat -> a
    natrec a
    g (((Nat, a) -> a) -> Nat -> a -> a
    forall a b c. ((a, b) -> c) -> a -> b -> c
    curry (((Nat, a) -> a) -> Nat -> a -> a)
    -> ((Nat, a) -> a) -> Nat -> a -> a
    forall a b. (a -> b) -> a -> b
    $ a -> a
    h (a -> a) -> ((Nat, a) -> a) -> (Nat, a) -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Nat, a) -> a
    forall a b. (a, b) -> b
    snd)

    steal :: (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat
    steal :: (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat
    steal Integer -> Integer -> Integer
    op Nat
    x Nat
    y = Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Nat) -> Integer -> Nat
    forall a b. (a -> b) -> a -> b
    $ (Nat -> Integer
    nat2int Nat
    x) Integer -> Integer -> Integer
    `op` (Nat -> Integer
    nat2int Nat
    y)

    instance Num Nat where
      + :: Nat -> Nat -> Nat
    (+) = (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat
    steal Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+)
      * :: Nat -> Nat -> Nat
    (*) = (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat
    steal Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (*)
      Nat
    x - :: Nat -> Nat -> Nat
    - Nat
    y = let x' :: Integer
    x' = Nat -> Integer
    nat2int Nat
    x; y' :: Integer
    y' = Nat -> Integer
    nat2int Nat
    y
              in if Integer
    x' Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    y' then
                [Char] -> Nat
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Nat: x - y undefined if y > x."
               else
                Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Nat) -> Integer -> Nat
    forall a b. (a -> b) -> a -> b
    $ Integer
    x' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    y'
      negate :: Nat -> Nat
    negate = [Char] -> Nat -> Nat
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Nat: negate undefined."
      signum :: Nat -> Nat
    signum Nat
    n = if Nat -> Bool
    isSucc Nat
    n then Nat
    1 else Nat
    0
      abs :: Nat -> Nat
    abs = Nat -> Nat
    forall a. a -> a
    id
      fromInteger :: Integer -> Nat
    fromInteger Integer
    i | Integer
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    0     = [Char] -> Nat
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Nat: No negative natural numbers."
                    | Bool
    otherwise = Integer -> Nat
    Nat Integer
    i

    instance Real Nat where
      toRational :: Nat -> Rational
    toRational = (Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % Integer
    1) (Integer -> Rational) -> (Nat -> Integer) -> Nat -> Rational
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Integer
    nat2int

    steal2 :: (Integer -> Integer -> (Integer, Integer))
              -> Nat -> Nat -> (Nat, Nat)
    steal2 :: (Integer -> Integer -> (Integer, Integer))
    -> Nat -> Nat -> (Nat, Nat)
    steal2 Integer -> Integer -> (Integer, Integer)
    op Nat
    x Nat
    y = let (Integer
    x', Integer
    y') = (Nat -> Integer
    nat2int Nat
    x) Integer -> Integer -> (Integer, Integer)
    `op` (Nat -> Integer
    nat2int Nat
    y)
                    in (Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger Integer
    x', Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger Integer
    y')

    instance Integral Nat where
      toInteger :: Nat -> Integer
    toInteger = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Integer) -> (Nat -> Int) -> Nat -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Int
    forall a. Enum a => a -> Int
    fromEnum
      Nat
    a quotRem :: Nat -> Nat -> (Nat, Nat)
    `quotRem` Nat
    b = if Nat
    b Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0 then
        [Char] -> (Nat, Nat)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Nat: quotRem undefined for zero divisors."
       else
        (Integer -> Integer -> (Integer, Integer))
    -> Nat -> Nat -> (Nat, Nat)
    steal2 Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    quotRem Nat
    a Nat
    b
      Nat
    a divMod :: Nat -> Nat -> (Nat, Nat)
    `divMod` Nat
    b = if Nat
    b Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0 then
        [Char] -> (Nat, Nat)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Nat: divMod undefined for zero divisors."
       else
        (Integer -> Integer -> (Integer, Integer))
    -> Nat -> Nat -> (Nat, Nat)
    steal2 Integer -> Integer -> (Integer, Integer)
    forall a. Integral a => a -> a -> (a, a)
    divMod Nat
    a Nat
    b

    instance Enum Nat where
      succ :: Nat -> Nat
    succ = (Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    1)
      pred :: Nat -> Nat
    pred = Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    subtract Nat
    1
      toEnum :: Int -> Nat
    toEnum = Integer -> Nat
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Nat) -> (Int -> Integer) -> Int -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger
      fromEnum :: Nat -> Int
    fromEnum = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Int) -> (Nat -> Integer) -> Nat -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Integer
    nat2int
      -- Add tests for enumFrom and friends if the default definitions are
      -- overridden.

    instance Show Nat where
      showsPrec :: Int -> Nat -> ShowS
    showsPrec Int
    _ = [Char] -> ShowS
    showString ([Char] -> ShowS) -> (Nat -> [Char]) -> Nat -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> [Char]
    forall a. Show a => a -> [Char]
    show (Integer -> [Char]) -> (Nat -> Integer) -> Nat -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Integer
    nat2int

    instance Arbitrary Nat where
      arbitrary :: Gen Nat
    arbitrary = do
        n <- Gen Integer
    forall a. Arbitrary a => Gen a
    arbitrary :: Gen Integer
        return $ fromInteger $ abs n

      shrink :: Nat -> [Nat]
    shrink Nat
    0 = []
      shrink Nat
    n = [Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]

    instance CoArbitrary Nat where
      coarbitrary :: forall b. Nat -> Gen b -> Gen b
    coarbitrary Nat
    n = Integer -> Gen b -> Gen b
    forall b. Integer -> Gen b -> Gen b
    forall a b. CoArbitrary a => a -> Gen b -> Gen b
    coarbitrary (Nat -> Integer
    forall a. Integral a => a -> Integer
    toInteger Nat
    n)