cflp 0.1 → 0.2.0

raw patch · 19 files changed

+837/−492 lines, 19 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• INSTALL +9/−9
• Makefile +6/−0
• README +3/−0
• cflp.cabal +12/−5
• configure +2/−0
• src/Control/CFLP.lhs +37/−20
• src/Control/CFLP/Tests/CallTimeChoice.lhs +8/−7
• src/Control/Monad/Constraint/Choice.lhs +31/−6
• src/Data/LazyNondet.lhs +13/−348
• src/Data/LazyNondet/Bool.lhs +0/−43
• src/Data/LazyNondet/Combinators.lhs +77/−0
• src/Data/LazyNondet/List.lhs +0/−54
• src/Data/LazyNondet/Matching.lhs +134/−0
• src/Data/LazyNondet/Narrowing.lhs +71/−0
• src/Data/LazyNondet/Primitive.lhs +118/−0
• src/Data/LazyNondet/Types.lhs +128/−0
• src/Data/LazyNondet/Types/Bool.lhs +54/−0
• src/Data/LazyNondet/Types/List.lhs +61/−0
• src/Data/LazyNondet/UniqueID.lhs +73/−0

@@ -1,16 +1,16 @@ # Installation Instructions -You can install the `cflp` package as follows.+You can install the `cflp` package as follows: - 1. Unpack the sources and move into the source directory.+    > ./configure+    > make+    > make install -        > tar -xzf cflp-*.tar.gz-        > cd cflp-*+This will register the package in your user package databse.  - 2. Run configure, build, test, and install.+If you want to install it globally, type: -        > runhaskell Setup.lhs configure --user-        > runhaskell Setup.lhs build-        > runhaskell Setup.lhs test-        > runhaskell Setup.lhs install+    > ./configure --global+    > make+    > sudo make install 

@@ -0,0 +1,6 @@+build:+	runhaskell Setup.lhs build++install:+	runhaskell Setup.lhs install+

@@ -12,3 +12,6 @@  [cflp]: http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html +Sebastian Fischer, 2008+sebf@informatik.uni-kiel.de+

@@ -1,5 +1,5 @@ Name:          cflp-Version:       0.1+Version:       0.2.0 Cabal-Version: >= 1.2 Synopsis:      Constraint Functional-Logic Programming in Haskell Description:   This package provides combinators for constraint@@ -17,7 +17,7 @@ Build-Type:    Custom Stability:     alpha -Extra-Source-Files: README, INSTALL, Test.lhs+Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs  Library   Build-Depends:    base >= 4, ghc, mtl, syb, HUnit@@ -25,8 +25,14 @@   Other-Modules:    Control.Monad.Constraint,                     Control.Monad.Constraint.Choice,                     Data.LazyNondet,-                    Data.LazyNondet.Bool,-                    Data.LazyNondet.List,+                    Data.LazyNondet.Types,+                    Data.LazyNondet.Types.Bool,+                    Data.LazyNondet.Types.List,+                    Data.LazyNondet.UniqueID,+                    Data.LazyNondet.Matching,+                    Data.LazyNondet.Narrowing,+                    Data.LazyNondet.Primitive,+                    Data.LazyNondet.Combinators,                     Control.CFLP.Tests,                     Control.CFLP.Tests.CallTimeChoice   Hs-Source-Dirs:   src@@ -34,9 +40,10 @@                     MultiParamTypeClasses,                     FlexibleInstances,                     FlexibleContexts,+                    PatternGuards,                     TypeFamilies,                     RankNTypes-  Ghc-Options:      -O2 -Wall -fno-warn-orphans+  Ghc-Options:      -Wall -fno-warn-orphans  Source-Repository head   type:     git

@@ -0,0 +1,2 @@+#!/bin/bash+runhaskell Setup.lhs configure ${1-"--user"}

