cflp 0.0.2.1 → 0.1

raw patch · 12 files changed

+267/−104 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• INSTALL +6/−7
• README +3/−3
• Test.lhs +15/−0
• cflp.cabal +7/−6
• src/Control/CFLP.lhs +12/−4
• src/Control/CFLP/Tests.lhs +6/−14
• src/Control/CFLP/Tests/CallTimeChoice.lhs +0/−1
• src/Control/Monad/Constraint.lhs +0/−1
• src/Control/Monad/Constraint/Choice.lhs +0/−2
• src/Data/LazyNondet.lhs +182/−35
• src/Data/LazyNondet/Bool.lhs +18/−14
• src/Data/LazyNondet/List.lhs +18/−17

@@ -1,17 +1,16 @@ # Installation Instructions -## Installation with Cabal--You can install the `cflp` package using Cabal as follows.+You can install the `cflp` package as follows.   1. Unpack the sources and move into the source directory.          > tar -xzf cflp-*.tar.gz         > cd cflp-* - 2. Run configure, build and install.+ 2. Run configure, build, test, and install. -        > ./Setup.lhs configure --user-        > ./Setup.lhs build-        > ./Setup.lhs install+        > runhaskell Setup.lhs configure --user+        > runhaskell Setup.lhs build+        > runhaskell Setup.lhs test+        > runhaskell Setup.lhs install 

@@ -2,9 +2,9 @@  The `cflp` package provides a module `Control.CFLP` with combinators for constraint functional-logic programming ((C)FLP) in Haskell. The-combinators can be used as a target language for compiling programs-written in an FLP language like Curry or Toy. Another application of-FLP is demand driven test-case generation.+combinators might later be used as a target language for compiling+programs written in an FLP language like Curry or Toy. Another+application of FLP is demand driven test-case generation.  Consult the LICENSE file for copyright issues, the INSTALL file for installation instructions, or the [project website][cflp] for

@@ -0,0 +1,15 @@+% Testing the `cflp` Package+% Sebastian Fischer (sebf@informatik.uni-kiel.de)+% November, 2008++This module is used in the hook that runs the tests for the `cflp`+package.++> import Test.HUnit+> import Control.CFLP.Tests.CallTimeChoice as CTC+>+> main :: IO ()+> main = do+>  runTestTT $ test [CTC.tests]+>  return ()+

@@ -1,12 +1,13 @@ Name:          cflp-Version:       0.0.2.1+Version:       0.1 Cabal-Version: >= 1.2 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint                functional-logic programming ((C)FLP) in Haskell. The -               combinators can be used as a target language for compiling -               programs written in an FLP language like Curry or Toy. Another -               application of FLP is demand driven test-case generation.+               combinators might later be used as a target language for +               compiling programs written in an FLP language like Curry +               or Toy. Another application of FLP is demand driven +               test-case generation. Category:      Control License:       BSD3 License-File:  LICENSE@@ -16,7 +17,7 @@ Build-Type:    Custom Stability:     alpha -Extra-Source-Files: README, INSTALL+Extra-Source-Files: README, INSTALL, Test.lhs  Library   Build-Depends:    base >= 4, ghc, mtl, syb, HUnit@@ -35,8 +36,8 @@                     FlexibleContexts,                     TypeFamilies,                     RankNTypes+  Ghc-Options:      -O2 -Wall -fno-warn-orphans  Source-Repository head   type:     git   location: git://github.com/sebfisch/cflp.git-

