SFKT.hs revision 90d7cac36f60438bd35124e3389b5bce6d114b46
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder{-# OPTIONS -fglasgow-exts #-}
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- Implementation of LogicT based on the two-continuation model of streams
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder{- Copyright (c) 2005, Amr Sabry, Chung-chieh Shan, Oleg Kiselyov,
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder and Daniel P. Friedman
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder SG, runM, observe
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder---------------------------------------------------------------
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder-- Monad with success, failure continuations, mzero, and mplus
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- We can also split computations using msplit
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder-- Cf. Hinze's ICFP00 paper, Fig. 8: CPS implementation of BACKTR
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder-- The extra `r' is just to be compatible with the SRReifT.hs
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype SG r m a = SFKT m a
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedernewtype SFKT m a = SFKT (forall ans. SK (m ans) a -> FK (m ans) -> m ans)
d48085f765fca838c1d972d2123601997174583dChristian MaederunSFKT (SFKT a) = a
d48085f765fca838c1d972d2123601997174583dChristian Maedertype FK ans = ans
d48085f765fca838c1d972d2123601997174583dChristian Maedertype SK ans a = a -> FK ans -> ans
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- the success continuation gets one answer(value) and a computation
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- to run to get more answers
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance Monad m => Monad (SFKT m) where
d48085f765fca838c1d972d2123601997174583dChristian Maeder return e = SFKT (\sk fk -> sk e fk) -- can be eta-reduced, as in Hinze's papr
d48085f765fca838c1d972d2123601997174583dChristian Maeder m >>= f = -- can be eta-reduced
d48085f765fca838c1d972d2123601997174583dChristian Maeder SFKT (\sk fk ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder (unSFKT m) (\a fk' -> unSFKT (f a) sk fk')
a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance Monad m => MonadPlus (SFKT m) where
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder mzero = SFKT (\_ fk -> fk)
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder m1 `mplus` m2 = SFKT (\sk fk -> unSFKT m1 sk (unSFKT m2 sk fk))
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance MonadTrans SFKT where
d48085f765fca838c1d972d2123601997174583dChristian Maeder -- Hinze's promote
d48085f765fca838c1d972d2123601997174583dChristian Maeder lift m = SFKT (\sk fk -> m >>= (\a -> sk a fk))
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance (MonadIO m) => MonadIO (SFKT m) where
d48085f765fca838c1d972d2123601997174583dChristian Maeder liftIO = lift . liftIO
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- But this is not in Hinze's paper
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederinstance LogicT SFKT where
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder msplit m = lift $ unSFKT m ssk (return Nothing)
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder where ssk a fk = return $ Just (a, (lift fk >>= reflect))
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- This is a poly-answer `observe' function of Hinze
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederrunM:: (Monad m) => Maybe Int -> SFKT m a -> m [a]
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederrunM Nothing (SFKT m) = m (\a fk -> fk >>= (return . (a:))) (return [])
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederrunM (Just n) (SFKT _m) | n <=0 = return []
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederrunM (Just 1) (SFKT m) = m (\a _fk -> return [a]) (return [])
5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederrunM (Just n) m = unSFKT (msplit m) runM' (return [])
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder where runM' Nothing _ = return []
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder runM' (Just (a,m')) _ = runM (Just (n-1)) m' >>= (return . (a:))
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederobserve :: Monad m => SFKT m a -> m a
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederobserve m = unSFKT m (\a _fk -> return a) (fail "no answer")