{-# LANGUAGE CPP #-}

-- 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 Sayo Koyoneda
License     :  MPL-2.0 (see the LICENSE file)
Maintainer  :  ymdfield@outlook.jp
Portability :  portable
-}
module Control.Monad.Hefty.NonDet where

import Control.Applicative (Alternative ((<|>)), empty, (<|>))
#if ( __GLASGOW_HASKELL__ < 906 )
import Control.Applicative (liftA2)
#endif
import Control.Arrow ((>>>))
import Control.Monad.Hefty (
    Eff,
    bundleN,
    interpretBy,
    interpretH,
    nil,
    (!+),
    type (<|),
    type (~>),
 )
import Data.Bool (bool)
import Data.Effect.NonDet (Choose (Choose), ChooseH (ChooseH), Empty (Empty), choose)

-- | 'NonDet' effects handler for alternative answer type.
runNonDet
    :: forall f ef a
     . (Alternative f)
    => Eff '[] (Choose ': Empty ': ef) a
    -> Eff '[] ef (f a)
runNonDet :: forall (f :: * -> *) (ef :: [* -> *]) a.
Alternative f =>
Eff '[] (Choose : Empty : ef) a -> Eff '[] ef (f a)
runNonDet =
    forall (len :: Nat) (ef :: [* -> *]) (eh :: [EffectH]).
KnownNat len =>
Eff eh ef ~> Eff eh (Union (Take len ef) : Drop len ef)
bundleN @2
        (Eff '[] (Choose : Empty : ef) a
 -> Eff '[] (Union '[Choose, Empty] : ef) a)