@@ -13,7 +13,7 @@ > > module Control.CFLP ( >->   CFLP, EvalStore, eval, evalPrint,+>   CFLP, Computation, eval, evalPrint, > >   Strategy, depthFirst, >@@ -37,7 +37,9 @@ >  => CFLP cs m  The type class `CFLP` is a shortcut for the type-class constraints on-constraint functional-logic operations.+constraint functional-logic computations that are parameterized over a+constraint store and a constraint monad. Hence, such computations can+be executed with different constraint stores and search strategies.  > instance CFLP ChoiceStore (ConstrT ChoiceStore []) @@ -48,6 +50,8 @@ > > noConstraints :: EvalStore > noConstraints = noChoices+>+> type Computation m a = EvalStore -> ID -> Nondet (ConstrT EvalStore m) a  Currently, the constraint store used to evaluate constraint functional-logic programs is simply a `ChoiceStore`. It will be a@@ -83,9 +87,13 @@ > printSols []     = putStrLn "No more solutions." > printSols (x:xs) = do >   print x->   putStr "more? [Y|n]: "+>   putStr "more? [Y(es)|n(o)|a(ll)]: " >   s <- getLine->   if s `elem` ["n","no"] then return () else printSols xs+>   if s `elem` ["n","no"] then+>     return ()+>    else if s `elem` ["a","all"]+>     then mapM_ print xs+>     else printSols xs  For convenience, we provide an `evalPrint` operation that interactively shows solutions of a constraint functional-logic

@@ -1,34 +1,26 @@ % Testing the `cflp` Package % Sebastian Fischer (sebf@informatik.uni-kiel.de) -This module defines auxiiary functions for the test suite.+This module defines auxiliary functions for the test suite.  > module Control.CFLP.Tests where > > import Control.CFLP-> import Control.Monad.Constraint > import Test.HUnit  We use HUnit for testing because we need to test IO actions and want to use errors when testing laziness.  > assertResults :: (Data a, Show a, Eq a)->               => (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)->               -> [a] -> Assertion+>               => (Computation [] a) -> [a] -> Assertion > assertResults = assertResultsLimit Nothing >-> assertResultsN ->   :: (Data a, Show a, Eq a)->   => Int->   -> (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)->   -> [a] -> Assertion+> assertResultsN :: (Data a, Show a, Eq a)+>                => Int -> (Computation [] a) -> [a] -> Assertion > assertResultsN = assertResultsLimit . Just >-> assertResultsLimit ->   :: (Data a, Show a, Eq a)->   => Maybe Int->   -> (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)->   -> [a] -> Assertion+> assertResultsLimit :: (Data a, Show a, Eq a)+>                    => Maybe Int -> (Computation [] a) -> [a] -> Assertion > assertResultsLimit limit op expected = do >   actual <- eval depthFirst op >   maybe id take limit actual @?= expected

@@ -13,7 +13,6 @@ > import Test.HUnit > > import Control.CFLP-> import Control.Monad.Constraint > > import Prelude hiding ( not, null, head ) >

@@ -22,7 +22,6 @@ > > ) where > -> import Control.Monad > import Control.Monad.State > import Control.Monad.Trans >

@@ -21,12 +21,10 @@ > > ) where >-> import Control.Monad > import Control.Monad.State > import Control.Monad.Constraint > > import Unique-> import UniqSupply > import UniqFM  We borrow unique identifiers from the package `ghc` which is hidden by