@@ -13,19 +13,20 @@ > > module Control.CFLP ( >->   CFLP, Computation, eval, evalPrint,+>   CFLP, ChoiceStore, Computation, eval, evalPartial, evalPrint, > >   Strategy, depthFirst, > >   module Data.LazyNondet,->   module Data.LazyNondet.Bool,->   module Data.LazyNondet.List+>   module Data.LazyNondet.Types.Bool,+>   module Data.LazyNondet.Types.List > > ) where > > import Data.LazyNondet-> import Data.LazyNondet.Bool-> import Data.LazyNondet.List+> import Data.LazyNondet.Primitive+> import Data.LazyNondet.Types.Bool+> import Data.LazyNondet.Types.List > > import Control.Monad.State > import Control.Monad.Constraint@@ -33,6 +34,7 @@ > > class (MonadConstr Choice m, >        ConstraintStore Choice cs,+>        ChoiceStore cs, >        MonadSolve cs m m) >  => CFLP cs m @@ -41,17 +43,17 @@ constraint store and a constraint monad. Hence, such computations can be executed with different constraint stores and search strategies. -> instance CFLP ChoiceStore (ConstrT ChoiceStore [])+> instance CFLP ChoiceStoreUnique (ConstrT ChoiceStoreUnique [])  We declare instances for every combination of monad and constraint store that we intend to use. -> type EvalStore = ChoiceStore+> type CS = ChoiceStoreUnique >-> noConstraints :: EvalStore+> noConstraints :: CS > noConstraints = noChoices >-> type Computation m a = EvalStore -> ID -> Nondet (ConstrT EvalStore m) a+> type Computation m a = CS -> ID -> Nondet CS (ConstrT CS m) a  Currently, the constraint store used to evaluate constraint functional-logic programs is simply a `ChoiceStore`. It will be a@@ -68,20 +70,28 @@  The strategy of the list monad is depth-first search. -> eval :: (CFLP EvalStore m, MonadSolve EvalStore m m', Data a)->      => Strategy m' -> (EvalStore -> ID -> Nondet m a)->      -> IO [a]-> eval enumerate op = do+> evaluate :: (CFLP CS m, MonadSolve CS m m')+>          => (Nondet CS m a -> CS -> m' b)+>          -> Strategy m' -> (CS -> ID -> Nondet CS m a)+>          -> IO [b]+> evaluate evalNondet enumerate op = do >   i <- initID->   return (enumerate (normalForm (op noConstraints i) noConstraints))+>   return $ enumerate $ evalNondet (op noConstraints i) noConstraints -The `eval` function enumerates the non-deterministic solutions of a+The `evaluate` function enumerates the non-deterministic solutions of a constraint functional-logic computation according to a given strategy. -> evalPrint :: (CFLP EvalStore m, MonadSolve EvalStore m m', Data a, Show a)->           => Strategy m' -> (EvalStore -> ID -> Nondet m a)+> eval, evalPartial :: (CFLP CS m, MonadSolve CS m m', Data a)+>                   => Strategy m' -> (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, MonadSolve CS m m', Data a, Show a)+>           => Strategy m' -> (CS -> ID -> Nondet CS m a) >           -> IO () > evalPrint s op = eval s op >>= printSols+>  -- evaluate partialNormalForm s op >>= printSols > > printSols :: Show a => [a] -> IO () > printSols []     = putStrLn "No more solutions."@@ -95,7 +105,14 @@ >     then mapM_ print xs >     else printSols xs -For convenience, we provide an `evalPrint` operation that-interactively shows solutions of a constraint functional-logic-computation.+We provide++  * an `eval` operation to compute Haskell terms from non-determinitic+    data,++  * an operation `evalPartial` to compute partial Haskell terms where+    logic variables are replaced with an error, and++  * an `evalPrint` operation that interactively shows (partial)+    solutions of a constraint functional-logic computation. 

@@ -30,9 +30,10 @@ > ignoreFirstNarrowSecond :: Assertion > ignoreFirstNarrowSecond = assertResults comp [True,False] >  where->   comp cs u = ignot (error "illegal demand") (unknown u) cs+>   comp cs u = ignot (error "illegal demand") (unknown cs u) cs >-> ignot :: CFLP cs m => Nondet m a -> Nondet m Bool -> cs -> Nondet m Bool+> ignot :: CFLP cs m+>       => Nondet cs m a -> Nondet cs m Bool -> cs -> Nondet cs m Bool > ignot _ x = not x  This test checks a function with two arguments, where the first must@@ -44,9 +45,9 @@ > sharedVarsAreEqual :: Assertion > sharedVarsAreEqual = assertResults comp [[False,False],[True,True]] >  where->   comp _ u = two (unknown u)+>   comp cs u = two (unknown cs u) >-> two :: Monad m => Nondet m a -> Nondet m [a]+> two :: Monad m => Nondet cs m a -> Nondet cs m [a] > two x = x ^: x ^: nil  This test checks call-time choice semantics: variables represent@@ -61,7 +62,7 @@ > noDemandOnSharedVar :: Assertion > noDemandOnSharedVar = assertResults comp [False] >  where->   comp cs _ = null (two (error "illegal demand")) cs+>   comp cs _ = null (two (error "illegal demand" :: Nondet cs m Bool)) cs  Even with an explicit combinator for sharing (to be used, e.g., in the definition of the function `two`) there must not be demand on@@ -70,9 +71,9 @@ > sharedCompoundTerms :: Assertion > sharedCompoundTerms = assertResults comp [[True,False],[False,True]] >  where->   comp cs u = negHeads (unknown u) cs+>   comp cs u = negHeads (unknown cs u) cs >-> negHeads :: CFLP cs m => Nondet m [Bool] -> cs -> Nondet m [Bool]+> negHeads :: CFLP cs m => Nondet cs m [Bool] -> 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

