cflp 2009.1.6 → 2009.1.13

raw patch · 15 files changed

+288/−64 lines, 15 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Test.lhs +2/−1
• cflp.cabal +3/−1
• src/Control/CFLP.lhs +10/−14
• src/Control/CFLP/Tests/CallTimeChoice.lhs +10/−9
• src/Control/CFLP/Tests/HigherOrder.lhs +78/−0
• src/Control/Constraint/Choice.lhs +1/−1
• src/Control/Monad/Update.lhs +1/−1
• src/Data/LazyNondet.lhs +4/−1
• src/Data/LazyNondet/HigherOrder.lhs +109/−0
• src/Data/LazyNondet/Matching.lhs +12/−9
• src/Data/LazyNondet/Narrowing.lhs +6/−5
• src/Data/LazyNondet/Primitive.lhs +9/−7
• src/Data/LazyNondet/Types.lhs +12/−4
• src/Data/LazyNondet/Types/Bool.lhs +5/−5
• src/Data/LazyNondet/Types/List.lhs +26/−6

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

@@ -1,5 +1,5 @@ Name:          cflp-Version:       2009.1.6+Version:       2009.1.13 Cabal-Version: >= 1.6 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint@@ -38,8 +38,10 @@                     Data.LazyNondet.Matching,                     Data.LazyNondet.Narrowing,                     Data.LazyNondet.Primitive,+                    Data.LazyNondet.HigherOrder,                     Control.CFLP.Tests,                     Control.CFLP.Tests.CallTimeChoice+                    Control.CFLP.Tests.HigherOrder   Hs-Source-Dirs:   src   Extensions:       FunctionalDependencies,                     MultiParamTypeClasses,

@@ -17,15 +17,11 @@ > >   Strategy, depthFirst, >->   module Data.LazyNondet,->   module Data.LazyNondet.Types.Bool,->   module Data.LazyNondet.Types.List+>   module Data.LazyNondet > > ) where > > import Data.LazyNondet-> import Data.LazyNondet.Types.Bool-> import Data.LazyNondet.Types.List > > import Control.Monad.State > import Control.Monad.Update@@ -46,10 +42,10 @@  > type CS = ChoiceStoreIM >-> noConstraints :: CS-> noConstraints = noChoices+> noConstraints :: Context CS+> noConstraints = Context noChoices >-> type Computation m a = CS -> ID -> Nondet CS (UpdateT CS m) a+> type Computation m a = Context CS -> ID -> Nondet CS (UpdateT CS m) a  Currently, the constraint store used to evaluate constraint functional-logic programs is simply a `ChoiceStore`. It will be a@@ -67,8 +63,8 @@ The strategy of the list monad is depth-first search.  > evaluate :: (CFLP CS m, Update CS m m')->          => (Nondet CS m a -> CS -> m' b)->          -> Strategy m' -> (CS -> ID -> Nondet CS m a)+>          => (Nondet CS m a -> Context CS -> m' b)+>          -> Strategy m' -> (Context CS -> ID -> Nondet CS m a) >          -> IO [b] > evaluate evalNondet enumerate op = do >   i <- initID@@ -78,13 +74,13 @@ constraint functional-logic computation according to a given strategy.  > eval, evalPartial :: (CFLP CS m, Update CS m m', Data a)->                   => Strategy m' -> (CS -> ID -> Nondet CS m 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 > > evalPrint :: (CFLP CS m, Update CS m m', Data a, Show a)->           => Strategy m' -> (CS -> ID -> Nondet CS m a)+>           => Strategy m' -> (Context CS -> ID -> Nondet CS m a) >           -> IO () > evalPrint s op = evaluate partialNormalForm s op >>= printSols >@@ -102,8 +98,8 @@  We provide -  * an `eval` operation to compute Haskell terms from non-determinitic-    data,+  * an `eval` operation to compute Haskell terms from+    non-deterministic data,    * an operation `evalPartial` to compute partial Haskell terms where     logic variables are replaced with an error, and

