{-# LANGUAGE RankNTypes #-}

{- |

Module : $Header$

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.Monad

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 { 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 => Monad (SFKT m) where

return e = SFKT (\ sk -> sk e)

m >>= f = SFKT (\ sk -> unSFKT m (\ a -> unSFKT (f a) sk))

instance Monad m => MonadPlus (SFKT m) where

mzero = SFKT (\ _ fk -> fk)

m1 `mplus` m2 = SFKT (\ sk fk -> unSFKT m1 sk (unSFKT m2 sk fk))

instance MonadTrans SFKT where

-- Hinze's promote

lift m = SFKT (\ sk fk -> m >>= (`sk` fk))

instance (MonadIO m) => MonadIO (SFKT m) where

liftIO = lift . liftIO

-- But this is not in Hinze's paper

instance LogicT SFKT where

msplit m = lift $ unSFKT m ssk (return Nothing)

where ssk a fk = return $ Just (a, lift fk >>= reflect)

-- This is a poly-answer `observe' function of Hinze

runM :: (Monad m) => Maybe Int -> SFKT m a -> m [a]

runM Nothing (SFKT m) = m (\ a -> liftM (a :)) (return [])

runM (Just n) (SFKT _m) | n <= 0 = return []

runM (Just 1) (SFKT m) = m (\ a _fk -> return [a]) (return [])

runM (Just n) m = unSFKT (msplit m) runM' (return [])

where runM' Nothing _ = return []

runM' (Just (a, m')) _ = liftM (a :) (runM (Just (n - 1)) m')

observe :: Monad m => SFKT m a -> m a

observe m = unSFKT m (\ a _fk -> return a) (fail "no answer")