{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
#if MIN_VERSION_base(4,8,0)
{-# LANGUAGE Safe                 #-}
#else
{-# LANGUAGE Trustworthy          #-}
#endif
-- | Positive binary natural numbers. @DataKinds@ stuff.
module Data.Type.BinP (
    -- * Singleton
    SBinP (..),
    sbinpToBinP,
    sbinpToNatural,
    -- * Implicit
    SBinPI (..),
    withSBinP,
    reify,
    reflect,
    reflectToNum,
    -- * Type equality
    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 Data.BinP       (BinP (..))
import Data.Nat        (Nat (..))
import Data.Proxy      (Proxy (..))
import Data.Typeable   (Typeable)
import Numeric.Natural (Natural)

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)

-------------------------------------------------------------------------------
-- 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 a -> Maybe ((:~:) @BinP a a)
forall a. a -> Maybe a
Just (:~:) @BinP a a
forall k (a :: k). (:~:) @k a a
Refl
    (SBinP a
SB0, SBinP b
SB0) -> Maybe ((:~:) @BinP a 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 :: 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 n) -> Maybe ((:~:) @BinP ('B0 n) ('B0 n))
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @BinP ('B0 n) ('B0 n)
forall k (a :: k). (:~:) @k a a
Refl
    (SBinP a
SB1, SBinP b
SB1) -> Maybe ((:~:) @BinP a 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 :: 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 n) -> Maybe ((:~:) @BinP ('B1 n) ('B1 n))
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @BinP ('B1 n) ('B1 n)
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 :: SBinP a -> SBinP b -> Maybe ((:~:) @BinP a b)
testEquality SBinP a
SBE SBinP b
SBE = (:~:) @BinP a a -> Maybe ((:~:) @BinP a a)
forall a. a -> Maybe a
Just (:~:) @BinP a a
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

-------------------------------------------------------------------------------
-- 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 :: 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 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 :: 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) 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 :: 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 :: 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

-------------------------------------------------------------------------------
-- 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 :: KP a b -> a
unKP = KP a b -> a
coerce

mapKP :: (a -> b) -> KP a bn -> KP b bn'
mapKP :: (a -> b) -> KP a bn -> KP b bn'
mapKP = (a -> b) -> KP a bn -> KP b bn'
coerce