{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Data.ZipMatchK.Mappings where

import           Data.Kind              (Type)
import           Generics.Kind

-- | Zip to lists of types into a single list of pair types.
type ZipLoT :: LoT k -> LoT k -> LoT k
type family ZipLoT as bs where
  ZipLoT LoT0 LoT0 = LoT0
  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)

infixr 5 :^:
type Mappings :: LoT k -> LoT k -> LoT k -> Type
-- | A collection of zipping functions for 'Data.ZipMatchK.zipMatchWithK'.
data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
  -- | An empty collection (when there no (more) type parameters).
  M0 :: Mappings LoT0 LoT0 LoT0
  -- | A non-empty collection (when there is at least one type parameter).
  (:^:) :: (a -> b -> Maybe c)    -- ^ Zipping for the first type parameter.
        -> Mappings as bs cs      -- ^ Zipping for other type parameters.
        -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)

class PairMappings (as :: LoT k) (bs :: LoT k) where
  -- | A collection of pairing functions @(\\x y -> Just (x, y))@ for 'Data.ZipMatchK.zipMatchK'.
  pairMappings :: Mappings as bs (ZipLoT as bs)

instance PairMappings LoT0 LoT0 where
  pairMappings :: Mappings 'LoT0 'LoT0 (ZipLoT 'LoT0 'LoT0)
pairMappings = Mappings 'LoT0 'LoT0 'LoT0
Mappings 'LoT0 'LoT0 (ZipLoT 'LoT0 'LoT0)
M0

instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where
  pairMappings :: Mappings
  (a ':&&: as) (b ':&&: bs) (ZipLoT (a ':&&: as) (b ':&&: bs))
pairMappings = a -> b -> Maybe (a, b)
forall (f :: * -> *) a b. Applicative f => a -> b -> f (a, b)
pairA (a -> b -> Maybe (a, b))
-> Mappings as bs (ZipLoT as bs)
-> Mappings (a ':&&: as) (b ':&&: bs) ((a, b) ':&&: ZipLoT as bs)
forall {k} a b c (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(a -> b -> Maybe c)
-> Mappings as bs cs
-> Mappings (a ':&&: as) (b ':&&: bs) (c ':&&: cs)
:^: Mappings as bs (ZipLoT as bs)
forall k (as :: LoT k) (bs :: LoT k).
PairMappings as bs =>
Mappings as bs (ZipLoT as bs)
pairMappings

class ApplyMappings (v :: TyVar d Type) where
  -- | Apply a collection of zipping functions to collections of values.
  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
       Mappings as bs cs      -- ^ A collection of zipping functions.
    -> Interpret (Var v) as   -- ^ First collection of values (one per type parameter).
    -> Interpret (Var v) bs   -- ^ Second collection of values (one per type parameter).
    -> Maybe (Interpret (Var v) cs)

instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where
  applyMappings :: forall (as :: LoT (* -> tys)) (bs :: LoT (* -> tys))
       (cs :: LoT (* -> tys)).
Mappings as bs cs
-> Interpret ('Var 'VZ) as
-> Interpret ('Var 'VZ) bs
-> Maybe (Interpret ('Var 'VZ) cs)
applyMappings (a -> b -> Maybe c
f :^: Mappings as bs cs
_) Interpret ('Var 'VZ) as
x Interpret ('Var 'VZ) bs
y = a -> b -> Maybe c
f a
Interpret ('Var 'VZ) as
x b
Interpret ('Var 'VZ) bs
y

instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where
  applyMappings :: forall (as :: LoT (ty -> tys)) (bs :: LoT (ty -> tys))
       (cs :: LoT (ty -> tys)).
Mappings as bs cs
-> Interpret ('Var ('VS v)) as
-> Interpret ('Var ('VS v)) bs
-> Maybe (Interpret ('Var ('VS v)) cs)
applyMappings (a -> b -> Maybe c
_ :^: Mappings as bs cs
fs) Interpret ('Var ('VS v)) as
x Interpret ('Var ('VS v)) bs
y = forall d (v :: TyVar d (*)) (as :: LoT d) (bs :: LoT d)
       (cs :: LoT d).
ApplyMappings v =>
Mappings as bs cs
-> Interpret ('Var v) as
-> Interpret ('Var v) bs
-> Maybe (Interpret ('Var v) cs)
applyMappings @_ @v Mappings as bs cs
Mappings as bs cs
fs Interpret ('Var v) as
Interpret ('Var ('VS v)) as
x Interpret ('Var v) bs
Interpret ('Var ('VS v)) bs
y

-- | Pair two values in a context.
pairA :: Applicative f => a -> b -> f (a, b)
pairA :: forall (f :: * -> *) a b. Applicative f => a -> b -> f (a, b)
pairA a
x b
y = (a, b) -> f (a, b)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
x, b
y)