8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE RankNTypes #-}
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) 2005, Amr Sabry, Chung-chieh Shan, Oleg Kiselyov
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian Maeder and Daniel P. Friedman
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : experimental
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (RankNTypes)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederImplementation of LogicT based on the two-continuation model of streams
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- Monad with success, failure continuations, mzero, and mplus
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederWe can also split computations using msplit
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederCf. Hinze's ICFP00 paper, Fig. 8: CPS implementation of BACKTR -}
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder{- The extra `r' is just to be compatible with the SRReifT.hs
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedertype SG r m a = SFKT m a -}
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedernewtype SFKT m a =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder SFKT { unSFKT :: forall ans . SK (m ans) a -> FK (m ans) -> m ans }
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedertype FK ans = ans
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maedertype SK ans a = a -> FK ans -> ans
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder{- the success continuation gets one answer(value) and a computation
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederto run to get more answers -}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Monad m => Functor (SFKT m) where
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederinstance Monad m => Applicative (SFKT m) where
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder pure = return
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maederinstance Monad m => Monad (SFKT m) where
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder return e = SFKT (\ sk -> sk e)
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder m >>= f = SFKT (\ sk -> unSFKT m (\ a -> unSFKT (f a) sk))
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maederinstance Monad m => Alternative (SFKT m) where
63324a97283728a30932828a612c7b0b0f687624Christian Maeder (<|>) = mplus
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder empty = mzero
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederinstance Monad m => MonadPlus (SFKT m) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mzero = SFKT (\ _ fk -> fk)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski m1 `mplus` m2 = SFKT (\ sk fk -> unSFKT m1 sk (unSFKT m2 sk fk))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance MonadTrans SFKT where
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- Hinze's promote
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lift m = SFKT (\ sk fk -> m >>= (`sk` fk))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (MonadIO m) => MonadIO (SFKT m) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski liftIO = lift . liftIO
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- But this is not in Hinze's paper
3a87487c048b275c56e502c4a933273788e8d0bbChristian Maederinstance LogicT SFKT where
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu msplit m = lift $ unSFKT m ssk (return Nothing)
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu where ssk a fk = return $ Just (a, lift fk >>= reflect)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder-- This is a poly-answer `observe' function of Hinze
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaederrunM :: (Monad m) => Maybe Int -> SFKT m a -> m [a]
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskirunM Nothing (SFKT m) = m (\ a -> liftM (a :)) (return [])
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill MossakowskirunM (Just n) (SFKT _m) | n <= 0 = return []
d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian MaederrunM (Just 1) (SFKT m) = m (\ a _fk -> return [a]) (return [])
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian MaederrunM (Just n) m = unSFKT (msplit m) runM' (return [])
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder where runM' Nothing _ = return []
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski runM' (Just (a, m')) _ = liftM (a :) (runM (Just (n - 1)) m')
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maederobserve :: Monad m => SFKT m a -> m a
bba825b39570777866d560bfde3807731131097eKlaus Luettichobserve m = unSFKT m (\ a _fk -> return a) (fail "no answer")