cflp 2009.1.23.2 → 2009.1.24

raw patch · 11 files changed

+60/−91 lines, 11 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• cflp.cabal +1/−1
• src/CFLP.lhs +8/−5
• src/CFLP/Control/Strategy.lhs +1/−33
• src/CFLP/Data/Primitive.lhs +16/−5
• src/CFLP/Strategies.lhs +8/−15
• src/CFLP/Strategies/CallTimeChoice.lhs +7/−7
• src/CFLP/Strategies/DepthCounter.lhs +6/−8
• src/CFLP/Strategies/DepthFirst.lhs +2/−2
• src/CFLP/Strategies/DepthLimit.lhs +9/−13
• src/CFLP/Tests.lhs +1/−1
• src/CFLP/Tests/HigherOrder.lhs +1/−1

@@ -1,5 +1,5 @@ Name:          cflp-Version:       2009.1.23.2+Version:       2009.1.24 Cabal-Version: >= 1.6 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint

@@ -28,7 +28,10 @@ > import Control.Monad.State > > import CFLP.Data+> import CFLP.Data.Types+> > import CFLP.Control.Monad.Update+> > import CFLP.Control.Strategy  The type class `CFLP` amalgamates all class constraints on constraint@@ -65,12 +68,12 @@  > eval, evalPartial >   :: (Monad s, CFLP s, Generic a) => s (Ctx s) -> Computation a -> IO [a]-> eval        s = liftM (liftM primitive) . evaluate s groundNormalForm-> evalPartial s = liftM (liftM primitive) . evaluate s partialNormalForm+> eval        s = liftM (liftM primitive) . evaluate s (groundNormalForm s)+> evalPartial s = liftM (liftM primitive) . evaluate s (partialNormalForm s) > > evalPrint :: (Monad s, CFLP s, Generic a) >           => s (Ctx s) -> Computation a -> IO ()-> evalPrint s op = evaluate s partialNormalForm op >>= printSols+> evalPrint s op = evaluate s (partialNormalForm s) op >>= printSols > > printSols :: Show a => [a] -> IO () > printSols []     = putStrLn "No more solutions."@@ -89,10 +92,10 @@  > evaluate :: CFLP s >          => s (Ctx s)->          -> (Nondet (Ctx s) s a -> Context (Ctx s) -> Res s b)+>          -> (Nondet (Ctx s) s a -> Res s b) >          -> Computation a >          -> IO [b] > evaluate s evalNondet op = do >   i <- initID >   return $ enumeration $->     evalNondet (op (Context (emptyContext s)) i) $ Context (emptyContext s)+>     evalNondet (Typed (s >>= untyped . flip op i . Context))

@@ -69,13 +69,6 @@  Strategies provide the following operations: ->   emptyContext :: s c -> Ctx s--yields an empty context of the associated type `Ctx s`. The argument-of type `s c` is sometimes necessary to satisfy the type checker. It-must always be safe to pass undefined, i.e., the argument must be-ignored.- >   choose :: c -> Int -> [s a] -> s a  is used to cconstruct non-deterministic choices of computations. We@@ -114,11 +107,6 @@  The operation ->   emptyContext _ = ()--yields `()` because stores are ignored by (untransformed) monadic-strategies.- >   choose _ _ [x] = x >   choose _ _ xs  = foldr mplus mzero xs @@ -192,11 +180,6 @@ that uses the base strategy. The first parameter is used to support type checking and must be ignored. ->   extendContext :: t s c -> Ctx s -> Ctx (t s)--may extend the evaluation context of the base strategy. Again, the-first argument must be ignored by instantiations of `StrategyT`.- >   extendChoices :: (Monad s, MonadUpdate c s) >                 => c -> Int -> [t s a] -> [t s a] >   extendChoices _ _ = id@@ -221,14 +204,6 @@ >       => Strategy c (t s) >  where -The operation `emptyContext` calls the corresponding operation of the-base strategy and extends the result accoring to the transformer.-->   emptyContext c = extendContext c (emptyContext (undefined `forBaseOf` c))--Here, we give a hint to the type checker using the type-constrained-`const` function `forBaseOf` (defined below).- The operation `choose` extends the choices according to the transformer and calls the `choose` operation of the base strategy with the resulting choices.@@ -238,17 +213,10 @@ >              . map (baseStrategy c) >              . extendChoices c n -Finally, the predicate `isNarrowed` is altered according the strategy+The predicate `isNarrowed` is altered according to the strategy transformer.  >   isNarrowed c n = alterNarrowed c n (liftStrategy c (isNarrowed c n))--The function `forBaseOf` is a `const` function with a specialised type-that supports the type checker in finding the corresponding operation-`emptyContext` for the base strategy.--> forBaseOf :: s a -> t s a -> s a-> forBaseOf = const   Uniform Liftings

