-- | The implementations of all functions are 
--   supposed to be as non-strict as possible. This is non-trivial as for
--   example a naive implementation of (*) yields O _|_ for the application
--   I _|_ * O IHi while a least-strict version yields O (I _|_). Also the
--   naive / standard implementations of (\-), compare, (\<), (\<=), (\>), 
--   (\>=) are more strict than necessary.
module Data.Number.Nat1 
  ( 
    -- * Datatype
    Nat1(..), 
    -- * Helper Functions
    cmpNat1LT, invOrd, minusNat1, fromNat1, toNat1  
  ) where


import Prelude hiding ( Int )
import Data.Ratio ( (%) )


-- | A binary representation of natural numbers which starts with the least
--   significant bit.
data Nat1
  -- | This constructor represents the most significant bit. There are no 
  --   leading zero bits. 
  = IHi 
  -- | A zero bit
  | O Nat1 
  -- | A one bit
  | I Nat1
  deriving Eq


instance Show Nat1 where
  show = show . fromEnum 


instance Read Nat1 where
  readsPrec n = map (\(x,str) -> (toEnum x,str)) . readsPrec n  


instance Ord Nat1 where
  compare IHi IHi   = EQ
  compare IHi (O _) = LT
  compare IHi (I _) = LT
  compare (O _) IHi = GT
  compare (I _) IHi = GT
  compare (O x) (O y) = compare x y
  compare (I x) (I y) = compare x y
  compare (O x) (I y) = cmpNat1LT x y
  compare (I x) (O y) = invOrd (cmpNat1LT y x)

  -- these instances are lazier than the standard implementation
  -- for example IHi <= _|_ = True
  -- while the standard implementation yields _|_
  x < y  = cmpNat1LT y x == GT
  x > y  = cmpNat1LT x y == GT
  x <= y = cmpNat1LT x y == LT
  x >= y = cmpNat1LT y x == LT

-- | This function is used to implement lazy instances of compare and (\<), 
--   (\<=), (\>), (\>=). It is used to transfer information to more significant
--   bits. Instead of yielding EQ it yields LT if the numbers are equal.
cmpNat1LT :: Nat1 -> Nat1 -> Ordering
cmpNat1LT IHi _     = LT
cmpNat1LT (O _) IHi = GT
cmpNat1LT (I _) IHi = GT
cmpNat1LT (O x) (O y) = cmpNat1LT x y
cmpNat1LT (I x) (I y) = cmpNat1LT x y
cmpNat1LT (O x) (I y) = cmpNat1LT x y
cmpNat1LT (I x) (O y) = invOrd (cmpNat1LT y x)

-- | Maps LT to GT and GT to LT. It is used instead of defining a function
--   cmpNat1GT.
invOrd :: Ordering -> Ordering
invOrd EQ = EQ
invOrd LT = GT
invOrd GT = LT


instance Enum Nat1 where
  succ (O bs) = I bs
  succ (I bs) = O (succ bs)
  succ IHi    = O IHi

  pred IHi         = error "predecessor of 1"
  pred (O IHi)     = IHi
  pred (O x@(O _)) = I (pred x)
  pred (O (I x))   = I (O x) 
  pred (I x)       = O x
 
  fromEnum = fromNat1

  toEnum = toNat1


instance Num Nat1 where
  O x + O y = O (x + y)
  O x + I y = I (x + y)
  O x + IHi = I x
  I x + O y = I (x + y)
  I x + I y = O (succ x + y)
  I x + IHi = O (succ x)
  IHi + y   = succ y

  x - y =
    case minusNat1 x y of
         IHi -> error "result zero in (-)"
         n   -> pred n

  IHi * y = y
  I x * y = O (y * x) + y
  O x * y = O (x * y)

  negate = error "no non-positive numbers in Nat1"

  abs = id

  signum = const IHi

  fromInteger = toNat1

-- | minusNat1 x y yields x - y + 1. This is used to implement (-) for natural
--   numbers.
minusNat1 :: Nat1 -> Nat1 -> Nat1
minusNat1 x   IHi = x
minusNat1 IHi (O _) = error "negative result in (-)"
minusNat1 IHi (I _) = error "negative result in (-)"
minusNat1 (O x) (O y) = pred (O $! minusNat1 x y)
minusNat1 (O x) (I y) = O $! pred (minusNat1 x y)
minusNat1 (I x) (O y) = O $! minusNat1 x y
minusNat1 (I x) (I y) = pred (O $! minusNat1 x y)  


instance Real Nat1 where
  toRational n = fromNat1 n % 1 


-- | This is used for the implementation of toInteger and fromEnum.
fromNat1 :: Num n => Nat1 -> n
fromNat1 IHi   = 1
fromNat1 (O n) = 2 * fromNat1 n
fromNat1 (I n) = 2 * fromNat1 n + 1

-- | This is used for the implementation of fromInteger and toEnum.
toNat1 :: (Integral n,Num n) => n -> Nat1
toNat1 n
  | n<0       = error "fromInteger/toEnum of negative number"
  | n==0      = error "fromInteger/toEnum of zero"
  | n==1      = IHi
  | even n    = O (toNat1 (n `div` 2))
  | otherwise = I (toNat1 (n `div` 2))