packages feed

cflp 2009.1.15.2 → 2009.1.16

raw patch · 8 files changed

+160/−75 lines, 8 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Control.CFLP: nondet :: (Monad m, Generic a) => a -> Nondet cs m a
+ Control.CFLP: nondet :: (Update cs m m, Generic a) => a -> Nondet cs m a

Files

LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2008, Sebastian Fischer+Copyright (c) 2008-2009, Sebastian Fischer  All rights reserved.
README view
@@ -12,6 +12,6 @@  [cflp]: http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html -Sebastian Fischer, 2008+Sebastian Fischer, sebf@informatik.uni-kiel.de
cflp.cabal view
@@ -1,5 +1,5 @@ Name:          cflp-Version:       2009.1.15.2+Version:       2009.1.16 Cabal-Version: >= 1.6 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint@@ -35,12 +35,12 @@                     Control.Constraint.Choice,                     Data.LazyNondet,                     Data.LazyNondet.Types,+                    Data.LazyNondet.Generic,                     Data.LazyNondet.UniqueID,                     Data.LazyNondet.Matching,                     Data.LazyNondet.Narrowing,                     Data.LazyNondet.Primitive,                     Data.LazyNondet.HigherOrder,-                    Data.LazyNondet.Generic,                     Control.CFLP.Tests,                     Control.CFLP.Tests.CallTimeChoice                     Control.CFLP.Tests.HigherOrder
src/Control/CFLP/Tests/HigherOrder.lhs view
@@ -10,7 +10,8 @@ > import Control.CFLP.Tests > import Test.HUnit >-> import Prelude hiding ( not, null, head, map, foldr )+> import Prelude hiding ( not, null, head, map, foldr, flip, id )+> import qualified Prelude as P > import Data.LazyNondet.Types.Bool > import Data.LazyNondet.Types.List >@@ -22,6 +23,10 @@ >   , "call-time choice" ~: callTimeChoice >   , "map shared unknowns" ~: mapSharedUnknowns >   , "memeber with fold" ~: memberWithFold+>   , "overApplication" ~: overApplication+>   , "reverse with foldr" ~: reverseWithFoldr+>   -- , "pointfree reverse" ~: pointfreeReverse+>   -- , "function conversion" ~: functionConversion >   ]  The following test simply applies the not function.@@ -75,4 +80,74 @@ > memberWithFold = assertResults comp [True,False] >  where >   comp = foldr (fun (?)) failure (true ^: false ^: nil)++The following test applies the composition function which is has a+function on its right-hand side:++> after :: CFLP cs m+>       => Nondet cs m (b -> c) -> Nondet cs m (a -> b)+>       -> Nondet cs m (a -> c)+> after f g = fun (\x cs -> withUnique $ \u -> apply f (apply g x cs u) cs)+>+> overApplication :: Assertion+> overApplication = assertResults comp [True]+>  where+>   comp = apply (after (fun not) (fun not)) true++The following test makes extensive use of higher-order features by+implementing the reverse function using `foldr`.++~~~ { .Haskell }+rev = flip (foldr (\x f l -> f (x:l)) id) []+~~~++> reverseWithFoldr :: Assertion+> reverseWithFoldr = assertResults comp [[True,False,False]]+>  where+>   comp = rev (false ^: false ^: true ^: nil)+>   rev  = flip (fun (foldr (fun (\x f l -> apply f (x ^: l))) (fun id))) nil+>+> flip :: CFLP cs m+>      => Nondet cs m (a -> b -> c) -> Nondet cs m b -> Nondet cs m a+>      -> Context cs -> ID -> Nondet cs m c+> flip f x y cs = withUnique $ \u -> apply (apply f y cs u) x cs+> +> id :: Nondet cs m a -> Nondet cs m a+> id x = x++The following uses even more higher-order functions by implementing a+pointfree version of the above reverse function.++~~~ { .Haskell }+rev = flip (foldr (flip (flip ((.).(.)) (:))) id) []+~~~++-- > pointfreeReverse :: Assertion+-- > pointfreeReverse = assertResults comp [[True,False,False]]+-- >  where+-- >   comp cs = withUnique $ \u ->+-- >               apply (rev cs u) (false ^: false ^: true ^: nil) cs+-- > rev cs u = fun (flip (fun (foldr (fun (flip (fun (flip ((fun after `after` fun after) cs u) (fun (^:)))))) (fun id))) nil)++Currently, GHC (6.10.1) fails to compile the definition. The problem+seems to occur with many uses of `fun`:++-- > compileTimePerformanceBug+-- >   = fun id `after` fun id+-- >            `after` fun id+-- >            `after` fun id+-- >            `after` fun id+-- >            `after` fun id+-- >            `after` fun id++The following test converts primitive Haskell functions to+non-deterministic ones and applies them to non-deterministic values.++> functionConversion :: Assertion+> functionConversion = assertResults comp [False]+>  where+>   comp cs = withUnique $ \u ->+>              apply (foldr (fun after) (fun id)+>                       (nondet [P.not,P.not,P.not]) cs u)+>                true cs
src/Data/LazyNondet/Generic.lhs view
@@ -12,7 +12,7 @@ > > module Data.LazyNondet.Generic ( >->   Generic(..), GenericOps, generic, primitive, nondet, consLabels,+>   Generic(..), GenericOps, generic, primitive, consLabels, > >   ApplyCons(..), Decons, (!), cons >@@ -50,17 +50,6 @@ > primitive :: Generic a => NormalForm -> a > primitive = fromJust . prim genericOps -We also provide a generic operation `nondet` to translate instances of-`Generic` into non-deterministic data.--> nondet :: (Monad m, Generic a) => a -> Nondet cs m a-> nondet = Typed . nf2hnf . generic->-> nf2hnf :: Monad m => NormalForm -> Untyped cs m-> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"-> nf2hnf (Fun _) = error "nf2hnf: conversion of function not yet implemented"-> nf2hnf (Data label args) = return (Cons label (map nf2hnf args))- The operation `consLabels` yields the list of constructors corresponding to a datatype `a`. @@ -150,7 +139,9 @@ Combinators ----------- -The combinator `(!)` used to enumerate the constructors of a datatype combines records with generic operations. The integer argument is used to label the different constructors.+The combinator `(!)` used to enumerate the constructors of a datatype+combines records with generic operations. The integer argument is used+to label the different constructors.  > infixr 0 ! > (!) :: (Int -> GenericOps a) -> (Int -> GenericOps a) -> Int -> GenericOps a
src/Data/LazyNondet/HigherOrder.lhs view
@@ -49,9 +49,6 @@  Here are private type classes that are used to implement `fun`. -> newtype Lifted cs m a b->   = Lifted { lifted :: Nondet cs m a -> Context cs -> ID -> Nondet cs m b }- > class NestLambda a >  where >   type C a :: *@@ -62,22 +59,24 @@  Single-argument functions can be lifted using `lambda`. -> instance NestLambda (Lifted cs m a b)+> instance NestLambda (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) >  where->   type C (Lifted cs m a b) = cs->   type M (Lifted cs m a b) = m->   type T (Lifted cs m a b) = a -> b+>   type C (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) = cs+>   type M (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) = m+>   type T (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) = a -> b >->   nestLambda = lambda . lifted+>   nestLambda = lambda  If we have a function on non-deterministic data we can lift it to the `Nondet` type with the following instance. -> instance (NestLambda f, C f ~ cs, M f ~ m) => NestLambda (Nondet cs m a -> f)+> instance (NestLambda (Nondet cs m b -> f),+>           C (Nondet cs m b -> f) ~ cs, M  (Nondet cs m b -> f) ~ m)+>       => NestLambda (Nondet cs m a -> Nondet cs m b -> f) >  where->   type C (Nondet cs m a -> f) = cs->   type M (Nondet cs m a -> f) = m->   type T (Nondet cs m a -> f) = a -> T f+>   type C (Nondet cs m a -> Nondet cs m b -> f) = cs+>   type M (Nondet cs m a -> Nondet cs m b -> f) = m+>   type T (Nondet cs m a -> Nondet cs m b -> f) = a -> T (Nondet cs m b -> f) > >   nestLambda f = lambda (\x _ _ -> nestLambda (f x)) @@ -98,33 +97,36 @@ > > instance LiftFun (Nondet cs m a -> Nondet cs m b) >  where->   type Lift (Nondet cs m a -> Nondet cs m b) = Lifted cs m a b+>   type Lift (Nondet cs m a -> Nondet cs m b)+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b >->   liftFun f = Lifted (\x _ _ -> f x)+>   liftFun f x _ _ = f x > > instance LiftFun (Nondet cs m a -> Context cs -> Nondet cs m b) >  where->   type Lift (Nondet cs m a -> Context cs -> Nondet cs m b) = Lifted cs m a b+>   type Lift (Nondet cs m a -> Context cs -> Nondet cs m b)+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b >->   liftFun f = Lifted (\x cs _ -> f x cs)+>   liftFun f x cs _ = f x cs > > instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b) >  where->   type Lift (Nondet cs m a -> ID -> Nondet cs m b) = Lifted cs m a b+>   type Lift (Nondet cs m a -> ID -> Nondet cs m b)+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b >->   liftFun f = Lifted (\x _ u -> f x u)+>   liftFun f x _ u = f x u > > instance LiftFun (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) >  where >   type Lift (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)->           = Lifted cs m a b+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b >->   liftFun = Lifted+>   liftFun = id > > instance LiftFun (Nondet cs m b -> f) >       => LiftFun (Nondet cs m a -> Nondet cs m b -> f) >  where >   type Lift (Nondet cs m a -> Nondet cs m b -> f)->           = Nondet cs m a -> Lift (Nondet cs m b -> f)+>     = Nondet cs m a -> Lift (Nondet cs m b -> f) > >   liftFun f = liftFun . f
src/Data/LazyNondet/Matching.lhs view
@@ -10,7 +10,7 @@ > > module Data.LazyNondet.Matching ( >->   Match, match, ConsPatList(..), constructors, patterns,+>   Match, ConsPatList(..), constructors, patterns, > >   withHNF, failure, caseOf, caseOf_ >@@ -137,6 +137,14 @@ to be checked how big the slowdown of using `caseOf` is compared to using `withHNF` directly. ++Defining Constructor and Destructor Functions+=============================================++We provide combinators `constructors` and `destructors` that can be+used to define functions for constructing and matching+non-deterministic values.+ > class MkCons a >  where >   type Ctx a :: *@@ -160,47 +168,47 @@ >   type Res (Nondet cs m a -> b) = Res b > >   mkCons l xs x = mkCons l (untyped x:xs)-+> > infixr 0 :! > > data ConsPatList a b = a :! b-+> > class ConsList a >  where >   type CData a > >   consList :: [ConsLabel] -> a-+> > instance ConsList () >  where >   type CData () = () >   consList _ = ()-+> > instance (MkCons a, ConsList b) => ConsList (ConsPatList a b) >  where >   type CData (ConsPatList a b) = Res a > >   consList (l:ls) = mkCons l [] :! consList ls >   consList _ = error "consList: insufficient cons labels"-+> > constructors :: (ConsList a, Generic (CData a)) => a > constructors = cs >  where cs = consList (consLabels (undefined `asCDataOf` cs)) > > asCDataOf :: ConsList a => CData a -> a -> CData a > asCDataOf = const-+> > class PatternList a >  where >   type PData a > >   patternList :: [ConsLabel] -> a-+> > instance PatternList () >  where >   type PData () = () >   patternList _ = ()-+> > instance (WithUntyped a, PatternList p, cs ~ C a, m ~ M a, b ~ T a) >       => PatternList (ConsPatList ((Context cs -> a) -> Match t cs m b) p) >  where@@ -208,7 +216,7 @@ > >   patternList (l:ls) = match (index l) :! patternList ls >   patternList _ = error "patternList: insufficient cons labels"-+> > patterns :: (PatternList a, Generic (PData a)) => a > patterns = cs >  where cs = patternList (consLabels (undefined `asPDataOf` cs))
src/Data/LazyNondet/Primitive.lhs view
@@ -1,19 +1,16 @@ % Primitive Generic Functions on Lazy Non-Deterministic Data % Sebastian Fischer (sebf@informatik.uni-kiel.de) -> {-# LANGUAGE->       FlexibleContexts->   #-}-> > module Data.LazyNondet.Primitive ( >->   groundNormalForm, partialNormalForm,+>   nondet, groundNormalForm, partialNormalForm, > >   prim_eq > > ) where > > import Data.LazyNondet.Types+> import Data.LazyNondet.Generic > > import Control.Monad.State > import Control.Monad.Update@@ -21,8 +18,26 @@ > import Control.Constraint.Choice > > import Data.Supply++We provide a generic operation `nondet` to translate instances of+`Generic` into non-deterministic data.++> nondet :: (Update cs m m, Generic a) => a -> Nondet cs m a+> nondet = Typed . return . nf2hnf . generic >+> nf2hnf :: Update cs m m => NormalForm -> HeadNormalForm cs m+> 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) $+>                  error "Primitive.nf2hnf: primitive function uses context" +The `...NormalForm` functions evaluate a non-deterministic value and+lift all non-deterministic choices to the top level. The results are+deterministic values and can be converted into their Haskell+representation. Partial normal forms may contain unbound logic+variables while ground normal forms are data terms.+ > groundNormalForm :: Update cs m m' >                  => Nondet cs m a -> Context cs -> m' NormalForm > groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs@@ -31,11 +46,13 @@ >                   => Nondet cs m a -> Context cs -> m' NormalForm > partialNormalForm x (Context cs) = evalStateT (pnf (untyped x)) cs -The `...NormalForm` functions evaluate a non-deterministic value and-lift all non-deterministic choices to the top level. The results are-deterministic values and can be converted into their Haskell-representation. Partial normal forms may contain unbound logic-variables while ground normal forms are data terms.+To compute ground normal forms, we ignore free variables and narrow+them to ground terms. To compute partial normal forms, we do not+narrow unbound variables and in a second phase bind those variables+that were bound after we have visited them. For example, when+computing the normal form of `let x free in (x,not x)` we don't know+that `x` will be bound in the result when we encounter it for the+first time.  > gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm > gnf = nf (\_ _ -> Just ()) Data mkVar Fun@@ -49,13 +66,8 @@ >    = nf lookupChoice ((return.).Cons) ((return.).FreeVar) (return.Lambda) x >  >>= nf lookupChoice Data mkVar Fun -To compute ground normal forms, we ignore free variables and narrow-them to ground terms. To compute partial normal forms, we do not-narrow unbound variables and in a second phase bind those variables-that were bound after we have visited them. For example, when-computing the normal form of `let x free in (x,not x)` we don't know-that `x` will be bound in the result when we encounter it for the-first time.+The `nf` function is used by all normal-form functions and performs+all the work.  > nf :: Update cs m m' >    => (Int -> cs -> Maybe a)@@ -75,8 +87,9 @@ >       return (cns label nfs) >     Lambda _ -> return . fun $ error "Data.LazyNondet.Primitive.nf: function" -The `nf` function is used by all normal-form functions and performs-all the work.+We provide a generic comparison function for untyped non-deterministic+data that is used to define a typed equality test in the+`Data.LazyNondet.Types.Bool` module.  > prim_eq :: Update cs m m >         => Untyped cs m -> Untyped cs m -> StateT cs m Bool@@ -91,9 +104,9 @@ >     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.Types.Bool` module.+The function `solveCons` is like `solve` but always yields a+constructor-rooted term, i.e., no free variable or delayed+computation.  > solveCons :: Update cs m m >           => Untyped cs m -> StateT cs m (HeadNormalForm cs m)@@ -104,8 +117,4 @@ >     Delayed _ res -> get >>= solveCons . res . Context >     Lambda _ -> error "Data.LazyNondet.Primitive.solveCons: matched lambda" >     _ -> return hnf--The function `solveCons` is like `solve` but always yields a-constructor-rooted term, i.e., no free variable or delayed-computation.