{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
-- | Kind-polymorphic syntactic (first-order) unification.
module Data.ZipMatchK (
  module Data.ZipMatchK.Mappings,
  ZipMatchK(..),
  zipMatchK,
  -- * Specializations
  -- ** Unification of plain 'Data.Kind.Type's
  zipMatchViaEq,
  zipMatchViaChooseLeft,
  -- ** Unification of 'Data.Functor.Functor's
  zipMatchWith1,
  zipMatch1,
  -- ** Unification of 'Data.Bifunctor.Bifunctor's
  zipMatchWith2,
  zipMatch2,
) where

import           Generics.Kind
import Data.Bitraversable

import Data.ZipMatchK.Generic
import Data.ZipMatchK.Mappings

-- | Perform one level of equality testing for two values and pair up components using @(,)@:
--
-- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0)
zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
zipMatchK :: forall {k} (f :: k) (as :: LoT k) (bs :: LoT k).
(ZipMatchK f, PairMappings as bs) =>
(f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: ZipLoT as bs)
zipMatchK = forall k (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ZipMatchK f =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
zipMatchWithK @_ @f @as @bs Mappings as bs (ZipLoT as bs)
forall k (as :: LoT k) (bs :: LoT k).
PairMappings as bs =>
Mappings as bs (ZipLoT as bs)
pairMappings

-- | Unify values via 'Eq'.
-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.
zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq :: forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq Mappings as bs cs
_ a
x a
y
  | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = a -> Maybe a
forall a. a -> Maybe a
Just a
x
  | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing

-- | Always successfully unify any two values of type @a@ by preferring the left value.
-- Can be used as an implementation of 'zipMatchWithK' when @k = 'Data.Kind.Type'@.
zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaChooseLeft :: forall {k} (as :: LoT k) (bs :: LoT k) (cs :: LoT k) a.
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaChooseLeft Mappings as bs cs
_ a
x a
_ = a -> Maybe a
forall a. a -> Maybe a
Just a
x

-- | 'zipMatchWithK' specialised to functors.
--
-- Note: 'Traversable' is a morally correct constraint here.
zipMatchWith1
  :: (Traversable f, ZipMatchK f)
  => (a -> a' -> Maybe a'')
  -> f a -> f a' -> Maybe (f a'')
zipMatchWith1 :: forall (f :: * -> *) a a' a''.
(Traversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'') -> f a -> f a' -> Maybe (f a'')
zipMatchWith1 a -> a' -> Maybe a''
f = Mappings (a ':&&: 'LoT0) (a' ':&&: 'LoT0) (a'' ':&&: 'LoT0)
-> (f :@@: (a ':&&: 'LoT0))
-> (f :@@: (a' ':&&: 'LoT0))
-> Maybe (f :@@: (a'' ':&&: 'LoT0))
forall k (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ZipMatchK f =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
forall (as :: LoT (* -> *)) (bs :: LoT (* -> *))
       (cs :: LoT (* -> *)).
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
zipMatchWithK (a -> a' -> Maybe a''
f (a -> a' -> Maybe a'')
-> Mappings 'LoT0 'LoT0 'LoT0
-> Mappings (a ':&&: 'LoT0) (a' ':&&: 'LoT0) (a'' ':&&: 'LoT0)
forall {k1} a b c (as1 :: LoT k1) (bs1 :: LoT k1) (cs1 :: LoT k1).
(a -> b -> Maybe c)
-> Mappings as1 bs1 cs1
-> Mappings (a ':&&: as1) (b ':&&: bs1) (c ':&&: cs1)
:^: Mappings 'LoT0 'LoT0 'LoT0
M0)

-- | 'zipMatchK' specialised to functors.
--
-- Note: 'Traversable' is a morally correct constraint here.
zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a'))
zipMatch1 :: forall (f :: * -> *) a a'.
(Traversable f, ZipMatchK f) =>
f a -> f a' -> Maybe (f (a, a'))
zipMatch1 = (a -> a' -> Maybe (a, a')) -> f a -> f a' -> Maybe (f (a, a'))
forall (f :: * -> *) a a' a''.
(Traversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'') -> f a -> f a' -> Maybe (f a'')
zipMatchWith1 a -> a' -> Maybe (a, a')
forall (f :: * -> *) a b. Applicative f => a -> b -> f (a, b)
pairA
-- | 'zipMatchWithK' specialised to bifunctors.
--
-- Note: 'Bitraversable' is a morally correct constraint here.
zipMatchWith2
  :: (Bitraversable f, ZipMatchK f)
  => (a -> a' -> Maybe a'')
  -> (b -> b' -> Maybe b'')
  -> f a b -> f a' b' -> Maybe (f a'' b'')
zipMatchWith2 :: forall (f :: * -> * -> *) a a' a'' b b' b''.
(Bitraversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'')
-> (b -> b' -> Maybe b'') -> f a b -> f a' b' -> Maybe (f a'' b'')
zipMatchWith2 a -> a' -> Maybe a''
f b -> b' -> Maybe b''
g = Mappings
  (a ':&&: (b ':&&: 'LoT0))
  (a' ':&&: (b' ':&&: 'LoT0))
  (a'' ':&&: (b'' ':&&: 'LoT0))
-> (f :@@: (a ':&&: (b ':&&: 'LoT0)))
-> (f :@@: (a' ':&&: (b' ':&&: 'LoT0)))
-> Maybe (f :@@: (a'' ':&&: (b'' ':&&: 'LoT0)))
forall k (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ZipMatchK f =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
forall (as :: LoT (* -> * -> *)) (bs :: LoT (* -> * -> *))
       (cs :: LoT (* -> * -> *)).
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
zipMatchWithK (a -> a' -> Maybe a''
f (a -> a' -> Maybe a'')
-> Mappings (b ':&&: 'LoT0) (b' ':&&: 'LoT0) (b'' ':&&: 'LoT0)
-> Mappings
     (a ':&&: (b ':&&: 'LoT0))
     (a' ':&&: (b' ':&&: 'LoT0))
     (a'' ':&&: (b'' ':&&: 'LoT0))
forall {k1} a b c (as1 :: LoT k1) (bs1 :: LoT k1) (cs1 :: LoT k1).
(a -> b -> Maybe c)
-> Mappings as1 bs1 cs1
-> Mappings (a ':&&: as1) (b ':&&: bs1) (c ':&&: cs1)
:^: b -> b' -> Maybe b''
g (b -> b' -> Maybe b'')
-> Mappings 'LoT0 'LoT0 'LoT0
-> Mappings (b ':&&: 'LoT0) (b' ':&&: 'LoT0) (b'' ':&&: 'LoT0)
forall {k1} a b c (as1 :: LoT k1) (bs1 :: LoT k1) (cs1 :: LoT k1).
(a -> b -> Maybe c)
-> Mappings as1 bs1 cs1
-> Mappings (a ':&&: as1) (b ':&&: bs1) (c ':&&: cs1)
:^: Mappings 'LoT0 'LoT0 'LoT0
M0)

-- | 'zipMatchK' specialised to bifunctors.
--
-- Note: 'Bitraversable' is a morally correct constraint here.
zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
zipMatch2 :: forall (f :: * -> * -> *) a b a' b'.
(Bitraversable f, ZipMatchK f) =>
f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
zipMatch2 = (a -> a' -> Maybe (a, a'))
-> (b -> b' -> Maybe (b, b'))
-> f a b
-> f a' b'
-> Maybe (f (a, a') (b, b'))
forall (f :: * -> * -> *) a a' a'' b b' b''.
(Bitraversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'')
-> (b -> b' -> Maybe b'') -> f a b -> f a' b' -> Maybe (f a'' b'')
zipMatchWith2 a -> a' -> Maybe (a, a')
forall (f :: * -> *) a b. Applicative f => a -> b -> f (a, b)
pairA b -> b' -> Maybe (b, b')
forall (f :: * -> *) a b. Applicative f => a -> b -> f (a, b)
pairA