naturals

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

Unsafe.hs (886B)

      1 module Naturals.Finat.Unsafe (
      2     Finat (..),
      3     finatMirror,
      4 ) where
      5 
      6 import GHC.Natural
      7 import Unsafe.Coerce
      8 
      9 import Naturals.IsFin
     10 import Naturals.Nat
     11 import Naturals.Natural
     12 import Naturals.Peano
     13 import Naturals.Snat.Unsafe
     14 
     15 -- | Finite (@Peano@-indexed) prefixes of @Nat@.
     16 newtype Finat (n :: Peano) = FinatUnsafe Nat deriving newtype (Show, Eq)
     17 
     18 instance ToNat (Finat n) where
     19     toNat (FinatUnsafe n) = n
     20 
     21 instance ToNatural (Finat n) where
     22     toNatural = wordToNatural . fromNat . toNat
     23 
     24 instance IsFin Finat where
     25     finZero = FinatUnsafe 0
     26 
     27     finSucc = FinatUnsafe . succ . toNat
     28 
     29     finPeel (FinatUnsafe 0) = unsafeCoerce FZeroOp
     30     finPeel (FinatUnsafe n) = unsafeCoerce FSuccOp . FinatUnsafe . pred $ n
     31 
     32     finWeaken (FinatUnsafe n) = FinatUnsafe n
     33 
     34 finatMirror :: Snat n -> Finat n -> Finat n
     35 finatMirror (SnatUnsafe n) (FinatUnsafe i) = FinatUnsafe (n - i - 1)