Skip to content

Instantly share code, notes, and snippets.

# JadenGeller/SignedNat.idr Created Dec 17, 2017

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))
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.