lazy-lambda-calculus: a887acf68941d8b2d99be2c4787022e75a5383b3

     1: {-# Language DeriveDataTypeable         #-}
     2: 
     3: module Data.Nat where
     4: 
     5: import Data.Data
     6: import Data.Typeable
     7: import Test.LazySmallCheck2012 hiding (Nat, Term, Const)
     8: import Test.LazySmallCheck2012.Core hiding (Term)
     9: 
    10: -- Peano-style natural numbers
    11: data Nat = Z
    12:          | S Nat
    13:            deriving (Eq, Typeable, Data)
    14: 
    15: instance Ord Nat where
    16:   (<=)  Z     Z    = True
    17:   (<=)  Z    (S _) = True
    18:   (<=) (S x)  Z    = False
    19:   (<=) (S x) (S y) = x <= y
    20: 
    21: natToInteger :: Nat -> Integer
    22: natToInteger Z = 0
    23: natToInteger x = let f n  Z    = n
    24:                      f n (S x) = f (n+1) x in
    25:                  f 0 x
    26: 
    27: natToInt :: Nat -> Int
    28: natToInt = fromInteger . natToInteger
    29: 
    30: instance Show Nat where
    31:   show = show . natToInteger
    32: 
    33: instance Num Nat where
    34:   x + y = fromInteger (natToInteger x + natToInteger y)
    35:   x * y = fromInteger (natToInteger x * natToInteger y)
    36: 
    37:   (-) x      Z    = x
    38:   (-) (S x) (S y) = x - y
    39:   (-) Z      _    = error "Subtraction was truncated"
    40: 
    41:   negate = error "Cannot negate a Nat"
    42: 
    43:   abs = id
    44: 
    45:   signum  Z    = Z
    46:   signum (S _) = S Z
    47: 
    48:   fromInteger = let f 0 = Z
    49:                     f n = S (f (n - 1)) in
    50:                 f . abs
    51: 
    52: instance Real Nat where
    53:   toRational = toRational . toInteger
    54: 
    55: instance Integral Nat where
    56:   quotRem x y = let x' = toInteger x'
    57:                     y' = toInteger y'
    58:                     (q, r) = quotRem x' y' in
    59:                 (fromInteger q, fromInteger r)
    60:   toInteger = toInteger . natToInt
    61: 
    62: instance Enum Nat where
    63:   toEnum   = fromInteger . fromIntegral
    64:   fromEnum = natToInt
    65: 
    66: instance Serial Nat where
    67:   series = cons0 Z \/
    68:            cons1 S
    69: 
    70: lookUp :: [a] -> Nat -> Maybe a
    71: lookUp []      _    = Nothing
    72: lookUp (x:xs)  Z    = Just x
    73: lookUp (x:xs) (S n) = lookUp xs n