cflp 2009.1.28 → 2009.2.1

raw patch · 17 files changed

+616/−92 lines, 17 filesdep +incremental-sat-solverdep ~basesetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: incremental-sat-solver

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Setup.lhs +1/−1
• Test.lhs +2/−1
• cflp.cabal +6/−3
• src/CFLP.lhs +17/−12
• src/CFLP/Constraints/Boolean.lhs +212/−0
• src/CFLP/Control/Strategy.lhs +27/−1
• src/CFLP/Data/Generic.lhs +13/−0
• src/CFLP/Data/Matching.lhs +28/−28
• src/CFLP/Data/Narrowing.lhs +66/−4
• src/CFLP/Data/Primitive.lhs +24/−11
• src/CFLP/Data/Types.lhs +29/−17
• src/CFLP/Strategies.lhs +92/−10
• src/CFLP/Tests.lhs +5/−2
• src/CFLP/Tests/Boolean.lhs +86/−0
• src/CFLP/Tests/HigherOrder.lhs +6/−0
• src/CFLP/Types/Bool.lhs +1/−1
• src/CFLP/Types/List.lhs +1/−1

@@ -9,6 +9,6 @@ > main = defaultMainWithHooks $ simpleUserHooks { runTests = runTestSuite } > > runTestSuite _ _ _ _ =->   runCommand "runhaskell -i.:src Test.lhs" >>= waitForProcess >>= exitWith+>   runCommand "ghc -i.:src -hide-package transformers -hide-package monads-fd -e main Test.lhs" >>= waitForProcess >>= exitWith  

@@ -8,9 +8,10 @@ > > import CFLP.Tests.CallTimeChoice as CTC > import CFLP.Tests.HigherOrder as HO+> import CFLP.Tests.Boolean as B > > main :: IO () > main = do->  runTestTT $ test [CTC.tests,HO.tests]+>  runTestTT $ test [CTC.tests,HO.tests,B.tests] >  return () 

@@ -1,5 +1,5 @@ Name:          cflp-Version:       2009.1.28+Version:       2009.2.1 Cabal-Version: >= 1.6 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint@@ -8,7 +8,7 @@                compiling programs written in an FLP language like Curry                 or Toy. Another application of FLP is demand driven                 test-case generation.-Category:      Control, Monads+Category:      Control License:       BSD3 License-File:  LICENSE Author:        Sebastian Fischer@@ -21,18 +21,21 @@ Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs  Library-  Build-Depends:    base >= 4, mtl, syb, containers,+  Build-Depends:    base == 4.*, mtl, syb, containers,                     control-monad-omega, logict, level-monad, stream-monad,+                    incremental-sat-solver,                     random, MonadRandom,                     value-supply,                     HUnit   Exposed-Modules:  CFLP+                    CFLP.Constraints.Boolean                     CFLP.Strategies                     CFLP.Strategies.CallTimeChoice                     CFLP.Strategies.DepthCounter                     CFLP.Strategies.DepthLimit                     CFLP.Strategies.Random                     CFLP.Tests+                    CFLP.Tests.Boolean                     CFLP.Tests.CallTimeChoice                     CFLP.Tests.HigherOrder                     CFLP.Types.Bool

