content: {-# LANGUAGE Safe #-}
  {-# LANGUAGE ViewPatterns #-}
  {-# LANGUAGE LambdaCase #-}
  
  -- | Logic primitives. See @LogicT@ paper for details.
  --
  -- * [@LogicT@] [LogicT - backtracking monad transformer with fair operations and pruning](http://okmij.org/ftp/Computation/monads.html#LogicT)
  module Control.Eff.Logic.Core where
  
  import Control.Monad
  
  import Control.Eff
  import Control.Eff.Exception
  
  import Data.Function (fix)
  
  -- | The MSplit primitive from LogicT paper.
  class MSplit m where
    -- | The laws for 'msplit' are:
    --
    -- > msplit mzero                = return Nothing
    -- > msplit (return a `mplus` m) = return (Just(a, m))
    msplit :: m a -> m (Maybe (a, m a))
  
  -- | Embed a pure value into MSplit
  {-# INLINE withMSplit #-}
  withMSplit :: MonadPlus m => a -> m a -> m (Maybe (a, m a))
  withMSplit a rest = return (Just (a, rest))
  -- The handlers are defined in terms of the specific non-determinism
  -- effects (instead of by way of a distinct MSplit handler
  
  -- | Laws for 'reflect':
  --
  -- > msplit (lift m >> mzero)   >>= reflect = lift m >> mzero
  -- > msplit (lift m `mplus` ma) >>= reflect = lift m `mplus` (msplit ma >>= reflect)
  {-# INLINE reflect #-}
  reflect :: MonadPlus m => Maybe (a, m a) -> m a
  reflect Nothing      = mzero
  reflect (Just (a,m)) = return a `mplus` m
  
  -- Other committed choice primitives can be implemented in terms of msplit
  -- The following implementations are directly from the LogicT paper
  
  -- | Soft-cut: non-deterministic if-then-else, aka Prolog's @*->@
  -- Declaratively,
  --
  -- >  ifte t th el = (t >>= th) `mplus` ((not t) >> el)
  --
  -- However, @t@ is evaluated only once. In other words, @ifte t th el@
  -- is equivalent to @t >>= th@ if @t@ has at least one solution.
  -- If @t@ fails, @ifte t th el@ is the same as @el@. Laws:
  --
  -- > ifte (return a) th el           = th a
  -- > ifte mzero th el                = el
  -- > ifte (return a `mplus` m) th el = th a `mplus` (m >>= th)
  ifte :: (MonadPlus m, MSplit m)
       => m t -> (t -> m b) -> m b -> m b
  ifte t th el = msplit t >>= check
   where check Nothing          = el
         check (Just (sg1,sg2)) = (th sg1) `mplus` (sg2 >>= th)
  
  -- | Another pruning operation (ifte is the other). This selects one
  -- solution out of possibly many.
  once :: (MSplit m, MonadPlus m) => m b -> m b
  once m = msplit m >>= check
   where check Nothing        = mzero
         check (Just (sg1,_)) = return sg1
  
  -- | Negation as failure
  gnot :: (MonadPlus m, MSplit m) => m b -> m ()
  gnot m = ifte (once m) (const mzero) (return ())
  
  -- | Fair (i.e., avoids starvation) disjunction. It obeys the
  -- following laws:
  --
  -- > interleave mzero m                  = m
  -- > interleave (return a `mplus` m1) m2 = return a `mplus` (interleave m2 m1)
  --
  -- corollary:
  --
  -- > interleave m mzero = m
  interleave :: (MSplit m, MonadPlus m) => m b -> m b -> m b
  interleave sg1 sg2 =
    do r <- msplit sg1
       case r of
         Nothing -> sg2
         Just (sg11,sg12) ->
           (return sg11) `mplus` (interleave sg2 sg12)
  
  -- | Fair (i.e., avoids starvation) conjunction. It obeys the
  -- following laws:
  --
  -- > mzero                >>- k = mzero
  -- > (return a `mplus` m) >>- k = interleave (k a) (m >>- k)
  (>>-) :: (MonadPlus m, MSplit m) => m a -> (a -> m b) -> m b
  sg >>- g =
    do r <- msplit sg
       case r of
         Nothing -> mzero
         Just (sg1 ,sg2) -> interleave (g sg1) (sg2 >>- g)
  
  -- | Collect all solutions. This is from Hinze's @Backtr@ monad
  -- class. Unsurprisingly, this can be implemented in terms of msplit.
  sols :: (Monad m, MSplit m) => m a -> m [a]
  sols m = (msplit m) >>= (fix step) [] where
    step _ jq Nothing          = return jq
    step next jq (Just(a, ma)) = (msplit ma) >>= next (a:jq)
  
  -- | Non-determinism with control (@cut@).
  --
  -- For the explanation of cut, see Section 5 of Hinze ICFP 2000 paper:
  --
  -- * [@Backtr@] [Deriving Backtracking Monad Transformers](https://dl.acm.org/citation.cfm?id=351240.351258)
  --
  -- Hinze suggests expressing @cut@ in terms of @cutfalse@:
  --
  -- > = return () `mplus` cutfalse
  -- > where
  -- >  cutfalse :: m a
  --
  -- satisfies the following laws:
  --
  -- >  cutfalse >>= k  = cutfalse              (F1)
  -- >  cutfalse | m    = cutfalse              (F2)
  --
  -- (note: @m \``mplus`\` cutfalse@ is different from @cutfalse \``mplus`\` m@).
  -- In other words, cutfalse is the left zero of both bind and mplus.
  --
  -- Hinze also introduces the operation @`call` :: m a -> m a@ that
  -- delimits the effect of cut: @`call` m@ executes m. If the cut is
  -- invoked in m, it discards only the choices made since m was called.
  -- Hinze postulates the axioms of `call`:
  --
  -- >  call false = false                          (C1)
  -- >  call (return a | m) = return a | call m     (C2)
  -- >  call (m | cutfalse) = call m                (C3)
  -- >  call (lift m >>= k) = lift m >>= (call . k) (C4)
  --
  -- @`call` m@ behaves like @m@ except any cut inside @m@ has only a local effect,
  -- he says.
  --
  -- Hinze noted a problem with the \"mechanical\" derivation of backtracing
  -- monad transformer with cut: no axiom specifying the interaction of
  -- call with bind; no way to simplify nested invocations of call.
  class Call r where
    -- | Mapping @Backtr@ interface to 'MonadPlus' and using exceptions for
    -- @cutfalse@, every instance should ensure that the following laws hold:
    --
    -- >  cutfalse `mplus` m        = cutfalse                --(F2)
    -- >  call mzero                = mzero                   --(C1)
    -- >  call (return a `mplus` m) = return a `mplus` call m --(C2)
    -- >  call (m `mplus` cutfalse) = call m                  --(C3)
    -- >  call (lift m >>= k)       = lift m >>= (call . k)   --(C4)
    call :: MonadPlus (Eff r) => Eff (Exc CutFalse : r) a -> Eff r a
  
  data CutFalse = CutFalse
  
  -- | We use exceptions for cutfalse
  -- Therefore, the law @cutfalse >>= k = cutfalse@
  -- is satisfied automatically since all exceptions have the above property.
  cutfalse :: Member (Exc CutFalse) r => Eff r a
  cutfalse = throwError CutFalse
  
  -- | Prolog @cut@, taken from Hinze 2000 (Deriving backtracking monad
  -- transformers).
  (!) :: (Member (Exc CutFalse) r, MonadPlus (Eff r)) => Eff r ()
  (!) = return () `mplus` cutfalse
  
  -- | Case analysis for lists
  {-# INLINE list #-}
  list :: b -> (a -> [a] -> b)
       -> [a] -> b
  list z _ [] = z
  list _ k (h:t) = k h t
  