-> (Eff '[] (Union '[Choose, Empty] : ef) a -> Eff '[] ef (f a))
-> Eff '[] (Choose : Empty : ef) a
-> Eff '[] ef (f a)
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (a -> Eff '[] ef (f a))
-> Interpreter (Union '[Choose, Empty]) (Eff '[] ef) (f a)
-> Eff '[] (Union '[Choose, Empty] : ef) a
-> Eff '[] ef (f a)
forall (e :: * -> *) (ef :: [* -> *]) ans a.
(a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
interpretBy
            (f a -> Eff '[] ef (f a)
forall a. a -> Eff '[] ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (f a -> Eff '[] ef (f a)) -> (a -> f a) -> a -> Eff '[] ef (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
            ( (\Choose x
Choose x -> Eff '[] ef (f a)
k -> (f a -> f a -> f a)
-> Eff '[] ef (f a) -> Eff '[] ef (f a) -> Eff '[] ef (f a)
forall a b c.
(a -> b -> c) -> Eff '[] ef a -> Eff '[] ef b -> Eff '[] ef c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f a -> f a -> f a
forall a. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (x -> Eff '[] ef (f a)
k x
Bool
False) (x -> Eff '[] ef (f a)
k x
Bool
True))
                (Choose x -> (x -> Eff '[] ef (f a)) -> Eff '[] ef (f a))
-> (Union '[Empty] x
    -> (x -> Eff '[] ef (f a)) -> Eff '[] ef (f a))
-> Union '[Choose, Empty] x
-> (x -> Eff '[] ef (f a))
-> Eff '[] ef (f a)
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ (\Empty x
Empty x -> Eff '[] ef (f a)
_ -> f a -> Eff '[] ef (f a)
forall a. a -> Eff '[] ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure f a
forall a. f a
forall (f :: * -> *) a. Alternative f => f a
empty)
                (Empty x -> (x -> Eff '[] ef (f a)) -> Eff '[] ef (f a))
-> (Union '[] x -> (x -> Eff '[] ef (f a)) -> Eff '[] ef (f a))
-> Union '[Empty] x
-> (x -> Eff '[] ef (f a))
-> Eff '[] ef (f a)
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ Union '[] x -> (x -> Eff '[] ef (f a)) -> Eff '[] ef (f a)
forall a r. Union '[] a -> r
nil
            )

-- | 'NonDet' effects handler for monoidal answer type.
runNonDetMonoid
    :: forall ans ef a
     . (Monoid ans)
    => (a -> Eff '[] ef ans)
    -> Eff '[] (Choose ': Empty ': ef) a
    -> Eff '[] ef ans
runNonDetMonoid :: forall ans (ef :: [* -> *]) a.
Monoid ans =>
(a -> Eff '[] ef ans)
-> Eff '[] (Choose : Empty : ef) a -> Eff '[] ef ans
runNonDetMonoid a -> Eff '[] ef ans
f =
    forall (len :: Nat) (ef :: [* -> *]) (eh :: [EffectH]).
KnownNat len =>
Eff eh ef ~> Eff eh (Union (Take len ef) : Drop len ef)
bundleN @2
        (Eff '[] (Choose : Empty : ef) a
 -> Eff '[] (Union '[Choose, Empty] : ef) a)
-> (Eff '[] (Union '[Choose, Empty] : ef) a -> Eff '[] ef ans)
-> Eff '[] (Choose : Empty : ef) a
-> Eff '[] ef ans
forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (a -> Eff '[] ef ans)
-> Interpreter (Union '[Choose, Empty]) (Eff '[] ef) ans
-> Eff '[] (Union '[Choose, Empty] : ef) a
-> Eff '[] ef ans
forall (e :: * -> *) (ef :: [* -> *]) ans a.
(a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
interpretBy
            a -> Eff '[] ef ans
f
            ( (\Choose x
Choose x -> Eff '[] ef ans
k -> (ans -> ans -> ans)
-> Eff '[] ef ans -> Eff '[] ef ans -> Eff '[] ef ans
forall a b c.
(a -> b -> c) -> Eff '[] ef a -> Eff '[] ef b -> Eff '[] ef c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ans -> ans -> ans
forall a. Semigroup a => a -> a -> a
(<>) (x -> Eff '[] ef ans
k x
Bool
False) (x -> Eff '[] ef ans
k x
Bool
True))
                (Choose x -> (x -> Eff '[] ef ans) -> Eff '[] ef ans)
-> (Union '[Empty] x -> (x -> Eff '[] ef ans) -> Eff '[] ef ans)
-> Union '[Choose, Empty] x
-> (x -> Eff '[] ef ans)
-> Eff '[] ef ans
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ (\Empty x
Empty x -> Eff '[] ef ans
_ -> ans -> Eff '[] ef ans
forall a. a -> Eff '[] ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ans
forall a. Monoid a => a
mempty)
                (Empty x -> (x -> Eff '[] ef ans) -> Eff '[] ef ans)
-> (Union '[] x -> (x -> Eff '[] ef ans) -> Eff '[] ef ans)
-> Union '[Empty] x
-> (x -> Eff '[] ef ans)
-> Eff '[] ef ans
forall (e :: * -> *) a r (es :: [* -> *]).
(e a -> r) -> (Union es a -> r) -> Union (e : es) a -> r
!+ Union '[] x -> (x -> Eff '[] ef ans) -> Eff '[] ef ans
forall a r. Union '[] a -> r
nil
            )

-- | 'Choose' effect handler for alternative answer type.
runChoose
    :: forall f ef a
     . (Alternative f)
    => Eff '[] (Choose ': ef) a
    -> Eff '[] ef (f a)
runChoose :: forall (f :: * -> *) (ef :: [* -> *]) a.
Alternative f =>
Eff '[] (Choose : ef) a -> Eff '[] ef (f a)
runChoose =
    (a -> Eff '[] ef (f a))
-> Interpreter Choose (Eff '[] ef) (f a)
-> Eff '[] (Choose : ef) a
-> Eff '[] ef (f a)
forall (e :: * -> *) (ef :: [* -> *]) ans a.
(a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
interpretBy (f a -> Eff '[] ef (f a)
forall a. a -> Eff '[] ef a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (f a -> Eff '[] ef (f a)) -> (a -> f a) -> a -> Eff '[] ef (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) \Choose x
Choose x -> Eff '[] ef (f a)
k ->
        (f a -> f a -> f a)
-> Eff '[] ef (f a) -> Eff '[] ef (f a) -> Eff '[] ef (f a)
forall a b c.
(a -> b -> c) -> Eff '[] ef a -> Eff '[] ef b -> Eff '[] ef c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f a -> f a -> f a
forall a. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (x -> Eff '[] ef (f a)
k x
Bool
False) (x -> Eff '[] ef (f a)
k x
Bool
True)

-- | 'Choose' effect handler for monoidal answer type.
runChooseMonoid
    :: forall ans ef a
     . (Semigroup ans)
    => (a -> Eff '[] ef ans)
    -> Eff '[] (Choose ': ef) a
    -> Eff '[] ef ans
runChooseMonoid :: forall ans (ef :: [* -> *]) a.
Semigroup ans =>
(a -> Eff '[] ef ans) -> Eff '[] (Choose : ef) a -> Eff '[] ef ans
runChooseMonoid a -> Eff '[] ef ans
f =
    (a -> Eff '[] ef ans)
-> Interpreter Choose (Eff '[] ef) ans
-> Eff '[] (Choose : ef) a
-> Eff '[] ef ans
forall (e :: * -> *) (ef :: [* -> *]) ans a.
(a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
interpretBy a -> Eff '[] ef ans
f \Choose x
Choose x -> Eff '[] ef ans
k ->
        (ans -> ans -> ans)
-> Eff '[] ef ans -> Eff '[] ef ans -> Eff '[] ef ans
forall a b c.
(a -> b -> c) -> Eff '[] ef a -> Eff '[] ef b -> Eff '[] ef c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ans -> ans -> ans
forall a. Semigroup a => a -> a -> a
(<>) (x -> Eff '[] ef ans
k x
Bool
False) (x -> Eff '[] ef ans
k x
Bool
True)

-- | 'Empty' effect handler.
runEmpty :: forall a r. Eff '[] (Empty ': r) a -> Eff '[] r (Maybe a)
runEmpty :: forall a (r :: [* -> *]).
Eff '[] (Empty : r) a -> Eff '[] r (Maybe a)
runEmpty =
    (a -> Eff '[] r (Maybe a))
-> Interpreter Empty (Eff '[] r) (Maybe a)
-> Eff '[] (Empty : r) a
-> Eff '[] r (Maybe a)
forall (e :: * -> *) (ef :: [* -> *]) ans a.
(a -> Eff '[] ef ans)
-> Interpreter e (Eff '[] ef) ans
-> Eff '[] (e : ef) a
-> Eff '[] ef ans
interpretBy
        (Maybe a -> Eff '[] r (Maybe a)
forall a. a -> Eff '[] r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe a -> Eff '[] r (Maybe a))
-> (a -> Maybe a) -> a -> Eff '[] r (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just)
        \Empty x
Empty x -> Eff '[] r (Maybe a)
_ -> Maybe a -> Eff '[] r (Maybe a)
forall a. a -> Eff '[] r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing

{- | 'ChooseH' effect elaborator.

    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
    :: (Choose <| ef)
    => Eff (ChooseH ': eh) ef ~> Eff eh ef
runChooseH :: forall (ef :: [* -> *]) (eh :: [EffectH]).
(Choose <| ef) =>
Eff (ChooseH : eh) ef ~> Eff eh ef
runChooseH = (ChooseH ~~> Eff eh ef) -> Eff (ChooseH : eh) ef ~> Eff eh ef
forall (e :: EffectH) (eh :: [EffectH]) (ef :: [* -> *]).
HFunctor e =>
(e ~~> Eff eh ef) -> Eff (e : eh) ef ~> Eff eh ef
interpretH \(ChooseH Eff eh ef x
a Eff eh ef x
b) -> Eff eh ef x -> Eff eh ef x -> Eff eh ef x
forall (ef :: [* -> *]) (eh :: [EffectH]) a.
(Choose <| ef) =>
Eff eh ef a -> Eff eh ef a -> Eff eh ef a
branch Eff eh ef x
a Eff eh ef x
b

-- | Faster than `<|>`.
branch :: (Choose <| ef) => Eff eh ef a -> Eff eh ef a -> Eff eh ef a
branch :: forall (ef :: [* -> *]) (eh :: [EffectH]) a.
(Choose <| ef) =>
Eff eh ef a -> Eff eh ef a -> Eff eh ef a
branch Eff eh ef a
a Eff eh ef a
b = do
    Bool
world <- Eff eh ef Bool
forall (f :: * -> *). SendFOE Choose f => f Bool
choose
    Eff eh ef a -> Eff eh ef a -> Bool -> Eff eh ef a
forall a. a -> a -> Bool -> a
bool Eff eh ef a
a Eff eh ef a
b Bool
world
{-# INLINE branch #-}