{-# 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
module Data.Type.BinP (
SBinP (..),
sbinpToBinP,
sbinpToNatural,
SBinPI (..),
withSBinP,
reify,
reflect,
reflectToNum,
eqBinP,
EqBinP,
induction,
Succ,
withSucc,
Plus,
ToGHC, FromGHC,
ToNat,
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
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)
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
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 :: 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 :: 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)
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)
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)
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)
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
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
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)
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))
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)
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))
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
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'
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
:: forall b f. SBinPI b
=> f 'BE
-> (forall bb. SBinPI bb => f bb -> f ('B0 bb))
-> (forall bb. SBinPI bb => f bb -> f ('B1 bb))
-> 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
instance SBinPI b => Boring (SBinP b) where
boring :: SBinP b
boring = forall (b :: BinP). SBinPI b => SBinP b
sbinp
instance Eq (SBinP a) where
SBinP a
_ == :: SBinP a -> SBinP a -> Bool
== SBinP a
_ = Bool
True
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)
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
instance GShow SBinP where
gshowsPrec :: forall (b :: BinP). Int -> SBinP b -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec
instance NFData (SBinP n) where
rnf :: SBinP n -> ()
rnf SBinP n
SBE = ()
rnf SBinP n
SB0 = ()
rnf SBinP n
SB1 = ()
instance GNFData SBinP where
grnf :: forall (n :: BinP). SBinP n -> ()
grnf = forall a. NFData a => a -> ()
rnf
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
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
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