implemented limited depth-first search as strategy transformers.

src/CFLP/Strategies.lhs

@@ -10,11 +10,12 @@ other modules in this package.
 >
 > module CFLP.Strategies (
 >
->   (+>), dfs,
+>   (<+), dfs, limDFS,
 >
 >   module CFLP.Strategies.DepthFirst,
 >   module CFLP.Strategies.CallTimeChoice,
->   module CFLP.Strategies.DepthCounter
+>   module CFLP.Strategies.DepthCounter,
+>   module CFLP.Strategies.DepthLimit
 >
 >  ) where
 >
@@ -24,23 +25,32 @@ other modules in this package.
 > import CFLP.Strategies.DepthFirst
 > import CFLP.Strategies.CallTimeChoice
 > import CFLP.Strategies.DepthCounter
+> import CFLP.Strategies.DepthLimit
 
 We provide a combinator `(+>)` to transform a strategy with a strategy
 transformer (the type is not descriptive, so better ignore it..).
 
-> infixl 5 +>
+> infixr 5 <+
 >
-> (+>) :: (a -> b) -> (b -> c) -> d -> c
-> (s +> t) _ = t (s undefined)
+> (<+) :: (b -> c) -> (a -> b) -> d -> c
+> (t <+ s) _ = t (s undefined)
 
 For convenience, we provide shortcuts for useful strategies.
 
 > dfs :: c -> CTC (Monadic (UpdateT (StoreCTC c) [])) a
-> dfs = dfsWithEvalTimeChoice +> callTimeChoice
+> dfs = callTimeChoice <+ dfsWithEvalTimeChoice
+>
+> limDFS :: c -> CTC (Depth (DepthLim (Monadic
+>                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx c))) [])))) a
+> limDFS = callTimeChoice <+ countDepth <+ limitDepth <+ dfsWithEvalTimeChoice
 
 Finally, we provide instances for the type class `CFLP` that is a
 shortcut for the class constraints of CFLP computations.
 
 > instance (MonadPlus m, Enumerable m)
 >       => CFLP (CTC (Monadic (UpdateT (StoreCTC ()) m)))
+>
+> instance (MonadPlus m, Enumerable m)
+>       => CFLP (CTC (Depth (DepthLim (Monadic
+>                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) m)))))
 

src/CFLP/Strategies/DepthCounter.lhs

@@ -7,13 +7,14 @@ evaluation context with a counter for the search depth.
 > {-# LANGUAGE
 >       GeneralizedNewtypeDeriving,
 >       MultiParamTypeClasses,
+>       OverlappingInstances,
 >       FlexibleInstances,
 >       TypeFamilies
 >   #-}
 >
 > module CFLP.Strategies.DepthCounter (
 >
->   DepthCounter(..), Depth, DepthCtx, depthCounter
+>   DepthCounter(..), Depth, DepthCtx, countDepth
 >
 >  ) where
 >
@@ -34,6 +35,15 @@ is given by the following type class.
 The first argument of `incrementDepth` will always be ignored and is
 only used to support the type checker.
 
+We define uniform liftings for depth counters over arbitrary context
+transformers.
+
+> instance (DepthCounter c, Transformer t) => DepthCounter (t c)
+>  where
+>   currentDepth = currentDepth . project
+>
+>   incrementDepth _ c = replace c (incrementDepth undefined (project c))
+
 A depth context adds a counter for the depth.
 
 > data DepthCtx c = DepthCtx Int c
@@ -60,10 +70,10 @@ We define a strategy transformer for depth counting.
 > type instance Ctx (Depth s) = DepthCtx (Ctx s)
 > type instance Res (Depth s) = Depth (Res s)
 
-The operation `depthCounter` the `Depth` constructor.
+The operation `countDepth` the `Depth` constructor.
 
-> depthCounter :: s a -> Depth s a
-> depthCounter = Depth
+> countDepth :: s a -> Depth s a
+> countDepth = Depth
 
 The strategy-transformer instance increments the counter at each
 non-deterministic choice.

src/CFLP/Tests.lhs

@@ -26,7 +26,7 @@ to use errors when testing laziness.
 > assertResultsLimit :: (Generic a, Show a, Eq a)
 >                    => Maybe Int -> Computation a -> [a] -> Assertion
 > assertResultsLimit limit op expected = do
->   actual <- eval (dfs ()) op
+>   actual <- eval (limDFS ()) op
 >   maybe id take limit actual @?= expected
 
 We provide auxiliary assertions `assertResults...` that compute (a