Aritmética de Peano

peano.hs

data Nat = Zero | Suc Nat
inc :: Nat -> Nat
inc x = Suc x

showNat :: Nat -> String
showNat Zero = "Zero"  
showNat (Suc v) = "Suc " ++ (show v)

type BinNat = (Nat -> Nat -> Nat)

addNat :: BinNat
addNat Zero x = x
addNat x Zero = x
addNat x (Suc y) = addNat (Suc x) y

multNat :: BinNat
multNat Zero x = Zero
multNat x Zero = Zero
multNat (Suc x) y = addNat y (multNat x y)

ltNat :: Nat -> Nat -> Bool
ltNat Zero Zero = False
ltNat Zero (Suc _) = True
ltNat (Suc _) Zero = False
ltNat (Suc x) (Suc y) = ltNat x y

diffNat :: BinNat
diffNat x Zero = x
diffNat Zero _ = Zero
diffNat (Suc x) (Suc y) = diffNat x y

modNat :: BinNat
modNat x Zero = Zero
modNat x y = if (ltNat x y) then x else modNat (diffNat x y) y

divNat :: BinNat
divNat x Zero = Zero
divNat x y = if (ltNat x y) then Zero else Suc (divNat (diffNat x y) y)

ackPeter :: BinNat
ackPeter Zero n = inc n
ackPeter (Suc m) Zero = ackPeter m (Suc Zero)
ackPeter (Suc m) (Suc n) = ackPeter m (ackPeter (inc m) n)


instance Show Nat where
    show = showNat

main :: IO ()
main =  do

let dois = (inc (inc Zero))

let quatro = addNat dois dois

print dois
print quatro

print (ackPeter dois quatro)
--print (inc (inc Zero))

--print (multNat (inc (Suc Zero)) (inc (inc (inc Zero))))
--print (ltNat (inc (Suc Zero)) (inc (inc (inc Zero))))

--print (diffNat (multNat (inc (Suc Zero)) (inc (inc (inc Zero)))) (inc (inc (inc (inc Zero)))))
--print (modNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (inc (inc (Suc (Suc Zero)))) )
--print (divNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (inc (inc (Suc (Suc Zero)))) )

--print (divNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (Suc (Suc Zero)) )
--print (modNat (multNat (inc (Suc (Suc Zero))) (inc (inc (inc Zero)))) (Suc (Suc Zero)) )

--print (ackPeter Zero Zero)