@@ -15,7 +15,7 @@ > > module CFLP ( >->   CFLP, Enumerable(..), Ctx, Data, Computation,+>   CFLP, Enumerable(..), Ctx, Data, > >   eval, evalPartial, evalPrint, >@@ -38,6 +38,7 @@ functional-logic computations.  > class (Strategy (Ctx s) s, MonadPlus s+>                          , Solvable (Ctx s) >                          , MonadUpdate (Ctx s) s >                          , Update (Ctx s) s s >                          , Update (Ctx s) s (Res s)@@ -50,13 +51,10 @@ > > instance (MonadPlus m, Enumerable m) => CFLP (Monadic (UpdateT () m)) -We define a shortcut for types of constraint functional-logic data and-computations that can be parameterized by an arbitrary strategy.+We define a shortcut for types of constraint functional-logic data+that can be parameterized by an arbitrary strategy.  > type Data s a = Nondet (Ctx s) s a->-> type Computation a->   = forall s . CFLP s => Context (Ctx s) -> ID -> Data s a  We provide @@ -70,12 +68,15 @@     solutions of a constraint functional-logic computation.  > eval, evalPartial->   :: (Monad s, CFLP s, Generic a) => [s (Ctx s)] -> Computation a -> IO [a]+>   :: (Monad s, CFLP s, Generic a)+>   => [s (Ctx s)]+>   -> (Context (Ctx s) -> ID -> Data s a)+>   -> IO [a] > eval        s = liftM (liftM primitive) . evaluate s groundNormalForm > evalPartial s = liftM (liftM primitive) . evaluate s partialNormalForm > > evalPrint :: (Monad s, CFLP s, Generic a)->           => [s (Ctx s)] -> Computation a -> IO ()+>           => [s (Ctx s)] -> (Context (Ctx s) -> ID -> Data s a) -> IO () > evalPrint s op = evaluate s partialNormalForm op >>= printSols > > printSols :: Show a => [a] -> IO ()@@ -95,10 +96,14 @@  > evaluate :: CFLP s >          => [s (Ctx s)]->          -> (s (Ctx s) -> Nondet (Ctx s) s a -> Res s b)->          -> Computation a+>          -> (s (Ctx s) -> Nondet (Ctx s) s a -> Res s (b, Ctx s))+>          -> (Context (Ctx s) -> ID -> Data s a) >          -> IO [b] > evaluate s evalNondet op = do >   i <- initID->   return $ concatMap enumeration $->     map (\c -> evalNondet c (Typed (c >>= untyped . flip op i . Context))) s+>   return $ concatMap enumeration $ map (run i) s+>  where+>   run i c = do+>     (res,ctx) <- evalNondet c (Typed (c >>= untyped . flip op i . Context))+>     guard (solvable ctx)+>     return res

@@ -0,0 +1,212 @@+% Boolean Constraints for CFLP+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides boolean constraints for constraint+functional-logic programming.++> {-# LANGUAGE+>       GeneralizedNewtypeDeriving,+>       NoMonomorphismRestriction,+>       MultiParamTypeClasses,+>       OverlappingInstances,+>       FlexibleInstances,+>       FlexibleContexts,+>       NoMonoPatBinds,+>       TypeFamilies+>   #-}+>+> module CFLP.Constraints.Boolean (+>+>   Boolean, yes, no, neg, (.&&.), (.||.),+>+>   BooleanSolver(..), SatCtx, Sat, satSolving,+>+>   ifThen, ifThenElse, booleanToBool+>+>  ) where+>+> import Control.Monad+>+> import CFLP+> import CFLP.Control.Strategy+>+> import CFLP.Control.Monad.Update+>+> import CFLP.Data.Types+>   ( HeadNormalForm(..), Nondet(..), Context(..), label, joinNondet )+> import CFLP.Data.Primitive+>+> import CFLP.Types.Bool+>+> import Data.Boolean.SatSolver++Generic Creation of Boolean Formulas+====================================++We make the type of boolean formulas an instance of `ApplyCons` and+`Generic` in order to be able to define boolean formulas in CFLP+programs.++> instance ApplyCons Boolean+>   where+>    type Result Boolean = Boolean+>    applyCons = const+>+> instance Generic Boolean+>  where+>   constr = cons "BVAR"  Var    dVar+>          ! cons "TRUE"  Yes    dYes+>          ! cons "FALSE" No     dNo+>          ! cons "NOT"   Not    dNot+>          ! cons "AND"   (:&&:) dAnd+>          ! cons "OR"    (:||:) dOr+>+> dVar, dYes, dNo, dNot, dAnd, dOr :: Decons Boolean+>+> dVar c (Var n) = Just (c [generic n])+> dVar _ _       = Nothing+>+> dYes c Yes = Just (c [])+> dYes _ _   = Nothing+>+> dNo c No = Just (c [])+> dNo _ _  = Nothing+>+> dNot c (Not x) = Just (c [generic x])+> dNot _ _       = Nothing+>+> dAnd c (x:&&:y) = Just (c [generic x, generic y])+> dAnd _ _        = Nothing+>+> dOr c (x:||:y) = Just (c [generic x, generic y])+> dOr _ _        = Nothing++We define functions for constructing boolean formulas, but none for+pattern matching.++> infixr 3 .&&.+> infixr 2 .||.+>+> var            :: Monad m => Nondet c m Int -> Nondet c m Boolean+> yes, no        :: Monad m => Nondet c m Boolean+> neg            :: Monad m => Nondet c m Boolean -> Nondet c m Boolean+> (.&&.), (.||.) :: Monad m => Nondet c m Boolean -> Nondet c m Boolean+>                           -> Nondet c m Boolean+>+> var :! yes :! no :! neg :! (.&&.) :! (.||.) :! () = constructors+++Extending Computations with SAT Solving+==============================================++An evaluation context that can satisfy boolean formulas is an instance+of the following type class.++> class BooleanSolver c+>  where+>   lookupBoolean :: Int -> c -> Maybe Bool+>   assertBoolean :: MonadPlus m => c -> Boolean -> c -> m c++A transformed boolean solver is still a boolean solver.++> instance (BooleanSolver c, Transformer t) => BooleanSolver (t c)+>  where+>   lookupBoolean n = lookupBoolean n . project+>   assertBoolean _ = inside . assertBoolean undefined++We define a context transformer that adds SAT-solving capabilities to+an arbitrary context.++> data SatCtx c = SatCtx SatSolver c+>+> instance Transformer SatCtx+>  where+>   project (SatCtx _ c) = c+>   replace (SatCtx s _) = SatCtx s++A context of type `SatCtx c` is always a boolean solver.++> instance BooleanSolver (SatCtx c)+>  where+>   lookupBoolean   n (SatCtx s _) = lookupVar n s+>   assertBoolean _ b (SatCtx s c) = liftM (flip SatCtx c) (assertTrue b s)++It is also solvable.++> instance Solvable c => Solvable (SatCtx c)+>  where+>   solvable (SatCtx s c) = isSolvable s && solvable c+>   bindVars (SatCtx s c) = liftM2 SatCtx (solve s) (bindVars c)++We define a strategy transformer to create SAT solving strategies.++> newtype Sat s a = Sat { fromSat :: s a }+>  deriving (Monad, MonadPlus, Enumerable)+>+> type instance Ctx (Sat s) = SatCtx (Ctx s)+> type instance Res (Sat s) = Sat (Res s)+>+> instance BooleanSolver c => StrategyT c Sat+>  where+>   liftStrategy _ = Sat+>   baseStrategy _ = fromSat+>+>   alterNarrowed c n b = maybe b (const (return True)) (lookupBoolean n c)++The context of a sat solving strategy is initialized with a new sat+solver.++> satSolving :: Monad s => s c -> Sat s (SatCtx c)+> satSolving = Sat . liftM (SatCtx newSatSolver)+++Narrowing and Guards+====================++We provide an instance of `Narrow` for booleans in order to be able to+create logic boolean variables. We can create such variables if the+evaluation context is a boolean solver.++> instance BooleanSolver c => Narrow c Boolean+>  where+>   narrow (Context c) u =+>     let v = label u+>      in maybe (var (nondet v))+>               (\b -> if b then yes else no)+>               (lookupBoolean v c)++The function `ifThen` implements a guard for boolean formulas.++> ifThen :: (CFLP s, BooleanSolver (Ctx s))+>        => Data s Boolean -> Data s a -> Context (Ctx s) -> Data s a+> ifThen x y = withPrim x $ \b c ->+>   joinNondet (do update (assertBoolean c b); return y)++We also provide `ifThenElse`.++> ifThenElse :: (CFLP s, BooleanSolver (Ctx s))+>            => Data s Boolean -> Data s a -> Data s a+>            -> Context (Ctx s) -> Data s a+> ifThenElse x y z = withPrim x $ \b c ->+>   joinNondet ((do update (assertBoolean c b); return y)+>               `mplus` -- don't need choice constraints here!+>               (do update (assertBoolean c (Not b)); return z))++Boolean constraints can be converted to boolean data terms.++> booleanToBool :: (CFLP s, BooleanSolver (Ctx s))+>               => Data s Boolean -> Context (Ctx s) -> Data s Bool+> booleanToBool b = withHNF b $ \b c@(Context cs) ->+>   case b of+>     FreeVar u x -> Typed $ +>       maybe (return (FreeVar u (untyped (ifThenElse (Typed x) true false c))))+>             (untyped . nondet)+>             (lookupBoolean (label u) cs)+>     Delayed check resume -> Typed $ do+>       narrowed <- check c+>       if narrowed+>        then untyped (booleanToBool (Typed (resume c)) c)+>        else return (Delayed check+>               (\c -> untyped (booleanToBool (Typed (resume c)) c)))+>     _ -> ifThenElse (Typed (return b)) true false c+

@@ -19,8 +19,10 @@ > > module CFLP.Control.Strategy ( >->   Enumerable(..), Ctx, Res, Strategy(..), Transformer(..), StrategyT(..),+>   Enumerable(..), Solvable(..), Ctx, Res,  >+>   Strategy(..), Transformer(..), StrategyT(..),+> >   Monadic(..), inside > >  ) where@@ -56,6 +58,21 @@  > type instance Res (UpdateT c m) = m +Evaluation context must provide a predicate that tells whether they+are solvable.++> class Solvable c+>  where+>   solvable     :: c -> Bool+>   bindVars :: MonadPlus m => c -> m c++The unit context is solvable.++> instance Solvable ()+>  where+>   solvable _ = True+>   bindVars   = return+ A strategy is parameterised by an evlauation context of type `c`. The type of this context may be different from `Ctx s` because a strategy can be transformed. The strategy operations need to be able to access@@ -150,6 +167,15 @@  transforms the base value of a transformed value with a monadic update operation.++If an evaluation context is solvable, then a transformed context also+is. This instance may overlap with more specific instances that+redefine the operation for specific solvers.++> instance (Solvable c, Transformer t) => Solvable (t c)+>  where+>   solvable = solvable . project+>   bindVars = inside bindVars   Strategy Transformers

@@ -137,6 +137,19 @@ > dTrue  c True  = Just (c []) > dTrue  _ _     = Nothing +We can even define an instance of integers:++> instance ApplyCons Int where type Result Int = Int; applyCons = const+> instance Generic Int+>  where constr = foldr1 (!) . map intCons $ interleaved [0..] [-1,-2..]+>+> interleaved :: [a] -> [a] -> [a]+> interleaved []     ys = ys+> interleaved (x:xs) ys = x : interleaved ys xs+>+> intCons :: Int -> Int -> GenericOps Int+> intCons n = cons (show n) n (\c m -> if n==m then Just (c []) else Nothing)+ Combinators ----------- 

@@ -22,14 +22,6 @@ > import CFLP.Data.Generic > > import CFLP.Control.Monad.Update->-> withHNF :: (Monad m, Update cs m m)->         => Nondet cs m a->         -> (HeadNormalForm cs m -> Context cs -> Nondet cs m b)->         -> Context cs -> Nondet cs m b-> withHNF x b (Context cs) = Typed (do->   (hnf,cs') <- runStateT (updateState (untyped x)) cs->   untyped (b hnf (Context cs')))  The `withHNF` operation can be used for pattern matching and solves constraints associated to the head constructor of a non-deterministic@@ -38,13 +30,13 @@ computed value by using an appropriate instance of `Update` that does not eliminate them. -> class WithUntyped a->  where->   type C a->   type M a :: * -> *->   type T a->->   withUntyped :: a -> [Untyped (C a) (M a)] -> Nondet (C a) (M a) (T a)+> withHNF :: (Monad m, Update cs m m)+>         => Nondet cs m a+>         -> (HeadNormalForm cs m -> Context cs -> Nondet cs m b)+>         -> Context cs -> Nondet cs m b+> withHNF x b (Context cs) = Typed (do+>   (hnf,cs') <- runStateT (updateState (untyped x)) cs+>   untyped (b hnf (Context cs')))  We repeat the definition of the type class `With` because the current implementation of GHC does not allow equality constraints in@@ -59,6 +51,14 @@ So it is just a copy of the type class `With` where the argument type is specialized to use the same monad. +> class WithUntyped a+>  where+>   type C a+>   type M a :: * -> *+>   type T a+>+>   withUntyped :: a -> [Untyped (C a) (M a)] -> Nondet (C a) (M a) (T a)+> > instance WithUntyped (Nondet cs m a) >  where >   type C (Nondet cs m a) = cs@@ -99,18 +99,26 @@ >   = Match { unMatch :: (Int, Context cs -> Branch cs m b) } > > type Branch cs m a = [Untyped cs m] -> Nondet cs m a->++The operation `match` is used to build destructor functions for+non-deterministic values that can be used with `caseOf`.+ > match :: WithUntyped a >       => Int -> (Context (C a) -> a) -> Match t (C a) (M a) (T a) > match n alt = Match (n, withUntyped . alt) -The operation `match` is used to build destructor functions for-non-deterministic values that can be used with `caseOf`.+Failure is just a type version of `mzero`.  > failure :: MonadPlus m => Nondet cs m a > failure = Typed mzero -Failure is just a type version of `mzero`.+We provide operations `caseOf_` and `caseOf` (with and without a+default alternative) for more convenient pattern matching. The untyped+values are hidden so functional-logic code does not need to match on+the `Cons` constructor explicitly. However, using this combinator+causes an additional slowdown because of the list lookup. It remains+to be checked how big the slowdown of using `caseOf` is compared to+using `withHNF` directly.  > caseOf :: (MonadPlus m, Update cs m m) >        => Nondet cs m a -> [Match a cs m b] -> Context cs -> Nondet cs m b@@ -123,7 +131,7 @@ >   withHNF x $ \hnf cs -> >   case hnf of >     FreeVar _ y -> caseOf_ (Typed y) bs def cs->     Delayed isn res -> Typed . join . liftM untyped $ do+>     Delayed isn res -> joinNondet $ do >       narrowed <- isn cs >       return $ if narrowed >                 then caseOf_ (Typed (res cs)) bs def cs@@ -131,14 +139,6 @@ >     Cons label args -> >       maybe def (\b -> b cs args) (lookup (index label) (map unMatch bs)) >     Lambda _ -> error "CFLP.Data.Matching.caseOf: cannot match lambda"--We provide operations `caseOf_` and `caseOf` (with and without a-default alternative) for more convenient pattern matching. The untyped-values are hidden so functional-logic code does not need to match on-the `Cons` constructor explicitly. However, using this combinator-causes an additional slowdown because of the list lookup. It remains-to be checked how big the slowdown of using `caseOf` is compared to-using `withHNF` directly.   Defining Constructor and Destructor Functions

@@ -3,17 +3,22 @@  > {-# LANGUAGE >       FlexibleContexts,+>       FlexibleInstances, >       MultiParamTypeClasses >   #-} > > module CFLP.Data.Narrowing ( >->   unknown, Narrow(..), oneOf, (?)+>   unknown, Narrow(..), -- Binding(..), narrowVar,  >+>   (?), oneOf+> > ) where > > import Data.Supply >+> import Control.Monad+> > import CFLP.Data.Types > > import CFLP.Control.Monad.Update@@ -22,7 +27,7 @@ The application of `unknown` to a constraint store and a unique identifier represents a logic variable of an arbitrary type.  -> unknown :: (Monad s, Strategy c s, MonadUpdate c s, Narrow a)+> unknown :: (Monad s, Strategy c s, MonadUpdate c s, Update c s s, Narrow c a) >         => ID -> Nondet c s a > unknown u = freeVar u (delayed (isNarrowedID u) (`narrow`u)) >@@ -36,9 +41,9 @@ non-deterministic generator using `oneOf`, but for specific types different strategies may be implemented. -> class Narrow a+> class Narrow c a >  where->   narrow :: (Monad s, Strategy c s, MonadUpdate c s)+>   narrow :: (Monad s, Strategy c s, MonadUpdate c s, Update c s s) >          => Context c -> ID -> Nondet c s a  The operator `(?)` wraps the combinator `oneOf` to generate a delayed@@ -59,3 +64,60 @@ >       => [Nondet c s a] -> Context c -> ID -> Nondet c s a > oneOf xs (Context c) (ID us) >   = Typed (choose c (supplyValue us) (map untyped xs))+++Constraint Solving+------------------++We provide a type class for constraint stores that support branching+on variables.++ class Solver c+  where+   branchOn :: MonadPlus m => c -> Int -> c -> m c++The first argument of `branchOn` is only used to support the type+checker. It must be ignored when instantiating the `Solver` class.++The type class `Binding` defines a function that looks up a variable+binding in a constraint store.++ class Binding c a+  where+   binding :: (Monad m, Update cs m m) => c -> Int -> Maybe (Nondet cs m a)++The result of the `binding` function is optional in order to allow for+composing results when transforming evaluation contexts.++The base instance for the unit context always returns `Nothing`:++ instance Binding () a where binding _ _ = Nothing++We provide a default implementation of the `narrow` function for+constraint solvers that support variable lookups. This function can be+used to define the `Narrow` instance for types that are handled by+constraint solvers.++ narrowVar :: (Monad s, Strategy c s, MonadUpdate c s, +               Update c s s, Narrow a, Solver c, Binding c a)+           => Context c -> ID -> Nondet c s a+ narrowVar (Context c) u@(ID us) = joinNondet $ do+   let v = supplyValue us+   isn <- isNarrowed c v+   if isn+    then maybe (error "no binding for narrowed variable") return (binding c v)+    else do+     update (branchOn c v)+     return (unknown u)++An evaluation context that is a `Solver` or supports `Binding` can be+transformed without losing this functionality.++ instance (Solver c, Transformer t) => Solver (t c)+  where+   branchOn _ = inside . branchOn undefined++ instance (Binding c a, Transformer t) => Binding (t c) a+  where+   binding = binding . project+

@@ -7,7 +7,7 @@ > > module CFLP.Data.Primitive ( >->   nondet, groundNormalForm, partialNormalForm,+>   nondet, groundNormalForm, partialNormalForm, withPrim, > >   prim_eq >@@ -33,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 = flip groundNormalForm (Typed x) $ return $ +>  where gnf x = liftM fst $ flip groundNormalForm (Typed x) $ return $  >                  error "Primitive.nf2hnf: primitive function uses context"  The `...NormalForm` functions evaluate a non-deterministic value and@@ -43,16 +43,17 @@ variables while ground normal forms are data terms.  > groundNormalForm :: (Monad s, Monad m, Update c s m)->                  => s c -> Nondet c s a -> m NormalForm+>                  => s c -> Nondet c s a -> m (NormalForm,c) > groundNormalForm c x >   = evalStateT (updateState c) (undefined `asContextOf` c) >>=->     evalStateT (gnf (untyped x))+>     runStateT (gnf (untyped x)) >-> partialNormalForm :: (Monad s, Strategy c s, Monad m, Update c s m)->                   => s c -> Nondet c s a -> m NormalForm+> partialNormalForm :: (Monad s, Strategy c s, Solvable c, +>                       MonadPlus m, Update c s m)+>                   => s c -> Nondet c s a -> m (NormalForm,c) > partialNormalForm c x >   = evalStateT (updateState c) (undefined `asContextOf` c) >>=->     evalStateT (pnf (untyped x))+>     runStateT (pnf (untyped x)) > > asContextOf :: c -> s c -> c > asContextOf = const@@ -72,11 +73,12 @@ > mkVar :: ID -> a -> NormalForm > mkVar (ID us) _ = Var (supplyValue us) >-> pnf :: (Monad s, Strategy c s, Monad m, Update c s m)+> pnf :: (Monad s, Strategy c s, Solvable c, MonadPlus m, Update c s m) >     => Untyped c s -> StateT c m NormalForm-> pnf x->    = nf isNarrowed ((return.).Cons) ((return.).FreeVar) (return.Lambda) x->  >>= nf isNarrowed Data mkVar Fun+> pnf x = do+>   y <- nf isNarrowed ((return.).Cons) ((return.).FreeVar) (return.Lambda) x+>   get >>= bindVars >>= put+>   nf isNarrowed Data mkVar Fun y  The `nf` function is used by all normal-form functions and performs all the work.@@ -100,6 +102,17 @@ >       nfs <- mapM (nf isn cns fv fun) args >       return (cns label nfs) >     Lambda _ -> return . fun $ error "Data.LazyNondet.Primitive.nf: function"++We provide combinator similar to `withHNF` for matching primitive+ground-normal forms.++> withPrim :: (Monad s, Update c s s, Generic a)+>          => Nondet c s a+>          -> (a -> c -> Nondet c s b)+>          -> Context c -> Nondet c s b+> withPrim x f (Context c) = Typed $ do+>   (y,c') <- runStateT (gnf (untyped x)) c+>   untyped (f (primitive y) c')  We provide a generic comparison function for untyped non-deterministic data that is used to define a typed equality test in the

@@ -11,22 +11,30 @@ > > module CFLP.Data.Types ( >->   Context(..), ID(..), +>   Context(..), ID(..), label, > >   ConsLabel(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..), >->   freeVar, delayed+>   freeVar, delayed, joinNondet > > ) where > > import Data.Supply >+> import Control.Monad+> > import CFLP.Control.Monad.Update > > newtype Context cs = Context cs > > newtype ID = ID (Supply Int) >+> label :: ID -> Int+> label (ID us) = supplyValue us++The normal form of data is represented by the type `NormalForm` which+defines a tree of constructors and logic variables or functions.+ > data NormalForm >   = Data ConsLabel [NormalForm] >   | Var  Int@@ -38,8 +46,10 @@ >  where >   showsPrec _ = (++) . name -The normal form of data is represented by the type `NormalForm` which-defines a tree of constructors and logic variables or functions.+Data in lazy functional-logic programs is evaluated on demand. The+evaluation of arguments of a constructor may lead to different+non-deterministic results. Hence, we use a monad around every+constructor in the head-normal form of a value.  > data HeadNormalForm cs m >   = Cons ConsLabel [Untyped cs m]@@ -49,41 +59,43 @@ > > type Untyped cs m = m (HeadNormalForm cs m) -Data in lazy functional-logic programs is evaluated on demand. The-evaluation of arguments of a constructor may lead to different-non-deterministic results. Hence, we use a monad around every-constructor in the head-normal form of a value.--> newtype Nondet cs m a = Typed { untyped :: Untyped cs m }- Untyped non-deterministic data can be phantom typed in order to define logic variables by overloading. The phantom type must be the Haskell data type that should be used for conversion into primitive data. +> newtype Nondet cs m a = Typed { untyped :: Untyped cs m }+ Free (logic) variables are represented by `FreeVar u x` where `u` is a uniqe identifier and `x` represents the result of narrowing the variable according to the constraint store passed to the operation that creates the variable. -> freeVar :: Monad m => ID -> Nondet cs m a -> Nondet cs m a-> freeVar u = Typed . return . FreeVar u . untyped- The function `freeVar` is used to put a name around a narrowed free variable. -> delayed :: Monad m => (Context cs -> m Bool) -> (Context cs -> Nondet cs m a)->         -> Nondet cs m a-> delayed p resume = Typed . return . Delayed p $ (untyped . resume)+> freeVar :: Monad m => ID -> Nondet cs m a -> Nondet cs m a+> freeVar u = Typed . return . FreeVar u . untyped  With `delayed` computations can be delayed to be reexecuted with the current constraint store whenever they are demanded. This is useful to avoid unessary branching when narrowing logic variables. Use with care: `delayed` intentionally destroys sharing! +> delayed :: Monad m => (Context cs -> m Bool) -> (Context cs -> Nondet cs m a)+>         -> Nondet cs m a+> delayed p resume = Typed . return . Delayed p $ (untyped . resume)+ The first parameter is a predicate on constraint stores that specifies whether the result of pattern matching the constructed delayed value is narrowed w.r.t. the current evaluation context. If it is not, pattern matching on it will be delayed again.++The function `joinNondet` transforms a monadic action that yields a+non-deterministic value into a single non-deterministic value by+lifting the monad inside the newtype constructor.++> joinNondet :: Monad m => m (Nondet c m a) -> Nondet c m a+> joinNondet = Typed . join . liftM untyped  `Show` Instances ----------------

@@ -7,13 +7,19 @@ > {-# LANGUAGE >       MultiParamTypeClasses, >       FlexibleInstances,->       TypeFamilies+>       FlexibleContexts,+>       TypeFamilies,+>       RankNTypes >   #-} > > module CFLP.Strategies ( >->   dfs, limDFS, iterDFS, bfs, diag, fair, rndDFS+>   Computation, >+>   dfs, limDFS, iterDFS, bfs, diag, fair, rndDFS,+>+>   dfs_B, limDFS_B, iterDFS_B, bfs_B, diag_B, fair_B, rndDFS_B+> >  ) where > > import Control.Monad.Logic@@ -26,6 +32,8 @@ > import CFLP.Strategies.DepthCounter > import CFLP.Strategies.DepthLimit > import CFLP.Strategies.Random+>+> import CFLP.Constraints.Boolean  We provide shortcuts for useful strategies. @@ -34,20 +42,20 @@ > instance Enumerable []    where enumeration = id > instance Enumerable Logic where enumeration = observeAll > -- using `Logic` instead of `[]` destroys sharing. Investigate.-> dfs :: [CTC (Monadic (UpdateT (StoreCTC ()) Logic)) (StoreCTC ())]+> dfs :: [CTC (Monadic (UpdateT (StoreCTC ()) [])) (StoreCTC ())] > dfs = [callTimeChoice monadic]  depth-first search with limited depth:  > limDFS :: Int >        -> [CTC (Depth (DepthLim (Monadic->                 (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) Logic))))+>                 (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) [])))) >                (StoreCTC (DepthCtx (DepthLimCtx ())))] > limDFS l = [limitedDepthFirstSearch l] > > limitedDepthFirstSearch >  :: Int -> CTC (Depth (DepthLim (Monadic->                  (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) Logic))))+>                  (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) [])))) >                (StoreCTC (DepthCtx (DepthLimCtx ()))) > limitedDepthFirstSearch l >   = callTimeChoice . countDepth . limitDepth l $ monadic@@ -55,7 +63,7 @@ iterative deepening depth-first search:  > iterDFS :: [CTC (Depth (DepthLim (Monadic->                   (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) Logic))))+>                   (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) [])))) >                 (StoreCTC (DepthCtx (DepthLimCtx ())))] > iterDFS = map limitedDepthFirstSearch [0..] @@ -75,9 +83,6 @@  Fair interleaving by Oleg Kiselyov: -Instead of using `Monadic` we provide a custom instance of-`Strategy`. We need to suspend choices in order to ensure fairness.- > instance Enumerable Stream where enumeration = runStream > > fair :: [CTC (Monadic (UpdateT (StoreCTC ()) Stream)) (StoreCTC ())]@@ -87,10 +92,68 @@ to use the call-time choice transformer *before* the randomizer shuffles choices. -> rndDFS :: [CTC (Rnd (Monadic (UpdateT (StoreCTC (RndCtx ())) Logic)))+> rndDFS :: [CTC (Rnd (Monadic (UpdateT (StoreCTC (RndCtx ())) []))) >                (StoreCTC (RndCtx ()))] > rndDFS = [callTimeChoice . randomise $ monadic] +depth-first search with boolean constraints:++> dfs_B :: [CTC (Sat (Monadic (UpdateT (StoreCTC (SatCtx ())) [])))+>               (StoreCTC (SatCtx ()))]+> dfs_B = [callTimeChoice . satSolving $ monadic]++depth-first search with boolean constraints and limited depth:++> limDFS_B :: Int+>          -> [CTC (Depth (DepthLim (Sat (Monadic+>                   (UpdateT (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))+>                            [])))))+>                  (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))]+> limDFS_B l = [limitedDepthFirstSearch_B l]+>+> limitedDepthFirstSearch_B+>  :: Int -> CTC (Depth (DepthLim (Sat (Monadic+>                  (UpdateT (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))+>                           [])))))+>                (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))+> limitedDepthFirstSearch_B l+>   = callTimeChoice . countDepth . limitDepth l . satSolving $ monadic++iterative deepening depth-first search with boolean constraints:++> iterDFS_B :: [CTC (Depth (DepthLim (Sat (Monadic+>                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))+>                              [])))))+>                   (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))]+> iterDFS_B = map limitedDepthFirstSearch_B [0..]++breadth-first search with boolean constraints:++> bfs_B :: [CTC (Sat (Monadic (UpdateT (StoreCTC (SatCtx ())) Levels)))+>               (StoreCTC (SatCtx ()))]+> bfs_B = [callTimeChoice . satSolving $ monadic]++Fair diagonalization by Luke Palmer with boolean constraints:++> diag_B :: [CTC (Sat (Monadic (UpdateT (StoreCTC (SatCtx ())) Omega)))+>                (StoreCTC (SatCtx ()))]+> diag_B = [callTimeChoice . satSolving $ monadic]++Fair interleaving by Oleg Kiselyov with boolean constraints:++> fair_B :: [CTC (Sat (Monadic (UpdateT (StoreCTC (SatCtx ())) Stream)))+>                (StoreCTC (SatCtx ()))]+> fair_B = [callTimeChoice . satSolving $ monadic]++We combine randomization with depth-first search. Here, it is crucial+to use the call-time choice transformer *before* the randomizer+shuffles choices.++> rndDFS_B :: [CTC (Rnd (Sat (Monadic (UpdateT (StoreCTC (RndCtx (SatCtx ())))+>                                         []))))+>                  (StoreCTC (RndCtx (SatCtx ())))]+> rndDFS_B = [callTimeChoice . randomise . satSolving $ monadic]+ Finally, we provide instances for the type class `CFLP` that is a shortcut for the class constraints of CFLP computations. @@ -103,4 +166,23 @@ > > instance (MonadPlus m, Enumerable m) >       => CFLP (CTC (Rnd (Monadic (UpdateT (StoreCTC (RndCtx ())) m))))+>+> instance (MonadPlus m, Enumerable m)+>       => CFLP (CTC (Sat (Monadic (UpdateT (StoreCTC (SatCtx ())) m))))+>+> instance (MonadPlus m, Enumerable m)+>       => CFLP (CTC (Depth (DepthLim (Sat (Monadic+>                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx (SatCtx ()))))+>                              m))))))+>+> instance (MonadPlus m, Enumerable m)+>       => CFLP (CTC (Rnd (Sat (Monadic (UpdateT+>                                        (StoreCTC (RndCtx (SatCtx ())))+>                                        m)))))++We also define a shortcut for computations.++> type Computation a+>   = forall s . (CFLP s, BooleanSolver (Ctx s)) =>+>     Context (Ctx s) -> ID -> Data s a 

@@ -3,7 +3,10 @@  This module defines auxiliary functions for the test suite. -> {-# LANGUAGE RankNTypes #-}+> {-# LANGUAGE+>       FlexibleContexts,+>       RankNTypes+>   #-} > > module CFLP.Tests where >@@ -26,7 +29,7 @@ > assertResultsLimit :: (Generic a, Show a, Eq a) >                    => Maybe Int -> Computation a -> [a] -> Assertion > assertResultsLimit limit op expected = do->   actual <- eval (limDFS 100) op+>   actual <- eval (limDFS_B 100) op >   maybe id take limit actual @?= expected  We provide auxiliary assertions `assertResults...` that compute (a

@@ -0,0 +1,86 @@+% Testing Boolean Constraints in CFLP+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module defines tests that show how to use boolean constraints in+constraint functional-logic programs.++> {-# LANGUAGE+>       FlexibleContexts+>   #-}+>+> module CFLP.Tests.Boolean where+>+> import Test.HUnit+>+> import CFLP+> import CFLP.Tests+>+> import CFLP.Strategies+> import CFLP.Constraints.Boolean+>+> import Prelude hiding ( map )+> import CFLP.Types.Bool+> import CFLP.Types.List+>+> tests :: Test+> tests = "boolean constraints" ~: test+>   [ "assert variable" ~: assertVariable,+>     "x and y and z" ~: xAndYandZ,+>     "unsatisfiable" ~: unsatisfiable,+>     "unsatisfiable with backtracking" ~: unsatisfiableWithBacktracking+>   ]++This tests asserts a logic variable and queries it afterwards.++> assertVariable :: Assertion+> assertVariable = assertResults comp [True]+>  where+>   comp :: Computation Bool+>   comp c u = let x = unknown u in ifThen x (booleanToBool x c) c++This test queries all solutions to the formula `x && y || z`.++> xAndYandZ :: Assertion+> xAndYandZ = assertResults comp [[True,True,True]]+>  where+>   comp :: Computation [Bool]+>   comp c = withUnique $ \u1 u2 u3 u4 ->+>              let x = unknown u1+>                  y = unknown u2+>                  z = unknown u3+>               in ifThen (x.&&.y.&&.z)+>                         (map (fun booleanToBool) (x^:y^:z^:nil) c u4) c++This tests asserts an unsatisfiable formula.++> unsatisfiable :: Assertion+> unsatisfiable = assertResults comp []+>  where+>   comp :: Computation [Bool]+>   comp c = withUnique $ \u1 u2 u3 u4 ->+>              let x = unknown u1+>                  y = unknown u2+>                  z = unknown u3+>                  vars = map (fun booleanToBool) (x^:y^:z^:nil) c u4+>                  formula = (neg x .||. y)+>                       .&&. (x .||. neg y)+>                       .&&. (neg y .||. z)+>                       .&&. (y .||. neg z)+>                       .&&. (neg x .||. neg z)+>                       .&&. (x .||. z)+>               in ifThen formula vars c++This test asserts an unsatisfiable formula that is only detected as+such after backtracking.++> unsatisfiableWithBacktracking :: Assertion+> unsatisfiableWithBacktracking = assertResults comp []+>  where+>   comp :: Computation Bool+>   comp c = withUnique $ \u1 u2 ->+>              let x = unknown u1+>                  y = unknown u2+>                  formula = (x .&&. neg x) .||. (y .&&. neg y)+>               in ifThen formula true c++

@@ -4,10 +4,16 @@ This module defines tests that show how to define higher-order functional-logic programs. +> {-# LANGUAGE+>       FlexibleContexts+>   #-}+> > module CFLP.Tests.HigherOrder where > > import CFLP > import CFLP.Tests+>+> import CFLP.Strategies > > import Test.HUnit >

@@ -31,7 +31,7 @@ In order to be able to use logic variables of boolean type, we make it an instance of the type class `Narrow`. -> instance Narrow Bool+> instance Narrow c Bool >  where >   narrow = oneOf [false,true] 

@@ -48,7 +48,7 @@ We can use logic variables of a list type if there are logic variables for the element type. -> instance (Narrow a, Generic a) => Narrow [a]+> instance (Narrow c a, Generic a) => Narrow c [a] >  where >   narrow cs u = withUnique (\u1 u2 ->  >                   (oneOf [nil, unknown u1 ^: unknown u2] cs u)) u