{-# LANGUAGE
  ConstraintKinds,
  FlexibleContexts,
  FlexibleInstances,
  InstanceSigs,
  MultiParamTypeClasses,
  RankNTypes,
  ScopedTypeVariables,
  TypeApplications,
  TypeFamilies,
  TypeOperators,
  UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}

module Generic.Functor.Internal.Implicit where

import Control.Arrow (Kleisli (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bifoldable (Bifoldable (..))
import Data.Bitraversable (Bitraversable (..))
import Data.Coerce (Coercible, coerce)
import Data.Kind (Type)

-- | Core of 'multimap'

multimapI :: forall arr x y. MultimapI arr x y => arr -> (x -> y)
multimapI :: arr -> x -> y
multimapI = arr -> x -> y
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf

multitraverse :: forall f arr x y. Multitraverse f arr x y => arr -> (x -> f y)
multitraverse :: arr -> x -> f y
multitraverse arr
f = Kleisli f x y -> x -> f y
forall (m :: * -> *) a b. Kleisli m a b -> a -> m b
runKleisli (WrapKleisli f arr -> Kleisli f x y
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf (arr -> WrapKleisli f arr
coerce arr
f :: WrapKleisli f arr))

-- | This is kept internal because of the 'Fold' wrapping.

multifold_ :: forall m arr x y. Multifold_ m arr x y => arr -> Fold m x y
multifold_ :: arr -> Fold m x y
multifold_ = arr -> Fold m x y
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf

multimapOf :: forall cat arr x y. MultimapOf cat arr x y => arr -> cat x y
multimapOf :: arr -> cat x y
multimapOf arr
f = S2 arr -> cat x y
forall (cat :: * -> * -> *) arr x y.
Multimap_ cat arr x y =>
arr -> cat x y
multimap_ (arr -> S2 arr
forall arr. arr -> S2 arr
s2 arr
f)

-- | Core of 'multimap'.

class    MultimapOf (->) arr x y => MultimapI arr x y
instance MultimapOf (->) arr x y => MultimapI arr x y

-- | Constraint for 'multifold_'.

class    MultimapOf (Fold m) arr x y => Multifold_ m arr x y
instance MultimapOf (Fold m) arr x y => Multifold_ m arr x y

-- | Constraint for 'multitraverse'.

class    Multitraverse_ f arr x y => Multitraverse f arr x y
instance Multitraverse_ f arr x y => Multitraverse f arr x y

-- | Internal definition of 'Multitraverse'

type Multitraverse_ f arr x y =
  ( MultimapOf (Kleisli f) (WrapKleisli f arr) x y,
    CoercibleKleisli f (WrapKleisli f arr) arr
  )

type family WrapKleisli (f :: Type -> Type) (arr :: Type)
type instance WrapKleisli _f NilArr = NilArr
type instance WrapKleisli _f (Rule rule mode)= Rule rule mode
type instance WrapKleisli f (a :+ arr) = WrapKleisli f a :+ WrapKleisli f arr
type instance WrapKleisli f (a -> f b) = Kleisli f a b

-- | Auxiliary constraint for 'Multitraverse'

class Coercible warr arr => CoercibleKleisli (f :: Type -> Type) warr arr
instance (d ~ NilArr) => CoercibleKleisli f d NilArr
instance (d ~ Rule rule mode) => CoercibleKleisli f d (Rule rule mode)
instance (CoercibleKleisli f a b, CoercibleKleisli f arr arr') => CoercibleKleisli f (a :+ arr) (b :+ arr')
instance (b2 ~ f c, a ~ Kleisli f b1 c) => CoercibleKleisli f a (b1 -> b2)

class    Multimap_ cat (S2 arr) x y => MultimapOf cat arr x y
instance Multimap_ cat (S2 arr) x y => MultimapOf cat arr x y

-- | @Fold m@ is like @Kleisli (Const m)@, but it has a different @FunctorOf@ instance,

-- with 'Foldable' instead of 'Traversable'.

newtype Fold m x y = Fold { Fold m x y -> x -> m
unFold :: x -> m }

instance Monoid m => CatLike (Fold m) where
  catid :: Fold m x x
catid = (x -> m) -> Fold m x x
forall m x y. (x -> m) -> Fold m x y
Fold (\x
_ -> m
forall a. Monoid a => a
mempty)

instance (Foldable t, Monoid m) => FunctorOf (Fold m) t where
  catmap :: Fold m a b -> Fold m (t a) (t b)
catmap (Fold a -> m
f) = (t a -> m) -> Fold m (t a) (t b)
forall m x y. (x -> m) -> Fold m x y
Fold ((a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f)

instance (Bifoldable t, Monoid m) => BifunctorOf (Fold m) t where
  catbimap :: Fold m a b -> Fold m c d -> Fold m (t a c) (t b d)
catbimap (Fold a -> m
f) (Fold c -> m
g) = (t a c -> m) -> Fold m (t a c) (t b d)
forall m x y. (x -> m) -> Fold m x y
Fold ((a -> m) -> (c -> m) -> t a c -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f c -> m
g)

-- * Internal


class CatLike cat where
  catid :: cat x x

instance CatLike (->) where
  catid :: x -> x
catid = x -> x
forall x. x -> x
id

instance Applicative f => CatLike (Kleisli f) where
  catid :: Kleisli f x x
catid = (x -> f x) -> Kleisli f x x
forall (m :: * -> *) a b. (a -> m b) -> Kleisli m a b
Kleisli x -> f x
forall (f :: * -> *) a. Applicative f => a -> f a
pure

class FunctorOf cat t where
  catmap :: cat a b -> cat (t a) (t b)

instance Functor t => FunctorOf (->) t where
  catmap :: (a -> b) -> t a -> t b
catmap = (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
fmap

instance (Applicative f, Traversable t) => FunctorOf (Kleisli f) t where
  catmap :: forall a b. Kleisli f a b -> Kleisli f (t a) (t b)
  catmap :: Kleisli f a b -> Kleisli f (t a) (t b)
catmap = ((a -> f b) -> t a -> f (t b))
-> Kleisli f a b -> Kleisli f (t a) (t b)
coerce (Applicative f => (a -> f b) -> t a -> f (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse @t @f @a @b)

class BifunctorOf cat t where
  catbimap :: cat a b -> cat c d -> cat (t a c) (t b d)

instance Bifunctor t => BifunctorOf (->) t where
  catbimap :: (a -> b) -> (c -> d) -> t a c -> t b d
catbimap = (a -> b) -> (c -> d) -> t a c -> t b d
forall (t :: * -> * -> *) a b c d.
Bifunctor t =>
(a -> b) -> (c -> d) -> t a c -> t b d
bimap

instance (Applicative f, Bitraversable t) => BifunctorOf (Kleisli f) t where
  catbimap :: forall a b c d. Kleisli f a b -> Kleisli f c d -> Kleisli f (t a c) (t b d)
  catbimap :: Kleisli f a b -> Kleisli f c d -> Kleisli f (t a c) (t b d)
catbimap = ((a -> f b) -> (c -> f d) -> t a c -> f (t b d))
-> Kleisli f a b -> Kleisli f c d -> Kleisli f (t a c) (t b d)
coerce (Applicative f => (a -> f b) -> (c -> f d) -> t a c -> f (t b d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse @t @f @a @b @c @d)

-- | Internal implementation of 'MultimapOf'.

class Multimap_ cat arr x y where
  multimap_ :: arr -> cat x y

-- | Heterogeneous lists of arrows are constructed as lists separated by

-- @(':+')@ and terminated by @()@.

--

-- === Example

--

-- Given @f :: a -> a'@ and @g :: b -> b'@,

-- @(f ':+' g ':+' ())@ is a list with the two elements @f@ and @g@.

--

-- @

-- if

--   f :: a -> a'

--   g :: b -> b'

--

-- then

--   f ':+' g ':+' ()  ::  (a -> a') ':+' (b -> b') ':+' ()

-- @

--

-- Those lists are used by 'gmultimap' and 'multimap'.

--

-- @

-- bimap_ :: (a -> a') -> (b -> b') -> (Maybe a, [Either b a]) -> (Maybe a', [Either b' a'])

-- bimap_ f g = 'multimap' (f ':+' g ':+' ())

-- @

data a :+ b = a :+ b

infixr 1 :+

-- Special arrows


data Rule rule mode = Rule rule mode
data AnyId = AnyId
data AnyFunctor = AnyFunctor
data AnyBifunctor = AnyBifunctor
data NilArr = NilArr

data Incoherent = Incoherent

type Default mode arr = arr :+ Rule AnyId mode :+ Rule AnyFunctor mode :+ Rule AnyBifunctor mode :+ NilArr

defaultIncoherent :: arr -> Default Incoherent arr
defaultIncoherent :: arr -> Default Incoherent arr
defaultIncoherent = Incoherent -> arr -> Default Incoherent arr
forall mode arr. mode -> arr -> Default mode arr
def Incoherent
Incoherent

def :: mode -> arr -> Default mode arr
def :: mode -> arr -> Default mode arr
def mode
mode arr
arr = arr
arr arr
-> (Rule AnyId mode
    :+ (Rule AnyFunctor mode :+ (Rule AnyBifunctor mode :+ NilArr)))
-> Default mode arr
forall a b. a -> b -> a :+ b
:+ AnyId -> mode -> Rule AnyId mode
forall rule mode. rule -> mode -> Rule rule mode
Rule AnyId
AnyId mode
mode Rule AnyId mode
-> (Rule AnyFunctor mode :+ (Rule AnyBifunctor mode :+ NilArr))
-> Rule AnyId mode
   :+ (Rule AnyFunctor mode :+ (Rule AnyBifunctor mode :+ NilArr))
forall a b. a -> b -> a :+ b
:+ AnyFunctor -> mode -> Rule AnyFunctor mode
forall rule mode. rule -> mode -> Rule rule mode
Rule AnyFunctor
AnyFunctor mode
mode Rule AnyFunctor mode
-> (Rule AnyBifunctor mode :+ NilArr)
-> Rule AnyFunctor mode :+ (Rule AnyBifunctor mode :+ NilArr)
forall a b. a -> b -> a :+ b
:+ AnyBifunctor -> mode -> Rule AnyBifunctor mode
forall rule mode. rule -> mode -> Rule rule mode
Rule AnyBifunctor
AnyBifunctor mode
mode Rule AnyBifunctor mode
-> NilArr -> Rule AnyBifunctor mode :+ NilArr
forall a b. a -> b -> a :+ b
:+ NilArr
NilArr

-- | @arr@ is the list of arrows provided by the user. It is constant.

-- When testing whether any arrow matches, @arr'@ is the remaining list of

-- arrows to be tested.

data S arr arr' = S arr arr'

type S2 arr = S arr arr

s2 :: arr -> S2 arr
s2 :: arr -> S2 arr
s2 arr
f = arr -> arr -> S2 arr
forall arr arr'. arr -> arr' -> S arr arr'
S arr
f arr
f

-- The head doesn't match anything, go to the next thing.

instance {-# OVERLAPPABLE #-} Multimap_ cat (S arr arr') x y => Multimap_ cat (S arr (arr0 :+ arr')) x y where
  multimap_ :: S arr (arr0 :+ arr') -> cat x y
multimap_ (S arr
f (arr0
_ :+ arr'
g')) = S arr arr' -> cat x y
forall (cat :: * -> * -> *) arr x y.
Multimap_ cat arr x y =>
arr -> cat x y
multimap_ (arr -> arr' -> S arr arr'
forall arr arr'. arr -> arr' -> S arr arr'
S arr
f arr'
g')

-- Reassociate to even handle tree-shaped parameters.

instance Multimap_ cat (S arr (arr0 :+ arr1 :+ arr2)) x y => Multimap_ cat (S arr ((arr0 :+ arr1) :+ arr2)) x y where
  multimap_ :: S arr ((arr0 :+ arr1) :+ arr2) -> cat x y
multimap_ (S arr
f ((arr0
f0 :+ arr1
f1) :+ arr2
f2)) = S arr (arr0 :+ (arr1 :+ arr2)) -> cat x y
forall (cat :: * -> * -> *) arr x y.
Multimap_ cat arr x y =>
arr -> cat x y
multimap_ (arr -> (arr0 :+ (arr1 :+ arr2)) -> S arr (arr0 :+ (arr1 :+ arr2))
forall arr arr'. arr -> arr' -> S arr arr'
S arr
f (arr0
f0 arr0 -> (arr1 :+ arr2) -> arr0 :+ (arr1 :+ arr2)
forall a b. a -> b -> a :+ b
:+ arr1
f1 arr1 -> arr2 -> arr1 :+ arr2
forall a b. a -> b -> a :+ b
:+ arr2
f2))

instance Multimap_ cat (S arr arr') x y => Multimap_ cat (S arr (NilArr :+ arr')) x y where
  multimap_ :: S arr (NilArr :+ arr') -> cat x y
multimap_ (S arr
f (NilArr
NilArr :+ arr'
f')) = S arr arr' -> cat x y
forall (cat :: * -> * -> *) arr x y.
Multimap_ cat arr x y =>
arr -> cat x y
multimap_ (arr -> arr' -> S arr arr'
forall arr arr'. arr -> arr' -> S arr arr'
S arr
f arr'
f')

instance Multimap_ cat (S arr arr') x y => Multimap_ cat (S arr (() :+ arr')) x y where
  multimap_ :: S arr (() :+ arr') -> cat x y
multimap_ (S arr
f (() :+ arr'
f')) = S arr arr' -> cat x y
forall (cat :: * -> * -> *) arr x y.
Multimap_ cat arr x y =>
arr -> cat x y
multimap_ (arr -> arr' -> S arr arr'
forall arr arr'. arr -> arr' -> S arr arr'
S arr
f arr'
f')

instance {-# INCOHERENT #-} Multimap_ cat (S arr (cat a b :+ arr')) a b where
  multimap_ :: S arr (cat a b :+ arr') -> cat a b
multimap_ (S arr
_ (cat a b
f :+ arr'
_)) = cat a b
f

-- "id" instance

instance {-# INCOHERENT #-} CatLike cat => Multimap_ cat (S arr (Rule AnyId Incoherent :+ arr')) x x where
  multimap_ :: S arr (Rule AnyId Incoherent :+ arr') -> cat x x
multimap_ S arr (Rule AnyId Incoherent :+ arr')
_ = cat x x
forall (cat :: * -> * -> *) x. CatLike cat => cat x x
catid

-- "Functor" instance

-- Note: if x ~ y, then @AnyId Incoherent@ should already have matched earlier

-- (if you remembered to put it in the list),

-- so we don't need another overlapping instance here.

instance
  {-# INCOHERENT #-}
  (FunctorOf cat f, MultimapOf cat arr x y) =>
  Multimap_ cat (S arr (Rule AnyFunctor Incoherent :+ arr')) (f x) (f y)
  where
  multimap_ :: S arr (Rule AnyFunctor Incoherent :+ arr') -> cat (f x) (f y)
multimap_ (S arr
f (Rule AnyFunctor
AnyFunctor Incoherent
Incoherent :+ arr'
_)) = cat x y -> cat (f x) (f y)
forall (cat :: * -> * -> *) (t :: * -> *) a b.
FunctorOf cat t =>
cat a b -> cat (t a) (t b)
catmap (arr -> cat x y
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf arr
f)

-- "Bifunctor" instance.

-- Note: the overlap with AnyId (where x1 ~ y1, x2 ~ y2) and AnyFunctor (where x1 ~ x2)

-- is handled by putting those rules before AnyBifunctor in the list.

instance
  {-# INCOHERENT #-}
  (BifunctorOf cat f, MultimapOf cat arr x1 y1, MultimapOf cat arr x2 y2) =>
  Multimap_ cat (S arr (Rule AnyBifunctor Incoherent :+ arr')) (f x1 x2) (f y1 y2)
  where
  multimap_ :: S arr (Rule AnyBifunctor Incoherent :+ arr')
-> cat (f x1 x2) (f y1 y2)
multimap_ (S arr
f (Rule AnyBifunctor
AnyBifunctor Incoherent
Incoherent :+ arr'
_)) = cat x1 y1 -> cat x2 y2 -> cat (f x1 x2) (f y1 y2)
forall (cat :: * -> * -> *) (t :: * -> * -> *) a b c d.
BifunctorOf cat t =>
cat a b -> cat c d -> cat (t a c) (t b d)
catbimap (arr -> cat x1 y1
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf arr
f) (arr -> cat x2 y2
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf arr
f)

-- Hardcoded special case for (->)

-- We know how to "Multimap_ (->)" over (->),

-- not "Multimap_ (Kleisli f)".

instance
  {-# INCOHERENT #-}
  (MultimapOf (->) arr y1 x1, MultimapOf (->) arr x2 y2) =>
  Multimap_ (->) (S arr (Rule AnyBifunctor Incoherent :+ arr')) (x1 -> x2) (y1 -> y2)
  where
  multimap_ :: S arr (Rule AnyBifunctor Incoherent :+ arr')
-> (x1 -> x2) -> y1 -> y2
multimap_ (S arr
f (Rule AnyBifunctor
AnyBifunctor Incoherent
Incoherent :+ arr'
_)) x1 -> x2
u = arr -> x2 -> y2
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf arr
f (x2 -> y2) -> (y1 -> x2) -> y1 -> y2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x1 -> x2
u (x1 -> x2) -> (y1 -> x1) -> y1 -> x2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. arr -> y1 -> x1
forall (cat :: * -> * -> *) arr x y.
MultimapOf cat arr x y =>
arr -> cat x y
multimapOf arr
f