Signed Natural Numbers

SignedNat.idr

module SignedNat

import Control.Isomorphism

%access public export
%default total

||| Signed natural numbers: unbounded, signed integers which can be pattern
||| matched.
data SignedNat : Type where
    ||| Zero
    ZZ : SignedNat
    ||| Negated Succesor
    NS : Nat -> SignedNat
    ||| Successor
    PS : Nat -> SignedNat

-- name hints for interactive editing
%name SignedNat k, j, i, n, m

Uninhabited (ZZ = NS n) where
    uninhabited Refl impossible
    
Uninhabited (ZZ = PS n) where
    uninhabited Refl impossible

--------------------------------------------------------------------------------
-- Syntactic tests
--------------------------------------------------------------------------------

data IsNeg : (n : SignedNat) -> Type where
    ItIsNeg : IsNeg (NS n)
    
Uninhabited (IsNeg ZZ) where
    uninhabited ItIsNeg impossible

Uninhabited (IsNeg (PS n)) where
    uninhabited ItIsNeg impossible
 
data IsPos : (n : SignedNat) -> Type where
    ItIsPos : IsPos (PS n)
    
Uninhabited (IsPos ZZ) where
    uninhabited ItIsPos impossible

Uninhabited (IsPos (NS n)) where
    uninhabited itIsPos impossible
        
--------------------------------------------------------------------------------
-- Basic arithmetic functions
--------------------------------------------------------------------------------

||| The absolute value of a signed natural number.
magnitude : (n : SignedNat) -> Nat
magnitude ZZ = Z
magnitude (NS n) = S n
magnitude (PS n) = S n

||| The successor of a signed natural number.
succ : (n : SignedNat) -> SignedNat
succ ZZ         = (PS Z)
succ (NS Z)     = ZZ
succ (NS (S n)) = NS n
succ (PS n)     = PS (S n)

||| The predecessor of a signed natural number.
pred : (n : SignedNat) -> SignedNat
pred ZZ         = (NS Z)
pred (PS Z)     = ZZ
pred (PS (S n)) = PS n
pred (NS n)     = NS (S n)


||| Convert a Nat to an SignedNat within a failable context
toNatSignedNat : SignedNat -> Maybe Nat
toNatSignedNat ZZ = Just Z
toNatSignedNat (NS _) = Nothing
toNatSignedNat (PS n) = Just (S n)

toSignedNatNat : Nat -> SignedNat
toSignedNatNat Z = ZZ
toSignedNatNat (S n) = PS n

diff : (n, m : Nat) -> SignedNat
diff Z     Z     = ZZ
diff Z     (S m) = NS m
diff (S n) Z     = PS n
diff (S n) (S m) = diff n m

negateSignedNat : SignedNat -> SignedNat
negateSignedNat ZZ     = ZZ
negateSignedNat (PS n) = (NS n)
negateSignedNat (NS n) = (PS n)

implementation Num SignedNat where
  ZZ     + m      = m
  n      + ZZ     = n
  (PS n) + (PS m) = PS (S (n + m))
  (PS n) + (NS m) = diff n m
  (NS n) + (PS m) = diff m n
  (NS n) + (NS m) = NS (S (n + m))

  ZZ     * m      = ZZ
  n      * ZZ     = ZZ
  (PS n) * (PS m) = toSignedNatNat ((S n) * (S m))
  (PS n) * (NS m) = negateSignedNat (toSignedNatNat ((S n) * (S m)))
  (NS n) * (PS m) = negateSignedNat (toSignedNatNat ((S n) * (S m)))
  (NS n) * (NS m) = toSignedNatNat ((S n) * (S m))

  fromInteger 0 = ZZ
  fromInteger n =
    if (n > 0) then
        PS (fromInteger (assert_smaller n (n - 1)))
    else
        NS (fromInteger (assert_smaller n (n - 1)))

implementation Neg SignedNat where
    negate = negateSignedNat

    n - m = n + (-m)

    abs ZZ     = ZZ
    abs (PS n) = PS n
    abs (NS n) = PS n
    
Cast Integer SignedNat where
    cast = fromInteger
   
Cast SignedNat Integer where
    cast ZZ = 0
    cast (PS n) = 1 + cast n
    cast (NS n) = -(1 + cast n)
 
Cast SignedNat String where
    cast n = cast (the Integer (cast n))