naturals

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

Unsafe.hs (3125B)

      1 module Naturals.FinatSeq.Unsafe (
      2     FinatSeq (..),
      3     pattern Empty,
      4     pattern (:<),
      5     pattern (:>),
      6     showsPrecl,
      7     showl,
      8     showsPrecr,
      9     showr,
     10     length,
     11     singleton,
     12     lookup,
     13     adjust,
     14     replace,
     15 ) where
     16 
     17 import Data.Coerce
     18 import Data.Sequence (Seq)
     19 import Data.Sequence qualified as Seq
     20 import Unsafe.Coerce
     21 import Prelude hiding (length, lookup)
     22 
     23 import Naturals.Finat.Unsafe
     24 import Naturals.Peano
     25 import Naturals.Snat.Unsafe
     26 
     27 newtype FinatSeq (n :: Peano) a = FinatSeqUnsafe (Seq a)
     28     deriving (Eq, Functor, Foldable, Traversable)
     29 
     30 --------------------------------------------------------------------------------
     31 -- Patterns
     32 
     33 data ViewL n a where
     34     EmptyL :: ViewL Z a
     35     ConsL :: a -> FinatSeq n a -> ViewL (S n) a
     36 
     37 viewl :: FinatSeq n a -> ViewL n a
     38 viewl (FinatSeqUnsafe Seq.Empty) = unsafeCoerce EmptyL
     39 viewl (FinatSeqUnsafe (x Seq.:<| xs)) = unsafeCoerce ConsL x (FinatSeqUnsafe xs)
     40 
     41 data ViewR n a where
     42     EmptyR :: ViewR Z a
     43     ConsR :: FinatSeq n a -> a -> ViewR (S n) a
     44 
     45 viewr :: FinatSeq n a -> ViewR n a
     46 viewr (FinatSeqUnsafe Seq.Empty) = unsafeCoerce EmptyR
     47 viewr (FinatSeqUnsafe (xs Seq.:|> x)) = unsafeCoerce ConsR (FinatSeqUnsafe xs) x
     48 
     49 pattern Empty :: () => (n ~ Z) => FinatSeq n a
     50 pattern Empty <- (viewl -> EmptyL) where Empty = FinatSeqUnsafe Seq.Empty
     51 
     52 infixr 5 :< -- Keep in sync with showsPrecl.
     53 pattern (:<) :: () => (n ~ S m) => a -> FinatSeq m a -> FinatSeq n a
     54 pattern x :< xs <- (viewl -> ConsL x xs) where x :< FinatSeqUnsafe xs = FinatSeqUnsafe (x Seq.:<| xs)
     55 {-# COMPLETE Empty, (:<) #-}
     56 
     57 infixl 5 :> -- Keep in sync with showsPrecr.
     58 pattern (:>) :: () => (n ~ S m) => FinatSeq m a -> a -> FinatSeq n a
     59 pattern xs :> x <- (viewr -> ConsR xs x) where FinatSeqUnsafe xs :> x = FinatSeqUnsafe (xs Seq.:|> x)
     60 {-# COMPLETE Empty, (:>) #-}
     61 
     62 --------------------------------------------------------------------------------
     63 -- Show
     64 
     65 showsPrecl :: (Show a) => Int -> FinatSeq n a -> ShowS
     66 showsPrecl _ Empty = showString "Empty"
     67 showsPrecl p (x :< xs) = showParen (p > 5) $ showsPrec 6 x . showString " :< " . showsPrecl 5 xs
     68 
     69 showl :: (Show a) => FinatSeq n a -> String
     70 showl xs = showsPrecl 0 xs ""
     71 
     72 showsPrecr :: (Show a) => Int -> FinatSeq n a -> ShowS
     73 showsPrecr _ Empty = showString "Empty"
     74 showsPrecr p (xs :> x) = showParen (p > 5) $ showsPrecr 5 xs . showString " :> " . showsPrec 6 x
     75 
     76 showr :: (Show a) => FinatSeq n a -> String
     77 showr xs = showsPrecr 0 xs ""
     78 
     79 instance (Show a) => Show (FinatSeq n a) where
     80     showsPrec = showsPrecl
     81 
     82 --------------------------------------------------------------------------------
     83 -- Common operations
     84 
     85 length :: FinatSeq n a -> Snat n
     86 length (FinatSeqUnsafe s) = SnatUnsafe . fromIntegral . Seq.length $ s
     87 
     88 singleton :: a -> FinatSeq SZ a
     89 singleton = FinatSeqUnsafe . Seq.singleton
     90 
     91 lookup :: Finat n -> FinatSeq n a -> a
     92 lookup (FinatUnsafe i) (FinatSeqUnsafe s) = Seq.index s (fromIntegral i)
     93 
     94 adjust :: (a -> a) -> Finat n -> FinatSeq n a -> FinatSeq n a
     95 adjust f (FinatUnsafe i) = coerce $ Seq.adjust' f (fromIntegral i)
     96 
     97 replace :: Finat n -> a -> FinatSeq n a -> FinatSeq n a
     98 replace i v = adjust (const v) i