Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Signed Natural Numbers
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.