Safe Haskell	Safe
Language	Haskell2010

Data.BinP.PosP

Contents

Synopsis

newtype PosP (b :: BinP) = PosP {
- unPosP :: PosP' 'Z b
}
data PosP' (n :: Nat) (b :: BinP) where
- AtEnd :: Wrd n -> PosP' n 'BE
- Here :: Wrd n -> PosP' n ('B1 b)
- There1 :: PosP' ('S n) b -> PosP' n ('B1 b)
- There0 :: PosP' ('S n) b -> PosP' n ('B0 b)
top :: SBinPI b => PosP b
pop :: (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => PosP a -> PosP b
explicitShow :: PosP b -> String
explicitShow' :: PosP' n b -> String
explicitShowsPrec :: Int -> PosP b -> ShowS
explicitShowsPrec' :: Int -> PosP' n b -> ShowS
toNatural :: PosP b -> Natural
toNatural' :: forall n b. SNatI n => PosP' n b -> Natural
boring :: PosP 'BE
weakenRight1 :: SBinPI b => PosP b -> PosP (Succ b)
weakenRight1' :: forall b n. SBinP b -> PosP' n b -> PosP' n (Succ b)
universe :: forall b. SBinPI b => [PosP b]
universe' :: forall b n. (SNatI n, SBinPI b) => [PosP' n b]

Documentation

newtype PosP (b :: BinP) Source #

PosP is to BinP is what Fin is to Nat, when n is Z.

Constructors

PosP
Fields unPosP :: PosP' 'Z b

Instances details

SBinPI b => Bounded (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods minBound :: PosP b # maxBound :: PosP b #
Eq (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods (==) :: PosP b -> PosP b -> Bool # (/=) :: PosP b -> PosP b -> Bool #
Ord (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods compare :: PosP b -> PosP b -> Ordering # (<) :: PosP b -> PosP b -> Bool # (<=) :: PosP b -> PosP b -> Bool # (>) :: PosP b -> PosP b -> Bool # (>=) :: PosP b -> PosP b -> Bool # max :: PosP b -> PosP b -> PosP b # min :: PosP b -> PosP b -> PosP b #
Show (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods showsPrec :: Int -> PosP b -> ShowS # show :: PosP b -> String # showList :: [PosP b] -> ShowS #
SBinPI b => Function (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods function :: (PosP b -> b0) -> PosP b :-> b0 #
SBinPI b => Arbitrary (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods arbitrary :: Gen (PosP b) # shrink :: PosP b -> [PosP b] #
CoArbitrary (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods coarbitrary :: PosP b -> Gen b0 -> Gen b0 #

data PosP' (n :: Nat) (b :: BinP) where Source #

PosP' is a structure inside PosP.

Constructors

AtEnd
Fields :: Wrd n -> PosP' n 'BE position is either at the last digit;
Here
Fields :: Wrd n -> PosP' n ('B1 b) somewhere here
There1
Fields :: PosP' ('S n) b -> PosP' n ('B1 b) or there, if the bit is one;
There0
Fields :: PosP' ('S n) b -> PosP' n ('B0 b) or only there if it is none.

Instances details

(SNatI n, SBinPI b) => Bounded (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods minBound :: PosP' n b # maxBound :: PosP' n b #
Eq (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods (==) :: PosP' n b -> PosP' n b -> Bool # (/=) :: PosP' n b -> PosP' n b -> Bool #
Ord (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods compare :: PosP' n b -> PosP' n b -> Ordering # (<) :: PosP' n b -> PosP' n b -> Bool # (<=) :: PosP' n b -> PosP' n b -> Bool # (>) :: PosP' n b -> PosP' n b -> Bool # (>=) :: PosP' n b -> PosP' n b -> Bool # max :: PosP' n b -> PosP' n b -> PosP' n b # min :: PosP' n b -> PosP' n b -> PosP' n b #
SNatI n => Show (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods showsPrec :: Int -> PosP' n b -> ShowS # show :: PosP' n b -> String # showList :: [PosP' n b] -> ShowS #
(SNatI n, SBinPI b) => Function (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods function :: (PosP' n b -> b0) -> PosP' n b :-> b0 #
(SNatI n, SBinPI b) => Arbitrary (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods arbitrary :: Gen (PosP' n b) # shrink :: PosP' n b -> [PosP' n b] #
SNatI n => CoArbitrary (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods coarbitrary :: PosP' n b -> Gen b0 -> Gen b0 #

Top & Pop

top and pop serve as FZ and FS, with types specified so type-inference works backwards from the result.

>>> top :: PosP BinP4
0

>>> pop (pop top) :: PosP BinP4
2

>>> pop (pop top) :: PosP BinP9
2

pop :: (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => PosP a -> PosP b Source #

See top.

Convert PosP to Natural.

Convert PosP' to Natural.

Counting to one is boring

>>> boring
0

universe :: forall b. SBinPI b => [PosP b] Source #

>>> universe :: [PosP BinP9]
[0,1,2,3,4,5,6,7,8]

universe' :: forall b n. (SNatI n, SBinPI b) => [PosP' n b] Source #

This gives a hint, what the n parameter means in PosP'.

>>> universe' :: [PosP' N.Nat2 BinP2]
[0,1,2,3,4,5,6,7]