@@ -12,17 +12,17 @@ > import Control.CFLP.Tests > import Test.HUnit >-> import Control.CFLP-> > import Prelude hiding ( not, null, head )+> import Data.LazyNondet.Types.Bool+> import Data.LazyNondet.Types.List > > tests :: Test > tests = "call-time choice" ~: test->  [ "ignore first, narrow second" ~: ignoreFirstNarrowSecond->  , "shared vars are equal" ~: sharedVarsAreEqual->  , "no demand on shared var" ~: noDemandOnSharedVar->  , "shared compound terms" ~: sharedCompoundTerms->  ]+>   [ "ignore first, narrow second" ~: ignoreFirstNarrowSecond+>   , "shared vars are equal" ~: sharedVarsAreEqual+>   , "no demand on shared var" ~: noDemandOnSharedVar+>   , "shared compound terms" ~: sharedCompoundTerms+>   ]  Every module under `Control.CFLP.Tests` defines a constant `tests` that collects all defined tests.@@ -33,7 +33,7 @@ >   comp cs u = ignot (error "illegal demand") (unknown u) cs > > ignot :: CFLP cs m->       => Nondet cs m a -> Nondet cs m Bool -> cs -> Nondet cs m Bool+>       => Nondet cs m a -> Nondet cs m Bool -> Context cs -> Nondet cs m Bool > ignot _ = not  This test checks a function with two arguments, where the first must@@ -73,7 +73,8 @@ >  where >   comp cs u = negHeads (unknown u) cs >-> negHeads :: CFLP cs m => Nondet cs m [Bool] -> cs -> Nondet cs m [Bool]+> negHeads :: CFLP cs m+>          => Nondet cs m [Bool] -> Context cs -> Nondet cs m [Bool] > negHeads l cs = not (head l cs) cs ^: head l cs ^: nil  This test checks whether sharing is ensured on aruments of compound

@@ -0,0 +1,78 @@+% Testing Higher-Order Functional-Logic Operations+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module defines tests that show how to define higher-order+functional-logic programs.++> module Control.CFLP.Tests.HigherOrder where+>+> import Control.CFLP+> import Control.CFLP.Tests+> import Test.HUnit+>+> import Prelude hiding ( not, null, head, map, foldr )+> import Data.LazyNondet.Types.Bool+> import Data.LazyNondet.Types.List+>+> tests :: Test+> tests = "higher order" ~: test+>   [ "apply not function" ~: applyNotFunction+>   , "apply binary constructor" ~: applyBinCons+>   , "apply non-deterministic choice" ~: applyChoice+>   , "call-time choice" ~: callTimeChoice+>   , "map shared unknowns" ~: mapSharedUnknowns+>   , "memeber with fold" ~: memberWithFold+>   ]++The following test simply applies the not function.++> applyNotFunction :: Assertion+> applyNotFunction = assertResults comp [True]+>  where+>   comp = apply (fun not) false++The following test applies the binary list constructor.++> applyBinCons :: Assertion+> applyBinCons = assertResults comp [[True]]+>  where+>   comp cs = withUnique $ \u1 u2 ->+>               apply (apply (fun (^:)) true cs u1) nil cs u2++The following tests applies the binary operator for non-deterministic+choice.++> applyChoice :: Assertion+> applyChoice = assertResults comp [False,True]+>  where+>   comp cs = withUnique $ \u1 u2 ->+>               apply (apply (fun (?)) false cs u1) true cs u2++The following test checks whether call-time choice is still obtained+when applying the choice combinator using higher-order features.++> callTimeChoice :: Assertion+> callTimeChoice = assertResults comp [[False,False],[True,True]]+>  where+>   comp cs = withUnique $ \u1 u2 u3 ->+>               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 x = x ^: x ^: nil++The following test maps the function `not` over a list with a+duplicated free variable.++> mapSharedUnknowns :: Assertion+> mapSharedUnknowns = assertResults comp [[True,True],[False,False]]+>  where+>   comp cs = withUnique $ \u -> map (fun not) (two (unknown u)) cs++The following test checks the member operation defined using `foldr`.++> memberWithFold :: Assertion+> memberWithFold = assertResults comp [True,False]+>  where+>   comp = foldr (fun (?)) failure (true ^: false ^: nil)+

@@ -46,7 +46,7 @@ >  where >   lookupChoice u (ChoiceStoreIM cs) = IM.lookup u cs >->   assertChoice _ u x (ChoiceStoreIM cs) = do+>   assertChoice _ u x (ChoiceStoreIM cs) = >     maybe (return (ChoiceStoreIM (IM.insert u x cs))) >           (\y -> do guard (x==y); return (ChoiceStoreIM cs)) >           (IM.lookup u cs)

