Safe Haskell	None
Language	Haskell2010

Data.BinP.PosP

Contents

Top & Pop
Showing
Conversions
Interesting
Weakening (succ)
Universe

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

Instances details

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

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

Instances details

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

Top & Pop

top :: SBinPI b => PosP b Source #

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 .

Showing

explicitShow :: PosP b -> String Source #

explicitShow' :: PosP' n b -> String Source #

explicitShowsPrec :: Int -> PosP b -> ShowS Source #

explicitShowsPrec' :: Int -> PosP' n b -> ShowS Source #

Conversions

toNatural :: PosP b -> Natural Source #

Convert PosP to Natural .

toNatural' :: forall n b. SNatI n => PosP' n b -> Natural Source #

Convert PosP' to Natural .

Interesting

boring :: PosP ' BE Source #

Counting to one is boring

>>> boring
0

Weakening (succ)

weakenRight1 :: SBinPI b => PosP b -> PosP ( Succ b) Source #

weakenRight1' :: forall b n. SBinP b -> PosP' n b -> PosP' n ( Succ b) Source #

Universe

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]