@@ -17,7 +17,7 @@ > > module Control.Monad.Constraint.Choice ( >->   Choice, ChoiceStore, noChoices, choice+>   Choice, ChoiceStore(..), ChoiceStoreUnique, noChoices, choice > > ) where >@@ -30,14 +30,27 @@ We borrow unique identifiers from the package `ghc` which is hidden by default. +> class ChoiceStore cs+>  where+>   lookupChoice :: Unique -> cs -> Maybe Int++We define an interface for choice stores that provide an operation to+lookup a previously made choice.+ > newtype Choice = Choice (Unique,Int)-> newtype ChoiceStore = ChoiceStore (UniqFM Int)+> newtype ChoiceStoreUnique = ChoiceStore (UniqFM Int) >-> noChoices :: ChoiceStore+> noChoices :: ChoiceStoreUnique > noChoices = ChoiceStore emptyUFM >-> instance ConstraintStore Choice ChoiceStore+> instance ChoiceStore ChoiceStoreUnique >  where+>   lookupChoice u (ChoiceStore cs) = lookupUFM_Directly cs u++A finite map mapping `Unique`s to integers is a `ChoiceStore`.++> instance ConstraintStore Choice ChoiceStoreUnique+>  where >   assert (Choice (u,x)) = do >     ChoiceStore cs <- get >     maybe (put (ChoiceStore (addToUFM_Directly cs u x)))@@ -49,8 +62,12 @@  The `assert` operations fails to insert conflicting choices. -> choice :: MonadConstr Choice m => Unique -> [m a] -> m a-> choice u = foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..]+> choice :: (MonadConstr Choice m, ChoiceStore cs)+>        => cs -> Unique -> [m a] -> m a+> choice cs u xs =+>   maybe (foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..] $ xs)+>         (xs!!)+>         (lookupChoice u cs) >  where constrain n = (constr (Choice (u,n))>>)  The operation `choice` takes a unique label and a list of monadic@@ -59,4 +76,12 @@ occurs more than once in a bigger monadic action, the result is constrained to take the same alternative everywhere when collecting constraints.++If a choice with the same label has been created previously and the+label is already constrained to an alternative, then this alternative+is returned directly and no choice is created.++This situation may occur if a shared logic variable is renarrowed+whenever it is demanded rather than shared and only narrowed on+creation. 

