Fin 0.1.1.0 → 0.2.0.0

raw patch · 2 files changed

+1/−100 lines, 2 files

Files

• Data/Fin.hs +0/−99
• Fin.cabal +1/−1

@@ -1,99 +0,0 @@-{-# LANGUAGE TypeApplications #-}--module Data.Fin where--import Prelude hiding (iterate)-import Control.Applicative-import Data.Ap-import Data.CList (CList (..))-import Data.Foldable-import Data.Function (on)-import Data.Functor.Compose-import Data.Maybe-import Data.Natural.Class-import Data.Peano (Peano)-import qualified Data.Peano as P-import Data.Semigroup (Endo (..))-import qualified Numeric.Natural as N-import qualified Text.ParserCombinators.ReadP as Read-import Text.ParserCombinators.ReadPrec (readP_to_Prec)-import Text.Read (Read (..))--data Fin :: Peano -> * where-    Zero :: Fin (P.Succ n)-    Succ :: Fin n -> Fin (P.Succ n)--deriving instance Eq (Fin n)-deriving instance Ord (Fin n)-deriving instance Show (Fin n)--instance Read (Fin P.Zero) where readPrec = empty-instance Read (Fin n) => Read (Fin (P.Succ n)) where-    readPrec = Succ <$ string "Succ" <*> readPrec <|> Zero <$ string "Zero"-      where string = readP_to_Prec . pure . Read.string--instance Bounded (Fin (P.Succ P.Zero)) where-    minBound = Zero-    maxBound = Zero--instance Bounded (Fin n) => Bounded (Fin (P.Succ n)) where-    minBound = Zero-    maxBound = Succ maxBound--instance Enum (Fin P.Zero) where-    toEnum _ = error "toEnum @(Fin Zero)"-    fromEnum = \ case-    succ = \ case-    pred = \ case--instance (Natural n, Enum (Fin n)) => Enum (Fin (P.Succ n)) where-    toEnum 0 = Zero-    toEnum n = Succ (toEnum (pred n))-    fromEnum Zero = 0-    fromEnum (Succ n) = succ (fromEnum n)-    enumFrom Zero = Zero : (Succ <$> toList enum)-    enumFrom (Succ n) = (tail . enumFrom . inj₁) n--enum :: Natural n => CList n (Fin n)-enum = ap $ natural (Ap Nil) (Ap (Zero :. (Succ <$> enum)))--instance Num (Fin P.Zero) where-    (+) = \ case-    (*) = \ case-    abs = id-    negate = \ case-    signum = \ case-    fromInteger _ = error "fromInteger @(Fin Zero)"--instance (Natural n, Num (Fin n)) => Num (Fin (P.Succ n)) where-    a + b = toFin $ ((+) @N.Natural `on` fromFin) a b-    a - b = toFin $ ((-) @  Integer `on` fromFin) a b-    a * b = toFin $ ((*) @N.Natural `on` fromFin) a b--    abs = id-    signum = lift₁ . appEndo . getCompose $-             natural @n (Compose . Endo $ \ case) (Compose . Endo $ pure Zero)--    fromInteger = toFin--inj₁ :: Fin n -> Fin (P.Succ n)-inj₁ Zero = Zero-inj₁ (Succ n) = Succ (inj₁ n)--lift₁ :: (Fin m -> Fin n) -> Fin (P.Succ m) -> Fin (P.Succ n)-lift₁ _ Zero = Zero-lift₁ f (Succ n) = Succ (f n)--fromFin :: Integral a => Fin n -> a-fromFin Zero = 0-fromFin (Succ n) = succ (fromFin n)--toFin :: ∀ n a . (Natural n, Integral a) => a -> Fin (P.Succ n)-toFin = fromJust . toFinMay . (`mod` getConst (iterate @n (+1) 1))--toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin (P.Succ n))-toFinMay = getCompose . getCompose . getCompose $-           natural (Compose . Compose . Compose $ \ case 0 -> Just Zero-                                                         _ -> Nothing)-                   (Compose . Compose . Compose $ \ case 0 -> Just Zero-                                                         n -> Succ <$> toFinMay (n-1))

@@ -1,5 +1,5 @@ name:                Fin-version:             0.1.1.0+version:             0.2.0.0 synopsis:            Finite totally-ordered sets -- description:          license:             BSD3