module Test.ChasingBottoms.Nat(Nat, isSucc, fromSucc, natrec, foldN) where
import Test.QuickCheck
import qualified Data.Generics as G
import Data.Ratio ((%))
import Data.Typeable
default ()
newtype Nat = Nat { nat2int :: Integer } deriving (Eq, Ord, Typeable)
isSucc :: Nat -> Bool
isSucc (Nat 0) = False
isSucc _ = True
fromSucc :: Nat -> Maybe Nat
fromSucc (Nat 0) = Nothing
fromSucc n = Just $ pred n
natrec :: a -> (Nat -> a -> a) -> Nat -> a
natrec g _ (Nat 0) = g
natrec g h n = let p = pred n in h p (natrec g h p)
foldN :: a -> (a -> a) -> Nat -> a
foldN g h = natrec g (curry $ h . snd)
steal :: (Integer -> Integer -> Integer) -> Nat -> Nat -> Nat
steal op x y = fromInteger $ (nat2int x) `op` (nat2int y)
instance Num Nat where
(+) = steal (+)
(*) = steal (*)
x y = let x' = nat2int x; y' = nat2int y
in if x' < y' then
error "Nat: x - y undefined if y > x."
else
fromInteger $ x' y'
negate = error "Nat: negate undefined."
signum n = if isSucc n then 1 else 0
abs = id
fromInteger i | i < 0 = error "Nat: No negative natural numbers."
| otherwise = Nat i
instance Real Nat where
toRational = (%1) . nat2int
steal2 :: (Integer -> Integer -> (Integer, Integer))
-> Nat -> Nat -> (Nat, Nat)
steal2 op x y = let (x', y') = (nat2int x) `op` (nat2int y)
in (fromInteger x', fromInteger y')
instance Integral Nat where
toInteger = toInteger . fromEnum
a `quotRem` b = if b == 0 then
error "Nat: quotRem undefined for zero divisors."
else
steal2 quotRem a b
a `divMod` b = if b == 0 then
error "Nat: divMod undefined for zero divisors."
else
steal2 divMod a b
instance Enum Nat where
succ = (+ 1)
pred = subtract 1
toEnum = fromInteger . toInteger
fromEnum = fromInteger . nat2int
instance Show Nat where
showsPrec _ = showString . show . nat2int
instance Arbitrary Nat where
arbitrary = do
n <- arbitrary :: Gen Integer
return $ fromInteger $ abs n
shrink 0 = []
shrink n = [n 1]
instance CoArbitrary Nat where
coarbitrary n = coarbitrary (toInteger n)