@@ -4,363 +4,28 @@ This module provides a datatype with operations for lazy non-deterministic programming. -> {-# LANGUAGE->       ExistentialQuantification,->       MultiParamTypeClasses,->       FlexibleInstances,->       FlexibleContexts,->       TypeFamilies,->       FunctionalDependencies->   #-}-> > module Data.LazyNondet ( >->   NormalForm, HeadNormalForm(..), mkHNF, Nondet(..),+>   NormalForm, Nondet, > >   ID, initID, withUnique, >->   Unknown(..), failure, oneOf, withHNF, caseOf, caseOf_, Match,+>   Narrow(..), NarrowPolicy(..), unknown,  >->   Data, nondet, normalForm,+>   failure, oneOf, >->   ConsRep(..), cons, match,+>   withHNF, caseOf, caseOf_, Match, >->   prim_eq+>   Data, nondet, groundNormalForm, partialNormalForm, >+>   ConsRep(..), cons, match,+> > ) where > > import Data.Data-> import Data.Generics.Twins ( gmapAccumT )->-> import Control.Monad.State-> import Control.Monad.Constraint-> import Control.Monad.Constraint.Choice->-> import UniqSupply--We borrow unique identifiers from the package `ghc` which is hidden by-default.--> data NormalForm = NormalForm Constr [NormalForm]->  deriving Show--The normal form of data is represented by the type `NormalForm` which-defines a tree of constructors. 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.--> data HeadNormalForm m = Cons DataType ConIndex [Untyped m]-> type Untyped m = m (HeadNormalForm m)->-> mkHNF :: Constr -> [Untyped m] -> HeadNormalForm m-> mkHNF c args = Cons (constrType c) (constrIndex c) args--Data in lazy functional-logic programs is evaluated on demand. The-evaluation of arguments of a constructor may lead to different-non-deterministic results. Hence, we use a monad around every-constructor in the head-normal form of a value.--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.--> newtype Nondet m a = Typed { untyped :: Untyped m }--Untyped non-deterministic data can be phantom typed in order to define-logic variables by overloading. The phantom type must be the Haskell-data type that should be used for conversion.--Threading Unique Identifiers-------------------------------Non-deterministic computations need a supply of unique identifiers in-order to constrain shared choices.--> newtype ID = ID UniqSupply->-> initID :: IO ID-> initID = liftM ID $ mkSplitUniqSupply 'x'->-> class With x a->  where->   type Mon x a :: * -> *->   type Typ x a->->   with :: a -> x -> Nondet (Mon x a) (Typ x a)->-> instance With x (Nondet m a)->  where->   type Mon x (Nondet m a) = m->   type Typ x (Nondet m a) = a->->   with = const->-> instance With ID a => With ID (ID -> a)->  where->   type Mon ID (ID -> a) = Mon ID a->   type Typ ID (ID -> a) = Typ ID a->->   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-non-deterministic operations. Non-deterministic operations have an-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-the same time:--    Nondet m a -> ID -> Nondet m a-    (ID -> Nondet m a) -> ID -> Nondet m a-    (ID -> ID -> Nondet m a) -> ID -> Nondet m a-    (ID -> ID -> ID -> Nondet m a) -> ID -> Nondet m a-    ...--We make use of type families because GHC considers equivalent-definitions with functional dependencies illegal due to the overly-restrictive "coverage condition".--Combinators for Functional-Logic Programming-----------------------------------------------> class Unknown a->  where->   unknown :: MonadConstr Choice m => ID -> Nondet m a--The application of `unknown` to a unique identifier represents a logic-variable of the corresponding type.--> oneOf :: MonadConstr Choice m => [Nondet m a] -> ID -> Nondet m a-> 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-the given list.--> failure :: MonadPlus m => Nondet m a-> failure = Typed mzero--A failing computation could be defined using `oneOf`, but we provide a-special combinator that does not need a supply of unique identifiers.--> 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 (b hnf cs'))--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----------------------------------------------------------> prim :: Data a => NormalForm -> a-> prim (NormalForm con args) =->   snd (gmapAccumT perkid args (fromConstr con))->  where->   perkid ts _ = (tail ts, prim (head ts))->-> generic :: Data a => a -> NormalForm-> generic x = NormalForm (toConstr x) (gmapQ generic x)->-> 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 . nf2hnf . generic--We provide generic operations to convert between instances of the-`Data` class and non-deterministic data.--> normalForm :: (MonadSolve cs m m', Data a) => Nondet m a -> cs -> m' a-> normalForm x cs = liftM prim $ evalStateT (nf (untyped x)) cs->-> nf :: MonadSolve cs m m' => Untyped m -> StateT cs m' NormalForm-> nf x = do->   Cons typ idx args <- solve x->   nfs <- mapM nf args->   return (NormalForm (indexConstr typ idx) nfs)--The `normalForm` function evaluates a non-deterministic value and-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->   show (Cons typ idx args) ->     | null args = show con->     | otherwise = unwords (("("++show con):map show args++[")"])->    where con = indexConstr typ idx->-> instance Show (Nondet [] a)->  where->   show = show . untyped->-> instance Show (Nondet (ConstrT cs []) a)->  where->   show = show . untyped->-> instance Show (HeadNormalForm (ConstrT cs []))->  where->   show (Cons typ idx [])   = show (indexConstr typ idx)->   show (Cons typ idx args) =->     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" --To simplify debugging, we provide `Show` instances for head-normal-forms and non-deterministic values.-+> import Data.LazyNondet.Types+> import Data.LazyNondet.UniqueID+> import Data.LazyNondet.Matching+> import Data.LazyNondet.Narrowing+> import Data.LazyNondet.Primitive+> import Data.LazyNondet.Combinators

@@ -1,43 +0,0 @@-% Lazy Non-Deterministic Bools-% Sebastian Fischer (sebf@informatik.uni-kiel.de)--This module provides non-deterministic booleans.--> module Data.LazyNondet.Bool where->-> import Data.Data-> import Data.LazyNondet->-> import Control.Monad.State-> import Control.Monad.Constraint->-> instance ConsRep Bool where consRep = toConstr->-> true :: Monad m => Nondet m Bool-> true = cons True->-> pTrue :: (cs -> Nondet m a) -> Match cs m a-> pTrue = match True->-> false :: Monad m => Nondet m Bool-> 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`.--> instance Unknown Bool->  where->   unknown = oneOf [false,true]--Some operations with `Bool`s:--> not :: MonadSolve cs m m => Nondet m Bool -> cs -> Nondet m Bool-> 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

@@ -0,0 +1,77 @@+% Combinators for Programs on Lazy Non-Deterministic Data+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++> {-# LANGUAGE+>       FlexibleContexts,+>       FlexibleInstances,+>       MultiParamTypeClasses,+>       FunctionalDependencies+>   #-}+>+> module Data.LazyNondet.Combinators (+>+>   cons, failure, oneOf, ConsRep(..)+>+> ) where+>+> import Data.Data+> import Data.LazyNondet.Types+>+> import Control.Monad+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> import UniqSupply+>+> oneOf :: (MonadConstr Choice m, ChoiceStore cs)+>       => [Nondet cs m a] -> cs -> ID -> Nondet cs m a+> oneOf xs cs (ID us) = Typed (choice cs (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+the given list.++> failure :: MonadPlus m => Nondet cs m a+> failure = Typed mzero++A failing computation could be defined using `oneOf`, but we provide a+special combinator that does not need a supply of unique identifiers.++> class MkCons cs m a b | b -> m, b -> cs+>  where+>   mkCons :: a -> [Untyped cs m] -> b+>+> instance (Monad m, Data a) => MkCons cs m a (Nondet cs m t)+>  where+>   mkCons c args = Typed (return (mkHNF (toConstr c) (reverse args)))+>+> instance MkCons cs m b c => MkCons cs m (a -> b) (Nondet cs m t -> c)+>  where+>   mkCons c xs x = mkCons (c undefined) (untyped x:xs)+>+> cons :: MkCons cs m a b => a -> b+> cons c = mkCons c []++The overloaded operation `cons` takes a Haskell constructor and yields+a corresponding constructor function for non-deterministic values.++> 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.

@@ -1,54 +0,0 @@-% Lazy Non-Deterministic Lists-% Sebastian Fischer (sebf@informatik.uni-kiel.de)--This module provides non-deterministic lists.--> {-# LANGUAGE->       FlexibleInstances->   #-}->-> module Data.LazyNondet.List where->-> import Data.Data-> import Data.LazyNondet-> import Data.LazyNondet.Bool->-> import Control.Monad.Constraint->-> instance ConsRep [()] where consRep = toConstr->-> nil :: Monad m => Nondet m [a]-> 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]-> (^:) = 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--We can use logic variables of a list type if there are logic variables-for the element type.--> instance Unknown a => Unknown [a]->  where->   unknown = withUnique $ \u1 u2 -> ->              oneOf [nil, unknown u1 ^: unknown u2]--Some operations on lists:--> null :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m Bool-> null xs = caseOf_ xs [pNil (\_ -> true)] false->-> head :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m a-> head l = caseOf l [pCons (\_ x _ -> x)]->-> tail :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m [a]-> tail l = caseOf l [pCons (\_ _ xs -> xs)]-

@@ -0,0 +1,134 @@+% Pattern Matching of Lazy Non-Deterministic Data+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++> {-# LANGUAGE+>       RankNTypes,+>       TypeFamilies,+>       FlexibleContexts,+>       FlexibleInstances,+>       ExistentialQuantification+>   #-}+>+> module Data.LazyNondet.Matching (+>+>   Match, match, withHNF, caseOf, caseOf_+>+> ) where+>+> import Data.Data+> import Data.LazyNondet.Types+> import Data.LazyNondet.Combinators+>+> import Control.Monad.State+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> withHNF :: (Monad m, MonadSolve 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+>   (hnf,cs') <- runStateT (solve (untyped x)) cs+>   untyped (b hnf cs'))++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.++> class WithUntyped a+>  where+>   type C a+>   type M a :: * -> *+>   type T a+>+>   withUntyped :: a -> [Untyped (C a) (M a)] -> Nondet (C a) (M a) (T a)++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 cs m] a, m ~ Mon [Untyped cs m] a) => WithUnique a+     where+      withUnique :: a -> [Untyped cs m] -> Nondet cs m (Typ [Untyped cs 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 cs m a)+>  where+>   type C (Nondet cs m a) = cs+>   type M (Nondet cs m a) = m+>   type T (Nondet cs m a) = a+>+>   withUntyped = const+>+> instance (WithUntyped a, cs ~ C a, m ~ M a)+>        => WithUntyped (Nondet cs m b -> a)+>  where+>   type C (Nondet cs m b -> a) = C a+>   type M (Nondet cs m b -> a) = M a+>   type T (Nondet cs 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 cs m a+                -> [Untyped cs m] -> Nondet cs m a++    withUntyped :: (Nondet cs m a -> Nondet cs m b)+                -> [Untyped cs m] -> Nondet cs m b++    withUntyped :: (Nondet cs m a -> Nondet cs m b -> Nondet cs m c)+                -> [Untyped cs m] -> Nondet cs m c+    ...++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 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) }+> data Branch cs m a =+>   forall t . (WithUntyped t, cs ~ C t, m ~ M t, a ~ T t) => Branch t+>+> match :: (ConsRep a, WithUntyped b)+>       => a -> (C b -> b) -> Match t (C b) (M b) (T b)+> match c alt = Match (constrIndex (consRep c), Branch . alt)++The operation `match` is used to build destructor functions for+non-deterministic values that can be used with `caseOf`.++> caseOf :: (MonadSolve cs m m, MonadConstr Choice m)+>        => Nondet cs m a -> [Match a cs m b] -> cs -> Nondet cs m b+> caseOf x bs = caseOf_ x bs failure+>+> caseOf_ :: (MonadSolve cs m m, MonadConstr Choice m)+>         => Nondet cs m a -> [Match a cs m b] -> Nondet cs m b+>         -> cs -> Nondet cs m b+> caseOf_ x bs def =+>   withHNF x $ \hnf cs ->+>   case hnf of+>     FreeVar _ y -> caseOf_ (Typed y) bs def cs+>     Delayed res -> caseOf_ (Typed (res cs)) bs def cs+>     Cons _ idx args ->+>       maybe def (\b -> branch (b cs) args) (lookup idx (map unMatch bs))+>+> branch :: Branch cs m a -> [Untyped cs m] -> Nondet cs 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.+

@@ -0,0 +1,71 @@+% Logic Variables and Narrowing+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++> {-# LANGUAGE+>       FlexibleContexts,+>       MultiParamTypeClasses+>   #-}+>+> module Data.LazyNondet.Narrowing (+>+>   unknown, Narrow(..), NarrowPolicy(..)+>+> ) where+>+> import Data.LazyNondet.Types+>+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> unknown :: (MonadConstr Choice m, Narrow cs a) => cs -> ID -> Nondet cs m a+> unknown cs u = freeVar u (narrowWithPolicy cs u)++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+>   narrowPolicy :: NarrowPolicy cs a+>   narrowPolicy = OnDemand+>+>   narrow :: MonadConstr Choice m => 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+may be used to find the possible results which are returned in a monad+that supports choices. Usually, `narrow` will be implemented as a+non-deterministic generator using `oneOf`, but for specific types+different strategies may be implemented.++The default policy is to narrow on demand in order to avoid+unnessesary choices in shared free variables that can lead to+exponential explosion of the search space.++A `NarrowPolicy` specifies whether a logic variable should be++ * narrowed whenever it is demanded according the current constraint+   store or++ * narrowed only on creation and shared on every demand.++> data NarrowPolicy cs a = OnDemand | OnCreation++Using `OnDemand` can avoid unnessesary branching when accessing a+variable with an updated constraint store. Using `OnCreation` will+avoid the reexecution of a non-deterministic generator.++> narrowWithPolicy :: (MonadConstr Choice m, Narrow cs a)+>                  => cs -> ID -> Nondet cs m a+> narrowWithPolicy cs u = x+>  where+>   x = case policy x of+>         OnDemand   -> delayed (`narrow`u)+>         OnCreation -> narrow cs u+>+> policy :: Narrow cs a => Nondet cs m a -> NarrowPolicy cs a+> policy _ = narrowPolicy++The function `narrowWithPolicy` narrows a logic variable or creates a+delayed execution that will be performed whenever the variable is+demanded. The definition uses a helper function in order to constrain+the type of the narrowing policy.

@@ -0,0 +1,118 @@+% Primitive Generic Functions on Lazy Non-Deterministic Data+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++> {-# LANGUAGE+>       FlexibleContexts+>   #-}+>+> module Data.LazyNondet.Primitive (+>+>   nondet, prim, groundNormalForm, partialNormalForm,+>+>   prim_eq+>+> ) where+>+> import Data.Data+> import Data.Generics.Twins+> import Data.LazyNondet.Types+>+> import Control.Monad.State+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> import Unique+> import UniqSupply+>+> 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 :: MonadSolve cs m m' => Nondet cs m a -> cs -> m' NormalForm+> groundNormalForm  = evalStateT . gnf . untyped+>+> partialNormalForm :: (MonadSolve cs m m', ChoiceStore cs)+>                   => Nondet cs m a -> cs -> m' NormalForm+> partialNormalForm = evalStateT . pnf . untyped++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.++> gnf :: MonadSolve cs m m' => Untyped cs m -> StateT cs m' NormalForm+> gnf = nf (\_ _ -> Just ()) NormalForm mkVar+>+> mkVar :: ID -> a -> NormalForm+> mkVar (ID us) _ = Var (uniqFromSupply us)+>+> pnf :: (MonadSolve 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++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.++> nf :: MonadSolve cs m m'+>    => (Unique -> cs -> Maybe a)+>    -> (Constr -> [nf] -> nf)+>    -> (ID -> Untyped cs m -> nf)+>    -> Untyped cs m -> StateT cs m' nf+> nf lkp cns fv x = do+>   hnf <- solve x+>   case hnf of+>     FreeVar u@(ID us) y ->+>       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))+>             . lkp (uniqFromSupply us)+>     Delayed resume -> get >>= nf lkp cns fv . resume+>     Cons typ idx args -> do+>       nfs <- mapM (nf lkp cns fv) args+>       return (cns (indexConstr typ idx) nfs)++The `nf` function is used by all normal-form functions and performs al+the work.++> prim_eq :: MonadSolve cs m m+>         => Untyped cs m -> Untyped cs 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.

@@ -0,0 +1,128 @@+% Basic Types for Lazy Non-Deterministic Data+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module defines the basic types to represent lazy+non-deterministic data.++> {-# LANGUAGE+>       PatternGuards,+>       FlexibleInstances+>   #-}+>+> module Data.LazyNondet.Types (+>+>   ID(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),+>+>   mkHNF, freeVar, delayed+>+> ) where+>+> import Data.Data+>+> import Control.Monad.Constraint+>+> import Unique+> import UniqSupply+>+> newtype ID = ID UniqSupply+>+> data NormalForm = NormalForm Constr [NormalForm] | Var Unique++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.++> data HeadNormalForm cs m+>   = Cons DataType ConIndex [Untyped cs m]+>   | FreeVar ID (Untyped cs m)+>   | Delayed (cs -> Untyped cs m)+>+> type Untyped cs m = m (HeadNormalForm cs m)++Data in lazy functional-logic programs is evaluated on demand. The+evaluation of arguments of a constructor may lead to different+non-deterministic results. Hence, we use a monad around every+constructor in the head-normal form of a value.++> newtype Nondet cs m a = Typed { untyped :: Untyped cs m }++Untyped non-deterministic data can be phantom typed in order to define+logic variables by overloading. The phantom type must be the Haskell+data type that should be used for conversion into primitive data.++> mkHNF :: Constr -> [Untyped cs m] -> HeadNormalForm cs m+> mkHNF c args = Cons (constrType c) (constrIndex c) args++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 `Unknown u x` where `u` is a+uniqe identifier and `x` represents the result of narrowing the+variable according to the constraint store passed to the operation+that creates the variable.++> freeVar :: Monad m => ID -> Nondet cs m a -> Nondet cs m a+> freeVar u = Typed . return . FreeVar u . untyped++The function `freeVar` is used to put a name around a narrowed free+variable.++> delayed :: Monad m => (cs -> Nondet cs m a) -> Nondet cs m a+> delayed resume = Typed . return . Delayed $ (untyped . resume)++With `delayed` computations can be delayed to be reexecuted with the+current constraint store whenever they are demanded. This is useful to+avoid unessary branching when narrowing logic variables. Use with+care: `delayed` intentionally destroys sharing!++`Show` Instances+----------------++> instance Show (HeadNormalForm cs [])+>  where+>   show (FreeVar (ID u) _) = show (uniqFromSupply u)+>   show (Delayed _) = "<delayed>"+>   show (Cons typ idx args) +>     | null args = show con+>     | otherwise = unwords (("("++show con):map show args++[")"])+>    where con = indexConstr typ idx+>+> instance Show (Nondet cs [] a)+>  where+>   show = show . untyped+>+> instance Show (Nondet cs (ConstrT cs []) a)+>  where+>   show = show . untyped+>+> instance Show (HeadNormalForm cs (ConstrT cs []))+>  where+>   show (FreeVar (ID u) _)  = show (uniqFromSupply u)+>   show (Delayed _)         = "<delayed>"+>   show (Cons typ idx [])   = show (indexConstr typ idx)+>   show (Cons typ idx args) =+>     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" ++To simplify debugging, we provide `Show` instances for head-normal+forms and non-deterministic values.++> instance Show NormalForm+>  where+>   showsPrec _ (Var u) = shows u+>   showsPrec _ (NormalForm cons []) = shows cons+>   showsPrec n x@(NormalForm cons args)+>     | Just xs <- fromList x = shows xs+>     | n == 0    = shows cons . foldr1 (\y z -> (' ':).y.z) (map shows 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 _ = Nothing++For normal forms we provide a custum `Show` instance because we want+to use it to print partial values in the evaluator.

@@ -0,0 +1,54 @@+% Lazy Non-Deterministic Bools+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides non-deterministic booleans.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts+>   #-}+>+> module Data.LazyNondet.Types.Bool where+>+> import Data.Data+> import Data.LazyNondet+> import Data.LazyNondet.Types+> import Data.LazyNondet.Primitive+>+> import Control.Monad.State+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> instance ConsRep Bool where consRep = toConstr+>+> true :: Monad m => Nondet cs m Bool+> true = cons True+>+> pTrue :: (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 = match False++In order to be able to use logic variables of boolean type, we make it+an instance of the type class `Narrow`.++> instance ChoiceStore cs => Narrow cs Bool+>  where+>   narrow = oneOf [false,true]++Some operations with `Bool`s:++> not :: (MonadSolve cs m m, MonadConstr Choice m)+>     => Nondet cs m Bool -> cs -> Nondet cs m Bool+> not x = caseOf_ x [pFalse (\_ -> true)] false+>+> (===) :: MonadSolve cs m m+>       => Nondet cs m a -> Nondet cs m a -> cs -> Nondet cs m Bool+> (x === y) cs = Typed $ do+>   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs+>   untyped $ if eq then true else false

@@ -0,0 +1,61 @@+% Lazy Non-Deterministic Lists+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides non-deterministic lists.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts+>   #-}+>+> module Data.LazyNondet.Types.List where+>+> import Data.Data+> import Data.LazyNondet+> import Data.LazyNondet.Types.Bool+>+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> 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 = 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)+>       -> Match [a] cs m b+> pCons = match ((:) :: () -> [()] -> [()])+>+> fromList :: Monad m => [Nondet cs m a] -> Nondet cs m [a]+> fromList = foldr (^:) nil++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]+>  where+>   narrow cs = withUnique $ \u1 u2 -> +>                 oneOf [nil, unknown cs u1 ^: unknown cs u2] cs++Some operations on lists:++> null :: (MonadSolve cs m m, MonadConstr Choice m)+>      => Nondet cs m [a] -> cs -> Nondet cs m Bool+> null xs = caseOf_ xs [pNil (\_ -> true)] false+>+> head :: (MonadSolve cs m m, MonadConstr Choice m)+>      => Nondet cs m [a] -> cs -> Nondet cs m a+> head l = caseOf l [pCons (\_ x _ -> x)]+>+> tail :: (MonadSolve cs m m, MonadConstr Choice m)+>      => Nondet cs m [a] -> cs -> Nondet cs m [a]+> tail l = caseOf l [pCons (\_ _ xs -> xs)]+

@@ -0,0 +1,73 @@+% Unique Identifiers+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++> {-# LANGUAGE+>       TypeFamilies,+>       FlexibleContexts,+>       FlexibleInstances,+>       MultiParamTypeClasses+>   #-}+>+> module Data.LazyNondet.UniqueID (+>+>   initID, withUnique+>+> ) where+>+> import Data.LazyNondet.Types+>+> import Control.Monad+>+> import UniqSupply++Non-deterministic computations need a supply of unique identifiers in+order to constrain shared choices.++> initID :: IO ID+> initID = liftM ID $ mkSplitUniqSupply 'x'+>+> class With x a+>  where+>   type C x a+>   type M x a :: * -> *+>   type T x a+>+>   with :: a -> x -> Nondet (C x a) (M x a) (T x a)+>+> instance With x (Nondet cs m a)+>  where+>   type C x (Nondet cs m a) = cs+>   type M x (Nondet cs m a) = m+>   type T x (Nondet cs m a) = a+>+>   with = const+>+> instance With ID a => With ID (ID -> a)+>  where+>   type C ID (ID -> a) = C ID a+>   type M ID (ID -> a) = M ID a+>   type T ID (ID -> a) = T ID a+>+>   with f (ID us) = withUnique (f (ID vs)) (ID ws)+>    where (vs,ws) = splitUniqSupply us+>+> withUnique :: With ID a => a -> ID -> Nondet (C ID a) (M ID a) (T ID a)+> withUnique = with++We provide an overloaded operation `withUnique` to simplify the+distribution of unique identifiers when defining possibly+non-deterministic operations. Non-deterministic operations have an+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+the same time:++    Nondet m a -> ID -> Nondet m a+    (ID -> Nondet m a) -> ID -> Nondet m a+    (ID -> ID -> Nondet m a) -> ID -> Nondet m a+    (ID -> ID -> ID -> Nondet m a) -> ID -> Nondet m a+    ...++We make use of type families because GHC considers equivalent+definitions with functional dependencies illegal due to the overly+restrictive "coverage condition".