{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Safe                 #-}
-- | Positive binary natural numbers. @DataKinds@ stuff.
module Data.Type.BinP (
    -- * Singleton
    SBinP (..),
    sbinpToBinP,
    sbinpToNatural,
    -- * Implicit
    SBinPI (..),
    withSBinP,
    reify,
    reflect,
    reflectToNum,
    -- * Type equality
    eqBinP,
    EqBinP,
    -- * Induction
    induction,
    -- * Arithmetic
    -- ** Successor
    Succ,
    withSucc,
    -- ** Addition
    Plus,
    -- * Conversions
    -- ** To GHC Nat
    ToGHC, FromGHC,
    -- ** To fin Nat
    ToNat,
    -- * Aliases
    BinP1, BinP2, BinP3, BinP4, BinP5, BinP6, BinP7, BinP8, BinP9,
    ) where

import Control.DeepSeq   (NFData (..))
import Data.BinP         (BinP (..))
import Data.Boring       (Boring (..))
import Data.GADT.Compare (GEq (..))
import Data.GADT.DeepSeq (GNFData (..))
import Data.GADT.Show    (GShow (..))
import Data.Nat          (Nat (..))
import Data.Proxy        (Proxy (..))
import Data.Typeable     (Typeable)
import Numeric.Natural   (Natural)
import Data.EqP          (EqP (..))
import Data.GADT.Compare (defaultEq)

import qualified Data.Type.Nat as N
import qualified GHC.TypeLits  as GHC

import TrustworthyCompat

-- $setup
-- >>> :set -XDataKinds
-- >>> import Data.Bin

-------------------------------------------------------------------------------
-- Singletons
-------------------------------------------------------------------------------

-- | Singleton of 'BinP'.
data SBinP (b :: BinP) where
    SBE :: SBinP 'BE
    SB0 :: SBinPI b => SBinP ('B0 b)
    SB1 :: SBinPI b => SBinP ('B1 b)
  deriving (Typeable)

deriving instance Show (SBinP b)

-------------------------------------------------------------------------------
-- Implicits
-------------------------------------------------------------------------------

-- | Let constraint solver construct 'SBinP'.
class                SBinPI (b :: BinP) where sbinp :: SBinP b
instance             SBinPI 'BE         where sbinp :: SBinP 'BE
sbinp = SBinP 'BE
SBE
instance SBinPI b => SBinPI ('B0 b)     where sbinp :: SBinP ('B0 b)
sbinp = SBinP ('B0 b)
forall (b :: BinP). SBinPI b => SBinP ('B0 b)
SB0
instance SBinPI b => SBinPI ('B1 b)     where sbinp :: SBinP ('B1 b)
sbinp = SBinP ('B1 b)
forall (b :: BinP). SBinPI b => SBinP ('B1 b)
SB1

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Construct 'SBinPI' dictionary from 'SBinP'.
withSBinP :: SBinP b -> (SBinPI b => r) -> r
withSBinP :: forall (b :: BinP) r. SBinP b -> (SBinPI b => r) -> r
withSBinP SBinP b
SBE SBinPI b => r
k = r
SBinPI b => r
k
withSBinP SBinP b
SB0 SBinPI b => r
k = r
SBinPI b => r
k
withSBinP SBinP b
SB1 SBinPI b => r
k = r
SBinPI b => r
k

-- | Reify 'BinP'.
reify :: forall r. BinP -> (forall b. SBinPI b => Proxy b -> r) -> r
reify :: forall r.
BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
reify BinP
BE     forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k = Proxy @BinP 'BE -> r
forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k (Proxy @BinP 'BE
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy 'BE)
reify (B0 BinP
b) forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k = BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
forall r.
BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
reify BinP
b (\(Proxy @BinP b
_ :: Proxy b) -> Proxy @BinP ('B0 b) -> r
forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k (Proxy @BinP ('B0 b)
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy ('B0 b)))
reify (B1 BinP
b) forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k = BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
forall r.
BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
reify BinP
b (\(Proxy @BinP b
_ :: Proxy b) -> Proxy @BinP ('B1 b) -> r
forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k (Proxy @BinP ('B1 b)
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy ('B1 b)))

-- | Reflect type-level 'BinP' to the term level.
reflect :: forall b proxy. SBinPI b => proxy b -> BinP
reflect :: forall (b :: BinP) (proxy :: BinP -> *).
SBinPI b =>
proxy b -> BinP
reflect proxy b
_ = KP BinP b -> BinP
forall a (b :: BinP). KP a b -> a
unKP (KP BinP 'BE
-> (forall (bb :: BinP).
    SBinPI bb =>
    KP BinP bb -> KP BinP ('B0 bb))
-> (forall (bb :: BinP).
    SBinPI bb =>
    KP BinP bb -> KP BinP ('B1 bb))
-> KP BinP b
forall (b :: BinP) (f :: BinP -> *).
SBinPI b =>
f 'BE
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb))
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb))
-> f b
induction (BinP -> KP BinP 'BE
forall a (b :: BinP). a -> KP a b
KP BinP
BE) ((BinP -> BinP) -> KP BinP bb -> KP BinP ('B0 bb)
forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP BinP -> BinP
B0) ((BinP -> BinP) -> KP BinP bb -> KP BinP ('B1 bb)
forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP BinP -> BinP
B1) :: KP BinP b)

-- | Reflect type-level 'BinP' to the term level 'Num'.
reflectToNum :: forall b proxy a. (SBinPI b, Num a) => proxy b -> a
reflectToNum :: forall (b :: BinP) (proxy :: BinP -> *) a.
(SBinPI b, Num a) =>
proxy b -> a
reflectToNum proxy b
_ = KP a b -> a
forall a (b :: BinP). KP a b -> a
unKP (KP a 'BE
-> (forall (bb :: BinP). SBinPI bb => KP a bb -> KP a ('B0 bb))
-> (forall (bb :: BinP). SBinPI bb => KP a bb -> KP a ('B1 bb))
-> KP a b
forall (b :: BinP) (f :: BinP -> *).
SBinPI b =>
f 'BE
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb))
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb))
-> f b
induction (a -> KP a 'BE
forall a (b :: BinP). a -> KP a b
KP a
1) ((a -> a) -> KP a bb -> KP a ('B0 bb)
forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (a
2a -> a -> a
forall a. Num a => a -> a -> a
*)) ((a -> a) -> KP a bb -> KP a ('B1 bb)
forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (\a
x -> a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
x a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)) :: KP a b)

-- | Cconvert 'SBinP' to 'BinP'.
sbinpToBinP :: forall n. SBinP n -> BinP
sbinpToBinP :: forall (n :: BinP). SBinP n -> BinP
sbinpToBinP SBinP n
s = SBinP n -> (SBinPI n => BinP) -> BinP
forall (b :: BinP) r. SBinP b -> (SBinPI b => r) -> r
withSBinP SBinP n
s ((SBinPI n => BinP) -> BinP) -> (SBinPI n => BinP) -> BinP
forall a b. (a -> b) -> a -> b
$ Proxy @BinP n -> BinP
forall (b :: BinP) (proxy :: BinP -> *).
SBinPI b =>
proxy b -> BinP
reflect (Proxy @BinP n
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy n)

-- | Convert 'SBinP' to 'Natural'.
--
-- >>> sbinpToNatural (sbinp :: SBinP BinP8)
-- 8
--
sbinpToNatural :: forall n. SBinP n -> Natural
sbinpToNatural :: forall (n :: BinP). SBinP n -> Natural
sbinpToNatural SBinP n
s = SBinP n -> (SBinPI n => Natural) -> Natural
forall (b :: BinP) r. SBinP b -> (SBinPI b => r) -> r
withSBinP SBinP n
s ((SBinPI n => Natural) -> Natural)
-> (SBinPI n => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ KP Natural n -> Natural
forall a (b :: BinP). KP a b -> a
unKP (KP Natural 'BE
-> (forall (bb :: BinP).
    SBinPI bb =>
    KP Natural bb -> KP Natural ('B0 bb))
-> (forall (bb :: BinP).
    SBinPI bb =>
    KP Natural bb -> KP Natural ('B1 bb))
-> KP Natural n
forall (b :: BinP) (f :: BinP -> *).
SBinPI b =>
f 'BE
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb))
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb))
-> f b
induction
    (Natural -> KP Natural 'BE
forall a (b :: BinP). a -> KP a b
KP Natural
1)
    ((Natural -> Natural) -> KP Natural bb -> KP Natural ('B0 bb)
forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
*))
    ((Natural -> Natural) -> KP Natural bb -> KP Natural ('B1 bb)
forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (\Natural
x -> Natural -> Natural
forall a. Enum a => a -> a
succ (Natural
2 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
x))) :: KP Natural n)

-------------------------------------------------------------------------------
-- Equality
-------------------------------------------------------------------------------

eqBinP :: forall a b. (SBinPI a, SBinPI b) => Maybe (a :~: b)
eqBinP :: forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP = case (SBinP a
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP a, SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b) of
    (SBinP a
SBE, SBinP b
SBE) -> (:~:) @BinP a b -> Maybe ((:~:) @BinP a b)
forall a. a -> Maybe a
Just (:~:) @BinP a a
(:~:) @BinP a b
forall {k} (a :: k). (:~:) @k a a
Refl
    (SBinP a
SB0, SBinP b
SB0) -> Maybe ((:~:) @BinP a b)
Maybe ((:~:) @BinP ('B0 b) ('B0 b))
forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @BinP ('B0 n) ('B0 m))
recur where
        recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('B0 n :~: 'B0 m)
        recur :: forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @BinP ('B0 n) ('B0 m))
recur = do
            (:~:) @BinP n m
Refl <- Maybe ((:~:) @BinP n m)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP :: Maybe (n :~: m)
            (:~:) @BinP ('B0 n) ('B0 m) -> Maybe ((:~:) @BinP ('B0 n) ('B0 m))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @BinP ('B0 n) ('B0 n)
(:~:) @BinP ('B0 n) ('B0 m)
forall {k} (a :: k). (:~:) @k a a
Refl
    (SBinP a
SB1, SBinP b
SB1) -> Maybe ((:~:) @BinP a b)
Maybe ((:~:) @BinP ('B1 b) ('B1 b))
forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @BinP ('B1 n) ('B1 m))
recur where
        recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('B1 n :~: 'B1 m)
        recur :: forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @BinP ('B1 n) ('B1 m))
recur = do
            (:~:) @BinP n m
Refl <- Maybe ((:~:) @BinP n m)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP :: Maybe (n :~: m)
            (:~:) @BinP ('B1 n) ('B1 m) -> Maybe ((:~:) @BinP ('B1 n) ('B1 m))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @BinP ('B1 n) ('B1 n)
(:~:) @BinP ('B1 n) ('B1 m)
forall {k} (a :: k). (:~:) @k a a
Refl
    (SBinP a, SBinP b)
_ -> Maybe ((:~:) @BinP a b)
forall a. Maybe a
Nothing

instance TestEquality SBinP where
    testEquality :: forall (a :: BinP) (b :: BinP).
SBinP a -> SBinP b -> Maybe ((:~:) @BinP a b)
testEquality SBinP a
SBE SBinP b
SBE = (:~:) @BinP a b -> Maybe ((:~:) @BinP a b)
forall a. a -> Maybe a
Just (:~:) @BinP a a
(:~:) @BinP a b
forall {k} (a :: k). (:~:) @k a a
Refl
    testEquality SBinP a
SB0 SBinP b
SB0 = Maybe ((:~:) @BinP a b)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP
    testEquality SBinP a
SB1 SBinP b
SB1 = Maybe ((:~:) @BinP a b)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP

    testEquality SBinP a
_ SBinP b
_ = Maybe ((:~:) @BinP a b)
forall a. Maybe a
Nothing

-- | @since 0.1.2
type family EqBinP (n :: BinP) (m :: BinP) where
    EqBinP 'BE 'BE         = 'True
    EqBinP ('B0 n) ('B0 m) = EqBinP n m
    EqBinP ('B1 n) ('B1 m) = EqBinP n m
    EqBinP n       m       = 'False

-------------------------------------------------------------------------------
-- Convert to GHC Nat
-------------------------------------------------------------------------------

type family ToGHC (b :: BinP) :: GHC.Nat where
    ToGHC 'BE = 1
    ToGHC ('B0 b) = 2 GHC.* (ToGHC b)
    ToGHC ('B1 b) = 1 GHC.+ 2 GHC.* (ToGHC b)

type family FromGHC (n :: GHC.Nat) :: BinP where
    FromGHC n = FromGHC' (FromGHCMaybe n)

-- internals

type family FromGHC' (b :: Maybe BinP) :: BinP where
    FromGHC' ('Just b) = b

type family FromGHCMaybe (n :: GHC.Nat) :: Maybe BinP where
    FromGHCMaybe n = FromGHCMaybe' (GhcDivMod2 n)

type family FromGHCMaybe' (p :: (GHC.Nat, Bool)) :: Maybe BinP where
    FromGHCMaybe' '(0, 'False) = 'Nothing
    FromGHCMaybe' '(0, 'True)  = 'Just 'BE
    FromGHCMaybe' '(n, 'False) = Mult2 (FromGHCMaybe n)
    FromGHCMaybe' '(n, 'True)  = 'Just (Mult2Plus1 (FromGHCMaybe n))

-- | >>> :kind! GhcDivMod2 13
-- GhcDivMod2 13 :: (GHC.Nat, Bool)
-- = '(6, 'True)
--
type family GhcDivMod2 (n :: GHC.Nat) :: (GHC.Nat, Bool) where
    GhcDivMod2 0 = '(0, 'False)
    GhcDivMod2 1 = '(0, 'True)
    GhcDivMod2 n = GhcDivMod2' (GhcDivMod2 (n GHC.- 2))

type family GhcDivMod2' (p :: (GHC.Nat, Bool)) :: (GHC.Nat, Bool) where
    GhcDivMod2' '(n, b) = '(1 GHC.+ n, b)

type family Mult2 (b :: Maybe BinP) :: Maybe BinP where
    Mult2 'Nothing  = 'Nothing
    Mult2 ('Just n) = 'Just ('B0 n)

type family Mult2Plus1 (b :: Maybe BinP) :: BinP where
    Mult2Plus1 'Nothing  = 'BE
    Mult2Plus1 ('Just n) = ('B1 n)

-------------------------------------------------------------------------------
-- Conversion to Nat
-------------------------------------------------------------------------------

type family ToNat (b :: BinP) :: Nat where
    ToNat 'BE     = 'S 'Z
    ToNat ('B0 b) = N.Mult2 (ToNat b)
    ToNat ('B1 b) = 'S (N.Mult2 (ToNat b))

-------------------------------------------------------------------------------
-- Arithmetic: Succ
-------------------------------------------------------------------------------

type family Succ (b :: BinP) :: BinP where
    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
withSucc :: forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
withSucc Proxy @BinP b
p SBinPI (Succ b) => r
k = case SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
    SBinP b
SBE -> r
SBinPI (Succ b) => r
k
    SBinP b
SB0 -> r
SBinPI (Succ b) => r
k
    SBinP b
SB1 -> Proxy @BinP ('B1 b) -> (SBinPI ('B0 (Succ b)) => r) -> r
forall (m :: BinP) s.
SBinPI m =>
Proxy @BinP ('B1 m) -> (SBinPI ('B0 (Succ m)) => s) -> s
recur Proxy @BinP b
Proxy @BinP ('B1 b)
p r
SBinPI ('B0 (Succ b)) => r
SBinPI (Succ b) => r
k
  where
    -- eta needed for older GHC
    recur :: forall m s. SBinPI m => Proxy ('B1 m) -> (SBinPI ('B0 (Succ m)) => s) -> s
    recur :: forall (m :: BinP) s.
SBinPI m =>
Proxy @BinP ('B1 m) -> (SBinPI ('B0 (Succ m)) => s) -> s
recur Proxy @BinP ('B1 m)
_ SBinPI ('B0 (Succ m)) => s
k' = Proxy @BinP m -> (SBinPI (Succ m) => s) -> s
forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
withSucc (Proxy @BinP m
forall {k} (t :: k). Proxy @k t
Proxy :: Proxy m) s
SBinPI ('B0 (Succ m)) => s
SBinPI (Succ m) => s
k'

-------------------------------------------------------------------------------
-- Arithmetic: Plus
-------------------------------------------------------------------------------

type family Plus (a :: BinP) (b :: BinP) :: BinP where
    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))

-------------------------------------------------------------------------------
-- Induction
-------------------------------------------------------------------------------

-- | Induction on 'BinP'.
induction
    :: 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 :: forall (b :: BinP) (f :: BinP -> *).
SBinPI b =>
f 'BE
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb))
-> (forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb))
-> f b
induction f 'BE
e forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb)
o forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb)
i = f b
forall (bb :: BinP). SBinPI bb => f bb
go where
    go :: forall bb. SBinPI bb => f bb
    go :: forall (bb :: BinP). SBinPI bb => f bb
go = case SBinP bb
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP bb of
        SBinP bb
SBE -> f bb
f 'BE
e
        SBinP bb
SB0 -> f b -> f ('B0 b)
forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb)
o f b
forall (bb :: BinP). SBinPI bb => f bb
go
        SBinP bb
SB1 -> f b -> f ('B1 b)
forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb)
i f b
forall (bb :: BinP). SBinPI bb => f bb
go

-------------------------------------------------------------------------------
-- Boring
-------------------------------------------------------------------------------

-- | @since 0.1.2
instance SBinPI b => Boring (SBinP b) where
    boring :: SBinP b
boring = SBinP b
forall (b :: BinP). SBinPI b => SBinP b
sbinp

-------------------------------------------------------------------------------
-- some
-------------------------------------------------------------------------------

-- | @since 0.1.3
instance Eq (SBinP a) where
    SBinP a
_ == :: SBinP a -> SBinP a -> Bool
== SBinP a
_ = Bool
True

-- | @since 0.1.3
instance Ord (SBinP a) where
    compare :: SBinP a -> SBinP a -> Ordering
compare SBinP a
_ SBinP a
_ = Ordering
EQ

-- | @since 0.1.3
instance EqP SBinP where eqp :: forall (a :: BinP) (b :: BinP). SBinP a -> SBinP b -> Bool
eqp = SBinP a -> SBinP b -> Bool
forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq @k f =>
f a -> f b -> Bool
defaultEq

-- | @since 0.1.2
instance GShow SBinP where
    gshowsPrec :: forall (b :: BinP). Int -> SBinP b -> ShowS
gshowsPrec = Int -> SBinP a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec

-- | @since 0.1.2
instance NFData (SBinP n) where
    rnf :: SBinP n -> ()
rnf SBinP n
SBE = ()
    rnf SBinP n
SB0 = ()
    rnf SBinP n
SB1 = ()

-- | @since 0.1.2
instance GNFData SBinP where
    grnf :: forall (n :: BinP). SBinP n -> ()
grnf = SBinP a -> ()
forall a. NFData a => a -> ()
rnf

-- | @since 0.1.2
instance GEq SBinP where
    geq :: forall (a :: BinP) (b :: BinP).
SBinP a -> SBinP b -> Maybe ((:~:) @BinP a b)
geq = SBinP a -> SBinP b -> Maybe ((:~:) @BinP a b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality @k f =>
f a -> f b -> Maybe ((:~:) @k a b)
forall (a :: BinP) (b :: BinP).
SBinP a -> SBinP b -> Maybe ((:~:) @BinP a b)
testEquality

-------------------------------------------------------------------------------
-- Aliases of BinP
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Aux
-------------------------------------------------------------------------------

newtype KP a (b :: BinP) = KP a

unKP :: KP a b -> a
unKP :: forall a (b :: BinP). KP a b -> a
unKP = KP a b -> a
forall a b. Coercible @(*) a b => a -> b
coerce

mapKP :: (a -> b) -> KP a bn -> KP b bn'
mapKP :: forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP = (a -> b) -> KP a bn -> KP b bn'
forall a b. Coercible @(*) a b => a -> b
coerce