{-# LANGUAGE RankNTypes #-}
{- |
Module      :  ./Common/SFKT.hs
Copyright   :  (c) 2005, Amr Sabry, Chung-chieh Shan, Oleg Kiselyov
                and Daniel P. Friedman
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  non-portable (RankNTypes)

Implementation of LogicT based on the two-continuation model of streams
-}

module Common.SFKT
  ( SFKT
  , runM
  , observe
  ) where

import Control.Applicative
import Control.Monad
import qualified Control.Monad.Fail as Fail
import Control.Monad.Trans
import Common.LogicT

{- Monad with success, failure continuations, mzero, and mplus
We can also split computations using msplit
Cf. Hinze's ICFP00 paper, Fig. 8: CPS implementation of BACKTR -}

{- The extra `r' is just to be compatible with the SRReifT.hs
type SG r m a = SFKT m a -}

newtype SFKT m a =
  SFKT { SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT :: forall ans . SK (m ans) a -> FK (m ans) -> m ans }

type FK ans = ans
type SK ans a = a -> FK ans -> ans
{- the success continuation gets one answer(value) and a computation
to run to get more answers -}

instance Monad m => Functor (SFKT m) where
  fmap :: (a -> b) -> SFKT m a -> SFKT m b
fmap = (a -> b) -> SFKT m a -> SFKT m b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Monad m => Applicative (SFKT m) where
  pure :: a -> SFKT m a
pure = a -> SFKT m a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: SFKT m (a -> b) -> SFKT m a -> SFKT m b
(<*>) = SFKT m (a -> b) -> SFKT m a -> SFKT m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad m => Monad (SFKT m) where
  return :: a -> SFKT m a
return e :: a
e = (forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
forall (m :: * -> *) a.
(forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
SFKT (\ sk :: SK (m ans) a
sk -> SK (m ans) a
sk a
e)
  m :: SFKT m a
m >>= :: SFKT m a -> (a -> SFKT m b) -> SFKT m b
>>= f :: a -> SFKT m b
f = (forall ans. SK (m ans) b -> m ans -> m ans) -> SFKT m b
forall (m :: * -> *) a.
(forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
SFKT (\ sk :: SK (m ans) b
sk -> SFKT m a -> SK (m ans) a -> m ans -> m ans
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT SFKT m a
m (\ a :: a
a -> SFKT m b -> SK (m ans) b -> m ans -> m ans
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT (a -> SFKT m b
f a
a) SK (m ans) b
sk))

instance Monad m => Alternative (SFKT m) where
  <|> :: SFKT m a -> SFKT m a -> SFKT m a
(<|>) = SFKT m a -> SFKT m a -> SFKT m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
  empty :: SFKT m a
empty = SFKT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

instance Monad m => MonadPlus (SFKT m) where
  mzero :: SFKT m a
mzero = (forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
forall (m :: * -> *) a.
(forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
SFKT (\ _ fk :: FK (m ans)
fk -> FK (m ans)
fk)
  m1 :: SFKT m a
m1 mplus :: SFKT m a -> SFKT m a -> SFKT m a
`mplus` m2 :: SFKT m a
m2 = (forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
forall (m :: * -> *) a.
(forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
SFKT (\ sk :: SK (m ans) a
sk fk :: m ans
fk -> SFKT m a -> SK (m ans) a -> m ans -> m ans
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT SFKT m a
m1 SK (m ans) a
sk (SFKT m a -> SK (m ans) a -> m ans -> m ans
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT SFKT m a
m2 SK (m ans) a
sk m ans
fk))

instance Fail.MonadFail m => Fail.MonadFail (SFKT m) where
  fail :: String -> SFKT m a
fail str :: String
str = (forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
forall (m :: * -> *) a.
(forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
SFKT (\ _ _ -> String -> m ans
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
str)

instance MonadTrans SFKT where
    -- Hinze's promote
    lift :: m a -> SFKT m a
lift m :: m a
m = (forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
forall (m :: * -> *) a.
(forall ans. SK (m ans) a -> m ans -> m ans) -> SFKT m a
SFKT (\ sk :: SK (m ans) a
sk fk :: m ans
fk -> m a
m m a -> (a -> m ans) -> m ans
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SK (m ans) a
`sk` m ans
fk))

instance (MonadIO m) => MonadIO (SFKT m) where
        liftIO :: IO a -> SFKT m a
liftIO = m a -> SFKT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> SFKT m a) -> (IO a -> m a) -> IO a -> SFKT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

-- But this is not in Hinze's paper
instance LogicT SFKT where
    msplit :: SFKT m a -> SFKT m (Maybe (a, SFKT m a))
msplit m :: SFKT m a
m = m (Maybe (a, SFKT m a)) -> SFKT m (Maybe (a, SFKT m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (a, SFKT m a)) -> SFKT m (Maybe (a, SFKT m a)))
-> m (Maybe (a, SFKT m a)) -> SFKT m (Maybe (a, SFKT m a))
forall a b. (a -> b) -> a -> b
$ SFKT m a
-> SK (m (Maybe (a, SFKT m a))) a
-> m (Maybe (a, SFKT m a))
-> m (Maybe (a, SFKT m a))
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT SFKT m a
m SK (m (Maybe (a, SFKT m a))) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (m :: * -> *) a b.
(Monad m, Monad m, LogicT t, MonadPlus (t m)) =>
a -> m (Maybe (b, t m b)) -> m (Maybe (a, t m b))
ssk (Maybe (a, SFKT m a) -> m (Maybe (a, SFKT m a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, SFKT m a)
forall a. Maybe a
Nothing)
        where ssk :: a -> m (Maybe (b, t m b)) -> m (Maybe (a, t m b))
ssk a :: a
a fk :: m (Maybe (b, t m b))
fk = Maybe (a, t m b) -> m (Maybe (a, t m b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, t m b) -> m (Maybe (a, t m b)))
-> Maybe (a, t m b) -> m (Maybe (a, t m b))
forall a b. (a -> b) -> a -> b
$ (a, t m b) -> Maybe (a, t m b)
forall a. a -> Maybe a
Just (a
a, m (Maybe (b, t m b)) -> t m (Maybe (b, t m b))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Maybe (b, t m b))
fk t m (Maybe (b, t m b)) -> (Maybe (b, t m b) -> t m b) -> t m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe (b, t m b) -> t m b
forall (m :: * -> *) (t :: (* -> *) -> * -> *) a.
(Monad m, LogicT t, MonadPlus (t m)) =>
Maybe (a, t m a) -> t m a
reflect)


-- This is a poly-answer `observe' function of Hinze
runM :: (Monad m) => Maybe Int -> SFKT m a -> m [a]
runM :: Maybe Int -> SFKT m a -> m [a]
runM Nothing (SFKT m :: forall ans. SK (m ans) a -> m ans -> m ans
m) = SK (m [a]) a -> m [a] -> m [a]
forall ans. SK (m ans) a -> m ans -> m ans
m (\ a :: a
a -> ([a] -> [a]) -> m [a] -> 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]
:)) ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
runM (Just n :: Int
n) (SFKT _m :: forall ans. SK (m ans) a -> m ans -> m ans
_m) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
runM (Just 1) (SFKT m :: forall ans. SK (m ans) a -> m ans -> m ans
m) = SK (m [a]) a -> m [a] -> m [a]
forall ans. SK (m ans) a -> m ans -> m ans
m (\ a :: a
a _fk :: m [a]
_fk -> [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a]) ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
runM (Just n :: Int
n) m :: SFKT m a
m = SFKT m (Maybe (a, SFKT m a))
-> SK (m [a]) (Maybe (a, SFKT m a)) -> m [a] -> m [a]
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT (SFKT m a -> SFKT m (Maybe (a, SFKT m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(LogicT t, Monad m, MonadPlus (t m)) =>
t m a -> t m (Maybe (a, t m a))
msplit SFKT m a
m) SK (m [a]) (Maybe (a, SFKT m a))
forall (m :: * -> *) a p.
Monad m =>
Maybe (a, SFKT m a) -> p -> m [a]
runM' ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
    where runM' :: Maybe (a, SFKT m a) -> p -> m [a]
runM' Nothing _ = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
          runM' (Just (a :: a
a, m' :: SFKT m a
m')) _ = ([a] -> [a]) -> m [a] -> 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]
:) (Maybe Int -> SFKT m a -> m [a]
forall (m :: * -> *) a. Monad m => Maybe Int -> SFKT m a -> m [a]
runM (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)) SFKT m a
m')

observe :: Fail.MonadFail m => SFKT m a -> m a
observe :: SFKT m a -> m a
observe m :: SFKT m a
m = SFKT m a -> SK (m a) a -> m a -> m a
forall (m :: * -> *) a.
SFKT m a -> forall ans. SK (m ans) a -> m ans -> m ans
unSFKT SFKT m a
m (\ a :: a
a _fk :: m a
_fk -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a) (String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "no answer")