{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Eff.NdetEff (
NdetEff
, withNdetEff
, left, right
, makeChoiceA
, makeChoiceA0
, makeChoiceLst
, msplit1
, module Control.Eff.Logic
) where
import Control.Eff
import Control.Eff.Extend
import Control.Eff.Logic
import Control.Applicative
import Control.Monad
import Control.Monad.Base
import Control.Monad.Trans.Control
import Data.Foldable (foldl')
data NdetEff a where
MZero :: NdetEff a
MPlus :: NdetEff Bool
withNdetEff :: Alternative f => Monad m => a -> m (f a)
withNdetEff = return . pure
left :: (Bool -> k) -> k
left k = k True
right :: (Bool -> k) -> k
right k = k False
instance (Alternative f, Monad m) => Handle NdetEff (m (f a)) where
handle _ MZero = return empty
handle k MPlus = liftM2 (<|>) (left k) (right k)
instance Member NdetEff r => Alternative (Eff r) where
empty = mzero
(<|>) = mplus
instance Member NdetEff r => MonadPlus (Eff r) where
mzero = send MZero
mplus m1 m2 = send MPlus >>= \x -> if x then m1 else m2
instance ( MonadBase m m
, LiftedBase m r
) => MonadBaseControl m (Eff (NdetEff ': r)) where
type StM (Eff (NdetEff ': r)) a = StM (Eff r) [a]
liftBaseWith f = raise $ liftBaseWith $ \runInBase ->
f (runInBase . makeChoiceLst)
restoreM x = do lst :: [a] <- raise (restoreM x)
foldl' (\r a -> r <|> pure a) mzero lst
makeChoiceA0 :: Alternative f => Eff (NdetEff ': r) a -> Eff r (f a)
makeChoiceA0 = handle_relay withNdetEff
makeChoiceA :: Alternative f => Eff (NdetEff ': r) a -> Eff r (f a)
makeChoiceA m = loop [] m where
loop [] (Val x) = withNdetEff x
loop (h:t) (Val x) = liftM2 (<|>) (withNdetEff x) (loop t h)
loop jq (E q u) = case decomp u of
Right MZero -> case jq of
[] -> return empty
(h:t) -> loop t h
Right MPlus -> loop (q ^$ False : jq) (q ^$ True)
Left u0 -> E (q ^|$^ (loop jq)) u0
makeChoiceLst :: Eff (NdetEff ': r) a -> Eff r [a]
makeChoiceLst = makeChoiceA
instance Member NdetEff r => MSplit (Eff r) where
msplit = respond_relay (flip withMSplit empty) $ \k x -> case x of
MZero -> return Nothing
MPlus -> left k >>= \r -> case r of
Nothing -> right k
Just(a, m) -> withMSplit a (m <|> (right k >>= reflect))
msplit1 :: Member NdetEff r => Eff r a -> Eff r (Maybe (a, Eff r a))
msplit1 = loop []
where
loop [] (Val x) = withMSplit x mzero
loop jq (Val x) = withMSplit x (msum jq)
loop jq (E q u) = case prj u of
Just MZero -> case jq of
[] -> return Nothing
(j:jqT) -> loop jqT j
Just MPlus -> loop ((q ^$ False):jq) (q ^$ True)
_ -> E (q ^|$^ (loop jq)) u