@@ -1,6 +1,10 @@ % Primitive Generic Functions on Lazy Non-Deterministic Data % Sebastian Fischer (sebf@informatik.uni-kiel.de) +> {-# LANGUAGE+>       FlexibleContexts+>   #-}+> > module CFLP.Data.Primitive ( > >   nondet, groundNormalForm, partialNormalForm,@@ -29,7 +33,7 @@ > nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable" > nf2hnf (Data label args) = Cons label (map (return . nf2hnf) args) > nf2hnf (Fun f) = Lambda (\x _ _ -> liftM (nf2hnf . f) $ gnf x)->  where gnf x = groundNormalForm (Typed x) $+>  where gnf x = flip groundNormalForm (Typed x) $ return $  >                  error "Primitive.nf2hnf: primitive function uses context"  The `...NormalForm` functions evaluate a non-deterministic value and@@ -39,12 +43,19 @@ variables while ground normal forms are data terms.  > groundNormalForm :: (Monad s, Monad m, Update c s m)->                  => Nondet c s a -> Context c -> m NormalForm-> groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs+>                  => s c -> Nondet c s a -> m NormalForm+> groundNormalForm c x+>   = evalStateT (updateState c) (undefined `asContextOf` c) >>=+>     evalStateT (gnf (untyped x)) > > partialNormalForm :: (Monad s, Strategy c s, Monad m, Update c s m)->                   => Nondet c s a -> Context c -> m NormalForm-> partialNormalForm x (Context cs) = evalStateT (pnf (untyped x)) cs+>                   => s c -> Nondet c s a -> m NormalForm+> partialNormalForm c x+>   = evalStateT (updateState c) (undefined `asContextOf` c) >>=+>     evalStateT (pnf (untyped x))+>+> asContextOf :: c -> s c -> c+> asContextOf = const  To compute ground normal forms, we ignore free variables and narrow them to ground terms. To compute partial normal forms, we do not

@@ -10,7 +10,7 @@ > > module CFLP.Strategies ( >->   (<+), dfs, limDFS,+>   dfs, limDFS, > >   module CFLP.Strategies.DepthFirst, >   module CFLP.Strategies.CallTimeChoice,@@ -27,22 +27,15 @@ > 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..).--> infixr 5 <+->-> (<+) :: (b -> c) -> (a -> b) -> d -> c-> (t <+ s) _ = t (s undefined)--For convenience, we provide shortcuts for useful strategies.+We provide shortcuts for useful strategies. -> dfs :: c -> CTC (Monadic (UpdateT (StoreCTC c) [])) a-> dfs = callTimeChoice <+ dfsWithEvalTimeChoice+> dfs :: CTC (Monadic (UpdateT (StoreCTC ()) [])) (StoreCTC ())+> dfs = callTimeChoice dfsWithEvalTimeChoice >-> limDFS :: c -> CTC (Depth (DepthLim (Monadic->                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx c))) [])))) a-> limDFS = callTimeChoice <+ countDepth <+ limitDepth <+ dfsWithEvalTimeChoice+> limDFS :: Int -> CTC (Depth (DepthLim (Monadic+>                       (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) []))))+>                       (StoreCTC (DepthCtx (DepthLimCtx ())))+> limDFS l = callTimeChoice.countDepth.limitDepth l$dfsWithEvalTimeChoice  Finally, we provide instances for the type class `CFLP` that is a shortcut for the class constraints of CFLP computations.

