2023-02-28 18:54:07 -08:00
|
|
|
module Control.Monad.Logic.Trans (SFKT, runSFKT) where
|
|
|
|
|
|
|
|
import Prelude (class Applicative, class Apply, class Bind, class Functor, class Monad, bind, pure, ($), (<<<), (>>=))
|
|
|
|
import Control.Monad.Logic.Class
|
|
|
|
|
|
|
|
import Control.MonadPlus (class MonadPlus, class Alternative, class Alt, class Plus, (<|>))
|
|
|
|
import Control.Monad.Reader.Class (class MonadReader, local, class MonadAsk, ask)
|
|
|
|
import Control.Monad.State.Class (class MonadState, state)
|
|
|
|
import Control.Monad.Trans.Class (class MonadTrans, lift)
|
2023-03-04 15:14:14 -08:00
|
|
|
import Data.Functor (map)
|
2023-02-28 18:54:07 -08:00
|
|
|
import Data.Tuple.Nested ((/\))
|
2023-03-04 15:14:14 -08:00
|
|
|
import Data.List (List(Nil), (:))
|
2023-02-28 18:54:07 -08:00
|
|
|
import Data.Maybe (Maybe(..))
|
|
|
|
|
|
|
|
type FK :: Type -> Type
|
|
|
|
type FK ans = ans
|
|
|
|
|
|
|
|
type SK :: Type -> Type -> Type
|
|
|
|
type SK ans a = a -> FK ans -> ans
|
|
|
|
|
|
|
|
newtype SFKT :: (Type -> Type) -> Type -> Type
|
|
|
|
newtype SFKT m a = SFKT (forall ans. SK (m ans) a -> FK (m ans) -> m ans)
|
|
|
|
|
2023-03-04 15:14:14 -08:00
|
|
|
unSFKT :: forall a m. SFKT m a -> forall ans. SK (m ans) a -> FK (m ans) -> m ans
|
|
|
|
unSFKT (SFKT f) = f
|
|
|
|
|
|
|
|
runSFKT :: forall a m. Applicative m => SFKT m a -> m (List a)
|
|
|
|
runSFKT (SFKT f) = f (map <<< (:)) (pure Nil)
|
2023-02-28 18:54:07 -08:00
|
|
|
|
|
|
|
instance Functor (SFKT m) where
|
2023-03-04 15:14:14 -08:00
|
|
|
map f m = SFKT (\sk -> unSFKT m (\a -> sk (f a)))
|
2023-02-28 18:54:07 -08:00
|
|
|
|
|
|
|
instance Apply m => Apply (SFKT m) where
|
2023-03-04 15:14:14 -08:00
|
|
|
apply mf ma = SFKT (\sk -> unSFKT mf (\f -> unSFKT ma (\a -> sk (f a))))
|
2023-02-28 18:54:07 -08:00
|
|
|
|
|
|
|
instance Applicative m => Applicative (SFKT m) where
|
|
|
|
pure a = SFKT (\sk fk -> sk a fk)
|
|
|
|
|
|
|
|
instance Bind m => Bind (SFKT m) where
|
2023-03-04 15:14:14 -08:00
|
|
|
bind m f = SFKT (\sk -> unSFKT m (\a -> unSFKT (f a) sk))
|
2023-02-28 18:54:07 -08:00
|
|
|
|
|
|
|
instance Monad m => Monad (SFKT m)
|
|
|
|
|
|
|
|
instance Alt (SFKT m) where
|
2023-03-04 15:14:14 -08:00
|
|
|
alt m1 m2 = SFKT (\sk fk -> unSFKT m1 sk (unSFKT m2 sk fk))
|
2023-02-28 18:54:07 -08:00
|
|
|
|
|
|
|
instance Plus (SFKT m) where
|
|
|
|
empty = SFKT (\_ fk -> fk)
|
|
|
|
|
|
|
|
instance Applicative m => Alternative (SFKT m)
|
|
|
|
|
|
|
|
instance Monad m => MonadPlus (SFKT m)
|
|
|
|
|
|
|
|
instance MonadTrans SFKT where
|
|
|
|
lift m = SFKT (\sk fk -> m >>= (\a -> sk a fk))
|
|
|
|
|
|
|
|
instance Monad m => MonadLogic (SFKT m) where
|
2023-03-04 15:14:14 -08:00
|
|
|
msplit ma = lift (unSFKT ma (\a fk -> pure (Just (a /\ (lift fk >>= reflect)))) (pure Nothing))
|
2023-02-28 18:54:07 -08:00
|
|
|
interleave m1 m2 = do
|
|
|
|
r <- msplit m1
|
|
|
|
case r of
|
|
|
|
Nothing -> m2
|
|
|
|
Just (a /\ m1') -> pure a <|> interleave m2 m1'
|
|
|
|
|
|
|
|
instance MonadAsk r m => MonadAsk r (SFKT m) where
|
|
|
|
ask = lift ask
|
|
|
|
|
|
|
|
instance MonadReader r m => MonadReader r (SFKT m) where
|
2023-03-04 15:14:14 -08:00
|
|
|
local f m = SFKT (\sk -> unSFKT m (\a -> local f <<< sk a))
|
2023-02-28 18:54:07 -08:00
|
|
|
|
|
|
|
instance MonadState s m => MonadState s (SFKT m) where
|
|
|
|
state f = lift $ state f
|