{- |
Module      :  ./Common/LogicT.hs
Description :  colimit of an arbitrary diagram in Set
Copyright   :  (c) 2005, Amr Sabry, Chung-chieh Shan, Oleg Kiselyov,
        and Daniel P. Friedman
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Mihai.Codescu@dfki.de
Stability   :  provisional
Portability :  portable

Logic Monad Transformer: MonadPlusT with interleave, bindi, ifte and once
Definition and implementation of generic operations, in terms of msplit
-}

module Common.LogicT (
  LogicT (..), bagofN, reflect
) where

import Control.Monad
import Control.Monad.Trans

class MonadTrans t => LogicT t where
    msplit :: (Monad m, MonadPlus (t m)) => t m a -> t m (Maybe (a, t m a))


    {- All other things are implemneted in terms of MonadPlus + msplit
    All the functions below have generic implementations -}

    -- fair disjunction
    interleave :: (Monad m, MonadPlus (t m)) =>
                  t m a -> t m a -> t m a
    {- Note the generic implementation below
    The code is *verbatim* from Logic.hs -}
    interleave sg1 :: t m a
sg1 sg2 :: t m a
sg2 =
        do Maybe (a, t m a)
r <- t m a -> t m (Maybe (a, t m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m (Maybe (a, t m a))
msplit t m a
sg1
           case Maybe (a, t m a)
r of
                  Nothing -> t m a
sg2
                  Just (sg11 :: a
sg11, sg12 :: t m a
sg12) -> a -> t m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
sg11 t m a -> t m a -> t m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` t m a -> t m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m a -> t m a
interleave t m a
sg2 t m a
sg12

    -- just conventional aliases
    gsuccess :: (Monad m, MonadPlus (t m)) => a -> t m a
    gsuccess = a -> t m a
forall (m :: * -> *) a. Monad m => a -> m a
return
    gfail :: (Monad m, MonadPlus (t m)) => t m a
    gfail = t m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

    {- standard `bind' is the conjunction
    the following is a fair conjunction
    Again, the old Logic.hs code works verbatim -}
    bindi :: (Monad m, MonadPlus (t m)) =>
            t m a -> (a -> t m b) -> t m b
    bindi sg :: t m a
sg g :: a -> t m b
g = do Maybe (a, t m a)
r <- t m a -> t m (Maybe (a, t m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m (Maybe (a, t m a))
msplit t m a
sg
                    case Maybe (a, t m a)
r of
                       Nothing -> t m b
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                       Just (sg1 :: a
sg1, sg2 :: t m a
sg2) -> t m b -> t m b -> t m b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m a -> t m a
interleave
                                            (a -> t m b
g a
sg1)
                                            (t m a -> (a -> t m b) -> t m b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> (a -> t m b) -> t m b
bindi t m a
sg2 a -> t m b
g)

    -- Pruning things

    {- Soft-cut (aka if-then-else)
    ifte t th el = (or (and t th) (and (not t) el))
    However, t is evaluated only once -}
    ifte :: (Monad m, MonadPlus (t m)) =>
            t m a -> (a -> t m b) -> t m b -> t m b
    ifte t :: t m a
t th :: a -> t m b
th el :: t m b
el =
        do Maybe (a, t m a)
r <- t m a -> t m (Maybe (a, t m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m (Maybe (a, t m a))
msplit t m a
t
           case Maybe (a, t m a)
r of
                  Nothing -> t m b
el
                  Just (sg1 :: a
sg1, sg2 :: t m a
sg2) -> a -> t m b
th a
sg1 t m b -> t m b -> t m b
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (t m a
sg2 t m a -> (a -> t m b) -> t m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> t m b
th)

    once :: (Monad m, MonadPlus (t m)) => t m a -> t m a
    once m :: t m a
m =
        do Maybe (a, t m a)
r <- t m a -> t m (Maybe (a, t m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m (Maybe (a, t m a))
msplit t m a
m
           case Maybe (a, t m a)
r of
                  Nothing -> t m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                  Just (sg1 :: a
sg1, _) -> a -> t m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
sg1

{- A particular transformer must define
    -- The inverse of `lift'. Hinze calls it `observe'. Others may call
    -- it `down'. It gives the first answer (or fails if there aren't any)
    observe :: (Monad m) => t m a -> m a
 It can't be put into the LogicT class because of in teh case of SRReif,
 the variable `r' will escape
-}

{- The following functions are not in the class LogicT
Their implementation is generic -}

    {- Note: the following gives t m [a] answer. To get back `m [a]'
    we should call ``observe''
    This is similar to Hinze's `sol' (at the very end of Section
    4.3, only we can select the arbitrary number of answers
    and do that even for non-stream-based monad) -}

bagofN :: (Monad m, LogicT t, MonadPlus (t m)) => Maybe Int -> t m a -> t m [a]
bagofN :: Maybe Int -> t m a -> t m [a]
bagofN (Just n :: Int
n) _ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = [a] -> t m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
bagofN n :: Maybe Int
n m :: t m a
m = t m a -> t m (Maybe (a, t m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m (Maybe (a, t m a))
msplit t m a
m t m (Maybe (a, t m a)) -> (Maybe (a, t m a) -> t m [a]) -> t m [a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe (a, t m a) -> t m [a]
forall (m :: * -> *) (t :: (* -> *) -> * -> *) a.
(Monad m, LogicT t, MonadPlus (t m)) =>
Maybe (a, t m a) -> t m [a]
bagofN'
    where bagofN' :: Maybe (a, t m a) -> t m [a]
bagofN' Nothing = [a] -> t m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
          bagofN' (Just (a :: a
a, m' :: t m a
m')) = ([a] -> [a]) -> t m [a] -> t m [a]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (t m [a] -> t m [a]) -> t m [a] -> t m [a]
forall a b. (a -> b) -> a -> b
$ Maybe Int -> t m a -> t m [a]
forall (m :: * -> *) (t :: (* -> *) -> * -> *) a.
(Monad m, LogicT t, MonadPlus (t m)) =>
Maybe Int -> t m a -> t m [a]
bagofN ((Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((-1) Int -> Int -> Int
forall a. Num a => a -> a -> a
+) Maybe Int
n) t m a
m'


    {- This is like the opposite of `msplit'
    The law is: msplit tm >>= reflect === tm -}
reflect :: (Monad m, LogicT t, MonadPlus (t m)) => Maybe (a, t m a) -> t m a
reflect :: Maybe (a, t m a) -> t m a
reflect r :: Maybe (a, t m a)
r = case Maybe (a, t m a)
r of
                   Nothing -> t m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                   Just (a :: a
a, tmr :: t m a
tmr) -> a -> t m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a t m a -> t m a -> t m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` t m a
tmr