{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

{-
Peano.hs

Provides integers in the type system, with addition.

Gregory Price (price mit.edu)
2003-11-12
lightly edited 2007-11-19 for a SIPB cluedump
-}

module Peano(Z, S, P, 
             Zero, One, MOne, Two, MTwo, Three, MThree, Four, MFour,
             UnPeano(unPeano), PNum(PNum),
             Add, Sub,
             Twice
            ) where


data Z   = Z   
data S a = S a
data P a = P a
data PNum a = PNum

type Zero   = Z
type  One   = S Zero
type MOne   = P Zero
type  Two   = S  One
type MTwo   = P MOne
type  Three = S  Two
type MThree = P MTwo
type  Four  = S  Three
type MFour  = P MThree


class UnPeano n where
    unPeano :: PNum n -> Int

instance              UnPeano    Z  where unPeano PNum = 0
instance UnPeano n => UnPeano (S n) where unPeano PNum = unPeano (PNum::PNum n)  +  1
instance UnPeano n => UnPeano (P n) where unPeano PNum = unPeano (PNum::PNum n)  -  1

class (Add' a b c, Sub' c b a, Sub' c a b) => Add a b c | a b -> c, b c -> a, c a -> b
    where padd :: PNum a -> PNum b -> PNum c
          padd _ _ = PNum
class (Sub' a b c, Add' c b a, Sub' a c b) => Sub a b c | a b -> c, b c -> a, c a -> b
    where psub :: PNum a -> PNum b -> PNum c
          psub _ _ = PNum
instance (Add' a b c, Sub' c b a, Sub' c a b) => Add a b c
instance (Sub' a b c, Add' c b a, Sub' a c b) => Sub a b c


class Add' a b c | a b -> c where
    padd' :: PNum a -> PNum b -> PNum c
class Sub' a b c | a b -> c where
    psub' :: PNum a -> PNum b -> PNum c

-- instance              Add'    Z     a        a   where add'    Z     a  =         a
instance               Add'    Z     Z        Z   where padd' _ _ = PNum

instance               Add' (S a)    Z     (S a)  where padd' _ _ = PNum
instance               Add' (P a)    Z     (P a)  where padd' _ _ = PNum
instance               Add'    Z  (S b)    (S b)  where padd' _ _ = PNum
instance               Add'    Z  (P b)    (P b)  where padd' _ _ = PNum

instance Add' a b c => Add' (S a) (S b) (S (S c)) where padd' _ _ = PNum
instance Add' a b c => Add' (S a) (P b)       c   where padd' _ _ = PNum
instance Add' a b c => Add' (P a) (S b)       c   where padd' _ _ = PNum
instance Add' a b c => Add' (P a) (P b) (P (P c)) where padd' _ _ = PNum


instance               Sub'    Z     Z        Z   where psub' _ _ = PNum

instance               Sub' (S a)    Z     (S a)  where psub' _ _ = PNum
instance               Sub' (P a)    Z     (P a)  where psub' _ _ = PNum
instance               Sub'    Z  (P b)    (S b)  where psub' _ _ = PNum
instance               Sub'    Z  (S b)    (P b)  where psub' _ _ = PNum

instance Sub' a b c => Sub' (S a) (P b) (S (S c)) where psub' _ _ = PNum
instance Sub' a b c => Sub' (S a) (S b)       c   where psub' _ _ = PNum
instance Sub' a b c => Sub' (P a) (P b)       c   where psub' _ _ = PNum
instance Sub' a b c => Sub' (P a) (S b) (P (P c)) where psub' _ _ = PNum



class Twice a b | a -> b, b -> a
instance Twice Z Z
instance Twice a b => Twice (S a) (S (S a))




class AddP a b c | a b -> c, b c -> a where paddp :: PNum a -> PNum b -> PNum c

instance               AddP    Z     Z        Z   where paddp _ _ = PNum
instance               AddP (S a)    Z     (S a)  where paddp _ _ = PNum
--instance AddP a b c => AddP (S a)    b     (S c)  where paddp _ _ = PNum
instance AddP a b c => AddP    a  (S b)    (S c)  where paddp _ _ = PNum