@@ -5,36 +5,38 @@ non-deterministic programming.  > {-# LANGUAGE+>       ExistentialQuantification, >       MultiParamTypeClasses, >       FlexibleInstances, >       FlexibleContexts,->       TypeFamilies+>       TypeFamilies,+>       FunctionalDependencies >   #-} > > module Data.LazyNondet ( > >   NormalForm, HeadNormalForm(..), mkHNF, Nondet(..), >->   ID, initID, WithUnique(..), +>   ID, initID, withUnique, >->   Unknown(..), failure, oneOf, caseOf,+>   Unknown(..), failure, oneOf, withHNF, caseOf, caseOf_, Match, >->   Data, normalForm+>   Data, nondet, normalForm, >+>   ConsRep(..), cons, match,+>+>   prim_eq+> > ) where > > import Data.Data > import Data.Generics.Twins ( gmapAccumT ) >-> import Control.Monad > import Control.Monad.State-> import Control.Monad.Trans > import Control.Monad.Constraint > import Control.Monad.Constraint.Choice >-> import Unique > import UniqSupply-> import UniqFM  We borrow unique identifiers from the package `ghc` which is hidden by default.@@ -75,32 +77,35 @@ Non-deterministic computations need a supply of unique identifiers in order to constrain shared choices. -> type ID = UniqSupply+> newtype ID = ID UniqSupply > > initID :: IO ID-> initID = mkSplitUniqSupply 'x'+> initID = liftM ID $ mkSplitUniqSupply 'x' >-> class WithUnique a+> class With x a >  where->   type Mon a :: * -> *->   type Typ a+>   type Mon x a :: * -> *+>   type Typ x a >->   withUnique :: a -> ID -> Nondet (Mon a) (Typ a)+>   with :: a -> x -> Nondet (Mon x a) (Typ x a) >-> instance WithUnique (Nondet m a)+> instance With x (Nondet m a) >  where->   type Mon (Nondet m a) = m->   type Typ (Nondet m a) = a+>   type Mon x (Nondet m a) = m+>   type Typ x (Nondet m a) = a >->   withUnique = const+>   with = const >-> instance WithUnique a => WithUnique (ID -> a)+> instance With ID a => With ID (ID -> a) >  where->   type Mon (ID -> a) = Mon a->   type Typ (ID -> a) = Typ a+>   type Mon ID (ID -> a) = Mon ID a+>   type Typ ID (ID -> a) = Typ ID a >->   withUnique f us = withUnique (f vs) ws+>   with f (ID us) = withUnique (f (ID vs)) (ID ws) >    where (vs,ws) = splitUniqSupply us+>+> withUnique :: With ID a => a -> ID -> Nondet (Mon ID a) (Typ ID a)+> withUnique = with  We provide an overloaded operation `withUnique` to simplify the distribution of unique identifiers when defining possibly@@ -108,7 +113,7 @@ additional argument for unique identifiers. The operation `withUnique` allows to consume an arbitrary number of unique identifiers hiding their generation. Conceptually, it has all of the following types at-once:+the same time:      Nondet m a -> ID -> Nondet m a     (ID -> Nondet m a) -> ID -> Nondet m a@@ -131,7 +136,7 @@ variable of the corresponding type.  > oneOf :: MonadConstr Choice m => [Nondet m a] -> ID -> Nondet m a-> oneOf xs us = Typed (choice (uniqFromSupply us) (map untyped xs))+> oneOf xs (ID us) = Typed (choice (uniqFromSupply us) (map untyped xs))  The operation `oneOf` takes a list of non-deterministic values and returns a non-deterministic value that yields one of the elements in@@ -143,21 +148,92 @@ A failing computation could be defined using `oneOf`, but we provide a special combinator that does not need a supply of unique identifiers. -> caseOf :: (Monad m, MonadSolve cs m m)->        => Nondet m a->        -> (HeadNormalForm m -> cs -> Nondet m b)->        -> cs -> Nondet m b-> caseOf x branch cs = Typed (do+> withHNF :: (Monad m, MonadSolve cs m m)+>         => Nondet m a+>         -> (HeadNormalForm m -> cs -> Nondet m b)+>         -> cs -> Nondet m b+> withHNF x b cs = Typed (do >   (hnf,cs') <- runStateT (solve (untyped x)) cs->   untyped (branch hnf cs'))+>   untyped (b hnf cs')) -The `caseOf` operation is used for pattern matching and solves+The `withHNF` operation can be used for pattern matching and solves constraints associated to the head constructor of a non-deterministic value. An updated constraint store is passed to the computation of the branch function. Collected constraints are kept attached to the computed value by using an appropriate instance of `MonadSolve` that does not eliminate them. +> caseOf :: MonadSolve cs m m+>        => Nondet m a -> [Match cs m b] -> cs -> Nondet m b+> caseOf x bs = caseOf_ x bs failure+>+> caseOf_ :: MonadSolve cs m m+>         => Nondet m a -> [Match cs m b] -> Nondet m b -> cs -> Nondet m b+> caseOf_ x bs def =+>   withHNF x $ \ (Cons _ idx args) cs ->+>                  maybe def (\b -> branch (b cs) args)+>                   (lookup idx (map unMatch bs))+>+> newtype Match cs m a = Match { unMatch :: (ConIndex, cs -> Branch m a) }+> data Branch m a = forall t . (WithUntyped t, m ~ M t, a ~ T t) => Branch t+>+> branch :: Branch m a -> [Untyped m] -> Nondet m a+> branch (Branch alt) = withUntyped alt++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.++> class WithUntyped a+>  where+>   type M a :: * -> *+>   type T a+>+>   withUntyped :: a -> [Untyped (M a)] -> Nondet (M a) (T a)++We repeat the definition of the type class `With` because the current+implementation of GHC does not allow equality constraints in+super-class constraints. We would prefer to define this class as+follows:++    class (With [Untyped m] a, m ~ Mon [Untyped m] a) => WithUnique a+     where+      withUnique :: a -> [Untyped m] -> Nondet m (Typ [Untyped m] a)+      withUnique = with++So it is just a copy of the type class `With` where the argument type+is specialized to use the same monad.++> instance WithUntyped (Nondet m a)+>  where+>   type M (Nondet m a) = m+>   type T (Nondet m a) = a+>+>   withUntyped = const+>+> instance (WithUntyped a, m ~ M a) => WithUntyped (Nondet m b -> a)+>  where+>   type M (Nondet m b -> a) = M a+>   type T (Nondet m b -> a) = T a+>+>   withUntyped alt (x:xs) = withUntyped (alt (Typed x)) xs+>   withUntyped _ _ = error "LazyNondet.withUntyped: too few arguments"++These instances define the overloaded function `withUntyped` that has+all of the following types at the same time:++    withUntyped :: Nondet m a -> [Untyped m] -> Nondet m a+    withUntyped :: (Nondet m a -> Nondet m b) -> [Untyped m] -> Nondet m b+    ...++If the function given as first argument has n arguments, then the+application of `withUntyped` to this function consumes n elements of+the list of untyped values.+ Converting Between Primitive and Non-Deterministic Data ------------------------------------------------------- @@ -165,16 +241,16 @@ > prim (NormalForm con args) = >   snd (gmapAccumT perkid args (fromConstr con)) >  where->   perkid (t:ts) _ = (ts, prim t)+>   perkid ts _ = (tail ts, prim (head ts)) > > generic :: Data a => a -> NormalForm > generic x = NormalForm (toConstr x) (gmapQ generic x) >-> hnf :: Monad m => NormalForm -> Untyped m-> hnf (NormalForm con args) = return (mkHNF con (map hnf args))+> nf2hnf :: Monad m => NormalForm -> Untyped m+> nf2hnf (NormalForm con args) = return (mkHNF con (map nf2hnf args)) > > nondet :: (Monad m, Data a) => a -> Nondet m a-> nondet = Typed . hnf . generic+> nondet = Typed . nf2hnf . generic  We provide generic operations to convert between instances of the `Data` class and non-deterministic data.@@ -192,6 +268,77 @@ lifts all non-deterministic choices to the top level. The results are deterministic values and can be converted into their Haskell representation.++Syntactic Sugar for Datatype Declarations+-----------------------------------------++> class MkCons m a b | b -> m+>  where+>   mkCons :: a -> [Untyped m] -> b+>+> instance (Monad m, Data a) => MkCons m a (Nondet m t)+>  where+>   mkCons c args = Typed (return (mkHNF (toConstr c) (reverse args)))+>+> instance MkCons m b c => MkCons m (a -> b) (Nondet m t -> c)+>  where+>   mkCons c xs x = mkCons (c undefined) (untyped x:xs)+>+> cons :: MkCons m a b => a -> b+> cons c = mkCons c []++The overloaded operation `constr` takes a Haskell constructor and yields+a corresponding constructor function for non-deterministic values.++> match :: (ConsRep a, WithUntyped b)+>       => a -> (cs -> b) -> Match cs (M b) (T b)+> match c alt = Match (constrIndex (consRep c), Branch . alt)++The operation `decons` is used to build destructor functions for+non-deterministic values that can be used with `caseOf`.++> class ConsRep a+>  where+>   consRep :: a -> Constr+>+> instance ConsRep b => ConsRep (a -> b)+>  where+>   consRep c = consRep (c undefined)++We provide an overloaded operation `consRep` that yields a `Constr`+representation for a constructor rather than for a constructed value+like `Data.Data.toConstr` does. We do not provide the base instance++    instance Data a => ConsRep a+     where+      consRep = toConstr++because this would require to allow undecidable instances. As a+consequence, specialized base instances need to be defined for every+used datatype. See `Data.LazyNondet.List` for an example of how to get+the representation of polymorphic constructors and destructors.++Primitive Generic Functions+---------------------------++> prim_eq :: MonadSolve cs m m => Untyped m -> Untyped m -> StateT cs m Bool+> prim_eq x y = do+>   Cons _ ix xs <- solve x+>   Cons _ iy ys <- solve y+>   if ix==iy then all_eq xs ys else return False+>  where+>   all_eq [] [] = return True+>   all_eq (v:vs) (w:ws) = do+>     eq <- prim_eq v w+>     if eq then all_eq vs ws else return False+>   all_eq _ _ = return False++We provide a generic comparison function for untyped non-deterministic+data that is used to define a typed equality test in the+`Data.LazyNondet.Bool` module.++`Show` Instances+----------------  > instance Show (HeadNormalForm []) >  where

@@ -3,24 +3,27 @@  This module provides non-deterministic booleans. -> {-# LANGUAGE->       MultiParamTypeClasses,->       FlexibleContexts->   #-}-> > module Data.LazyNondet.Bool where > > import Data.Data > import Data.LazyNondet >+> import Control.Monad.State > import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice >+> instance ConsRep Bool where consRep = toConstr+> > true :: Monad m => Nondet m Bool-> true = Typed (return (mkHNF (toConstr True) []))+> true = cons True >+> pTrue :: (cs -> Nondet m a) -> Match cs m a+> pTrue = match True+> > false :: Monad m => Nondet m Bool-> false = Typed (return (mkHNF (toConstr False) []))+> false = cons False+>+> pFalse :: (cs -> Nondet m a) -> Match cs m a+> pFalse = match False  In order to be able to use logic variables of boolean type, we make it an instance of the type class `Unknown`.@@ -29,11 +32,12 @@ >  where >   unknown = oneOf [false,true] -Some operations on `Bool`s:+Some operations with `Bool`s:  > not :: MonadSolve cs m m => Nondet m Bool -> cs -> Nondet m Bool-> not x = ->   caseOf x $ \x' _ ->->   case x' of->     Cons _ 1 _ -> true->     Cons _ 2 _ -> false+> not x = caseOf_ x [pFalse (\_ -> true)] false++> (===) :: MonadSolve cs m m => Nondet m a -> Nondet m a -> cs -> Nondet m Bool+> (x === y) cs = Typed $ do+>   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs+>   untyped $ if eq then true else false

@@ -3,6 +3,10 @@  This module provides non-deterministic lists. +> {-# LANGUAGE+>       FlexibleInstances+>   #-}+> > module Data.LazyNondet.List where > > import Data.Data@@ -11,13 +15,21 @@ > > import Control.Monad.Constraint >+> instance ConsRep [()] where consRep = toConstr+> > nil :: Monad m => Nondet m [a]-> nil = Typed (return (mkHNF (toConstr ([]::[()])) []))+> nil = cons ([] :: [()]) >+> pNil :: (cs -> Nondet m a) -> Match cs m a+> pNil = match ([] :: [()])+> > infixr 5 ^: > (^:) :: Monad m => Nondet m a -> Nondet m [a] -> Nondet m [a]-> x^:xs = Typed (return (mkHNF (toConstr [()]) [untyped x, untyped xs]))+> (^:) = cons ((:) :: () -> [()] -> [()]) >+> pCons :: (cs -> Nondet m a -> Nondet m [a] -> Nondet m b) -> Match cs m b+> pCons = match ((:) :: () -> [()] -> [()])+> > fromList :: Monad m => [Nondet m a] -> Nondet m [a] > fromList = foldr (^:) nil @@ -32,22 +44,11 @@ Some operations on lists:  > null :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m Bool-> null xs =->   caseOf xs $ \xs' _ ->->   case xs' of->     Cons _ 1 _ -> true->     _ -> false+> null xs = caseOf_ xs [pNil (\_ -> true)] false > > head :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m a-> head l =->   caseOf l $ \l' cs ->->   case l' of->     Cons _ 1 _ -> failure->     Cons _ 2 [x',_] -> Typed x'+> head l = caseOf l [pCons (\_ x _ -> x)] > > tail :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m [a]-> tail l =->   caseOf l $ \l' cs ->->   case l' of->     Cons _ 1 _ -> failure->     Cons _ 2 [_,xs'] -> Typed xs'+> tail l = caseOf l [pCons (\_ _ xs -> xs)]+