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

Data.Type.BinP

Description

Positive binary natural numbers. DataKinds stuff.

Synopsis

Singleton

data SBinP (b :: BinP) where Source #

Singleton of BinP.

Constructors

SBE :: SBinP 'BE 
SB0 :: SBinPI b => SBinP ('B0 b) 
SB1 :: SBinPI b => SBinP ('B1 b) 

Instances

Instances details
TestEquality SBinP Source # 
Instance details

Defined in Data.Type.BinP

Methods

testEquality :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Maybe (a :~: b) #

EqP SBinP Source #

Since: 0.1.3

Instance details

Defined in Data.Type.BinP

Methods

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

GNFData SBinP Source #

Since: 0.1.2

Instance details

Defined in Data.Type.BinP

Methods

grnf :: forall (a :: k). SBinP a -> () #

GEq SBinP Source #

Since: 0.1.2

Instance details

Defined in Data.Type.BinP

Methods

geq :: forall (a :: k) (b :: k). SBinP a -> SBinP b -> Maybe (a :~: b) #

GShow SBinP Source #

Since: 0.1.2

Instance details

Defined in Data.Type.BinP

Methods

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

Show (SBinP b) Source # 
Instance details

Defined in Data.Type.BinP

Methods

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

show :: SBinP b -> String #

showList :: [SBinP b] -> ShowS #

SBinPI b => Boring (SBinP b) Source #

Since: 0.1.2

Instance details

Defined in Data.Type.BinP

Methods

boring :: SBinP b #

NFData (SBinP n) Source #

Since: 0.1.2

Instance details

Defined in Data.Type.BinP

Methods

rnf :: SBinP n -> () #

Eq (SBinP a) Source #

Since: 0.1.3

Instance details

Defined in Data.Type.BinP

Methods

(==) :: SBinP a -> SBinP a -> Bool #

(/=) :: SBinP a -> SBinP a -> Bool #

Ord (SBinP a) Source #

Since: 0.1.3

Instance details

Defined in Data.Type.BinP

Methods

compare :: SBinP a -> SBinP a -> Ordering #

(<) :: SBinP a -> SBinP a -> Bool #

(<=) :: SBinP a -> SBinP a -> Bool #

(>) :: SBinP a -> SBinP a -> Bool #

(>=) :: SBinP a -> SBinP a -> Bool #

max :: SBinP a -> SBinP a -> SBinP a #

min :: SBinP a -> SBinP a -> SBinP a #

sbinpToBinP :: forall n. SBinP n -> BinP Source #

Cconvert SBinP to BinP.

sbinpToNatural :: forall n. SBinP n -> Natural Source #

Convert SBinP to Natural.

>>> sbinpToNatural (sbinp :: SBinP BinP8)
8

Implicit

class SBinPI (b :: BinP) where Source #

Let constraint solver construct SBinP.

Methods

sbinp :: SBinP b Source #

Instances

Instances details
SBinPI 'BE Source # 
Instance details

Defined in Data.Type.BinP

Methods

sbinp :: SBinP 'BE Source #

SBinPI b => SBinPI ('B0 b) Source # 
Instance details

Defined in Data.Type.BinP

Methods

sbinp :: SBinP ('B0 b) Source #

SBinPI b => SBinPI ('B1 b) Source # 
Instance details

Defined in Data.Type.BinP

Methods

sbinp :: SBinP ('B1 b) Source #

withSBinP :: SBinP b -> (SBinPI b => r) -> r Source #

Construct SBinPI dictionary from SBinP.

reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r Source #

Reify BinP.

reflect :: forall b proxy. SBinPI b => proxy b -> BinP Source #

Reflect type-level BinP to the term level.

reflectToNum :: forall b proxy a. (SBinPI b, Num a) => proxy b -> a Source #

Reflect type-level BinP to the term level Num.

Type equality

eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b) Source #

type family EqBinP (n :: BinP) (m :: BinP) where ... Source #

Since: 0.1.2

Equations

EqBinP 'BE 'BE = 'True 
EqBinP ('B0 n) ('B0 m) = EqBinP n m 
EqBinP ('B1 n) ('B1 m) = EqBinP n m 
EqBinP n m = 'False 

Induction

induction Source #

Arguments

:: forall b f. SBinPI b 
=> f 'BE

\(P(1)\)

-> (forall bb. SBinPI bb => f bb -> f ('B0 bb))

\(\forall b. P(b) \to P(2b)\)

-> (forall bb. SBinPI bb => f bb -> f ('B1 bb))

\(\forall b. P(b) \to P(2b + 1)\)

-> f b 

Induction on BinP.

Arithmetic

Successor

type family Succ (b :: BinP) :: BinP where ... Source #

Equations

Succ 'BE = 'B0 'BE 
Succ ('B0 n) = 'B1 n 
Succ ('B1 n) = 'B0 (Succ n) 

withSucc :: forall b r. SBinPI b => Proxy b -> (SBinPI (Succ b) => r) -> r Source #

Addition

type family Plus (a :: BinP) (b :: BinP) :: BinP where ... Source #

Equations

Plus 'BE b = Succ b 
Plus a 'BE = Succ a 
Plus ('B0 a) ('B0 b) = 'B0 (Plus a b) 
Plus ('B1 a) ('B0 b) = 'B1 (Plus a b) 
Plus ('B0 a) ('B1 b) = 'B1 (Plus a b) 
Plus ('B1 a) ('B1 b) = 'B0 (Succ (Plus a b)) 

Conversions

To GHC Nat

type family ToGHC (b :: BinP) :: Nat where ... Source #

Equations

ToGHC 'BE = 1 
ToGHC ('B0 b) = 2 * ToGHC b 
ToGHC ('B1 b) = 1 + (2 * ToGHC b) 

type family FromGHC (n :: Nat) :: BinP where ... Source #

Equations

FromGHC n = FromGHC' (FromGHCMaybe n) 

To fin Nat

type family ToNat (b :: BinP) :: Nat where ... Source #

Equations

ToNat 'BE = 'S 'Z 
ToNat ('B0 b) = Mult2 (ToNat b) 
ToNat ('B1 b) = 'S (Mult2 (ToNat b)) 

Aliases

type BinP1 = 'BE Source #