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)
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 #-}
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 #-}
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)
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)
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
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
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))
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