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 :: forall (n :: Nat). Wrd n -> PosP' n 'BE
- Here :: forall (n :: Nat) (b1 :: BinP). Wrd n -> PosP' n ('B1 b1)
- There1 :: forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B1 b1)
- There0 :: forall (n :: Nat) (b1 :: BinP). PosP' ('S n) b1 -> PosP' n ('B0 b1)
top :: forall (b :: BinP). SBinPI b => PosP b
pop :: forall (a :: BinP) (b :: BinP). (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => PosP a -> PosP b
explicitShow :: forall (b :: BinP). PosP b -> String
explicitShow' :: forall (n :: Nat) (b :: BinP). PosP' n b -> String
explicitShowsPrec :: forall (b :: BinP). Int -> PosP b -> ShowS
explicitShowsPrec' :: forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS
toNatural :: forall (b :: BinP). PosP b -> Natural
toNatural' :: forall (n :: Nat) (b :: BinP). SNatI n => PosP' n b -> Natural
boring :: PosP 'BE
weakenRight1 :: forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b)
weakenRight1' :: forall (b :: BinP) (n :: Nat). SBinP b -> PosP' n b -> PosP' n (Succ b)
universe :: forall (b :: BinP). SBinPI b => [PosP b]
universe' :: forall (b :: BinP) (n :: Nat). (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

EqP PosP Source #	Since: 0.1.3
Instance details Defined in Data.BinP.PosP Methods eqp :: forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Bool #
GShow PosP Source #	Since: 0.1.3
Instance details Defined in Data.BinP.PosP Methods gshowsPrec :: forall (a :: BinP). Int -> PosP a -> ShowS #
OrdP PosP Source #	Since: 0.1.3
Instance details Defined in Data.BinP.PosP Methods comparep :: forall (a :: BinP) (b :: BinP). PosP a -> PosP b -> Ordering #
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 #
SBinPI b => Function (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods function :: (PosP b -> b0) -> PosP b :-> b0 #
SBinPI b => Bounded (PosP b) Source #
Instance details Defined in Data.BinP.PosP Methods minBound :: PosP b # maxBound :: 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 #
b ~ 'BE => Boring (PosP b) Source #	Since: 0.1.2
Instance details Defined in Data.BinP.PosP Methods boring :: PosP b #
NFData (PosP b) Source #	Since: 0.1.2
Instance details Defined in Data.BinP.PosP Methods rnf :: 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 #

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

PosP' is a structure inside PosP.

Constructors

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

Instances

Instances details

SNatI n => GShow (PosP' n :: BinP -> Type) Source #	Since: 0.1.3
Instance details Defined in Data.BinP.PosP Methods gshowsPrec :: forall (a :: BinP). Int -> PosP' n a -> ShowS #
(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 #
(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) => Bounded (PosP' n b) Source #
Instance details Defined in Data.BinP.PosP Methods minBound :: PosP' n b # maxBound :: 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 #
NFData (PosP' n b) Source #	Since: 0.1.2
Instance details Defined in Data.BinP.PosP Methods rnf :: 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 #

Top & Pop

top :: forall (b :: BinP). 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 :: forall (a :: BinP) (b :: BinP). (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => PosP a -> PosP b Source #

See top.

Showing

explicitShow :: forall (b :: BinP). PosP b -> String Source #

explicitShow' :: forall (n :: Nat) (b :: BinP). PosP' n b -> String Source #

explicitShowsPrec :: forall (b :: BinP). Int -> PosP b -> ShowS Source #

explicitShowsPrec' :: forall (n :: Nat) (b :: BinP). Int -> PosP' n b -> ShowS Source #

Conversions

toNatural :: forall (b :: BinP). PosP b -> Natural Source #

Convert PosP to Natural.

toNatural' :: forall (n :: Nat) (b :: BinP). 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 :: forall (b :: BinP). SBinPI b => PosP b -> PosP (Succ b) Source #

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

Universe

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

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

universe' :: forall (b :: BinP) (n :: Nat). (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]