module Data.Tuple.Ops.Internal where
import GHC.Generics ((:*:)(..), Rec0, D1, S1, Meta(..), SourceUnpackedness(..), SourceStrictness(..), DecidedStrictness(..))
import Data.Proxy
import Data.Type.Combinator
import Data.Type.Product
import Type.Family.List
import Type.Class.Witness
import qualified Type.Family.Nat as Nat
newtype TupleR (f :: [* -> *]) x = TupleR { unTupleR :: Tuple (f <&> x)}
class AppDistributive (a :: [* -> *]) where
appDistrWit :: (Proxy a, Proxy b, Proxy x) -> Wit (((a ++ b) <&> x) ~ ((a <&> x) ++ (b <&> x)))
instance AppDistributive '[] where
appDistrWit _ = Wit
instance AppDistributive as => AppDistributive (a :< as) where
appDistrWit (_ :: Proxy (a :< as), pb, px) =
case appDistrWit (Proxy :: Proxy as, pb, px) of
Wit -> Wit
appDistrWitPassArg :: (f :*: g) x -> (Proxy (L f), Proxy (L g), Proxy x)
appDistrWitPassArg _ = (Proxy, Proxy, Proxy)
class Linearize (t :: * -> *) where
type L t :: [* -> *]
linearize :: t x -> TupleR (L t) x
instance Linearize (S1 MetaS (Rec0 t)) where
type L (S1 MetaS (Rec0 t)) = '[S1 MetaS (Rec0 t)]
linearize = TupleR . only . I
instance (Linearize v, Linearize u, AppDistributive (L u)) => Linearize (u :*: v) where
type L (u :*: v) = L u ++ L v
linearize (a :*: b) =
case appDistrWit (appDistrWitPassArg (a :*: b)) of
Wit -> TupleR $ append' (unTupleR $ linearize a) (unTupleR $ linearize b)
length' :: TupleR a x -> Proxy (Nat.Len a)
length' _ = Proxy
type family Half (a :: Nat.N) :: Nat.N where
Half ('Nat.S 'Nat.Z) = 'Nat.Z
Half ('Nat.S ('Nat.S 'Nat.Z)) = 'Nat.S 'Nat.Z
Half ('Nat.S ('Nat.S n)) = 'Nat.S (Half n)
half :: Proxy n -> Proxy (Half n)
half _ = Proxy
class Take (n :: Nat.N) (a :: [* -> *]) where
type T n a :: [* -> *]
take' :: Proxy n -> TupleR a x -> TupleR (T n a) x
instance Take 'Nat.Z xs where
type T 'Nat.Z xs = '[]
take' _ _ = TupleR Ø
instance Take n as => Take ('Nat.S n) (a : as) where
type T ('Nat.S n) (a : as) = a : T n as
take' (_ :: Proxy ('Nat.S n)) (TupleR (a :< as) :: TupleR (a : as) x) =
let as' = unTupleR $ take' (Proxy :: Proxy n) (TupleR as :: TupleR as x)
in TupleR (a :< as')
class Drop (n :: Nat.N) (a :: [* -> *]) where
type D n a :: [* -> *]
drop' :: Proxy n -> TupleR a x -> TupleR (D n a) x
instance Drop 'Nat.Z as where
type D 'Nat.Z as = as
drop' _ a = a
instance Drop n as => Drop ('Nat.S n) (a : as) where
type D ('Nat.S n) (a : as) = D n as
drop' (_ :: Proxy ('Nat.S n)) (TupleR (a :< as) :: TupleR (a : as) x) =
drop' (Proxy :: Proxy n) (TupleR as :: TupleR as x)
class Normalize (a :: [* -> *]) where
type N a :: * -> *
normalize :: TupleR a x -> N a x
instance Normalize '[S1 MetaS (Rec0 t)] where
type N '[S1 MetaS (Rec0 t)] = S1 MetaS (Rec0 t)
normalize a = getI $ head' $ unTupleR a
instance (Take (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c),
Drop (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c),
Normalize (T (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)),
Normalize (D (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)))
=> Normalize (a :< b :< c) where
type N (a :< b :< c) = N (T (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c)) :*:
N (D (Half (Nat.N2 Nat.+ Nat.Len c)) (a :< b :< c))
normalize v = let n = half (length' v)
in normalize (take' n v) :*: normalize (drop' n v)
type MetaS = 'MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy
type family UnRec0 t where
UnRec0 (Rec0 t) = t
type family UnS1 t where
UnS1 (S1 _ t) = t
type family UnD1 t where
UnD1 (D1 _ t) = t
type family MetaOfD1 t where
MetaOfD1 (D1 m _) = m