-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Bin: binary natural numbers.
--
-- This package provides binary natural numbers (Data.Bin);
-- also utilities to work on the type level with DataKinds
-- (Data.Type.Bin).
--
--
-- data Bin
-- = BZ -- ^ zero
-- | BP BinP -- ^ non-zero
--
-- data BinP
-- = BE -- ^ one
-- | B0 BinP -- ^ double
-- | B1 BinP -- ^ double plus 1
--
--
-- There are ordinals in Data.Bin.Pos module, as well as
-- fixed width integers in Data.Wrd.
--
-- Another implementation is at
-- https://hackage.haskell.org/package/nat, this differs in
-- naming, and provides promoted variant.
@package bin
@version 0.1.2
-- | Positive binary natural numbers, BinP.
--
-- This module is designed to be imported qualified.
module Data.BinP
-- | Non-zero binary natural numbers.
--
-- We could have called this type Bin1, but that's used as type
-- alias for promoted BP BE in
-- Data.Type.Bin.
data BinP
-- | one
BE :: BinP
-- | mult2
B0 :: BinP -> BinP
-- | mult2 plus 1
B1 :: BinP -> BinP
-- | Fold BinP.
cata :: a -> (a -> a) -> (a -> a) -> BinP -> a
-- | toNatural for BinP.
toNatural :: BinP -> Natural
-- | fromNatural for BinP.
--
-- Throws when given 0.
fromNatural :: Natural -> BinP
-- | Convert from BinP to Nat.
toNat :: BinP -> Nat
-- | show displaying a structure of BinP.
--
--
-- >>> explicitShow 11
-- "B1 (B1 (B0 BE))"
--
explicitShow :: BinP -> String
-- | showsPrec displaying a structure of BinP.
explicitShowsPrec :: Int -> BinP -> ShowS
predMaybe :: BinP -> Maybe BinP
binP1 :: BinP
binP2 :: BinP
binP3 :: BinP
binP4 :: BinP
binP5 :: BinP
binP6 :: BinP
binP7 :: BinP
binP8 :: BinP
binP9 :: BinP
instance Data.Data.Data Data.BinP.BinP
instance GHC.Classes.Eq Data.BinP.BinP
instance GHC.Classes.Ord Data.BinP.BinP
instance GHC.Show.Show Data.BinP.BinP
instance GHC.Num.Num Data.BinP.BinP
instance GHC.Real.Real Data.BinP.BinP
instance GHC.Real.Integral Data.BinP.BinP
instance GHC.Enum.Enum Data.BinP.BinP
instance Control.DeepSeq.NFData Data.BinP.BinP
instance Data.Hashable.Class.Hashable Data.BinP.BinP
instance Data.Bits.Bits Data.BinP.BinP
instance Test.QuickCheck.Arbitrary.Arbitrary Data.BinP.BinP
instance Test.QuickCheck.Arbitrary.CoArbitrary Data.BinP.BinP
instance Test.QuickCheck.Function.Function Data.BinP.BinP
-- | Binary natural numbers, Bin.
--
-- This module is designed to be imported qualified.
module Data.Bin
-- | Binary natural numbers.
--
-- Numbers are represented in little-endian order, the representation is
-- unique.
--
--
-- >>> mapM_ (putStrLn . explicitShow) [0 .. 7]
-- BZ
-- BP BE
-- BP (B0 BE)
-- BP (B1 BE)
-- BP (B0 (B0 BE))
-- BP (B1 (B0 BE))
-- BP (B0 (B1 BE))
-- BP (B1 (B1 BE))
--
data Bin
-- | zero
BZ :: Bin
-- | non-zero
BP :: BinP -> Bin
-- | Convert Bin to Natural
--
--
-- >>> toNatural 0
-- 0
--
--
--
-- >>> toNatural 2
-- 2
--
--
--
-- >>> toNatural $ BP $ B0 $ B1 $ BE
-- 6
--
toNatural :: Bin -> Natural
-- | Convert Natural to Nat
--
--
-- >>> fromNatural 4
-- 4
--
--
--
-- >>> explicitShow (fromNatural 4)
-- "BP (B0 (B0 BE))"
--
fromNatural :: Natural -> Bin
-- | Convert from Bin to Nat.
--
--
-- >>> toNat 5
-- 5
--
--
--
-- >>> N.explicitShow (toNat 5)
-- "S (S (S (S (S Z))))"
--
toNat :: Bin -> Nat
-- | Convert from Nat to Bin.
--
--
-- >>> fromNat 5
-- 5
--
--
--
-- >>> explicitShow (fromNat 5)
-- "BP (B1 (B0 BE))"
--
fromNat :: Nat -> Bin
-- | Fold Bin.
cata :: a -> a -> (a -> a) -> (a -> a) -> Bin -> a
-- | Non-zero binary natural numbers.
--
-- We could have called this type Bin1, but that's used as type
-- alias for promoted BP BE in
-- Data.Type.Bin.
data BinP
-- | one
BE :: BinP
-- | mult2
B0 :: BinP -> BinP
-- | mult2 plus 1
B1 :: BinP -> BinP
-- | show displaying a structure of Bin.
--
--
-- >>> explicitShow 0
-- "BZ"
--
--
--
-- >>> explicitShow 2
-- "BP (B0 BE)"
--
explicitShow :: Bin -> String
-- | showsPrec displaying a structure of Bin.
explicitShowsPrec :: Int -> Bin -> ShowS
-- | This is a total function.
--
--
-- >>> map predP [1..10]
-- [0,1,2,3,4,5,6,7,8,9]
--
predP :: BinP -> Bin
mult2 :: Bin -> Bin
mult2Plus1 :: Bin -> BinP
andP :: BinP -> BinP -> Bin
xorP :: BinP -> BinP -> Bin
complementBitP :: BinP -> Int -> Bin
clearBitP :: BinP -> Int -> Bin
bin0 :: Bin
bin1 :: Bin
bin2 :: Bin
bin3 :: Bin
bin4 :: Bin
bin5 :: Bin
bin6 :: Bin
bin7 :: Bin
bin8 :: Bin
bin9 :: Bin
instance Data.Data.Data Data.Bin.Bin
instance GHC.Classes.Ord Data.Bin.Bin
instance GHC.Classes.Eq Data.Bin.Bin
instance GHC.Show.Show Data.Bin.Bin
instance GHC.Num.Num Data.Bin.Bin
instance GHC.Real.Real Data.Bin.Bin
instance GHC.Real.Integral Data.Bin.Bin
instance GHC.Enum.Enum Data.Bin.Bin
instance Control.DeepSeq.NFData Data.Bin.Bin
instance Data.Hashable.Class.Hashable Data.Bin.Bin
instance Test.QuickCheck.Arbitrary.Arbitrary Data.Bin.Bin
instance Test.QuickCheck.Arbitrary.CoArbitrary Data.Bin.Bin
instance Test.QuickCheck.Function.Function Data.Bin.Bin
instance Data.Bits.Bits Data.Bin.Bin
-- | Fixed-Wrdth (unsigned) integers.
module Data.Wrd
-- | Fixed-width unsigned integers, Wrds for short.
--
-- The number is thought to be stored in big-endian format, i.e.
-- most-significant bit first. (as in binary literals).
data Wrd (n :: Nat)
[WE] :: Wrd 'Z
[W0] :: Wrd n -> Wrd ('S n)
[W1] :: Wrd n -> Wrd ('S n)
-- | show displaying a structure of Wrd n
--
--
-- >>> explicitShow WE
-- "WE"
--
--
--
-- >>> explicitShow $ W0 WE
-- "W0 WE"
--
--
--
-- >>> explicitShow $ W1 $ W0 $ W1 $ W0 WE
-- "W1 $ W0 $ W1 $ W0 WE"
--
explicitShow :: Wrd n -> String
-- | showsPrec displaying a structure of Wrd n.
--
--
-- >>> explicitShowsPrec 0 (W0 WE) ""
-- "W0 WE"
--
--
--
-- >>> explicitShowsPrec 1 (W0 WE) ""
-- "(W0 WE)"
--
explicitShowsPrec :: Int -> Wrd n -> ShowS
-- | Convert to Natural number
--
--
-- >>> let u = W0 $ W1 $ W1 $ W1 $ W0 $ W1 $ W0 WE
--
-- >>> u
-- 0b0111010
--
--
--
-- >>> toNatural u
-- 58
--
--
--
-- >>> map toNatural (universe :: [Wrd N.Nat3])
-- [0,1,2,3,4,5,6,7]
--
toNatural :: Wrd n -> Natural
-- | All values, i.e. universe of Wrd .
--
--
-- >>> universe :: [Wrd 'Z]
-- [WE]
--
--
--
-- >>> universe :: [Wrd N.Nat3]
-- [0b000,0b001,0b010,0b011,0b100,0b101,0b110,0b111]
--
universe :: forall n. SNatI n => [Wrd n]
xor :: Wrd n -> Wrd n -> Wrd n
(.&.) :: Wrd n -> Wrd n -> Wrd n
(.|.) :: Wrd n -> Wrd n -> Wrd n
complement :: Wrd n -> Wrd n
-- |
-- complement2 w = complement w + 1
--
complement2 :: Wrd n -> Wrd n
shiftR :: Wrd n -> Int -> Wrd n
shiftL :: Wrd n -> Int -> Wrd n
rotateL :: Wrd n -> Int -> Wrd n
rotateR :: Wrd n -> Int -> Wrd n
popCount :: Wrd n -> Int
setBit :: Wrd n -> Int -> Wrd n
clearBit :: Wrd n -> Int -> Wrd n
complementBit :: Wrd n -> Int -> Wrd n
testBit :: Wrd n -> Int -> Bool
shiftL1 :: Wrd n -> Wrd n
shiftR1 :: Wrd n -> Wrd n
rotateL1 :: Wrd n -> Wrd n
rotateR1 :: Wrd n -> Wrd n
instance GHC.Classes.Eq (Data.Wrd.Wrd n)
instance GHC.Classes.Ord (Data.Wrd.Wrd n)
instance GHC.Show.Show (Data.Wrd.Wrd n)
instance Control.DeepSeq.NFData (Data.Wrd.Wrd n)
instance Data.Hashable.Class.Hashable (Data.Wrd.Wrd n)
instance Data.Type.Nat.SNatI n => GHC.Enum.Bounded (Data.Wrd.Wrd n)
instance Data.Type.Nat.SNatI n => GHC.Num.Num (Data.Wrd.Wrd n)
instance Data.Type.Nat.SNatI n => Data.Bits.Bits (Data.Wrd.Wrd n)
instance Data.Type.Nat.SNatI n => Data.Bits.FiniteBits (Data.Wrd.Wrd n)
instance Data.Type.Nat.SNatI n => Test.QuickCheck.Arbitrary.Arbitrary (Data.Wrd.Wrd n)
instance Test.QuickCheck.Arbitrary.CoArbitrary (Data.Wrd.Wrd n)
instance Data.Type.Nat.SNatI n => Test.QuickCheck.Function.Function (Data.Wrd.Wrd n)
-- | Positive binary natural numbers. DataKinds stuff.
module Data.Type.BinP
-- | Singleton of BinP.
data SBinP (b :: BinP)
[SBE] :: SBinP 'BE
[SB0] :: SBinPI b => SBinP ('B0 b)
[SB1] :: SBinPI b => SBinP ('B1 b)
-- | Cconvert SBinP to BinP.
sbinpToBinP :: forall n. SBinP n -> BinP
-- | Convert SBinP to Natural.
--
--
-- >>> sbinpToNatural (sbinp :: SBinP BinP8)
-- 8
--
sbinpToNatural :: forall n. SBinP n -> Natural
-- | Let constraint solver construct SBinP.
class SBinPI (b :: BinP)
sbinp :: SBinPI b => SBinP b
-- | Construct SBinPI dictionary from SBinP.
withSBinP :: SBinP b -> (SBinPI b => r) -> r
-- | Reify BinP.
reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r
-- | Reflect type-level BinP to the term level.
reflect :: forall b proxy. SBinPI b => proxy b -> BinP
-- | Reflect type-level BinP to the term level Num.
reflectToNum :: forall b proxy a. (SBinPI b, Num a) => proxy b -> a
eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b)
type family EqBinP (n :: BinP) (m :: BinP)
-- | Induction on BinP.
induction :: forall b f. SBinPI b => f 'BE -> (forall bb. SBinPI bb => f bb -> f ('B0 bb)) -> (forall bb. SBinPI bb => f bb -> f ('B1 bb)) -> f b
type family Succ (b :: BinP) :: BinP
withSucc :: forall b r. SBinPI b => Proxy b -> (SBinPI (Succ b) => r) -> r
type family Plus (a :: BinP) (b :: BinP) :: BinP
type family ToGHC (b :: BinP) :: Nat
type family FromGHC (n :: Nat) :: BinP
type family ToNat (b :: BinP) :: Nat
type BinP1 = 'BE
type BinP2 = 'B0 BinP1
type BinP3 = 'B1 BinP1
type BinP4 = 'B0 BinP2
type BinP5 = 'B1 BinP2
type BinP6 = 'B0 BinP3
type BinP7 = 'B1 BinP3
type BinP8 = 'B0 BinP4
type BinP9 = 'B1 BinP4
instance GHC.Show.Show (Data.Type.BinP.SBinP b)
instance Data.Type.BinP.SBinPI 'Data.BinP.BE
instance Data.Type.BinP.SBinPI b => Data.Type.BinP.SBinPI ('Data.BinP.B0 b)
instance Data.Type.BinP.SBinPI b => Data.Type.BinP.SBinPI ('Data.BinP.B1 b)
instance Data.Type.Equality.TestEquality @{Data.BinP.BinP} Data.Type.BinP.SBinP
instance Data.Type.BinP.SBinPI b => Data.Boring.Boring (Data.Type.BinP.SBinP b)
instance Data.GADT.Internal.GShow @Data.BinP.BinP Data.Type.BinP.SBinP
instance Control.DeepSeq.NFData (Data.Type.BinP.SBinP n)
instance Data.GADT.DeepSeq.GNFData @Data.BinP.BinP Data.Type.BinP.SBinP
instance Data.GADT.Internal.GEq @Data.BinP.BinP Data.Type.BinP.SBinP
-- | Binary natural numbers. DataKinds stuff.
module Data.Type.Bin
-- | Singleton of Bin.
data SBin (b :: Bin)
[SBZ] :: SBin 'BZ
[SBP] :: SBinPI b => SBin ('BP b)
-- | Singleton of BinP.
data SBinP (b :: BinP)
[SBE] :: SBinP 'BE
[SB0] :: SBinPI b => SBinP ('B0 b)
[SB1] :: SBinPI b => SBinP ('B1 b)
-- | Convert SBin to Bin.
sbinToBin :: forall n. SBin n -> Bin
-- | Cconvert SBinP to BinP.
sbinpToBinP :: forall n. SBinP n -> BinP
-- | Convert SBin to Natural.
--
--
-- >>> sbinToNatural (sbin :: SBin Bin9)
-- 9
--
sbinToNatural :: forall n. SBin n -> Natural
-- | Convert SBinP to Natural.
--
--
-- >>> sbinpToNatural (sbinp :: SBinP BinP8)
-- 8
--
sbinpToNatural :: forall n. SBinP n -> Natural
-- | Let constraint solver construct SBin.
class SBinI (b :: Bin)
sbin :: SBinI b => SBin b
-- | Let constraint solver construct SBinP.
class SBinPI (b :: BinP)
sbinp :: SBinPI b => SBinP b
-- | Construct SBinI dictionary from SBin.
withSBin :: SBin b -> (SBinI b => r) -> r
-- | Construct SBinPI dictionary from SBinP.
withSBinP :: SBinP b -> (SBinPI b => r) -> r
-- | Reify Bin
--
--
-- >>> reify bin3 reflect
-- 3
--
reify :: forall r. Bin -> (forall b. SBinI b => Proxy b -> r) -> r
-- | Reflect type-level Bin to the term level.
reflect :: forall b proxy. SBinI b => proxy b -> Bin
-- | Reflect type-level Bin to the term level Num.
reflectToNum :: forall b proxy a. (SBinI b, Num a) => proxy b -> a
eqBin :: forall a b. (SBinI a, SBinI b) => Maybe (a :~: b)
type family EqBin (n :: Bin) (m :: Bin)
-- | Induction on Bin.
induction :: forall b f. SBinI b => f 'BZ -> f ('BP 'BE) -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb))) -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb))) -> f b
-- | Successor type family.
--
--
-- >>> :kind! Succ Bin5
-- Succ Bin5 :: Bin
-- = 'BP ('B0 ('B1 'BE))
--
--
--
-- Succ :: Bin -> Bin
-- Succ` :: Bin -> BinP
-- Succ'` :: BinP -> Bin
--
type Succ b = 'BP (Succ' b)
type family Succ' (b :: Bin) :: BinP
type Succ'' b = 'BP (Succ b)
withSucc :: forall b r. SBinI b => Proxy b -> (SBinPI (Succ' b) => r) -> r
-- | Predecessor type family..
--
--
-- >>> :kind! Pred BP.BinP1
-- Pred BP.BinP1 :: Bin
-- = 'BZ
--
--
--
-- >>> :kind! Pred BP.BinP5 == Bin4
-- Pred BP.BinP5 == Bin4 :: Bool
-- = 'True
--
--
--
-- >>> :kind! Pred BP.BinP8 == Bin7
-- Pred BP.BinP8 == Bin7 :: Bool
-- = 'True
--
--
--
-- >>> :kind! Pred BP.BinP6 == Bin5
-- Pred BP.BinP6 == Bin5 :: Bool
-- = 'True
--
type family Pred (b :: BinP) :: Bin
-- | Addition.
--
--
-- >>> :kind! Plus Bin3 Bin3 == Bin6
-- Plus Bin3 Bin3 == Bin6 :: Bool
-- = 'True
--
--
--
-- >>> :kind! Mult2 Bin3 == Bin6
-- Mult2 Bin3 == Bin6 :: Bool
-- = 'True
--
type family Plus (a :: Bin) (b :: Bin) :: Bin
-- | Multiply by two.
--
--
-- >>> :kind! Mult2 Bin0 == Bin0
-- Mult2 Bin0 == Bin0 :: Bool
-- = 'True
--
--
--
-- >>> :kind! Mult2 Bin3 == Bin6
-- Mult2 Bin3 == Bin6 :: Bool
-- = 'True
--
type family Mult2 (b :: Bin) :: Bin
-- | Multiply by two and add one.
--
--
-- >>> :kind! Mult2Plus1 Bin0
-- Mult2Plus1 Bin0 :: BinP
-- = 'BE
--
--
--
-- >>> :kind! Mult2Plus1 Bin4 == BinP9
-- Mult2Plus1 Bin4 == BinP9 :: Bool
-- = 'True
--
type family Mult2Plus1 (b :: Bin) :: BinP
-- | Convert to GHC Nat.
--
--
-- >>> :kind! ToGHC Bin5
-- ToGHC Bin5 :: GHC.Nat...
-- = 5
--
type family ToGHC (b :: Bin) :: Nat
-- | Convert from GHC Nat.
--
--
-- >>> :kind! FromGHC 7
-- FromGHC 7 :: Bin
-- = 'BP ('B1 ('B1 'BE))
--
type family FromGHC (n :: Nat) :: Bin
-- | Convert to fin Nat.
--
--
-- >>> :kind! ToNat Bin5
-- ToNat Bin5 :: Nat
-- = 'S ('S ('S ('S ('S 'Z))))
--
type family ToNat (b :: Bin) :: Nat
-- | Convert from fin Nat.
--
--
-- >>> :kind! FromNat N.Nat5
-- FromNat N.Nat5 :: Bin
-- = 'BP ('B1 ('B0 'BE))
--
type family FromNat (n :: Nat) :: Bin
type Bin0 = 'BZ
type Bin1 = 'BP BinP1
type Bin2 = 'BP BinP2
type Bin3 = 'BP BinP3
type Bin4 = 'BP BinP4
type Bin5 = 'BP BinP5
type Bin6 = 'BP BinP6
type Bin7 = 'BP BinP7
type Bin8 = 'BP BinP8
type Bin9 = 'BP BinP9
instance GHC.Show.Show (Data.Type.Bin.SBin b)
instance Data.Type.Bin.SBinI 'Data.Bin.BZ
instance Data.Type.BinP.SBinPI b => Data.Type.Bin.SBinI ('Data.Bin.BP b)
instance Data.Type.Bin.SBinI b => Data.Boring.Boring (Data.Type.Bin.SBin b)
instance Data.Type.Equality.TestEquality @{Data.Bin.Bin} Data.Type.Bin.SBin
instance Data.GADT.Internal.GShow @Data.Bin.Bin Data.Type.Bin.SBin
instance Control.DeepSeq.NFData (Data.Type.Bin.SBin n)
instance Data.GADT.DeepSeq.GNFData @Data.Bin.Bin Data.Type.Bin.SBin
instance Data.GADT.Internal.GEq @Data.Bin.Bin Data.Type.Bin.SBin
module Data.BinP.PosP
-- | PosP is to BinP is what Fin is to Nat,
-- when n is Z.
newtype PosP (b :: BinP)
PosP :: PosP' 'Z b -> PosP (b :: BinP)
[unPosP] :: PosP (b :: BinP) -> PosP' 'Z b
-- | PosP' is a structure inside PosP.
data PosP' (n :: Nat) (b :: BinP)
[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 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
--
top :: SBinPI b => PosP b
-- | See top.
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
-- | Convert PosP to Natural.
toNatural :: PosP b -> Natural
-- | Convert PosP' to Natural.
toNatural' :: forall n b. SNatI n => PosP' n b -> Natural
-- | Counting to one is boring
--
--
-- >>> boring
-- 0
--
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 :: [PosP BinP9]
-- [0,1,2,3,4,5,6,7,8]
--
universe :: forall b. SBinPI b => [PosP b]
-- | This gives a hint, what the n parameter means in
-- PosP'.
--
--
-- >>> universe' :: [PosP' N.Nat2 BinP2]
-- [0,1,2,3,4,5,6,7]
--
universe' :: forall b n. (SNatI n, SBinPI b) => [PosP' n b]
instance GHC.Classes.Ord (Data.BinP.PosP.PosP b)
instance GHC.Classes.Eq (Data.BinP.PosP.PosP b)
instance GHC.Classes.Eq (Data.BinP.PosP.PosP' n b)
instance (Data.Type.Nat.SNatI n, Data.Type.BinP.SBinPI b) => Test.QuickCheck.Arbitrary.Arbitrary (Data.BinP.PosP.PosP' n b)
instance GHC.Show.Show (Data.BinP.PosP.PosP b)
instance Data.Type.BinP.SBinPI b => GHC.Enum.Bounded (Data.BinP.PosP.PosP b)
instance Control.DeepSeq.NFData (Data.BinP.PosP.PosP b)
instance Data.Type.BinP.SBinPI b => Test.QuickCheck.Arbitrary.Arbitrary (Data.BinP.PosP.PosP b)
instance Test.QuickCheck.Arbitrary.CoArbitrary (Data.BinP.PosP.PosP b)
instance Data.Type.BinP.SBinPI b => Test.QuickCheck.Function.Function (Data.BinP.PosP.PosP b)
instance ((b :: Data.BinP.BinP) GHC.Types.~ ('Data.BinP.BE :: Data.BinP.BinP)) => Data.Boring.Boring (Data.BinP.PosP.PosP b)
instance GHC.Classes.Ord (Data.BinP.PosP.PosP' n b)
instance Data.Type.Nat.SNatI n => GHC.Show.Show (Data.BinP.PosP.PosP' n b)
instance (Data.Type.Nat.SNatI n, Data.Type.BinP.SBinPI b) => GHC.Enum.Bounded (Data.BinP.PosP.PosP' n b)
instance Control.DeepSeq.NFData (Data.BinP.PosP.PosP' n b)
instance Data.Type.Nat.SNatI n => Test.QuickCheck.Arbitrary.CoArbitrary (Data.BinP.PosP.PosP' n b)
instance (Data.Type.Nat.SNatI n, Data.Type.BinP.SBinPI b) => Test.QuickCheck.Function.Function (Data.BinP.PosP.PosP' n b)
module Data.Bin.Pos
-- | Pos is to Bin is what Fin is to Nat.
--
-- The name is picked, as the lack of better alternatives.
data Pos (b :: Bin)
[Pos] :: PosP b -> Pos ('BP b)
-- | PosP is to BinP is what Fin is to Nat,
-- when n is Z.
data PosP (b :: BinP)
-- | 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
--
top :: SBinPI b => Pos ('BP b)
-- | See top.
pop :: (SBinPI a, Pred b ~ 'BP a, Succ a ~ b) => Pos ('BP a) -> Pos ('BP b)
explicitShow :: Pos b -> String
explicitShowsPrec :: Int -> Pos b -> ShowS
-- | Convert Pos to Natural
--
--
-- >>> map toNatural (universe :: [Pos Bin7])
-- [0,1,2,3,4,5,6]
--
toNatural :: Pos b -> Natural
-- | Pos BZ is not inhabited.
absurd :: Pos 'BZ -> b
-- | Counting to one is boring
--
--
-- >>> boring
-- 0
--
boring :: Pos ('BP 'BE)
-- | 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]
--
weakenRight1 :: SBinPI b => Pos ('BP b) -> Pos (Succ'' b)
-- | 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))))
--
universe :: forall b. SBinI b => [Pos b]
instance GHC.Classes.Eq (Data.Bin.Pos.Pos b)
instance GHC.Classes.Ord (Data.Bin.Pos.Pos b)
instance GHC.Show.Show (Data.Bin.Pos.Pos b)
instance (Data.Type.BinP.SBinPI n, (b :: Data.Bin.Bin) GHC.Types.~ ('Data.Bin.BP n :: Data.Bin.Bin)) => GHC.Enum.Bounded (Data.Bin.Pos.Pos b)
instance Control.DeepSeq.NFData (Data.Bin.Pos.Pos b)
instance (Data.Type.BinP.SBinPI n, (b :: Data.Bin.Bin) GHC.Types.~ ('Data.Bin.BP n :: Data.Bin.Bin)) => Test.QuickCheck.Arbitrary.Arbitrary (Data.Bin.Pos.Pos b)
instance Test.QuickCheck.Arbitrary.CoArbitrary (Data.Bin.Pos.Pos b)
instance (Data.Type.BinP.SBinPI n, (b :: Data.Bin.Bin) GHC.Types.~ ('Data.Bin.BP n :: Data.Bin.Bin)) => Test.QuickCheck.Function.Function (Data.Bin.Pos.Pos b)
instance ((b :: Data.Bin.Bin) GHC.Types.~ ('Data.Bin.BP 'Data.BinP.BE :: Data.Bin.Bin)) => Data.Boring.Boring (Data.Bin.Pos.Pos b)
instance ((b :: Data.Bin.Bin) GHC.Types.~ ('Data.Bin.BZ :: Data.Bin.Bin)) => Data.Boring.Absurd (Data.Bin.Pos.Pos b)