{-# LANGUAGE DeriveDataTypeable #-}

-- |
-- Module      :  Test.ChasingBottoms.Nat
-- Copyright   :  (c) Nils Anders Danielsson 2004-2021
-- 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
/= :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c== :: 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
min :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmax :: Nat -> Nat -> Nat
>= :: Nat -> Nat -> Bool
$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
compare :: Nat -> Nat -> Ordering
$ccompare :: Nat -> Nat -> Ordering
$cp1Ord :: Eq 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 :: 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 :: 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
    Integer
n <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary :: Gen Integer
    Nat -> Gen Nat
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat -> Gen Nat) -> Nat -> Gen Nat
forall a b. (a -> b) -> a -> b
$ Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer -> Nat) -> Integer -> Nat
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
abs Integer
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 :: Nat -> Gen b -> Gen b
coarbitrary Nat
n = 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)