content: {- |
  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 sg2 =
          do r <- msplit sg1
             case r of
                    Nothing -> sg2
                    Just (sg11, sg12) -> return sg11 `mplus` interleave sg2 sg12
  
      -- just conventional aliases
      gsuccess :: (Monad m, MonadPlus (t m)) => a -> t m a
      gsuccess = return
      gfail :: (Monad m, MonadPlus (t m)) => t m a
      gfail = 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 g = do r <- msplit sg
                      case r of
                         Nothing -> mzero
                         Just (sg1, sg2) -> interleave
                                              (g sg1)
                                              (bindi sg2 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 th el =
          do r <- msplit t
             case r of
                    Nothing -> el
                    Just (sg1, sg2) -> th sg1 `mplus` (sg2 >>= th)
  
      once :: (Monad m, MonadPlus (t m)) => t m a -> t m a
      once m =
          do r <- msplit m
             case r of
                    Nothing -> mzero
                    Just (sg1, _) -> return 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 (Just n) _ | n <= 0 = return []
  bagofN n m = msplit m >>= bagofN'
      where bagofN' Nothing = return []
            bagofN' (Just (a, m')) = liftM (a :) $ bagofN (fmap ((-1) +) n) 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 r = case r of
                     Nothing -> mzero
                     Just (a, tmr) -> return a `mplus` tmr
  