{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

{- |
Module      :  Control.Monad.Trans.Indexed.Free.Fold
Copyright   :  (C) 2024 Eitan Chatav
License     :  BSD 3-Clause License (see the file LICENSE)
Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>

An instance of the free indexed monad transformer encoded as `foldFreeIx`.
-}

module Control.Monad.Trans.Indexed.Free.Fold
  ( FreeIx (..)
  ) where

import Control.Monad
import Control.Monad.Free
import Control.Monad.Trans
import Control.Monad.Trans.Indexed
import Control.Monad.Trans.Indexed.Free

{- |
`FreeIx` is the free indexed monad transformer encoded as its `foldFreeIx`.

prop> foldFreeIx f freeIx = runFreeIx freeIx f
-}
newtype FreeIx g i j m x = FreeIx
  {forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
FreeIx g i j m x
-> forall (t :: k -> k -> (* -> *) -> * -> *).
   (IxMonadTrans t, Monad m) =>
   (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x
runFreeIx :: forall t. (IxMonadTrans t, Monad m)
    => (forall i j x. g i j x -> t i j m x) -> t i j m x}
instance (IxFunctor f, Monad m) => Functor (FreeIx f i j m) where
  fmap :: forall a b. (a -> b) -> FreeIx f i j m a -> FreeIx f i j m b
fmap a -> b
f (FreeIx forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a
k) = (forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m b)
-> FreeIx f i j m b
forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
(forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
FreeIx ((forall (t :: k -> k -> (* -> *) -> * -> *).
  (IxMonadTrans t, Monad m) =>
  (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m b)
 -> FreeIx f i j m b)
-> (forall (t :: k -> k -> (* -> *) -> * -> *).
    (IxMonadTrans t, Monad m) =>
    (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m b)
-> FreeIx f i j m b
forall a b. (a -> b) -> a -> b
$ \forall (i :: k) (j :: k) x. f i j x -> t i j m x
step -> (a -> b) -> t i j m a -> t i j m b
forall a b. (a -> b) -> t i j m a -> t i j m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ((forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a
forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a
k f i j x -> t i j m x
forall (i :: k) (j :: k) x. f i j x -> t i j m x
step)
instance (IxFunctor f, i ~ j, Monad m)
  => Applicative (FreeIx f i j m) where
    pure :: forall a. a -> FreeIx f i j m a
pure a
x = (forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
-> FreeIx f i j m a
forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
(forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
FreeIx ((forall (t :: k -> k -> (* -> *) -> * -> *).
  (IxMonadTrans t, Monad m) =>
  (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
 -> FreeIx f i j m a)
-> (forall (t :: k -> k -> (* -> *) -> * -> *).
    (IxMonadTrans t, Monad m) =>
    (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
-> FreeIx f i j m a
forall a b. (a -> b) -> a -> b
$ t i j m a
-> (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a
forall a b. a -> b -> a
const (t i j m a
 -> (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
-> t i j m a
-> (forall (i :: k) (j :: k) x. f i j x -> t i j m x)
-> t i j m a
forall a b. (a -> b) -> a -> b
$ a -> t i j m a
forall a. a -> t i j m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
    <*> :: forall a b.
FreeIx f i j m (a -> b) -> FreeIx f i j m a -> FreeIx f i j m b
(<*>) = FreeIx f i j m (a -> b) -> FreeIx f i j m a -> FreeIx f i j m b
FreeIx f i j m (a -> b) -> FreeIx f j j m a -> FreeIx f i j m b
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) (i :: k)
       (j :: k) x y (k1 :: k).
(IxMonadTrans t, Monad m) =>
t i j m (x -> y) -> t j k1 m x -> t i k1 m y
forall (m :: * -> *) (i :: k) (j :: k) x y (k1 :: k).
Monad m =>
FreeIx f i j m (x -> y) -> FreeIx f j k1 m x -> FreeIx f i k1 m y
apIx
instance (IxFunctor f, i ~ j, Monad m)
  => Monad (FreeIx f i j m) where
    return :: forall a. a -> FreeIx f i j m a
return = a -> FreeIx f i j m a
forall a. a -> FreeIx f i j m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    >>= :: forall a b.
FreeIx f i j m a -> (a -> FreeIx f i j m b) -> FreeIx f i j m b
(>>=) = ((a -> FreeIx f i j m b) -> FreeIx f i j m a -> FreeIx f i j m b)
-> FreeIx f i j m a -> (a -> FreeIx f i j m b) -> FreeIx f i j m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> FreeIx f i j m b) -> FreeIx f i i m a -> FreeIx f i j m b
(a -> FreeIx f i j m b) -> FreeIx f i j m a -> FreeIx f i j m b
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) x
       (j :: k) (k1 :: k) y (i :: k).
(IxMonadTrans t, Monad m) =>
(x -> t j k1 m y) -> t i j m x -> t i k1 m y
forall (m :: * -> *) x (j :: k) (k1 :: k) y (i :: k).
Monad m =>
(x -> FreeIx f j k1 m y) -> FreeIx f i j m x -> FreeIx f i k1 m y
bindIx
instance (IxFunctor f, i ~ j)
  => MonadTrans (FreeIx f i j) where
    lift :: forall (m :: * -> *) a. Monad m => m a -> FreeIx f i j m a
lift m a
m = (forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
-> FreeIx f i j m a
forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
(forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
FreeIx ((forall (t :: k -> k -> (* -> *) -> * -> *).
  (IxMonadTrans t, Monad m) =>
  (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
 -> FreeIx f i j m a)
-> (forall (t :: k -> k -> (* -> *) -> * -> *).
    (IxMonadTrans t, Monad m) =>
    (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
-> FreeIx f i j m a
forall a b. (a -> b) -> a -> b
$ t i j m a
-> (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a
forall a b. a -> b -> a
const (t i j m a
 -> (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m a)
-> t i j m a
-> (forall (i :: k) (j :: k) x. f i j x -> t i j m x)
-> t i j m a
forall a b. (a -> b) -> a -> b
$ m a -> t i j m a
forall (m :: * -> *) a. Monad m => m a -> t i j m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m
instance IxFunctor f
  => IxMonadTrans (FreeIx f) where
    joinIx :: forall (m :: * -> *) (i :: k) (j :: k) (k1 :: k) y.
Monad m =>
FreeIx f i j m (FreeIx f j k1 m y) -> FreeIx f i k1 m y
joinIx (FreeIx forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x)
-> t i j m (FreeIx f j k1 m y)
g) = (forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i k1 m y)
-> FreeIx f i k1 m y
forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
(forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
FreeIx ((forall (t :: k -> k -> (* -> *) -> * -> *).
  (IxMonadTrans t, Monad m) =>
  (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i k1 m y)
 -> FreeIx f i k1 m y)
-> (forall (t :: k -> k -> (* -> *) -> * -> *).
    (IxMonadTrans t, Monad m) =>
    (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i k1 m y)
-> FreeIx f i k1 m y
forall a b. (a -> b) -> a -> b
$ \forall (i :: k) (j :: k) x. f i j x -> t i j m x
k -> (FreeIx f j k1 m y -> t j k1 m y)
-> t i j m (FreeIx f j k1 m y) -> t i k1 m y
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) x
       (j :: k) (k1 :: k) y (i :: k).
(IxMonadTrans t, Monad m) =>
(x -> t j k1 m y) -> t i j m x -> t i k1 m y
forall (m :: * -> *) x (j :: k) (k1 :: k) y (i :: k).
Monad m =>
(x -> t j k1 m y) -> t i j m x -> t i k1 m y
bindIx (\(FreeIx forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t j k1 m y
f) -> (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t j k1 m y
forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t j k1 m y
f f i j x -> t i j m x
forall (i :: k) (j :: k) x. f i j x -> t i j m x
k) ((forall (i :: k) (j :: k) x. f i j x -> t i j m x)
-> t i j m (FreeIx f j k1 m y)
forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x)
-> t i j m (FreeIx f j k1 m y)
g f i j x -> t i j m x
forall (i :: k) (j :: k) x. f i j x -> t i j m x
k)
instance
  ( IxFunctor f
  , Monad m
  , i ~ j
  ) => MonadFree (f i j) (FreeIx f i j m) where
    wrap :: forall a. f i j (FreeIx f i j m a) -> FreeIx f i j m a
wrap = FreeIx f i j m (FreeIx f i j m a) -> FreeIx f i j m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (FreeIx f i j m (FreeIx f i j m a) -> FreeIx f i j m a)
-> (f i j (FreeIx f i j m a) -> FreeIx f i j m (FreeIx f i j m a))
-> f i j (FreeIx f i j m a)
-> FreeIx f i j m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f i j (FreeIx f i j m a) -> FreeIx f i j m (FreeIx f i j m a)
forall {k}
       (freeIx :: (k -> k -> * -> *) -> k -> k -> (* -> *) -> * -> *)
       (f :: k -> k -> * -> *) (m :: * -> *) (i :: k) (j :: k) x.
(IxMonadTransFree freeIx, IxFunctor f, Monad m) =>
f i j x -> freeIx f i j m x
forall (f :: k -> k -> * -> *) (m :: * -> *) (i :: k) (j :: k) x.
(IxFunctor f, Monad m) =>
f i j x -> FreeIx f i j m x
liftFreeIx
instance IxMonadTransFree FreeIx where
  liftFreeIx :: forall (f :: k -> k -> * -> *) (m :: * -> *) (i :: k) (j :: k) x.
(IxFunctor f, Monad m) =>
f i j x -> FreeIx f i j m x
liftFreeIx f i j x
m = (forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x)
-> FreeIx f i j m x
forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
(forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
FreeIx ((forall (t :: k -> k -> (* -> *) -> * -> *).
  (IxMonadTrans t, Monad m) =>
  (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x)
 -> FreeIx f i j m x)
-> (forall (t :: k -> k -> (* -> *) -> * -> *).
    (IxMonadTrans t, Monad m) =>
    (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x)
-> FreeIx f i j m x
forall a b. (a -> b) -> a -> b
$ \forall (i :: k) (j :: k) x. f i j x -> t i j m x
k -> f i j x -> t i j m x
forall (i :: k) (j :: k) x. f i j x -> t i j m x
k f i j x
m
  hoistFreeIx :: forall (f :: k -> k -> * -> *) (g :: k -> k -> * -> *)
       (m :: * -> *) (i :: k) (j :: k) x.
(IxFunctor f, IxFunctor g, Monad m) =>
(forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> g i1 j1 x1)
-> FreeIx f i j m x -> FreeIx g i j m x
hoistFreeIx forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> g i1 j1 x1
f (FreeIx forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x
k) = (forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
forall {k} (g :: k -> k -> * -> *) (i :: k) (j :: k) (m :: * -> *)
       x.
(forall (t :: k -> k -> (* -> *) -> * -> *).
 (IxMonadTrans t, Monad m) =>
 (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
FreeIx ((forall (t :: k -> k -> (* -> *) -> * -> *).
  (IxMonadTrans t, Monad m) =>
  (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
 -> FreeIx g i j m x)
-> (forall (t :: k -> k -> (* -> *) -> * -> *).
    (IxMonadTrans t, Monad m) =>
    (forall (i :: k) (j :: k) x. g i j x -> t i j m x) -> t i j m x)
-> FreeIx g i j m x
forall a b. (a -> b) -> a -> b
$ \forall (i :: k) (j :: k) x. g i j x -> t i j m x
g -> (forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x
forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x
k (g i j x -> t i j m x
forall (i :: k) (j :: k) x. g i j x -> t i j m x
g (g i j x -> t i j m x)
-> (f i j x -> g i j x) -> f i j x -> t i j m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f i j x -> g i j x
forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> g i1 j1 x1
f)
  foldFreeIx :: forall (f :: k -> k -> * -> *) (t :: k -> k -> (* -> *) -> * -> *)
       (m :: * -> *) (i :: k) (j :: k) x.
(IxFunctor f, IxMonadTrans t, Monad m) =>
(forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> t i1 j1 m x1)
-> FreeIx f i j m x -> t i j m x
foldFreeIx forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> t i1 j1 m x1
f (FreeIx forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x
k) = (forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> t i1 j1 m x1)
-> t i j m x
forall (t :: k -> k -> (* -> *) -> * -> *).
(IxMonadTrans t, Monad m) =>
(forall (i :: k) (j :: k) x. f i j x -> t i j m x) -> t i j m x
k f i j x -> t i j m x
forall (i1 :: k) (j1 :: k) x1. f i1 j1 x1 -> t i1 j1 m x1
f