{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A type class to abstract away the encoding details of the Freer carriers.
-}
module Control.Freer where

import Control.Applicative (Alternative, empty, (<|>))
import Control.Applicative.Free (Ap, liftAp, runAp)
import Control.Applicative.Free.Fast qualified as Fast
import Control.Effect (SendIns, sendIns, type (~>))
import Control.Effect.Key (SendInsBy, sendInsBy)
import Control.Monad (MonadPlus)
import Control.Monad.Base (MonadBase)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.State.Class (MonadState, get, put)
import Data.Bool (bool)
import Data.Effect (InsClass)
import Data.Effect.Fail (Fail (Fail))
import Data.Effect.NonDet (Choose, Empty, choose)
import Data.Effect.NonDet qualified as NonDet
import Data.Effect.State (State, get'', put'')
import Data.Functor.Coyoneda (Coyoneda, hoistCoyoneda, liftCoyoneda, lowerCoyoneda)
import Data.Kind (Type)

-- | A type class to abstract away the encoding details of the Freer carrier.
class (forall e. c (f e)) => Freer c f | f -> c where
    {-# MINIMAL liftIns, (interpretFreer | retractFreer, transformFreer) #-}

    -- | Lift a /instruction/ into a Freer carrier.
    liftIns :: e a -> f e a

    interpretFreer :: c m => (e ~> m) -> f e a -> m a
    interpretFreer e ~> m
i = forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Freer c f, c m) =>
f m a -> m a
retractFreer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) (e' :: * -> *) a.
Freer c f =>
(e ~> e') -> f e a -> f e' a
transformFreer e ~> m
i
    {-# INLINE interpretFreer #-}

    retractFreer :: c m => f m a -> m a
    retractFreer = forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (m :: * -> *) (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer forall a. a -> a
id
    {-# INLINE retractFreer #-}

    -- | Translate /instruction/s embedded in a Freer carrier.
    transformFreer ::
        (e ~> e') ->
        f e a ->
        f e' a
    transformFreer e ~> e'
phi = forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (m :: * -> *) (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer forall a b. (a -> b) -> a -> b
$ forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. e ~> e'
phi
    {-# INLINE transformFreer #-}

    reinterpretFreer :: (e ~> f e) -> f e a -> f e a
    reinterpretFreer = forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (m :: * -> *) (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer
    {-# INLINE reinterpretFreer #-}

instance Freer Functor Coyoneda where
    liftIns :: forall (e :: * -> *) a. e a -> Coyoneda e a
liftIns = forall (e :: * -> *) a. e a -> Coyoneda e a
liftCoyoneda
    interpretFreer :: forall (m :: * -> *) (e :: * -> *) a.
Functor m =>
(e ~> m) -> Coyoneda e a -> m a
interpretFreer e ~> m
i = forall (m :: * -> *) a. Functor m => Coyoneda m a -> m a
lowerCoyoneda forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (e' :: * -> *) a.
(e ~> e') -> Coyoneda e a -> Coyoneda e' a
hoistCoyoneda e ~> m
i
    {-# INLINE liftIns #-}
    {-# INLINE interpretFreer #-}

instance Freer Applicative Ap where
    liftIns :: forall (e :: * -> *) a. e a -> Ap e a
liftIns = forall (e :: * -> *) a. e a -> Ap e a
liftAp
    interpretFreer :: forall (m :: * -> *) (e :: * -> *) a.
Applicative m =>
(e ~> m) -> Ap e a -> m a
interpretFreer = forall (m :: * -> *) (e :: * -> *) a.
Applicative m =>
(e ~> m) -> Ap e a -> m a
runAp
    {-# INLINE liftIns #-}
    {-# INLINE interpretFreer #-}

instance Freer Applicative Fast.Ap where
    liftIns :: forall (e :: * -> *) a. e a -> Ap e a
liftIns = forall (e :: * -> *) a. e a -> Ap e a
Fast.liftAp
    interpretFreer :: forall (m :: * -> *) (e :: * -> *) a.
Applicative m =>
(e ~> m) -> Ap e a -> m a
interpretFreer = forall (m :: * -> *) (e :: * -> *) a.
Applicative m =>
(e ~> m) -> Ap e a -> m a
Fast.runAp
    {-# INLINE liftIns #-}
    {-# INLINE interpretFreer #-}

newtype
    ViaFreer
        (fr :: InsClass -> Type -> Type)
        (e :: InsClass)
        (a :: Type) = ViaFreer
    {forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
ViaFreer fr e a -> fr e a
viaFreer :: fr e a}

deriving newtype instance Functor (fr e) => Functor (ViaFreer fr e)
deriving newtype instance Applicative (fr e) => Applicative (ViaFreer fr e)
deriving newtype instance Monad (fr e) => Monad (ViaFreer fr e)
deriving newtype instance (MonadBase b (fr e), Monad b) => MonadBase b (ViaFreer fr e)

deriving newtype instance Foldable (fr e) => Foldable (ViaFreer fr e)
deriving stock instance Traversable (fr e) => Traversable (ViaFreer fr e)
deriving newtype instance Eq (fr e a) => Eq (ViaFreer fr e a)
deriving newtype instance Ord (fr e a) => Ord (ViaFreer fr e a)
deriving newtype instance Read (fr e a) => Read (ViaFreer fr e a)
deriving newtype instance Show (fr e a) => Show (ViaFreer fr e a)

deriving newtype instance (Freer c fr, forall e. c (ViaFreer fr e)) => Freer c (ViaFreer fr)

instance (Freer c fr, InjectIns e e') => SendIns e (ViaFreer fr e') where
    sendIns :: forall a. e a -> ViaFreer fr e' a
sendIns = forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
fr e a -> ViaFreer fr e a
ViaFreer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (e' :: * -> *). InjectIns e e' => e ~> e'
injectIns
    {-# INLINE sendIns #-}

class InjectIns e (e' :: InsClass) where
    injectIns :: e ~> e'

instance (Freer c fr, InjectInsBy key e e') => SendInsBy key e (ViaFreer fr e') where
    sendInsBy :: forall a. e a -> ViaFreer fr e' a
sendInsBy = forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
fr e a -> ViaFreer fr e a
ViaFreer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (key :: k) (e :: * -> *) (e' :: * -> *).
InjectInsBy key e e' =>
e ~> e'
injectInsBy @key
    {-# INLINE sendInsBy #-}

class InjectInsBy key e (e' :: InsClass) | key e' -> e where
    injectInsBy :: e ~> e'

overFreer :: (fr e a -> fr' e' b) -> ViaFreer fr e a -> ViaFreer fr' e' b
overFreer :: forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a
       (fr' :: (* -> *) -> * -> *) (e' :: * -> *) b.
(fr e a -> fr' e' b) -> ViaFreer fr e a -> ViaFreer fr' e' b
overFreer fr e a -> fr' e' b
f = forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
fr e a -> ViaFreer fr e a
ViaFreer forall b c a. (b -> c) -> (a -> b) -> a -> c
. fr e a -> fr' e' b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
ViaFreer fr e a -> fr e a
viaFreer
{-# INLINE overFreer #-}

reencodeFreer :: (Freer c fr, Freer c' fr', c (fr' f)) => fr f ~> fr' f
reencodeFreer :: forall (c :: (* -> *) -> Constraint) (fr :: (* -> *) -> * -> *)
       (c' :: (* -> *) -> Constraint) (fr' :: (* -> *) -> * -> *)
       (f :: * -> *).
(Freer c fr, Freer c' fr', c (fr' f)) =>
fr f ~> fr' f
reencodeFreer = forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (m :: * -> *) (e :: * -> *) a.
(Freer c f, c m) =>
(e ~> m) -> f e a -> m a
interpretFreer forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) a.
Freer c f =>
e a -> f e a
liftIns
{-# INLINE reencodeFreer #-}

instance (Freer c fr, InjectInsBy StateKey (State s) e, Monad (fr e)) => MonadState s (ViaFreer fr e) where
    get :: ViaFreer fr e s
get = forall {k} (key :: k) s (f :: * -> *).
SendInsBy key (State s) f =>
f s
get'' @StateKey
    put :: s -> ViaFreer fr e ()
put = forall {k} (key :: k) s (f :: * -> *).
SendInsBy key (State s) f =>
s -> f ()
put'' @StateKey
    {-# INLINE get #-}
    {-# INLINE put #-}

data StateKey

instance
    ( Freer c fr
    , InjectIns Empty e
    , InjectIns Choose e
    , Monad (fr e)
    ) =>
    Alternative (ViaFreer fr e)
    where
    empty :: forall a. ViaFreer fr e a
empty = forall a (f :: * -> *). SendIns Empty f => f a
NonDet.empty
    ViaFreer fr e a
a <|> :: forall a. ViaFreer fr e a -> ViaFreer fr e a -> ViaFreer fr e a
<|> ViaFreer fr e a
b = do
        Bool
world <- forall (f :: * -> *). SendIns Choose f => f Bool
choose
        forall a. a -> a -> Bool -> a
bool ViaFreer fr e a
a ViaFreer fr e a
b Bool
world
    {-# INLINE empty #-}
    {-# INLINE (<|>) #-}

instance
    ( Freer c fr
    , InjectIns Empty e
    , InjectIns Choose e
    , Monad (fr e)
    ) =>
    MonadPlus (ViaFreer fr e)

instance (Freer c fr, InjectIns IO e, Monad (fr e)) => MonadIO (ViaFreer fr e) where
    liftIO :: forall a. IO a -> ViaFreer fr e a
liftIO = forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
fr e a -> ViaFreer fr e a
ViaFreer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (e' :: * -> *). InjectIns e e' => e ~> e'
injectIns
    {-# INLINE liftIO #-}

instance (Freer c fr, InjectIns Fail e, Monad (fr e)) => MonadFail (ViaFreer fr e) where
    fail :: forall a. String -> ViaFreer fr e a
fail = forall (fr :: (* -> *) -> * -> *) (e :: * -> *) a.
fr e a -> ViaFreer fr e a
ViaFreer forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: (* -> *) -> * -> *)
       (e :: * -> *) a.
Freer c f =>
e a -> f e a
liftIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: * -> *) (e' :: * -> *). InjectIns e e' => e ~> e'
injectIns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> Fail a
Fail
    {-# INLINE fail #-}