diff options
| author | Gregor Kleen <gkleen@yggdrasil.li> | 2016-06-01 01:21:03 +0200 |
|---|---|---|
| committer | Gregor Kleen <gkleen@yggdrasil.li> | 2016-06-01 01:21:03 +0200 |
| commit | 69081d160dbf6f7d06b9cafd876e0fea423b8066 (patch) | |
| tree | 691cdf8f3350401cfca5443786dea6787d561416 | |
| parent | 97bde0359940a1f6fe2cdbc4bffb9bcaec2a0e54 (diff) | |
| download | events-69081d160dbf6f7d06b9cafd876e0fea423b8066.tar events-69081d160dbf6f7d06b9cafd876e0fea423b8066.tar.gz events-69081d160dbf6f7d06b9cafd876e0fea423b8066.tar.bz2 events-69081d160dbf6f7d06b9cafd876e0fea423b8066.tar.xz events-69081d160dbf6f7d06b9cafd876e0fea423b8066.zip | |
NDT – nondeterminism with monotonous pruning
| -rw-r--r-- | events/src/Events/Types/NDT.hs | 92 |
1 files changed, 92 insertions, 0 deletions
diff --git a/events/src/Events/Types/NDT.hs b/events/src/Events/Types/NDT.hs new file mode 100644 index 0000000..94a84f0 --- /dev/null +++ b/events/src/Events/Types/NDT.hs | |||
| @@ -0,0 +1,92 @@ | |||
| 1 | {-# LANGUAGE GADTs #-} | ||
| 2 | {-# LANGUAGE TupleSections #-} | ||
| 3 | {-# LANGUAGE ViewPatterns #-} | ||
| 4 | {-# LANGUAGE FlexibleContexts, FlexibleInstances #-} | ||
| 5 | |||
| 6 | module Events.Types.NDT | ||
| 7 | ( NDT | ||
| 8 | , foldNDT | ||
| 9 | , cons | ||
| 10 | , fromFoldable | ||
| 11 | ) where | ||
| 12 | |||
| 13 | import Data.Monoid | ||
| 14 | import Data.Foldable (foldr) | ||
| 15 | import Data.Maybe | ||
| 16 | import Data.Either | ||
| 17 | |||
| 18 | import Control.Monad | ||
| 19 | import Control.Monad.Identity | ||
| 20 | |||
| 21 | import Control.Monad.Trans | ||
| 22 | |||
| 23 | import Debug.Trace | ||
| 24 | |||
| 25 | data NDT m a where | ||
| 26 | NDTBind :: NDT m a -> (a -> NDT m b) -> NDT m b | ||
| 27 | NDTCons :: m (Maybe (a, NDT m a)) -> NDT m a | ||
| 28 | |||
| 29 | instance Show (NDT Identity a) where | ||
| 30 | show (NDTBind x _) = "Bind (" ++ show x ++ ") _" | ||
| 31 | show x = show . (\(NDTCons x) -> x) $ fmap (const ()) x | ||
| 32 | |||
| 33 | instance Functor m => Functor (NDT m) where | ||
| 34 | fmap f (NDTBind a g) = NDTBind a (fmap f . g) | ||
| 35 | fmap f (NDTCons x) = NDTCons $ fmap f' x | ||
| 36 | where | ||
| 37 | f' Nothing = Nothing | ||
| 38 | f' (Just (x, xs)) = Just (f x, fmap f xs) | ||
| 39 | |||
| 40 | instance Applicative m => Applicative (NDT m) where | ||
| 41 | pure x = NDTCons . pure $ Just (x, empty) | ||
| 42 | fs <*> xs = fs >>= (\f -> xs >>= pure . (f $)) | ||
| 43 | |||
| 44 | instance Applicative m => Monad (NDT m) where | ||
| 45 | return = pure | ||
| 46 | fail = const empty | ||
| 47 | (>>=) = NDTBind | ||
| 48 | |||
| 49 | instance Monad m => Monoid (NDT m a) where | ||
| 50 | mempty = empty | ||
| 51 | mappend (NDTCons x) y'@(NDTCons y) = trace "(cons <> cons)" . NDTCons . trace "[cons <> cons]" $ maybe y (\(x, xs) -> return $ Just (x, xs <> y')) =<< x | ||
| 52 | mappend (NDTBind x f) (NDTBind y g) = trace "(bind <> bind)" $ NDTBind (fmap Left x <> fmap Right y) (either f g) | ||
| 53 | mappend x@(NDTBind _ _) y = trace "(bind <>)" $ x <> NDTBind y return | ||
| 54 | mappend x y@(NDTBind _ _) = trace "(<> bind)" $ NDTBind x return <> y | ||
| 55 | |||
| 56 | instance MonadTrans NDT where | ||
| 57 | lift = NDTCons . fmap Just . fmap (,empty) | ||
| 58 | |||
| 59 | empty :: Applicative m => NDT m a | ||
| 60 | empty = NDTCons $ pure Nothing | ||
| 61 | |||
| 62 | cons :: Applicative m => a -> NDT m a -> NDT m a | ||
| 63 | cons x xs = NDTCons . pure $ Just (x, xs) | ||
| 64 | |||
| 65 | foldNDT :: (Monoid a, Monad m) => (a -> m Bool) -> NDT m a -> m a | ||
| 66 | foldNDT sel = fmap snd . foldNDT' sel | ||
| 67 | |||
| 68 | foldNDT' :: (Monoid a, Monad m) => (a -> m Bool) -> NDT m a -> m (Any, a) | ||
| 69 | -- ^ Evaluate depth-first, pruning leaves under the assumption that the selection predicate is monotonic on siblings | ||
| 70 | foldNDT' sel (NDTCons mx) = do | ||
| 71 | mx' <- mx | ||
| 72 | case mx' of | ||
| 73 | Nothing -> return mempty | ||
| 74 | Just (x, mxs) -> do | ||
| 75 | continue <- sel x | ||
| 76 | case trace ("(cons "++ show continue ++ ")") continue of | ||
| 77 | False -> return (Any True, mempty) | ||
| 78 | True -> ((Any True, x) <>) <$> foldNDT' sel mxs | ||
| 79 | foldNDT' sel (NDTBind (NDTCons x) f) = trace "(bind cons)" $ do | ||
| 80 | x' <- x | ||
| 81 | case x' of | ||
| 82 | Nothing -> return mempty | ||
| 83 | Just (x'', xs) -> do -- foldNDT' sel . NDTCons $ Just . (, NDTBind xs f) . snd <$> foldNDT' sel (f x'') | ||
| 84 | (productive, x3) <- foldNDT' sel $ f x'' | ||
| 85 | continue <- sel x3 | ||
| 86 | case trace ("(bind cons " ++ show (productive, continue) ++ ")") $ continue || not (getAny productive) of | ||
| 87 | False -> return mempty | ||
| 88 | True -> ((mempty, x3) <>) <$> foldNDT' sel (NDTBind xs f) | ||
| 89 | foldNDT' sel (NDTBind (NDTBind x g) f) = trace "(bind bind)" . foldNDT' sel $ NDTBind x (f <=< g) | ||
| 90 | |||
| 91 | fromFoldable :: (Foldable f, Monad m) => f a -> NDT m a | ||
| 92 | fromFoldable = foldr cons empty | ||