@@ -126,12 +126,6 @@ > type instance Ctx (CTC s) = StoreCTC (Ctx s) > type instance Res (CTC s) = CTC (Res s) -We provide a constructor function that allows us to hide the-corresponding newtype constructor.--> callTimeChoice :: s a -> CTC s a-> callTimeChoice = CTC- The type `CTC` is a strategy transformer for strategies that have acces to a choice store. @@ -140,9 +134,15 @@ >   liftStrategy _ = CTC >   baseStrategy _ = fromCTC >->   extendContext _ = StoreCTC noChoices >   extendChoices   = labeledChoices > >   alterNarrowed c n isn >     | isJust (lookupChoice n c) = return True >     | otherwise = isn++We provide a strategy transformer function that is used to add+call-time choice to arbitrary strategies.++> callTimeChoice :: Monad s => s c -> CTC s (StoreCTC c)+> callTimeChoice = CTC . liftM (StoreCTC noChoices)+

@@ -1,4 +1,4 @@-% Depth Monitoring for Non-Deterministic Computations.+% Depth Monitoring for Non-Deterministic Computations % Sebastian Fischer (sebf@informatik.uni-kiel.de)  This module provides a strategy transformer that extends the@@ -70,11 +70,6 @@ > type instance Ctx (Depth s) = DepthCtx (Ctx s) > type instance Res (Depth s) = Depth (Res s) -The operation `countDepth` the `Depth` constructor.--> countDepth :: s a -> Depth s a-> countDepth = Depth- The strategy-transformer instance increments the counter at each non-deterministic choice. @@ -83,6 +78,9 @@ >   liftStrategy _ = Depth >   baseStrategy _ = fromDepth >->   extendContext _ = DepthCtx 0-> >   extendChoices c _ = map (update (return . incrementDepth c)>>)++The operation `countDepth` adds a depth counter to a strategy.++> countDepth :: Monad s => s c -> Depth s (DepthCtx c)+> countDepth = Depth . liftM (DepthCtx 0)

@@ -26,6 +26,6 @@ semantics. In order to get call-time choice, this needs to be transformed with the call-time choice transformer. -> dfsWithEvalTimeChoice :: c -> Monadic (UpdateT c []) a-> dfsWithEvalTimeChoice _ = Monadic undefined+> dfsWithEvalTimeChoice :: Monadic (UpdateT c []) ()+> dfsWithEvalTimeChoice = Monadic (return ()) 

@@ -1,4 +1,4 @@-% Depth Limiting for Non-Deterministic Computations.+% Depth Limiting for Non-Deterministic Computations % Sebastian Fischer (sebf@informatik.uni-kiel.de)  This module provides a strategy transformer that extends the@@ -43,12 +43,9 @@ > >   resetDepthLimit _ l c = replace c (resetDepthLimit undefined l (project c)) -The default limit is 100, but you can use the operation-`setDepthLimit` in computations to change it.+The operation `setDepthLimit` is used in computations to change the+depth limit. -> defaultLimit :: Int-> defaultLimit = 100-> > setDepthLimit :: (Monad s, DepthLimiter c, MonadUpdate c s) >               => c -> Int -> s () > setDepthLimit c l = update (return . resetDepthLimit c l)@@ -80,11 +77,6 @@ > type instance Ctx (DepthLim s) = DepthLimCtx (Ctx s) > type instance Res (DepthLim s) = DepthLim (Res s) -The operation `depthCounter` the `Depth` constructor.--> limitDepth :: s a -> DepthLim s a-> limitDepth = DepthLim- The strategy-transformer instance increments the counter at each non-deterministic choice and prunes the choices if the limit is exceeded.@@ -94,9 +86,13 @@ >   liftStrategy _ = DepthLim >   baseStrategy _ = fromDepthLim >->   extendContext _ = DepthLimCtx defaultLimit-> >   extendChoices c _ xs >     | currentDepth c < depthLimit c >       = map (update (return . incrementDepth c)>>) xs >     | otherwise = []++The operation `limitDepth` adds a depth limit to a strategy.++> limitDepth :: Monad s => Int -> s c -> DepthLim s (DepthLimCtx c)+> limitDepth l = DepthLim . liftM (DepthLimCtx l)+

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

@@ -23,7 +23,7 @@ >   , "apply non-deterministic choice" ~: applyChoice >   , "call-time choice" ~: callTimeChoice >   , "map shared unknowns" ~: mapSharedUnknowns->   , "memeber with fold" ~: memberWithFold+>   , "member with fold" ~: memberWithFold >   , "overApplication" ~: overApplication >   , "reverse with foldr" ~: reverseWithFoldr >   , "pointfree reverse" ~: pointfreeReverse