naturals

natural numbers in Haskell
git clone git://git.rr3.xyz/naturals
Log | Files | Refs

Unsafe.hs (815B)

      1 module Naturals.Snat.Unsafe (
      2     Snat (..),
      3 ) where
      4 
      5 import GHC.Natural
      6 import Unsafe.Coerce
      7 
      8 import Naturals.IsSpeano
      9 import Naturals.Nat
     10 import Naturals.Natural
     11 import Naturals.Peano
     12 
     13 -- | Singleton (@Peano@-indexed) natural numbers represented as a @Nat@.
     14 newtype Snat (n :: Peano) = SnatUnsafe Nat deriving newtype (Show)
     15 
     16 instance Eq (Snat n) where
     17     _ == _ = True
     18 
     19 instance ToNat (Snat n) where
     20     toNat (SnatUnsafe n) = n
     21 
     22 instance ToNatural (Snat n) where
     23     toNatural = wordToNatural . fromNat . toNat
     24 
     25 instance IsSpeano Snat where
     26     speanoZero = SnatUnsafe 0
     27 
     28     speanoSucc = SnatUnsafe . succ . toNat
     29 
     30     speanoPeel (SnatUnsafe 0) = unsafeCoerce ZeroOp
     31     speanoPeel (SnatUnsafe n) = unsafeCoerce SuccOp . SnatUnsafe . pred $ n
     32 
     33     speanoAdd (SnatUnsafe m) (SnatUnsafe n) = SnatUnsafe (m + n)