naturals

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

Unsafe.hs (898B)

      1 module Naturals.Finatural.Unsafe (
      2     Finatural (..),
      3     finaturalMirror,
      4 ) where
      5 
      6 import GHC.Natural
      7 import Unsafe.Coerce
      8 
      9 import Naturals.IsFin
     10 import Naturals.Natural
     11 import Naturals.Peano
     12 import Naturals.Snatural.Unsafe
     13 
     14 -- | Finite (@Peano@-indexed) prefixes of @Natural@.
     15 newtype Finatural (n :: Peano) = FinaturalUnsafe Natural deriving newtype (Show, Eq)
     16 
     17 instance ToNatural (Finatural n) where
     18     toNatural (FinaturalUnsafe n) = n
     19 
     20 instance IsFin Finatural where
     21     finZero = FinaturalUnsafe 0
     22 
     23     finSucc = FinaturalUnsafe . succ . toNatural
     24 
     25     finPeel (FinaturalUnsafe 0) = unsafeCoerce FZeroOp
     26     finPeel (FinaturalUnsafe n) = unsafeCoerce FSuccOp . FinaturalUnsafe . pred $ n
     27 
     28     finWeaken (FinaturalUnsafe n) = FinaturalUnsafe n
     29 
     30 finaturalMirror :: Snatural n -> Finatural n -> Finatural n
     31 finaturalMirror (SnaturalUnsafe n) (FinaturalUnsafe i) = FinaturalUnsafe (n - i - 1)