bin-0.1.4: Bin: binary natural numbers.
Safe HaskellSafe
LanguageHaskell2010

Data.Bin.Pos

Synopsis

Documentation

data Pos (b :: Bin) where Source #

Pos is to Bin is what Fin is to Nat.

The name is picked, as the lack of better alternatives.

Constructors

Pos :: PosP b -> Pos ('BP b) 

Instances

Instances details
EqP Pos Source #
>>> eqp (top :: Pos Bin4) (top :: Pos Bin6)
True
>>> let xs = universe @Bin4; ys = universe @Bin6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]

Since: 0.1.3

Instance details

Defined in Data.Bin.Pos

Methods

eqp :: forall (a :: k) (b :: k). Pos a -> Pos b -> Bool #

GShow Pos Source #

Since: 0.1.3

Instance details

Defined in Data.Bin.Pos

Methods

gshowsPrec :: forall (a :: k). Int -> Pos a -> ShowS #

OrdP Pos Source #
>>> let xs = universe @Bin4; ys = universe @Bin6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]

Since: 0.1.3

Instance details

Defined in Data.Bin.Pos

Methods

comparep :: forall (a :: k) (b :: k). Pos a -> Pos b -> Ordering #

(SBinPI n, b ~ 'BP n) => Arbitrary (Pos b) Source # 
Instance details

Defined in Data.Bin.Pos

Methods

arbitrary :: Gen (Pos b) #

shrink :: Pos b -> [Pos b] #

CoArbitrary (Pos b) Source # 
Instance details

Defined in Data.Bin.Pos

Methods

coarbitrary :: Pos b -> Gen b0 -> Gen b0 #

(SBinPI n, b ~ 'BP n) => Function (Pos b) Source # 
Instance details

Defined in Data.Bin.Pos

Methods

function :: (Pos b -> b0) -> Pos b :-> b0 #

(SBinPI n, b ~ 'BP n) => Bounded (Pos b) Source #
>>> minBound < (maxBound :: Pos Bin5)
True
Instance details

Defined in Data.Bin.Pos

Methods

minBound :: Pos b #

maxBound :: Pos b #

Show (Pos b) Source # 
Instance details

Defined in Data.Bin.Pos

Methods

showsPrec :: Int -> Pos b -> ShowS #

show :: Pos b -> String #

showList :: [Pos b] -> ShowS #

b ~ 'BZ => Absurd (Pos b) Source #

Since: 0.1.2

Instance details

Defined in Data.Bin.Pos

Methods

absurd :: Pos b -> b0 #

b ~ 'BP 'BE => Boring (Pos b) Source #

Since: 0.1.2

Instance details

Defined in Data.Bin.Pos

Methods

boring :: Pos b #

NFData (Pos b) Source #

Since: 0.1.2

Instance details

Defined in Data.Bin.Pos

Methods

rnf :: Pos b -> () #

Eq (Pos b) Source # 
Instance details

Defined in Data.Bin.Pos

Methods

(==) :: Pos b -> Pos b -> Bool #

(/=) :: Pos b -> Pos b -> Bool #

Ord (Pos b) Source # 
Instance details

Defined in Data.Bin.Pos

Methods

compare :: Pos b -> Pos b -> Ordering #

(<) :: Pos b -> Pos b -> Bool #

(<=) :: Pos b -> Pos b -> Bool #

(>) :: Pos b -> Pos b -> Bool #

(>=) :: Pos b -> Pos b -> Bool #

max :: Pos b -> Pos b -> Pos b #

min :: Pos b -> Pos b -> Pos b #

data PosP (b :: BinP) Source #

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

Instances

Instances details
EqP PosP Source #

Since: 0.1.3

Instance details

Defined in Data.BinP.PosP

Methods

eqp :: forall (a :: k) (b :: k). PosP a -> PosP b -> Bool #

GShow PosP Source #

Since: 0.1.3

Instance details

Defined in Data.BinP.PosP

Methods

gshowsPrec :: forall (a :: k). Int -> PosP a -> ShowS #

OrdP PosP Source #

Since: 0.1.3

Instance details

Defined in Data.BinP.PosP

Methods

comparep :: forall (a :: k) (b :: k). 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 #

Top & Pop

top :: SBinPI b => Pos ('BP b) Source #

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

>>> top :: Pos Bin4
0
>>> pop (pop top) :: Pos Bin4
2
>>> pop (pop top) :: Pos Bin9
2

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

See top.

Showing

Conversions

toNatural :: Pos b -> Natural Source #

Convert Pos to Natural

>>> map toNatural (universe :: [Pos Bin7])
[0,1,2,3,4,5,6]

Interesting

absurd :: Pos 'BZ -> b Source #

Pos BZ is not inhabited.

boring :: Pos ('BP 'BE) Source #

Counting to one is boring

>>> boring
0

Weakening (succ)

weakenRight1 :: SBinPI b => Pos ('BP b) -> Pos (Succ'' b) Source #

Like FS for Fin.

Some tests:

>>> map weakenRight1 $ (universe :: [Pos Bin2])
[1,2]
>>> map weakenRight1 $ (universe :: [Pos Bin3])
[1,2,3]
>>> map weakenRight1 $ (universe :: [Pos Bin4])
[1,2,3,4]
>>> map weakenRight1 $ (universe :: [Pos Bin5])
[1,2,3,4,5]
>>> map weakenRight1 $ (universe :: [Pos Bin6])
[1,2,3,4,5,6]

Universe

universe :: forall b. SBinI b => [Pos b] Source #

Universe, i.e. all [Pos b]

>>> universe :: [Pos Bin9]
[0,1,2,3,4,5,6,7,8]
>>> traverse_ (putStrLn . explicitShow) (universe :: [Pos Bin5])
Pos (PosP (Here WE))
Pos (PosP (There1 (There0 (AtEnd 0b00))))
Pos (PosP (There1 (There0 (AtEnd 0b01))))
Pos (PosP (There1 (There0 (AtEnd 0b10))))
Pos (PosP (There1 (There0 (AtEnd 0b11))))