{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Binary natural numbers. @DataKinds@ stuff.
module Data.Type.Bin (
    -- * Singleton
    SBin (..), SBinP (..),
    sbinToBin, BP.sbinpToBinP,
    sbinToNatural, BP.sbinpToNatural,
    -- * Implicit
    SBinI (..), SBinPI (..),
    withSBin, BP.withSBinP,
    reify,
    reflect,
    reflectToNum,
    -- * Type equality
    eqBin,
    -- * Induction
    induction,
    -- * Arithmetic
    -- ** Successor
    Succ, Succ', Succ'',
    withSucc,
    -- ** Predecessor
    Pred,
    -- ** Addition
    Plus,
    -- ** Extras
    Mult2, Mult2Plus1,
    -- * Conversions
    -- ** To GHC Nat
    ToGHC, FromGHC,
    -- ** To fin Nat
    ToNat, FromNat,
    -- * Aliases
    Bin0, Bin1, Bin2, Bin3, Bin4, Bin5, Bin6, Bin7, Bin8, Bin9,
    ) where

import Data.Bin           (Bin (..), BinP (..))
import Data.Nat           (Nat (..))
import Data.Proxy         (Proxy (..))
import Data.Type.Equality ((:~:) (..), TestEquality (..))
import Data.Typeable      (Typeable)
import Numeric.Natural    (Natural)
import Data.Type.BinP (SBinP (..), SBinPI (..))

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

-- $setup
-- >>> :set -XDataKinds
-- >>> import Data.Bin
-- >>> import Data.Type.BinP (BinP2, BinP3)

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

-- | Singleton of 'Bin'.
data SBin (b :: Bin) where
    SBZ :: SBin 'BZ
    SBP :: SBinPI b => SBin ('BP b)
  deriving (Typeable)

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

-- | Let constraint solver construct 'SBin'.
class                SBinI (b :: Bin) where sbin :: SBin b
instance             SBinI 'BZ        where sbin :: SBin 'BZ
sbin = SBin 'BZ
SBZ
instance SBinPI b => SBinI ('BP b )   where sbin :: SBin ('BP b)
sbin = SBin ('BP b)
forall (b :: BinP). SBinPI b => SBin ('BP b)
SBP

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

-- | Construct 'SBinI' dictionary from 'SBin'.
withSBin :: SBin b -> (SBinI b => r) -> r
withSBin :: SBin b -> (SBinI b => r) -> r
withSBin SBin b
SBZ SBinI b => r
k = r
SBinI b => r
k
withSBin SBin b
SBP SBinI b => r
k = r
SBinI b => r
k

-- | Reify 'Bin'
--
-- >>> reify bin3 reflect
-- 3
--
reify :: forall r. Bin -> (forall b. SBinI b => Proxy b -> r) -> r
reify :: Bin -> (forall (b :: Bin). SBinI b => Proxy @Bin b -> r) -> r
reify Bin
BZ     forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k = Proxy @Bin 'BZ -> r
forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k (Proxy @Bin 'BZ
forall k (t :: k). Proxy @k t
Proxy :: Proxy 'BZ)
reify (BP BinP
b) forall (b :: Bin). SBinI b => Proxy @Bin 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
BP.reify BinP
b (\(Proxy @BinP b
_ :: Proxy b) -> Proxy @Bin ('BP b) -> r
forall (b :: Bin). SBinI b => Proxy @Bin b -> r
k (Proxy @Bin ('BP b)
forall k (t :: k). Proxy @k t
Proxy :: Proxy ('BP b)))

-- | Reflect type-level 'Bin' to the term level.
reflect :: forall b proxy. SBinI b => proxy b -> Bin
reflect :: proxy b -> Bin
reflect proxy b
p = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> Bin
BZ
    SBin b
SBP -> BinP -> Bin
BP (proxy ('BP b) -> BinP
forall (bn :: BinP). SBinPI bn => proxy ('BP bn) -> BinP
aux proxy b
proxy ('BP b)
p)
  where
    aux :: forall bn. SBinPI bn => proxy ('BP bn) -> BinP
    aux :: proxy ('BP bn) -> BinP
aux proxy ('BP bn)
_ = Proxy @BinP bn -> BinP
forall (b :: BinP) (proxy :: BinP -> *).
SBinPI b =>
proxy b -> BinP
BP.reflect (Proxy @BinP bn
forall k (t :: k). Proxy @k t
Proxy :: Proxy bn)

-- | Reflect type-level 'Bin' to the term level 'Num'.
reflectToNum :: forall b proxy a. (SBinI b, Num a) => proxy b -> a
reflectToNum :: proxy b -> a
reflectToNum proxy b
p = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> a
0
    SBin b
SBP -> proxy ('BP b) -> a
forall (bn :: BinP). SBinPI bn => proxy ('BP bn) -> a
aux proxy b
proxy ('BP b)
p
  where
    aux :: forall bn. SBinPI bn => proxy ('BP bn) -> a
    aux :: proxy ('BP bn) -> a
aux proxy ('BP bn)
_ = Proxy @BinP bn -> a
forall (b :: BinP) (proxy :: BinP -> *) a.
(SBinPI b, Num a) =>
proxy b -> a
BP.reflectToNum (Proxy @BinP bn
forall k (t :: k). Proxy @k t
Proxy :: Proxy bn)

-- | Convert 'SBin' to 'Bin'.
sbinToBin :: forall n. SBin n -> Bin
sbinToBin :: SBin n -> Bin
sbinToBin SBin n
SBZ   = Bin
BZ
sbinToBin s :: SBin n
s@SBin n
SBP = SBin ('BP b) -> Bin
forall (m :: BinP). SBinPI m => SBin ('BP m) -> Bin
aux SBin n
SBin ('BP b)
s where
    aux :: forall m. SBinPI m => SBin ('BP m) -> Bin
    aux :: SBin ('BP m) -> Bin
aux SBin ('BP m)
_ = BinP -> Bin
BP (SBinP m -> BinP
forall (n :: BinP). SBinP n -> BinP
BP.sbinpToBinP (SBinP m
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP m))

-- | Convert 'SBin' to 'Natural'.
--
-- >>> sbinToNatural (sbin :: SBin Bin9)
-- 9
--
sbinToNatural :: forall n. SBin n -> Natural
sbinToNatural :: SBin n -> Natural
sbinToNatural SBin n
SBZ = Natural
0
sbinToNatural s :: SBin n
s@SBin n
SBP = SBin ('BP b) -> Natural
forall (m :: BinP). SBinPI m => SBin ('BP m) -> Natural
aux SBin n
SBin ('BP b)
s where
    aux :: forall m. SBinPI m => SBin ('BP m) -> Natural
    aux :: SBin ('BP m) -> Natural
aux SBin ('BP m)
_ = SBinP m -> Natural
forall (n :: BinP). SBinP n -> Natural
BP.sbinpToNatural (SBinP m
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP m)

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

eqBin :: forall a b. (SBinI a, SBinI b) => Maybe (a :~: b)
eqBin :: Maybe ((:~:) @Bin a b)
eqBin = case (SBin a
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin a, SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b) of
    (SBin a
SBZ, SBin b
SBZ) -> (:~:) @Bin a a -> Maybe ((:~:) @Bin a a)
forall a. a -> Maybe a
Just (:~:) @Bin a a
forall k (a :: k). (:~:) @k a a
Refl
    (SBin a
SBP, SBin b
SBP) -> Maybe ((:~:) @Bin a b)
forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @Bin ('BP n) ('BP m))
recur where
      recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('BP n :~: 'BP m)
      recur :: Maybe ((:~:) @Bin ('BP n) ('BP m))
recur = do
          (:~:) @BinP n m
Refl <- Maybe ((:~:) @BinP n m)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
BP.eqBinP :: Maybe (n :~: m)
          (:~:) @Bin ('BP n) ('BP n) -> Maybe ((:~:) @Bin ('BP n) ('BP n))
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Bin ('BP n) ('BP n)
forall k (a :: k). (:~:) @k a a
Refl

    (SBin a, SBin b)
_          -> Maybe ((:~:) @Bin a b)
forall a. Maybe a
Nothing

instance TestEquality SBin where
    testEquality :: SBin a -> SBin b -> Maybe ((:~:) @Bin a b)
testEquality SBin a
SBZ SBin b
SBZ = (:~:) @Bin a a -> Maybe ((:~:) @Bin a a)
forall a. a -> Maybe a
Just (:~:) @Bin a a
forall k (a :: k). (:~:) @k a a
Refl
    testEquality SBin a
SBP SBin b
SBP = Maybe ((:~:) @Bin a b)
forall (n :: BinP) (m :: BinP).
(SBinPI n, SBinPI m) =>
Maybe ((:~:) @Bin ('BP n) ('BP m))
recur where
        recur :: forall n m. (SBinPI n, SBinPI m) => Maybe ('BP n :~: 'BP m)
        recur :: Maybe ((:~:) @Bin ('BP n) ('BP m))
recur = do
            (:~:) @BinP n m
Refl <- Maybe ((:~:) @BinP n m)
forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
BP.eqBinP :: Maybe (n :~: m)
            (:~:) @Bin ('BP n) ('BP n) -> Maybe ((:~:) @Bin ('BP n) ('BP n))
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Bin ('BP n) ('BP n)
forall k (a :: k). (:~:) @k a a
Refl
    testEquality SBin a
_   SBin b
_   = Maybe ((:~:) @Bin a b)
forall a. Maybe a
Nothing

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

-- | Induction on 'Bin'.
induction
    :: forall b f. SBinI b
    => f 'BZ                                                     -- ^ \(P(0)\)
    -> f ('BP 'BE)                                               -- ^ \(P(1)\)
    -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb)))  -- ^ \(\forall b. P(b) \to P(2b)\)
    -> (forall bb. SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb)))  -- ^ \(\forall b. P(b) \to P(2b + 1)\)
    -> f b
induction :: f 'BZ
-> f ('BP 'BE)
-> (forall (bb :: BinP).
    SBinPI bb =>
    f ('BP bb) -> f ('BP ('B0 bb)))
-> (forall (bb :: BinP).
    SBinPI bb =>
    f ('BP bb) -> f ('BP ('B1 bb)))
-> f b
induction f 'BZ
z f ('BP 'BE)
e forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb))
o forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb))
i = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> f b
f 'BZ
z
    SBin b
SBP -> f b
forall (bb :: BinP). SBinPI bb => f ('BP bb)
go
  where
    go :: forall bb. SBinPI bb => f ('BP bb)
    go :: f ('BP bb)
go = case SBinP bb
forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP bb of
        SBinP bb
SBE -> f ('BP bb)
f ('BP 'BE)
e
        SBinP bb
SB0 -> f ('BP b) -> f ('BP ('B0 b))
forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B0 bb))
o f ('BP b)
forall (bb :: BinP). SBinPI bb => f ('BP bb)
go
        SBinP bb
SB1 -> f ('BP b) -> f ('BP ('B1 b))
forall (bb :: BinP). SBinPI bb => f ('BP bb) -> f ('BP ('B1 bb))
i f ('BP b)
forall (bb :: BinP). SBinPI bb => f ('BP bb)
go

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

-- | Convert to GHC 'GHC.Nat'.
--
-- >>> :kind! ToGHC Bin5
-- ToGHC Bin5 :: GHC.Nat
-- = 5
--
type family ToGHC (b :: Bin) :: GHC.Nat where
    ToGHC 'BZ     = 0
    ToGHC ('BP n) = BP.ToGHC n

-- | Convert from GHC 'GHC.Nat'.
--
-- >>> :kind! FromGHC 7
-- FromGHC 7 :: Bin
-- = 'BP ('B1 ('B1 'BE))
--
type family FromGHC (n :: GHC.Nat) :: Bin where
    FromGHC n = FromGHC' (GhcDivMod2 n)

type family FromGHC' (p :: (GHC.Nat, Bool)) :: Bin where
    FromGHC' '(0, 'False) = 'BZ
    FromGHC' '(0, 'True)  = 'BP 'BE
    FromGHC' '(n, 'False) = Mult2 (FromGHC n)
    FromGHC' '(n, 'True)  = 'BP (Mult2Plus1 (FromGHC 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)

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

-- | Convert to @fin@ 'Nat'.
--
-- >>> :kind! ToNat Bin5
-- ToNat Bin5 :: Nat
-- = 'S ('S ('S ('S ('S 'Z))))
--
type family ToNat (b :: Bin) :: Nat where
    ToNat 'BZ     = 'Z
    ToNat ('BP n) = BP.ToNat n

-- | Convert from @fin@ 'Nat'.
--
-- >>> :kind! FromNat N.Nat5
-- FromNat N.Nat5 :: Bin
-- = 'BP ('B1 ('B0 'BE))
--
type family FromNat (n :: Nat) :: Bin where
    FromNat n = FromNat' (N.DivMod2 n)

type family FromNat' (p :: (Nat, Bool)) :: Bin where
    FromNat' '( 'Z, 'False) = 'BZ
    FromNat' '( 'Z, 'True)  = 'BP 'BE
    FromNat' '( n,  'False) = Mult2 (FromNat n)
    FromNat' '( n,  'True)  = 'BP (Mult2Plus1 (FromNat n))

-------------------------------------------------------------------------------
-- Extras
-------------------------------------------------------------------------------

-- | Multiply by two.
--
-- >>> :kind! Mult2 Bin0
-- Mult2 Bin0 :: Bin
-- = 'BZ
--
-- >>> :kind! Mult2 Bin7
-- Mult2 Bin7 :: Bin
-- = 'BP ('B0 ('B1 BinP3))
type family Mult2 (b :: Bin) :: Bin where
    Mult2 'BZ     = 'BZ
    Mult2 ('BP n) = 'BP ('B0 n)

-- | Multiply by two and add one.
--
-- >>> :kind! Mult2Plus1 Bin0
-- Mult2Plus1 Bin0 :: BinP
-- = 'BE
--
-- >>> :kind! Mult2Plus1 Bin5
-- Mult2Plus1 Bin5 :: BinP
-- = 'B1 ('B1 BinP2)
type family Mult2Plus1 (b :: Bin) :: BinP where
    Mult2Plus1 'BZ     = 'BE
    Mult2Plus1 ('BP n) = ('B1 n)

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

-- | 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 where
    Succ' 'BZ     = 'BE
    Succ' ('BP b) = BP.Succ b

type Succ'' b = 'BP (BP.Succ b)

withSucc :: forall b r. SBinI b => Proxy b -> (SBinPI (Succ' b) => r) -> r
withSucc :: Proxy @Bin b -> (SBinPI (Succ' b) => r) -> r
withSucc Proxy @Bin b
p SBinPI (Succ' b) => r
k = case SBin b
forall (b :: Bin). SBinI b => SBin b
sbin :: SBin b of
    SBin b
SBZ -> r
SBinPI (Succ' b) => r
k
    SBin b
SBP -> Proxy @Bin ('BP b) -> (SBinPI (Succ b) => r) -> r
forall (b :: BinP) r.
SBinPI b =>
Proxy @Bin ('BP b) -> (SBinPI (Succ b) => r) -> r
withSucc' Proxy @Bin b
Proxy @Bin ('BP b)
p SBinPI (Succ b) => r
SBinPI (Succ' b) => r
k

withSucc' :: forall b r. SBinPI b => Proxy ('BP b) -> (SBinPI (BP.Succ b) => r) -> r
withSucc' :: Proxy @Bin ('BP b) -> (SBinPI (Succ b) => r) -> r
withSucc' Proxy @Bin ('BP b)
_ SBinPI (Succ b) => r
k = Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
BP.withSucc (Proxy @BinP b
forall k (t :: k). Proxy @k t
Proxy :: Proxy b) SBinPI (Succ b) => r
k

-------------------------------------------------------------------------------
-- Predecessor
-------------------------------------------------------------------------------

-- | Predecessor type family..
--
-- >>> :kind! Pred BP.BinP1
-- Pred BP.BinP1 :: Bin
-- = 'BZ
--
-- >>> :kind! Pred BP.BinP5
-- Pred BP.BinP5 :: Bin
-- = 'BP ('B0 ('B0 BP.BinP1))
--
-- >>> :kind! Pred BP.BinP8
-- Pred BP.BinP8 :: Bin
-- = 'BP ('B1 ('B1 'BE))
--
-- >>> :kind! Pred BP.BinP6
-- Pred BP.BinP6 :: Bin
-- = 'BP ('B1 ('B0 'BE))
--
type family Pred (b :: BinP) :: Bin where
    Pred 'BE     = 'BZ
    Pred ('B1 n) = 'BP ('B0 n)
    Pred ('B0 n) = 'BP (Pred' n)

type family Pred' (b :: BinP) :: BinP where
    Pred' 'BE     = 'BE
    Pred' ('B1 m) = 'B1 ('B0 m)
    Pred' ('B0 m) = 'B1 (Pred' m)

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

-- | Addition.
--
-- >>> :kind! Plus Bin7 Bin7
-- Plus Bin7 Bin7 :: Bin
-- = 'BP ('B0 ('B1 ('B1 'BE)))
--
-- >>> :kind! Mult2 Bin7
-- Mult2 Bin7 :: Bin
-- = 'BP ('B0 ('B1 BinP3))
--
type family Plus (a :: Bin) (b :: Bin) :: Bin where
    Plus 'BZ     b       = b
    Plus a       'BZ     = a
    Plus ('BP a) ('BP b) = 'BP (BP.Plus a b)

-------------------------------------------------------------------------------
--- Aliases of Bin
-------------------------------------------------------------------------------

type Bin0 = 'BZ
type Bin1 = 'BP BP.BinP1
type Bin2 = 'BP BP.BinP2
type Bin3 = 'BP BP.BinP3
type Bin4 = 'BP BP.BinP4
type Bin5 = 'BP BP.BinP5
type Bin6 = 'BP BP.BinP6
type Bin7 = 'BP BP.BinP7
type Bin8 = 'BP BP.BinP8
type Bin9 = 'BP BP.BinP9