-- 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) 2024 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable
-}
module Control.Effect.Interpreter.Heftia.NonDet where

import Control.Applicative (Alternative ((<|>)), empty, liftA2, (<|>))
import Control.Arrow ((>>>))
import Control.Effect (type (~>))
import Control.Effect.Hefty (Eff, injectF, interpretFin, interpretFinH, interpretK, interpretRecH)
import Control.Freer (Freer)
import Control.Monad.Freer (MonadFreer)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT), runMaybeT)
import Data.Bool (bool)
import Data.Effect.HFunctor (HFunctor)
import Data.Effect.NonDet (Choose (Choose), ChooseH (ChooseH), Empty (Empty), LChoose, LEmpty, choose)
import Data.Functor.Compose (Compose (Compose), getCompose)
import Data.Hefty.Union (ForallHFunctor, HFunctorUnion, Member, Union)

-- | 'NonDet' effects handler for Monad use.
runNonDet ::
    forall f ef a fr u c.
    ( Alternative f
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] ef)
    , c (Eff u fr '[] (LEmpty : ef))
    ) =>
    Eff u fr '[] (LChoose ': LEmpty ': ef) a ->
    Eff u fr '[] ef (f a)
runNonDet :: forall (f :: * -> *) (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 c (Eff u fr '[] (LEmpty : ef))) =>
Eff u fr '[] (LChoose : LEmpty : ef) a -> Eff u fr '[] ef (f a)
runNonDet =
    forall (f :: * -> *) (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
Eff u fr '[] (LChoose : ef) a -> Eff u fr '[] ef (f a)
runChoose forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: SigClass) (rs :: [SigClass]) r a (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(a -> Eff u fr ehs rs r)
-> (forall x.
    (x -> Eff u fr ehs rs r)
    -> UnliftIfSingle e x -> Eff u fr ehs rs r)
-> Eff u fr '[] (e : rs) a
-> Eff u fr ehs rs r
interpretK forall (f :: * -> *) a. Applicative f => a -> f a
pure \x -> Eff u fr '[] ef (f a)
_ Empty x
UnliftIfSingle LEmpty x
Empty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Alternative f => f a
empty
{-# INLINE runNonDet #-}

-- | 'NonDet' effects handler for Monad use.
runNonDetK ::
    forall r ef a fr u c.
    ( Monoid r
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] ef)
    , c (Eff u fr '[] (LEmpty ': ef))
    , HFunctor (u '[])
    ) =>
    (a -> Eff u fr '[] (LEmpty ': ef) r) ->
    Eff u fr '[] (LChoose ': LEmpty ': ef) a ->
    Eff u fr '[] ef r
runNonDetK :: forall r (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Monoid r, MonadFreer c fr, Union u, c (Eff u fr '[] ef),
 c (Eff u fr '[] (LEmpty : ef)), HFunctor (u '[])) =>
(a -> Eff u fr '[] (LEmpty : ef) r)
-> Eff u fr '[] (LChoose : LEmpty : ef) a -> Eff u fr '[] ef r
runNonDetK a -> Eff u fr '[] (LEmpty : ef) r
f =
    forall r (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Semigroup r, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
(a -> Eff u fr '[] ef r)
-> Eff u fr '[] (LChoose : ef) a -> Eff u fr '[] ef r
runChooseK a -> Eff u fr '[] (LEmpty : ef) r
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (e :: SigClass) (rs :: [SigClass]) r a (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(a -> Eff u fr ehs rs r)
-> (forall x.
    (x -> Eff u fr ehs rs r)
    -> UnliftIfSingle e x -> Eff u fr ehs rs r)
-> Eff u fr '[] (e : rs) a
-> Eff u fr ehs rs r
interpretK forall (f :: * -> *) a. Applicative f => a -> f a
pure \x -> Eff u fr '[] ef r
_ Empty x
UnliftIfSingle LEmpty x
Empty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty
{-# INLINE runNonDetK #-}

-- | 'Choose' effect handler for Monad use.
runChoose ::
    forall f ef a fr u c.
    ( Alternative f
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] ef)
    ) =>
    Eff u fr '[] (LChoose ': ef) a ->
    Eff u fr '[] ef (f a)
runChoose :: forall (f :: * -> *) (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
Eff u fr '[] (LChoose : ef) a -> Eff u fr '[] ef (f a)
runChoose =
    forall (e :: SigClass) (rs :: [SigClass]) r a (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(a -> Eff u fr ehs rs r)
-> (forall x.
    (x -> Eff u fr ehs rs r)
    -> UnliftIfSingle e x -> Eff u fr ehs rs r)
-> Eff u fr '[] (e : rs) a
-> Eff u fr ehs rs r
interpretK (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure) \x -> Eff u fr '[] ef (f a)
k Choose x
UnliftIfSingle LChoose x
Choose ->
        forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (x -> Eff u fr '[] ef (f a)
k Bool
False) (x -> Eff u fr '[] ef (f a)
k Bool
True)

-- | 'Choose' effect handler for Monad use.
runChooseK ::
    forall r ef a fr u c.
    ( Semigroup r
    , MonadFreer c fr
    , Union u
    , c (Eff u fr '[] ef)
    ) =>
    (a -> Eff u fr '[] ef r) ->
    Eff u fr '[] (LChoose ': ef) a ->
    Eff u fr '[] ef r
runChooseK :: forall r (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Semigroup r, MonadFreer c fr, Union u, c (Eff u fr '[] ef)) =>
(a -> Eff u fr '[] ef r)
-> Eff u fr '[] (LChoose : ef) a -> Eff u fr '[] ef r
runChooseK a -> Eff u fr '[] ef r
f =
    forall (e :: SigClass) (rs :: [SigClass]) r a (ehs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(MonadFreer c fr, Union u, HeadIns e, c (Eff u fr ehs rs)) =>
(a -> Eff u fr ehs rs r)
-> (forall x.
    (x -> Eff u fr ehs rs r)
    -> UnliftIfSingle e x -> Eff u fr ehs rs r)
-> Eff u fr '[] (e : rs) a
-> Eff u fr ehs rs r
interpretK a -> Eff u fr '[] ef r
f \x -> Eff u fr '[] ef r
k Choose x
UnliftIfSingle LChoose x
Choose ->
        forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. Semigroup a => a -> a -> a
(<>) (x -> Eff u fr '[] ef r
k Bool
False) (x -> Eff u fr '[] ef r
k Bool
True)

-- | 'Empty' effect handler for Monad use.
runEmpty ::
    forall a r fr u c.
    ( Freer c fr
    , Union u
    , Applicative (Eff u fr '[] r)
    , c (MaybeT (Eff u fr '[] r))
    ) =>
    Eff u fr '[] (LEmpty ': r) a ->
    Eff u fr '[] r (Maybe a)
runEmpty :: forall a (r :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, Applicative (Eff u fr '[] r),
 c (MaybeT (Eff u fr '[] r))) =>
Eff u fr '[] (LEmpty : r) a -> Eff u fr '[] r (Maybe a)
runEmpty =
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: SigClass) (r :: [SigClass]) (f :: * -> *)
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e, c f) =>
(u r Nop ~> f)
-> (UnliftIfSingle e ~> f) -> Eff u fr '[] (e : r) ~> f
interpretFin
        (forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
        \Empty x
UnliftIfSingle LEmpty x
Empty -> forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

{- | 'ChooseH' effect handler for Monad use.

    Convert a higher-order effect of the form

        @chooseH :: m a -> m a -> m a@

    into a first-order effect of the form:

        @choose :: m Bool@
-}
runChooseH ::
    ( Freer c fr
    , HFunctorUnion u
    , Member u Choose ef
    , ForallHFunctor u eh
    , Monad (Eff u fr eh ef)
    ) =>
    Eff u fr (ChooseH ': eh) ef ~> Eff u fr eh ef
runChooseH :: forall (c :: (* -> *) -> Constraint) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (ef :: [SigClass])
       (eh :: [SigClass]).
(Freer c fr, HFunctorUnion u, Member u Choose ef,
 ForallHFunctor u eh, Monad (Eff u fr eh ef)) =>
Eff u fr (ChooseH : eh) ef ~> Eff u fr eh ef
runChooseH =
    forall (e :: SigClass) (rs :: [SigClass]) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HFunctor e, HFunctor (u rs),
 HFunctor (u (e : rs))) =>
(e (Eff u fr rs efs) ~> Eff u fr rs efs)
-> Eff u fr (e : rs) efs ~> Eff u fr rs efs
interpretRecH \(ChooseH Eff u fr eh ef x
a Eff u fr eh ef x
b) -> do
        Bool
world <- forall (f :: * -> *). SendIns Choose f => f Bool
choose
        forall a. a -> a -> Bool -> a
bool Eff u fr eh ef x
a Eff u fr eh ef x
b Bool
world

-- | 'NonDet' effect handler for Applicative use.
runNonDetA ::
    forall f ef a fr u c.
    ( Alternative f
    , Freer c fr
    , Union u
    , Applicative (Eff u fr '[] ef)
    , c (Compose (Eff u fr '[] ef) f)
    ) =>
    Eff u fr '[ChooseH] (LEmpty ': ef) a ->
    Eff u fr '[] ef (f a)
runNonDetA :: forall (f :: * -> *) (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, Freer c fr, Union u, Applicative (Eff u fr '[] ef),
 c (Compose (Eff u fr '[] ef) f)) =>
Eff u fr '[ChooseH] (LEmpty : ef) a -> Eff u fr '[] ef (f a)
runNonDetA =
    forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: SigClass) (f :: * -> *) (efs :: [SigClass])
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, c f) =>
(u efs Nop ~> f)
-> (e (Eff u fr '[e] efs) ~> f) -> Eff u fr '[e] efs ~> f
interpretFinH
            (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a (r :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, Freer c fr, Union u, Applicative (Eff u fr '[] r),
 c (Compose (Eff u fr '[] r) f)) =>
Eff u fr '[] (LEmpty : r) a -> Eff u fr '[] r (f a)
runEmptyA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
            (\(ChooseH Eff u fr '[ChooseH] (LEmpty : ef) x
a Eff u fr '[ChooseH] (LEmpty : ef) x
b) -> forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (forall (f :: * -> *) (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, Freer c fr, Union u, Applicative (Eff u fr '[] ef),
 c (Compose (Eff u fr '[] ef) f)) =>
Eff u fr '[ChooseH] (LEmpty : ef) a -> Eff u fr '[] ef (f a)
runNonDetA Eff u fr '[ChooseH] (LEmpty : ef) x
a) (forall (f :: * -> *) (ef :: [SigClass]) a (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, Freer c fr, Union u, Applicative (Eff u fr '[] ef),
 c (Compose (Eff u fr '[] ef) f)) =>
Eff u fr '[ChooseH] (LEmpty : ef) a -> Eff u fr '[] ef (f a)
runNonDetA Eff u fr '[ChooseH] (LEmpty : ef) x
b))

-- | 'Empty' effect handler for Applicative use.
runEmptyA ::
    forall f a r fr u c.
    ( Alternative f
    , Freer c fr
    , Union u
    , Applicative (Eff u fr '[] r)
    , c (Compose (Eff u fr '[] r) f)
    ) =>
    Eff u fr '[] (LEmpty ': r) a ->
    Eff u fr '[] r (f a)
runEmptyA :: forall (f :: * -> *) a (r :: [SigClass]) (fr :: SigClass)
       (u :: [SigClass] -> SigClass) (c :: (* -> *) -> Constraint).
(Alternative f, Freer c fr, Union u, Applicative (Eff u fr '[] r),
 c (Compose (Eff u fr '[] r) f)) =>
Eff u fr '[] (LEmpty : r) a -> Eff u fr '[] r (f a)
runEmptyA =
    forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e :: SigClass) (r :: [SigClass]) (f :: * -> *)
       (fr :: SigClass) (u :: [SigClass] -> SigClass)
       (c :: (* -> *) -> Constraint).
(Freer c fr, Union u, HeadIns e, c f) =>
(u r Nop ~> f)
-> (UnliftIfSingle e ~> f) -> Eff u fr '[] (e : r) ~> f
interpretFin
            (forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: (* -> *) -> Constraint) (f :: SigClass)
       (u :: [SigClass] -> SigClass) (efs :: [SigClass])
       (ehs :: [SigClass]).
Freer c f =>
u efs Nop ~> Eff u f ehs efs
injectF)
            \Empty x
UnliftIfSingle LEmpty x
Empty -> forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Alternative f => f a
empty