@@ -110,7 +110,7 @@ >     run x = lift (lift (unUpdateT x)) >>= doUpdate > >     doUpdate (Return a)     = return a->     doUpdate (Update upd y) = do lift (update upd); update upd; run y+>     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

@@ -6,7 +6,7 @@  > module Data.LazyNondet ( >->   NormalForm, Nondet,+>   NormalForm, Nondet, Context(..), > >   ID, initID, withUnique, >@@ -20,6 +20,8 @@ > >   ConsRep(..), cons, match, >+>   apply, fun+> > ) where > > import Data.Data@@ -28,3 +30,4 @@ > import Data.LazyNondet.Matching > import Data.LazyNondet.Narrowing > import Data.LazyNondet.Primitive+> import Data.LazyNondet.HigherOrder

@@ -0,0 +1,109 @@+% Higher-Order Non-Deterministic Operations+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module defines combinators for higher-order CFLP.++> {-# LANGUAGE +>       MultiParamTypeClasses, NoMonomorphismRestriction,+>       FunctionalDependencies,+>       TypeSynonymInstances,+>       UndecidableInstances,+>       FlexibleInstances,+>       FlexibleContexts+>   #-}+>+> module Data.LazyNondet.HigherOrder (+>+>   fun, apply+>+> ) where+>+> import Data.LazyNondet.Types+> import Data.LazyNondet.Matching ( withHNF )+>+> import Control.Monad.Update++With the `lambda` combinator functions on non-deterministic data are+lifted to the `Nondet` type.++> lambda :: Monad m+>        => (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)+>        -> Nondet cs m (a -> b)+> lambda f = Typed . return $ Lambda (\x cs -> untyped . f (Typed x) cs)++To apply a lambda, we provide the combinator `apply`.++> apply :: Update cs m m+>       => Nondet cs m (a -> b) -> Nondet cs m a+>       -> Context cs -> ID -> Nondet cs m b+> apply f x cs u = withHNF f (\f cs ->+>   case f of+>     Lambda f -> Typed (f (untyped x) cs u)+>     FreeVar _ f -> apply (Typed f) x cs u+>     _ -> error "Data.LazyNondet.HigherOrder: cannot apply") cs++The overloaded operation `fun` converts a function on+non-deterministic data (of arbitrary arity) into a (possibly nested)+lambda.++> fun :: (Monad m, LiftFun f g, NestLambda g cs m t)+>     => f -> Nondet cs m t+> fun = nestLambda . liftFun++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 cs m b | a -> cs, a -> m, a -> b+>  where+>   nestLambda :: Monad m => a -> Nondet cs m b++Single-argument functions can be lifted using `lambda`.++> instance NestLambda (Lifted cs m a b) cs m (a -> b)+>  where+>   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)+>  where+>   nestLambda f = lambda (\x _ _ -> nestLambda (f x))++We provide a combinator `liftFun` for ++  * constructor functions that do not take a constraint store or a+    unique id,++  * deterministic functions that only take a constraint store, and++  * non-deterministic functions that only take a unique id.++> class LiftFun f g | f -> g+>  where+>   liftFun :: f -> g+>+> instance LiftFun (Nondet cs m a -> Nondet cs m b) (Lifted cs m a b)+>  where+>   liftFun f = Lifted (\x _ _ -> f x)+>+> instance LiftFun (Nondet cs m a -> Context cs -> Nondet cs m b)+>                  (Lifted cs m a b)+>  where+>   liftFun f = Lifted (\x cs _ -> f x cs)+>+> instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b) (Lifted cs m a b)+>  where+>   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+>   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)+>  where+>   liftFun f = liftFun . f

@@ -24,13 +24,13 @@ > import Control.Monad.State > import Control.Monad.Update >-> withHNF :: (Monad m, Update cs m m)+> withHNF :: Update cs m m >         => Nondet cs m a->         -> (HeadNormalForm cs m -> cs -> Nondet cs m b)->         -> cs -> Nondet cs m b-> withHNF x b cs = Typed (do+>         -> (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 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@@ -96,11 +96,13 @@ the list of untyped values and yields the result of applying the given function to typed versions of these values. -> newtype Match a cs m b = Match { unMatch :: (ConIndex, cs -> Branch cs m b) }+> newtype Match a cs m b+>   = Match { unMatch :: (ConIndex, Context cs -> Branch cs m b) }+> > type Branch cs m a = [Untyped cs m] -> Nondet cs m a > > match :: (ConsRep a, WithUntyped b)->       => a -> (C b -> b) -> Match t (C b) (M b) (T b)+>       => a -> (Context (C b) -> b) -> Match t (C b) (M b) (T b) > match c alt = Match (constrIndex (consRep c), withUntyped . alt)  The operation `match` is used to build destructor functions for@@ -112,12 +114,12 @@ Failure is just a type version of `mzero`.  > caseOf :: Update cs m m->        => Nondet cs m a -> [Match a cs m b] -> cs -> Nondet cs m b+>        => Nondet cs m a -> [Match a cs m b] -> Context cs -> Nondet cs m b > caseOf x bs = caseOf_ x bs failure > > caseOf_ :: Update cs m m >         => Nondet cs m a -> [Match a cs m b] -> Nondet cs m b->         -> cs -> Nondet cs m b+>         -> Context cs -> Nondet cs m b > caseOf_ x bs def = >   withHNF x $ \hnf cs -> >   case hnf of@@ -127,6 +129,7 @@ >       | otherwise -> caseOf_ (Typed (res cs)) bs def cs >     Cons _ idx args -> >       maybe def (\b -> b cs args) (lookup idx (map unMatch bs))+>     Lambda _ -> error "Data.LazyNondet.Matching.caseOf: cannot match lambda"  We provide operations `caseOf_` and `caseOf` (with and without a default alternative) for more convenient pattern matching. The untyped

@@ -24,15 +24,15 @@ > unknown :: (MonadUpdate cs m, Narrow cs a) => ID -> Nondet cs m a > unknown u = freeVar u (delayed (redelay u) (\cs -> narrow cs u)) >-> redelay :: ChoiceStore cs => ID -> cs -> Bool-> redelay (ID us) = isNothing . lookupChoice (supplyValue us)+> redelay :: ChoiceStore cs => ID -> Context cs -> Bool+> redelay (ID us) (Context cs) = isNothing . lookupChoice (supplyValue us) $ cs  The application of `unknown` to a constraint store and a unique identifier represents a logic variable of an arbitrary type.   > class ChoiceStore cs => Narrow cs a >  where->   narrow :: MonadUpdate cs m => cs -> ID -> Nondet cs m a+>   narrow :: MonadUpdate cs m => Context cs -> ID -> Nondet cs m a  Logic variables of type `a` can be narrowed to head-normal form if there is an instance of the type class `Narrow`. A constraint store@@ -52,8 +52,9 @@ executions and *not* reexecuted.  > oneOf :: (MonadUpdate cs m, ChoiceStore cs)->       => [Nondet cs m a] -> cs -> ID -> Nondet cs m a-> oneOf xs cs (ID us) = Typed (choice cs (supplyValue us) (map untyped xs))+>       => [Nondet cs m a] -> Context cs -> ID -> Nondet cs m a+> oneOf xs (Context cs) (ID us)+>   = Typed (choice cs (supplyValue 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

@@ -40,7 +40,7 @@ > 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 (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@@ -49,12 +49,13 @@ 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 -> cs -> m' NormalForm-> groundNormalForm = evalStateT . gnf . untyped+> groundNormalForm :: Update cs m m'+>                  => Nondet cs m a -> Context cs -> m' NormalForm+> groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs > > partialNormalForm :: (Update cs m m', ChoiceStore cs)->                   => Nondet cs m a -> cs -> m' NormalForm-> partialNormalForm = evalStateT . pnf . untyped+>                   => 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@@ -92,10 +93,11 @@ >     FreeVar u@(ID us) y -> >       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y)) >             . lkp (supplyValue us)->     Delayed _ resume -> get >>= nf lkp cns fv . resume+>     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"  The `nf` function is used by all normal-form functions and performs all the work.@@ -123,7 +125,7 @@ >   hnf <- updateState x >   case hnf of >     FreeVar _ y -> solveCons y->     Delayed _ res -> get >>= solveCons . res+>     Delayed _ res -> get >>= solveCons . res . Context >     _ -> return hnf  The function `solveCons` is like `solve` but always yields a

@@ -11,8 +11,10 @@ > > module Data.LazyNondet.Types ( >->   ID(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),+>   Context(..), ID(..),  >+>   NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),+> >   mkHNF, freeVar, delayed > > ) where@@ -23,6 +25,8 @@ > > import Data.Supply >+> newtype Context cs = Context cs+> > newtype ID = ID (Supply Int) > > data NormalForm = NormalForm Constr [NormalForm] | Var Int@@ -36,7 +40,8 @@ > data HeadNormalForm cs m >   = Cons DataType ConIndex [Untyped cs m] >   | FreeVar ID (Untyped cs m)->   | Delayed (cs -> Bool) (cs -> Untyped cs m)+>   | Delayed (Context cs -> Bool) (Context cs -> Untyped cs m)+>   | Lambda (Untyped cs m -> Context cs -> ID -> Untyped cs m) > > type Untyped cs m = m (HeadNormalForm cs m) @@ -69,7 +74,8 @@ The function `freeVar` is used to put a name around a narrowed free variable. -> delayed :: Monad m => (cs -> Bool) -> (cs -> Nondet cs m a) -> Nondet cs m a+> delayed :: Monad m => (Context cs -> Bool) -> (Context cs -> Nondet cs m a)+>         -> Nondet cs m a > delayed p resume = Typed . return . Delayed p $ (untyped . resume)  With `delayed` computations can be delayed to be reexecuted with the@@ -88,6 +94,7 @@ >  where >   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++[")"])@@ -104,7 +111,8 @@ > instance Show (HeadNormalForm cs (UpdateT cs [])) >  where >   show (FreeVar (ID u) _)  = '_':show (supplyValue u)->   show (Delayed _ _)         = "<delayed>"+>   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)++")" 

@@ -26,13 +26,13 @@ > true :: Monad m => Nondet cs m Bool > true = cons True >-> pTrue :: (cs -> Nondet cs m a) -> Match Bool cs m a+> 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 >-> pFalse :: (cs -> Nondet cs m a) -> Match Bool cs m a+> pFalse :: (Context cs -> Nondet cs m a) -> Match Bool cs m a > pFalse = match False  In order to be able to use logic variables of boolean type, we make it@@ -44,11 +44,11 @@  Some operations with `Bool`s: -> not :: Update cs m m => Nondet cs m Bool -> cs -> Nondet cs m Bool+> not :: Update cs m m => Nondet cs m Bool -> Context cs -> Nondet cs m Bool > not x = caseOf_ x [pFalse (const true)] false > > (===) :: Update cs m m->       => Nondet cs m a -> Nondet cs m a -> cs -> Nondet cs m Bool-> (x === y) cs = Typed $ do+>       => Nondet cs m a -> Nondet cs m a -> Context cs -> Nondet cs m Bool+> (x === y) (Context cs) = Typed $ do >   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs >   untyped $ if eq then true else false

@@ -19,24 +19,27 @@ > > import Control.Constraint.Choice >+> import Prelude hiding ( map, foldr )+> import qualified Prelude as P+> > instance ConsRep [()] where consRep = toConstr > > nil :: Monad m => Nondet cs m [a] > nil = cons ([] :: [()]) >-> pNil :: (cs -> Nondet cs m b) -> Match [a] cs m b+> pNil :: (Context cs -> Nondet cs m b) -> Match [a] cs m b > pNil = match ([] :: [()]) > > infixr 5 ^: > (^:) :: Monad m => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a] > (^:) = cons ((:) :: () -> [()] -> [()]) >-> pCons :: (cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)+> pCons :: (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 = foldr (^:) nil+> fromList = P.foldr (^:) nil  We can use logic variables of a list type if there are logic variables for the element type.@@ -48,12 +51,29 @@  Some operations on lists: -> null :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m Bool+> null :: Update cs m m => 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] -> cs -> Nondet cs m a+> head :: Update cs m m => 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] -> cs -> Nondet cs m [a]+> tail :: Update cs m m => 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+>     => 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+>       => 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 ->+>   caseOf l+>     [ pNil (const y)+>     , pCons (\cs x xs -> apply (apply f x cs u1) (foldr f y xs cs u2) cs u3)+>     ] cs