packages feed

cflp 2009.1.13 → 2009.1.15

raw patch · 14 files changed

+414/−276 lines, 14 files

Files

cflp.cabal view
@@ -1,5 +1,5 @@ Name:          cflp-Version:       2009.1.13+Version:       2009.1.15 Cabal-Version: >= 1.6 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint@@ -39,14 +39,16 @@                     Data.LazyNondet.Narrowing,                     Data.LazyNondet.Primitive,                     Data.LazyNondet.HigherOrder,+                    Data.LazyNondet.Generic,                     Control.CFLP.Tests,                     Control.CFLP.Tests.CallTimeChoice                     Control.CFLP.Tests.HigherOrder   Hs-Source-Dirs:   src-  Extensions:       FunctionalDependencies,+  Extensions:       NoMonomorphismRestriction,                     MultiParamTypeClasses,                     FlexibleInstances,                     FlexibleContexts,+                    NoMonoPatBinds,                     PatternGuards,                     TypeFamilies,                     RankNTypes
src/Control/CFLP.lhs view
@@ -25,6 +25,7 @@ > > import Control.Monad.State > import Control.Monad.Update+> import Control.Monad.Trans.Update > > import Control.Constraint.Choice >@@ -73,13 +74,13 @@ The `evaluate` function enumerates the non-deterministic solutions of a constraint functional-logic computation according to a given strategy. -> eval, evalPartial :: (CFLP CS m, Update CS m m', Data a)+> eval, evalPartial :: (CFLP CS m, Update CS m m', Generic a) >                   => Strategy m' -> (Context CS -> ID -> Nondet CS m a) >                   -> IO [a]-> eval        s = liftM (map prim) . evaluate groundNormalForm  s-> evalPartial s = liftM (map prim) . evaluate partialNormalForm s+> eval        s = liftM (map primitive) . evaluate groundNormalForm  s+> evalPartial s = liftM (map primitive) . evaluate partialNormalForm s >-> evalPrint :: (CFLP CS m, Update CS m m', Data a, Show a)+> evalPrint :: (CFLP CS m, Update CS m m', Generic a) >           => Strategy m' -> (Context CS -> ID -> Nondet CS m a) >           -> IO () > evalPrint s op = evaluate partialNormalForm s op >>= printSols
src/Control/CFLP/Tests.lhs view
@@ -11,15 +11,15 @@ 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)+> assertResults :: (Generic a, Show a, Eq a) >               => (Computation [] a) -> [a] -> Assertion > assertResults = assertResultsLimit Nothing >-> assertResultsN :: (Data a, Show a, Eq a)+> assertResultsN :: (Generic a, Show a, Eq a) >                => Int -> (Computation [] a) -> [a] -> Assertion > assertResultsN = assertResultsLimit . Just >-> assertResultsLimit :: (Data a, Show a, Eq a)+> assertResultsLimit :: (Generic a, Show a, Eq a) >                    => Maybe Int -> (Computation [] a) -> [a] -> Assertion > assertResultsLimit limit op expected = do >   actual <- eval depthFirst op
src/Control/CFLP/Tests/CallTimeChoice.lhs view
@@ -47,7 +47,7 @@ >  where >   comp _ = two . unknown >-> two :: Monad m => Nondet cs m a -> Nondet cs m [a]+> two :: (Monad m, Generic a) => Nondet cs m a -> Nondet cs m [a] > two x = x ^: x ^: nil  This test checks call-time choice semantics: variables represent
src/Control/CFLP/Tests/HigherOrder.lhs view
@@ -58,7 +58,7 @@ >               apply (fun two) >                     (apply (apply (fun (?)) false cs u1) true cs u2) cs u3 >-> two :: Monad m => Nondet cs m a -> Nondet cs m [a]+> two :: (Monad m, Generic a) => Nondet cs m a -> Nondet cs m [a] > two x = x ^: x ^: nil  The following test maps the function `not` over a list with a
src/Control/Monad/Update.lhs view
@@ -2,37 +2,28 @@ % Sebastian Fischer (sebf@informatik.uni-kiel.de)  We define type classes and instances for monads that-non-deterministically update state. The challenge is to define the-interface such that instances can implement it without threading a-store through monadic computations and shared monadic computations are-evaluated only once.+non-deterministically update state.  > {-# LANGUAGE  >       MultiParamTypeClasses, >       FlexibleInstances,->       FlexibleContexts, >       RankNTypes >   #-} > > module Control.Monad.Update ( >->   -- type classes >   MonadUpdate(..), Update(..), >->   -- monad transformer->   UpdateT-> > ) where >  > import Control.Monad.State-> import Control.Monad.Trans > > class MonadPlus m => MonadUpdate s m >  where >   update :: (forall m' . MonadPlus m' => s -> m' s) -> m ()  A monad that supports non-deterministic state updates is an instance-of the class `MonadUpdate` that provides an operation to incorporate a+of the class `MonadUpdate` that defines an operation to incorporate a monadic update-action into monadic computations.  > instance MonadPlus m => MonadUpdate s (StateT s m)@@ -63,91 +54,3 @@ State monads are a natural choice for a monad that updates state, but they have a drawback: monadic values are functions that are reexecuted for each shared occurrence of a monadic sub computation.--Shared Monadic Values------------------------We define a monad transformer `UpdateT` that adds the capability of-non-deterministic state updates to arbitrary instances of-`MonadPlus`. Monadic actions in the resulting monads are data terms if-monadic actions are data terms in the base monad. As a consequence,-they are evaluated only once if they are shared.--> newtype UpdateT s m a = UpdateT { unUpdateT :: m (WithUpdate s m a) }-> data WithUpdate s m a->   = Return a->   | Update (forall m' . MonadPlus m' => s -> m' s)->            (UpdateT s m a)--The updating monadic action must be polymorphic in the used monad-`m'`.--> instance MonadPlus m => MonadUpdate s (UpdateT s m)->  where->   update upd = UpdateT (return (Update upd (return ())))--A transformed instance of `MonadPlus` is an instance of `MonadUpdate`.--> instance MonadPlus m => Update s (UpdateT s m) m->  where->   updateState = run->    where->     run :: MonadPlus m => UpdateT s m a -> StateT s m a->     run x = lift (unUpdateT x) >>= doUpdate->->     doUpdate (Return a)     = return a->     doUpdate (Update upd y) = do update upd; run y--It is also an instance of `Update` where results are returned in the-base monad. In order to perform stored updates, we thread a state-through the monadic computation.--> instance MonadPlus m => Update s (UpdateT s m) (UpdateT s m)->  where->   updateState = run->    where->     run :: MonadPlus m => UpdateT s m a -> StateT s (UpdateT s m) a->     run x = lift (lift (unUpdateT x)) >>= doUpdate->->     doUpdate (Return a)     = return a->     doUpdate (Update upd y) = do update upd; lift (update upd); run y--We define another instance of `Update` where results are not returned-in the base monad but in the transformed base monad. This instance is-useful to support computations that may or may not consider the-threaded store. All upcate actions are kept in the monadic values and-threaded additionally.--> instance Monad m => Monad (UpdateT s m)->  where->   return = UpdateT . return . Return->->   x >>= f = UpdateT (unUpdateT x >>= g)->    where g (Return a)     = unUpdateT (f a)->          g (Update upd y) = return (Update upd (y >>= f))->-> instance MonadPlus m => MonadPlus (UpdateT s m)->  where->   mzero       = UpdateT mzero->   x `mplus` y = UpdateT (unUpdateT x `mplus` unUpdateT y)->-> instance MonadTrans (UpdateT s)->  where->   lift = UpdateT . liftM Return--We specify that a transformed monad is indeed a monad, that it is an-instance of `MonadPlus` if the base monad is, and that, `UpdateT`-(with an arbitrary store `s`) is a monad transformer.--> instance Show a => Show (UpdateT s [] a)->  where->   show (UpdateT x) = show x->-> instance Show a => Show (WithUpdate cs [] a)->  where->   show (Return x) = "(Return "++show x++")"->   show (Update _ (UpdateT x)) = "(Update _ "++show x++")"--To simplify debugging, we define `Show` instances for transformed list-monads.-
src/Data/LazyNondet.lhs view
@@ -16,16 +16,20 @@ > >   withHNF, caseOf, caseOf_, Match, >->   Data, nondet, prim, groundNormalForm, partialNormalForm,+>   Generic(..), primitive, generic, nondet, >->   ConsRep(..), cons, match,+>   Decons, ApplyCons(..), (!), cons, >+>   groundNormalForm, partialNormalForm,+>+>   ConsPatList(..), constructors, patterns,+> >   apply, fun > > ) where >-> import Data.Data > import Data.LazyNondet.Types+> import Data.LazyNondet.Generic > import Data.LazyNondet.UniqueID > import Data.LazyNondet.Matching > import Data.LazyNondet.Narrowing
+ src/Data/LazyNondet/Generic.lhs view
@@ -0,0 +1,186 @@+% Generic Operations on Lazy Non-Deterministic Data+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides generic operations on the datatypes used+internally for constraint functional-logic programming. We cannot use+the `Data.Data` class, because we also want to handle functions.++`Typeable` or `DrIFT` may be applicable, however, to derive some of+the instances for classes defined in this module.++> {-# LANGUAGE TypeFamilies #-}+>+> module Data.LazyNondet.Generic (+>+>   Generic(..), GenericOps, generic, primitive, nondet, consLabels,+>+>   ApplyCons(..), Decons, (!), cons+>+>  ) where+>+> import Data.Maybe+> import Data.LazyNondet.Types++Here is a record with generic operations:++> data GenericOps a = GenericOps {++The operation `gen` converts a value of type `a` into the generic+normal-form representation.++>   gen :: a -> Maybe NormalForm ,++The operation `prim` converts a normal form into a primitive Haskell+value of type `a`.++>   prim :: NormalForm -> Maybe a ,++The field `labels` stores a list of `ConsLabels` corresponding to the+constructors of a datatype.++>   labels :: [ConsLabel] }++The generic operations `gen` and `prim` return optional+results. However, failure is only used internally and there are+wrapper functions that always succeed:++> generic :: Generic a => a -> NormalForm+> generic = fromJust . gen genericOps+>+> 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`.++> consLabels :: Generic a => a -> [ConsLabel]+> consLabels x = labels (genericOps `forTypeOf` x)+>+> forTypeOf :: GenericOps a -> a -> GenericOps a+> forTypeOf = const++The operation `genericOps` is defined in the type class `Generic`:++> class Generic a+>  where+>   genericOps :: GenericOps a+>   genericOps = constr 0+>+>   constr :: Int -> GenericOps a+>   constr _ = error "Generic.constr: not implemented"++Primitive Haskell types that should be convertible to be used in+constraint functional-logic programs need to be instances of+`Generic`.++The operation `genericOps` has a default implementation in terms of+`constr` to simplify the definition of instances for *data*types. The+instance for function types defines `genericOps` directly:++> instance (Generic a, Generic b) => Generic (a -> b)+>  where+>   genericOps = GenericOps {+>     gen    = \ f       -> Just (Fun (generic   . f . primitive)) ,+>     prim   = \ (Fun f) -> Just      (primitive . f . generic   ) ,+>     labels = [] }+++Defining Instances+==================++We provide combinators to simplify the definition of `Generic`+instances for datatypes. For example, the instance for booleans looks+like this:++> instance Generic Bool+>  where+>   constr = cons "False" False dFalse ! cons "True" True dTrue++The arguments `dFalse` and `dTrue` are deconstructors for the+corresponding constructors:++> type Decons a = ([NormalForm] -> NormalForm) -> Result a -> Maybe NormalForm++The type `Result a` used in the type of deconstructors is associated+to the type class `ApplyCons`. ++> class ApplyCons a+>  where+>   type Result a+>   applyCons :: a -> [NormalForm] -> Result a++We can use `applyCons` to apply constructors of arbitrary arity:++> instance (Generic a, ApplyCons b) => ApplyCons (a -> b)+>  where+>   type Result (a -> b) = Result b+>+>   applyCons c (x:xs) = applyCons (c (primitive x)) xs+>   applyCons _ _ = error "applyCons: insufficient arguments"++We need an instance of `ApplyCons` for booleans in order to define the+`Generic` instance using our combinators. Instantiating `ApplyCons` is+easy, however. The definitions are always the same: `Result a = a` and+`applyCons = const`.++> instance ApplyCons Bool+>  where+>   type Result Bool = Bool+>   applyCons = const++Deconstructors are also defined mechanically:++> dFalse, dTrue :: Decons Bool+> dFalse c False = Just (c [])+> dFalse _ _     = Nothing+> dTrue  c True  = Just (c [])+> dTrue  _ _     = Nothing++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.++> infixr 0 !+> (!) :: (Int -> GenericOps a) -> (Int -> GenericOps a) -> Int -> GenericOps a+> (c1!c2) n =+>   GenericOps {+>     gen    = \x -> maybe (gen  genOps2 x) Just (gen  genOps1 x) ,+>     prim   = \x -> maybe (prim genOps2 x) Just (prim genOps1 x) ,+>     labels = labels genOps1 ++ labels genOps2 }+>  where genOps1 = c1 n; genOps2 = c2 (n+1)++We rely on `(!)` to be right associative: if `(!)` takes the result of+a different call to `(!)` as left argument then the distributed+numbers won't be distinct!++Finally, we define the `cons` combinator that takes constructors and+corresponding destructors.++> cons :: ApplyCons a => String -> a -> Decons a -> Int -> GenericOps (Result a)+> cons s c d n =+>   GenericOps {+>     gen    = d (Data (ConsLabel n s)),+>     prim   = \ (Data l xs) ->+>                  if n == index l then Just (applyCons c xs) else Nothing,+>     labels = [ConsLabel n s]+>    }++In order to convert a value to the generic normal-form representation+we can use the destructor function. To convert in the other direction+we check whether the label of the constructor equals the label of the+converter and, if it does, we use `applyCons` to apply the+corresponding constructor.++
src/Data/LazyNondet/HigherOrder.lhs view
@@ -4,10 +4,7 @@ This module defines combinators for higher-order CFLP.  > {-# LANGUAGE ->       MultiParamTypeClasses, NoMonomorphismRestriction,->       FunctionalDependencies,->       TypeSynonymInstances,->       UndecidableInstances,+>       TypeFamilies, >       FlexibleInstances, >       FlexibleContexts >   #-}@@ -46,7 +43,7 @@ non-deterministic data (of arbitrary arity) into a (possibly nested) lambda. -> fun :: (Monad m, LiftFun f g, NestLambda g cs m t)+> fun :: (Monad m, LiftFun f, NestLambda g, g ~ Lift f, m~M g, cs~C g, t~T g) >     => f -> Nondet cs m t > fun = nestLambda . liftFun @@ -55,21 +52,33 @@ > newtype Lifted cs m a b >   = Lifted { lifted :: Nondet cs m a -> Context cs -> ID -> Nondet cs m b } -> class NestLambda a cs m b | a -> cs, a -> m, a -> b+> class NestLambda a >  where->   nestLambda :: Monad m => a -> Nondet cs m b+>   type C a :: *+>   type M a :: * -> *+>   type T a :: *+>+>   nestLambda :: Monad (M a) => a -> Nondet (C a) (M a) (T a)  Single-argument functions can be lifted using `lambda`. -> instance NestLambda (Lifted cs m a b) cs m (a -> b)+> instance NestLambda (Lifted cs m a 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+> >   nestLambda = lambda . lifted  If we have a function on non-deterministic data we can lift it to the `Nondet` type with the following instance. -> instance NestLambda f cs m b => NestLambda (Nondet cs m a -> f) cs m (a -> b)+> instance (NestLambda f, C f ~ cs, M f ~ m) => NestLambda (Nondet cs m a -> 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+> >   nestLambda f = lambda (\x _ _ -> nestLambda (f x))  We provide a combinator `liftFun` for @@ -81,29 +90,41 @@    * non-deterministic functions that only take a unique id. -> class LiftFun f g | f -> g+> class LiftFun f >  where->   liftFun :: f -> g+>   type Lift f >-> instance LiftFun (Nondet cs m a -> Nondet cs m b) (Lifted cs m a b)+>   liftFun :: f -> Lift f+>+> 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+> >   liftFun f = Lifted (\x _ _ -> f x) > > instance LiftFun (Nondet cs m a -> Context cs -> Nondet cs m b)->                  (Lifted cs m a b) >  where+>   type Lift (Nondet cs m a -> Context cs -> Nondet cs m b) = Lifted cs m a b+> >   liftFun f = Lifted (\x cs _ -> f x cs) >-> instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b) (Lifted cs m a b)+> 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+> >   liftFun f = Lifted (\x _ u -> f x u) > > instance LiftFun (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)->                  (Lifted cs m a b) >  where+>   type Lift (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)+>           = Lifted cs m a b+> >   liftFun = Lifted >-> instance LiftFun (Nondet cs m b -> f) g => ->          LiftFun (Nondet cs m a -> Nondet cs m b -> f) (Nondet cs m a -> g)+> 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)+> >   liftFun f = liftFun . f
src/Data/LazyNondet/Matching.lhs view
@@ -5,21 +5,19 @@ >       RankNTypes, >       TypeFamilies, >       FlexibleContexts,->       FlexibleInstances,->       MultiParamTypeClasses,->       FunctionalDependencies+>       FlexibleInstances >   #-} > > module Data.LazyNondet.Matching ( >->   Match, match, ConsRep(..), cons,+>   Match, match, ConsPatList(..), constructors, patterns, > >   withHNF, failure, caseOf, caseOf_ > > ) where >-> import Data.Data > import Data.LazyNondet.Types+> import Data.LazyNondet.Generic > > import Control.Monad.State > import Control.Monad.Update@@ -97,13 +95,13 @@ function to typed versions of these values.  > newtype Match a cs m b->   = Match { unMatch :: (ConIndex, Context cs -> Branch cs m b) }+>   = Match { unMatch :: (Int, Context cs -> Branch cs m b) } > > type Branch cs m a = [Untyped cs m] -> Nondet cs m a >-> match :: (ConsRep a, WithUntyped b)->       => a -> (Context (C b) -> b) -> Match t (C b) (M b) (T b)-> match c alt = Match (constrIndex (consRep c), withUntyped . alt)+> 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`.@@ -127,8 +125,8 @@ >     Delayed p res >       | p cs      -> delayed p (\cs -> caseOf_ (Typed (res cs)) bs def cs) >       | otherwise -> caseOf_ (Typed (res cs)) bs def cs->     Cons _ idx args ->->       maybe def (\b -> b cs args) (lookup idx (map unMatch bs))+>     Cons label args ->+>       maybe def (\b -> b cs args) (lookup (index label) (map unMatch bs)) >     Lambda _ -> error "Data.LazyNondet.Matching.caseOf: cannot match lambda"  We provide operations `caseOf_` and `caseOf` (with and without a@@ -139,41 +137,82 @@ to be checked how big the slowdown of using `caseOf` is compared to using `withHNF` directly. -> class MkCons cs m a b | b -> m, b -> cs+> class MkCons a >  where->   mkCons :: a -> [Untyped cs m] -> b+>   type Ctx a :: *+>   type Mon a :: * -> *+>   type Res a :: * >-> instance (Monad m, Data a) => MkCons cs m a (Nondet cs m t)+>   mkCons :: ConsLabel -> [Untyped (Ctx a) (Mon a)] -> a+>+> instance Monad m => MkCons (Nondet cs m a) >  where->   mkCons c = Typed . return . mkHNF (toConstr c) . reverse+>   type Ctx (Nondet cs m a) = cs+>   type Mon (Nondet cs m a) = m+>   type Res (Nondet cs m a) = a >-> instance MkCons cs m b c => MkCons cs m (a -> b) (Nondet cs m t -> c)+>   mkCons l = Typed . return . Cons l . reverse+>+> instance (MkCons b, cs ~ Ctx b, m ~ Mon b) => MkCons (Nondet cs m a -> b) >  where->   mkCons c xs x = mkCons (c undefined) (untyped x:xs)+>   type Ctx (Nondet cs m a -> b) = cs+>   type Mon (Nondet cs m a -> b) = m+>   type Res (Nondet cs m a -> b) = Res b >-> cons :: MkCons cs m a b => a -> b-> cons c = mkCons c []+>   mkCons l xs x = mkCons l (untyped x:xs) -The overloaded operation `cons` takes a Haskell constructor and yields-a corresponding constructor function for non-deterministic values.+> infixr 0 :!+>+> data ConsPatList a b = a :! b -> class ConsRep a+> class ConsList a >  where->   consRep :: a -> Constr+>   type CData a >-> instance ConsRep b => ConsRep (a -> b)+>   consList :: [ConsLabel] -> a++> instance ConsList () >  where->   consRep c = consRep (c undefined)+>   type CData () = ()+>   consList _ = () -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 (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" -    instance Data a => ConsRep a-     where-      consRep = toConstr+> 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 -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.+> 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+>   type PData (ConsPatList ((Context cs -> a) -> Match t cs m b) p) = t+>+>   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))+>+> asPDataOf :: PatternList a => PData a -> a -> PData a+> asPDataOf = const+
src/Data/LazyNondet/Primitive.lhs view
@@ -7,14 +7,12 @@ > > module Data.LazyNondet.Primitive ( >->   nondet, prim, groundNormalForm, partialNormalForm,+>   groundNormalForm, partialNormalForm, > >   prim_eq > > ) where >-> import Data.Data-> import Data.Generics.Twins > import Data.LazyNondet.Types > > import Control.Monad.State@@ -24,31 +22,7 @@ > > import Data.Supply >-> prim :: Data a => NormalForm -> a-> prim (Var u) = error $ "demand on logic variable " ++ show u-> prim (NormalForm con args) =->   snd (gmapAccumT perkid args (fromConstr con))->  where->   perkid ts _ = (tail ts, prim (head ts)) -The operation `prim` translates a normal form into a primitive Haskell-value. Free logic variables are translated into a call to `error` so-the result is a partial value if the argument contains logic-variables.--> generic :: Data a => a -> NormalForm-> generic x = NormalForm (toConstr x) (gmapQ generic x)->-> nf2hnf :: Monad m => NormalForm -> Untyped cs m-> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"-> nf2hnf (NormalForm con args) = return (mkHNF con (map nf2hnf args))->-> nondet :: (Monad m, Data a) => a -> Nondet cs m a-> nondet = Typed . nf2hnf . generic--We also provide a generic operation `nondet` to translate instances of-the `Data` class into non-deterministic data.- > groundNormalForm :: Update cs m m' >                  => Nondet cs m a -> Context cs -> m' NormalForm > groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs@@ -64,15 +38,16 @@ variables while ground normal forms are data terms.  > gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm-> gnf = nf (\_ _ -> Just ()) NormalForm mkVar+> gnf = nf (\_ _ -> Just ()) Data mkVar Fun > > mkVar :: ID -> a -> NormalForm > mkVar (ID us) _ = Var (supplyValue us) > > pnf :: (Update cs m m', ChoiceStore cs) >     => Untyped cs m -> StateT cs m' NormalForm-> pnf x = nf lookupChoice ((return.).mkHNF) ((return.).FreeVar) x->     >>= nf lookupChoice NormalForm mkVar+> pnf x+>    = 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@@ -84,20 +59,21 @@  > nf :: Update cs m m' >    => (Int -> cs -> Maybe a)->    -> (Constr -> [nf] -> nf)+>    -> (ConsLabel -> [nf] -> nf) >    -> (ID -> Untyped cs m -> nf)+>    -> (b -> nf) >    -> Untyped cs m -> StateT cs m' nf-> nf lkp cns fv x = do+> nf lkp cns fv fun x = do >   hnf <- updateState x >   case hnf of >     FreeVar u@(ID us) y ->->       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))+>       get >>= maybe (return (fv u y)) (const (nf lkp cns fv fun y)) >             . lkp (supplyValue us)->     Delayed _ resume -> get >>= nf lkp cns fv . resume . Context->     Cons typ idx args -> do->       nfs <- mapM (nf lkp cns fv) args->       return (cns (indexConstr typ idx) nfs)->     Lambda _ -> error "Data.LazyNondet.Primitive.nf: cannot convert lambda"+>     Delayed _ resume -> get >>= nf lkp cns fv fun . resume . Context+>     Cons label args -> do+>       nfs <- mapM (nf lkp cns fv fun) args+>       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.@@ -105,9 +81,9 @@ > prim_eq :: Update cs m m >         => Untyped cs m -> Untyped cs m -> StateT cs m Bool > prim_eq x y = do->   Cons _ ix xs <- solveCons x->   Cons _ iy ys <- solveCons y->   if ix==iy then all_eq xs ys else return False+>   Cons lx xs <- solveCons x+>   Cons ly ys <- solveCons y+>   if index lx == index ly then all_eq xs ys else return False >  where >   all_eq [] [] = return True >   all_eq (v:vs) (w:ws) = do@@ -126,6 +102,7 @@ >   case hnf of >     FreeVar _ y -> solveCons y >     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
src/Data/LazyNondet/Types.lhs view
@@ -13,32 +13,36 @@ > >   Context(..), ID(..),  >->   NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),+>   ConsLabel(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..), >->   mkHNF, freeVar, delayed+>   freeVar, delayed > > ) where >-> import Data.Data->-> import Control.Monad.Update-> > import Data.Supply >+> import Control.Monad.Trans.Update+> > newtype Context cs = Context cs > > newtype ID = ID (Supply Int) >-> data NormalForm = NormalForm Constr [NormalForm] | Var Int+> data NormalForm+>   = Data ConsLabel [NormalForm]+>   | Var  Int+>   | Fun  (NormalForm -> NormalForm)+>+> data ConsLabel = ConsLabel { index :: Int, name :: String }+>+> instance Show ConsLabel+>  where+>   showsPrec _ = (++) . name  The normal form of data is represented by the type `NormalForm` which-defines a tree of constructors and logic variables. The type `Constr`-is a representation of constructors defined in the `Data.Generics`-package. With generic programming we can convert between Haskell data-types and the `NormalForm` type.+defines a tree of constructors and logic variables or functions.  > data HeadNormalForm cs m->   = Cons DataType ConIndex [Untyped cs m]+>   = Cons ConsLabel [Untyped cs m] >   | FreeVar ID (Untyped cs m) >   | Delayed (Context cs -> Bool) (Context cs -> Untyped cs m) >   | Lambda (Untyped cs m -> Context cs -> ID -> Untyped cs m)@@ -56,13 +60,6 @@ logic variables by overloading. The phantom type must be the Haskell data type that should be used for conversion into primitive data. -> mkHNF :: Constr -> [Untyped cs m] -> HeadNormalForm cs m-> mkHNF c = Cons (constrType c) (constrIndex c)--In head-normal forms we split the constructor representation into a-representation of the data type and the index of the constructor, to-enable pattern matching on the index.- 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@@ -95,10 +92,9 @@ >   show (FreeVar (ID u) _) = '_':show (supplyValue u) >   show (Delayed _ _) = "<delayed>" >   show (Lambda _) = "<function>"->   show (Cons typ idx args) ->     | null args = show con->     | otherwise = unwords (('(':show con):map show args++[")"])->    where con = indexConstr typ idx+>   show (Cons label args) +>     | null args = show label+>     | otherwise = unwords (('(':show label):map show args++[")"]) > > instance Show (Nondet cs [] a) >  where@@ -110,12 +106,12 @@ > > instance Show (HeadNormalForm cs (UpdateT cs [])) >  where->   show (FreeVar (ID u) _)  = '_':show (supplyValue u)->   show (Delayed _ _)       = "<delayed>"->   show (Lambda _)          = "<function>"->   show (Cons typ idx [])   = show (indexConstr typ idx)->   show (Cons typ idx args) =->     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" +>   show (FreeVar (ID u) _) = '_':show (supplyValue u)+>   show (Delayed _ _)      = "<delayed>"+>   show (Lambda _)         = "<function>"+>   show (Cons label [])    = show label+>   show (Cons label args)  =+>     "("++show label++" "++unwords (map show args)++")"   To simplify debugging, we provide `Show` instances for head-normal forms and non-deterministic values.@@ -123,17 +119,18 @@ > instance Show NormalForm >  where >   showsPrec _ (Var u) = ('_':) . shows u->   showsPrec _ (NormalForm cons []) = shows cons->   showsPrec n x@(NormalForm cons args)+>   showsPrec _ (Fun _) = ("<function>"++)+>   showsPrec _ (Data label []) = shows label+>   showsPrec n x@(Data label args) >     | Just xs <- fromList x = shows xs->     | n == 0 = shows cons . (' ':) . foldr1 (\y z -> y.(' ':).z)+>     | n == 0 = shows label . (' ':) . foldr1 (\y z -> y.(' ':).z) >                 (map (showsPrec 1) args) >     | otherwise = ('(':) . shows x . (')':) > > fromList :: NormalForm -> Maybe [NormalForm]-> fromList (NormalForm cons args)->   | show cons == "[]" = Just []->   | show cons == "(:)", [x,l] <- args, Just xs <- fromList l = Just (x:xs)+> fromList (Data label args)+>   | show label == "[]" = Just []+>   | show label == "(:)", [x,l] <- args, Just xs <- fromList l = Just (x:xs) > fromList _ = Nothing  For normal forms we provide a custum `Show` instance because we want
src/Data/LazyNondet/Types/Bool.lhs view
@@ -4,14 +4,15 @@ This module provides non-deterministic booleans.  > {-# LANGUAGE+>       NoMonomorphismRestriction, >       MultiParamTypeClasses, >       FlexibleInstances,->       FlexibleContexts+>       FlexibleContexts,+>       NoMonoPatBinds >   #-} > > module Data.LazyNondet.Types.Bool where >-> import Data.Data > import Data.LazyNondet > import Data.LazyNondet.Types > import Data.LazyNondet.Primitive@@ -20,20 +21,15 @@ > import Control.Monad.Update > > import Control.Constraint.Choice->-> instance ConsRep Bool where consRep = toConstr->-> true :: Monad m => Nondet cs m Bool-> true = cons True->-> pTrue :: (Context cs -> Nondet cs m a) -> Match Bool cs m a-> pTrue = match True->-> false :: Monad m => Nondet cs m Bool-> false = cons False++Instances for the classes `ApplyCons` and `Generic` for booleans are+defined in the module `Data.LazyNondet.Generic`.++> false, true :: Monad m => Nondet cs m Bool+> false :! true :! () = constructors >-> pFalse :: (Context cs -> Nondet cs m a) -> Match Bool cs m a-> pFalse = match False+> pFalse, pTrue :: (Context cs -> Nondet cs m a) -> Match Bool cs m a+> pFalse :! pTrue :! () = patterns  In order to be able to use logic variables of boolean type, we make it an instance of the type class `Narrow`.
src/Data/LazyNondet/Types/List.lhs view
@@ -4,15 +4,18 @@ This module provides non-deterministic lists.  > {-# LANGUAGE+>       NoMonomorphismRestriction, >       MultiParamTypeClasses, >       FlexibleInstances,->       FlexibleContexts+>       FlexibleContexts,+>       NoMonoPatBinds,+>       TypeFamilies >   #-} > > module Data.LazyNondet.Types.List where >-> import Data.Data > import Data.LazyNondet+> import Data.LazyNondet.Types > import Data.LazyNondet.Types.Bool > > import Control.Monad.Update@@ -22,53 +25,62 @@ > import Prelude hiding ( map, foldr ) > import qualified Prelude as P >-> instance ConsRep [()] where consRep = toConstr+> instance ApplyCons [a] where type Result [a] = [a]; applyCons = const >-> nil :: Monad m => Nondet cs m [a]-> nil = cons ([] :: [()])+> instance Generic a => Generic [a]+>  where constr = cons "[]" [] dNil ! cons "(:)" (:) dCons >-> pNil :: (Context cs -> Nondet cs m b) -> Match [a] cs m b-> pNil = match ([] :: [()])+> dNil :: Decons [a]+> dNil c [] = Just (c [])+> dNil _ _  = Nothing >+> dCons :: Generic a => Decons [a]+> dCons c (x:xs) = Just (c [generic x, generic xs])+> dCons _ _      = Nothing+> > infixr 5 ^:-> (^:) :: Monad m => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a]-> (^:) = cons ((:) :: () -> [()] -> [()])+> nil  :: (Monad m, Generic a) => Nondet cs m [a]+> (^:) :: (Monad m, Generic a)+>      => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a]+> nil :! (^:) :! () = constructors >-> pCons :: (Context cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)+> pNil  :: Generic a => (Context cs -> Nondet cs m b) -> Match [a] cs m b+> pCons :: Generic a+>       => (Context cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b) >       -> Match [a] cs m b-> pCons = match ((:) :: () -> [()] -> [()])->-> fromList :: Monad m => [Nondet cs m a] -> Nondet cs m [a]-> fromList = P.foldr (^:) nil+> pNil :! pCons :! () = patterns  We can use logic variables of a list type if there are logic variables for the element type. -> instance (ChoiceStore cs, Narrow cs a) => Narrow cs [a]+> instance (ChoiceStore cs, Narrow cs a, Generic a) => Narrow cs [a] >  where >   narrow cs u = withUnique (\u1 u2 ->  >                   (oneOf [nil, unknown u1 ^: unknown u2] cs u)) u  Some operations on lists: -> null :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m Bool+> null :: (Update cs m m, Generic a)+>      => Nondet cs m [a] -> Context cs -> Nondet cs m Bool > null xs = caseOf_ xs [pNil (const true)] false >-> head :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m a+> head :: (Update cs m m, Generic a)+>      => Nondet cs m [a] -> Context cs -> Nondet cs m a > head l = caseOf l [pCons (\_ x _ -> x)] >-> tail :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m [a]+> tail :: (Update cs m m, Generic a)+>      => Nondet cs m [a] -> Context cs -> Nondet cs m [a] > tail l = caseOf l [pCons (\_ _ xs -> xs)]  Higher-order functions: -> map :: Update cs m m+> map :: (Update cs m m, Generic a, Generic b) >     => Nondet cs m (a -> b) -> Nondet cs m [a] >     -> Context cs -> ID -> Nondet cs m [b] > map f l cs = withUnique $ \u -> >               foldr (fun (\x xs -> apply f x cs u ^: xs)) nil l cs >-> foldr :: Update cs m m+> foldr :: (Update cs m m, Generic a) >       => Nondet cs m (a -> b -> b) -> Nondet cs m b -> Nondet cs m [a] >       -> Context cs -> ID -> Nondet cs m b > foldr f y l cs = withUnique $ \u1 u2 u3 ->