{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# 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,
    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)

#if MIN_VERSION_some(1,0,5)
import Data.EqP          (EqP (..))
import Data.GADT.Compare (defaultEq)
#endif

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 = forall (b :: BinP). SBinPI b => SBinP ('B0 b)
SB0
instance SBinPI b => SBinPI ('B1 b)     where sbinp :: SBinP ('B1 b)
sbinp = 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 = SBinPI b => r
k
withSBinP SBinP b
SB0 SBinPI b => r
k = SBinPI b => r
k
withSBinP SBinP b
SB1 SBinPI b => r
k = 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 = forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy 'BE)
reify (B0 BinP
b) forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k = forall r.
BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
reify BinP
b (\(Proxy @BinP b
_ :: Proxy b) -> forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k (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 = forall r.
BinP -> (forall (b :: BinP). SBinPI b => Proxy @BinP b -> r) -> r
reify BinP
b (\(Proxy @BinP b
_ :: Proxy b) -> forall (b :: BinP). SBinPI b => Proxy @BinP b -> r
k (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
_ = forall a (b :: BinP). KP a b -> a
unKP (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 (forall a (b :: BinP). a -> KP a b
KP BinP
BE) (forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP BinP -> BinP
B0) (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
_ = forall a (b :: BinP). KP a b -> a
unKP (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 (forall a (b :: BinP). a -> KP a b
KP a
1) (forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (a
2forall a. Num a => a -> a -> a
*)) (forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (\a
x -> a
2 forall a. Num a => a -> a -> a
* a
x 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 = forall (b :: BinP) r. SBinP b -> (SBinPI b => r) -> r
withSBinP SBinP n
s forall a b. (a -> b) -> a -> b
$ forall (b :: BinP) (proxy :: BinP -> *).
SBinPI b =>
proxy b -> BinP
reflect (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 = forall (b :: BinP) r. SBinP b -> (SBinPI b => r) -> r
withSBinP SBinP n
s forall a b. (a -> b) -> a -> b
$ forall a (b :: BinP). KP a b -> a
unKP (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
    (forall a (b :: BinP). a -> KP a b
KP Natural
1)
    (forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (Natural
2 forall a. Num a => a -> a -> a
*))
    (forall a b (bn :: BinP) (bn' :: BinP).
(a -> b) -> KP a bn -> KP b bn'
mapKP (\Natural
x -> forall a. Enum a => a -> a
succ (Natural
2 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 (forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP a, forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b) of
    (SBinP a
SBE, SBinP b
SBE) -> forall a. a -> Maybe a
Just forall {k} (a :: k). (:~:) @k a a
Refl
    (SBinP a
SB0, SBinP b
SB0) -> 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 <- forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP :: Maybe (n :~: m)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). (:~:) @k a a
Refl
    (SBinP a
SB1, SBinP b
SB1) -> 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 <- forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP :: Maybe (n :~: m)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). (:~:) @k a a
Refl
    (SBinP a, SBinP 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 = forall a. a -> Maybe a
Just forall {k} (a :: k). (:~:) @k a a
Refl
    testEquality SBinP a
SB0 SBinP b
SB0 = forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP
    testEquality SBinP a
SB1 SBinP b
SB1 = forall (a :: BinP) (b :: BinP).
(SBinPI a, SBinPI b) =>
Maybe ((:~:) @BinP a b)
eqBinP

    testEquality SBinP a
_ SBinP 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

#if !MIN_VERSION_base(4,11,0)
type instance n == m = EqBinP n m
#endif

-------------------------------------------------------------------------------
-- 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 forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP b of
    SBinP b
SBE -> SBinPI (Succ b) => r
k
    SBinP b
SB0 -> SBinPI (Succ b) => r
k
    SBinP b
SB1 -> forall (m :: BinP) s.
SBinPI m =>
Proxy @BinP ('B1 m) -> (SBinPI ('B0 (Succ m)) => s) -> s
recur Proxy @BinP b
p 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' = forall (b :: BinP) r.
SBinPI b =>
Proxy @BinP b -> (SBinPI (Succ b) => r) -> r
withSucc (forall {k} (t :: k). Proxy @k t
Proxy :: Proxy m) SBinPI ('B0 (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 = 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 forall (b :: BinP). SBinPI b => SBinP b
sbinp :: SBinP bb of
        SBinP bb
SBE -> f 'BE
e
        SBinP bb
SB0 -> forall (bb :: BinP). SBinPI bb => f bb -> f ('B0 bb)
o forall (bb :: BinP). SBinPI bb => f bb
go
        SBinP bb
SB1 -> forall (bb :: BinP). SBinPI bb => f bb -> f ('B1 bb)
i forall (bb :: BinP). SBinPI bb => f bb
go

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

-- | @since 0.1.2
instance SBinPI b => Boring (SBinP b) where
    boring :: SBinP b
boring = 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

#if MIN_VERSION_some(1,0,5)
-- | @since 0.1.3
instance EqP SBinP where eqp :: forall (a :: BinP) (b :: BinP). SBinP a -> SBinP b -> Bool
eqp = forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq @k f =>
f a -> f b -> Bool
defaultEq
#endif

-- | @since 0.1.2
instance GShow SBinP where
    gshowsPrec :: forall (b :: BinP). Int -> SBinP b -> ShowS
gshowsPrec = 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 = 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 = forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality @k f =>
f a -> f b -> Maybe ((:~:) @k 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 = coerce :: 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 = coerce :: forall a b. Coercible @(*) a b => a -> b
coerce