packages feed

cflp (empty) → 0.0.2

raw patch · 13 files changed

+881/−0 lines, 13 filesdep +HUnitdep +basedep +ghcbuild-type:Customsetup-changed

Dependencies added: HUnit, base, ghc, mtl, syb

Files

+ INSTALL view
@@ -0,0 +1,17 @@+# Installation Instructions++## Installation with Cabal++You can install the `cflp` package using Cabal as follows.++ 1. Unpack the sources and move into the source directory.++        > tar -xzf cflp-*.tar.gz+        > cd cflp-*++ 2. Run configure, build and install.++        > ./Setup.lhs configure --user+        > ./Setup.lhs build+        > ./Setup.lhs install+
+ LICENSE view
@@ -0,0 +1,32 @@+Copyright (c) 2008, Sebastian Fischer++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ 1. Redistributions of source code must retain the above copyright+    notice, this list of conditions and the following disclaimer.++ 2. Redistributions in binary form must reproduce the above copyright+    notice, this list of conditions and the following disclaimer in+    the documentation and/or other materials provided with the+    distribution.++ 3. Neither the name of the author nor the names of his contributors+    may be used to endorse or promote products derived from this+    software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+
+ README view
@@ -0,0 +1,14 @@+# Constraint Functional-Logic Programming in Haskell++The `cflp` package provides a module `Control.CFLP` with combinators+for constraint functional-logic programming ((C)FLP) in Haskell. The+combinators can be used as a target language for compiling programs+written in an FLP language like Curry or Toy. Another application of+FLP is demand driven test-case generation.++Consult the LICENSE file for copyright issues, the INSTALL file for+installation instructions, or the [project website][cflp] for+background information on this package.++[cflp]: http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html+
+ Setup.lhs view
@@ -0,0 +1,14 @@+% Cabal Setup File for the `cflp` Package+% Sebastian Fischer (sebf@informatik.uni-kiel.de)+% November, 2008++> import System.Process+> import System.Exit+> import Distribution.Simple+>+> main = defaultMainWithHooks $ simpleUserHooks { runTests = runTestSuite }+>+> runTestSuite _ _ _ _ =+>   runCommand "runhaskell -i.:src Test.lhs" >>= waitForProcess >>= exitWith++
+ cflp.cabal view
@@ -0,0 +1,42 @@+Name:          cflp+Version:       0.0.2+Cabal-Version: >= 1.2+Synopsis:      Constraint Functional-Logic Programming in Haskell+Description:   This package provides combinators for constraint+               functional-logic programming ((C)FLP) in Haskell. The +               combinators can be used as a target language for compiling +               programs written in an FLP language like Curry or Toy. Another +               application of FLP is demand driven test-case generation.+Category:      Control+License:       BSD3+License-File:  LICENSE+Author:        Sebastian Fischer+Maintainer:    sebf@informatik.uni-kiel.de+Homepage:      http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html+Build-Type:    Custom+Stability:     alpha++Extra-Source-Files: README, INSTALL++Library+  Build-Depends:    base, ghc, mtl, syb, HUnit+  Exposed-Modules:  Control.CFLP+  Other-Modules:    Control.Monad.Constraint,+                    Control.Monad.Constraint.Choice,+                    Data.LazyNondet,+                    Data.LazyNondet.Bool,+                    Data.LazyNondet.List,+                    Control.CFLP.Tests,+                    Control.CFLP.Tests.CallTimeChoice+  Hs-Source-Dirs:   src+  Extensions:       ExistentialQuantification,+                    MultiParamTypeClasses,+                    FlexibleInstances,+                    FlexibleContexts,+                    TypeFamilies,+                    RankNTypes++Source-Repository head+  type:     git+  location: git://github.com/sebfisch/cflp.git+
+ src/Control/CFLP.lhs view
@@ -0,0 +1,93 @@+% Constraint Functional-Logic Programming+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides an interface that can be used for constraint+functional-logic programming in Haskell.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts,+>       RankNTypes+>   #-}+>+> module Control.CFLP (+>+>   CFLP, EvalStore, eval, evalPrint,+>+>   Strategy, depthFirst,+>+>   module Data.LazyNondet,+>   module Data.LazyNondet.Bool,+>   module Data.LazyNondet.List+>+> ) where+>+> import Data.LazyNondet+> import Data.LazyNondet.Bool+> import Data.LazyNondet.List+>+> import Control.Monad.State+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> class (MonadConstr Choice m,+>        ConstraintStore Choice cs,+>        MonadSolve cs m m)+>  => CFLP cs m++The type class `CFLP` is a shortcut for the type-class constraints on+constraint functional-logic operations.++> instance CFLP ChoiceStore (ConstrT ChoiceStore [])++We declare instances for every combination of monad and constraint+store that we intend to use.++> type EvalStore = ChoiceStore+>+> noConstraints :: EvalStore+> noConstraints = noChoices++Currently, the constraint store used to evaluate constraint+functional-logic programs is simply a `ChoiceStore`. It will be a+combination of different constraint stores, when more constraint+solvers have been implemented.++> type Strategy m = forall a . m a -> [a]++A `Strategy` specifies how to enumerate non-deterministic results in a+list.++> depthFirst :: Strategy []+> depthFirst = id++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+>   i <- initID+>   return (enumerate (normalForm (op noConstraints i) noConstraints))++The `eval` 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)+>           -> IO ()+> evalPrint s op = eval s op >>= printSols+>+> printSols :: Show a => [a] -> IO ()+> printSols []     = putStrLn "No more solutions."+> printSols (x:xs) = do+>   print x+>   putStr "more? [Y|n]: "+>   s <- getLine+>   if s `elem` ["n","no"] then return () else printSols xs++For convenience, we provide an `evalPrint` operation that+interactively shows solutions of a constraint functional-logic+computation.+
+ src/Control/CFLP/Tests.lhs view
@@ -0,0 +1,40 @@+% Testing the `cflp` Package+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module defines auxiiary functions for the test suite.++> module Control.CFLP.Tests where+>+> import Control.CFLP+> import Control.Monad.Constraint+> import Test.HUnit++We use HUnit for testing because we need to test IO actions and want+to use errors when testing laziness.++> assertResults :: (Data a, Show a, Eq a)+>               => (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)+>               -> [a] -> Assertion+> assertResults = assertResultsLimit Nothing+>+> assertResultsN +>   :: (Data a, Show a, Eq a)+>   => Int+>   -> (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)+>   -> [a] -> Assertion+> assertResultsN = assertResultsLimit . Just+>+> assertResultsLimit +>   :: (Data a, Show a, Eq a)+>   => Maybe Int+>   -> (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)+>   -> [a] -> Assertion+> assertResultsLimit limit op expected = do+>   actual <- eval depthFirst op+>   maybe id take limit actual @?= expected++We provide auxiliary assertions `assertResults...` that compute (a+possibly limited number of) non-deterministic results of a functional+logic computation in depth-first order and compare them with a list of+given expected results.+
+ src/Control/CFLP/Tests/CallTimeChoice.lhs view
@@ -0,0 +1,83 @@+% Testing Call-Time Choice of Functional-Logic Operations+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module defines tests that specify the intended behaviour of+functional-logic programs w.r.t. laziness and sharing. Although+non-deterministic computations must be executed on demand, their+results have to be as if they were executed eagerly.++> module Control.CFLP.Tests.CallTimeChoice where+>+> import Control.CFLP+> import Control.CFLP.Tests+> import Test.HUnit+>+> import Control.CFLP+> import Control.Monad.Constraint+>+> import Prelude hiding ( not, null, head )+>+> 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+>  ]++Every module under `Control.CFLP.Tests` defines a constant `tests`+that collects all defined tests.++> ignoreFirstNarrowSecond :: Assertion+> ignoreFirstNarrowSecond = assertResults comp [True,False]+>  where+>   comp cs u = ignot (error "illegal demand") (unknown u) cs+>+> ignot :: CFLP cs m => Nondet m a -> Nondet m Bool -> cs -> Nondet m Bool+> ignot _ x = not x++This test checks a function with two arguments, where the first must+be ignored. Any changes in the translation scheme must not lead to+demand on the first argument of `ignot`. I have no better idea to+check demand than with using `error`. So an *error* is considered a+*failure* in this test case.++> sharedVarsAreEqual :: Assertion+> sharedVarsAreEqual = assertResults comp [[False,False],[True,True]]+>  where+>   comp _ u = two (unknown u)+>+> two :: Monad m => Nondet m a -> Nondet m [a]+> two x = x ^: x ^: nil++This test checks call-time choice semantics: variables represent+identical ground values. The elements of the constructed list must be+equal although they are computed from a free variable. ++In the current translation scheme sharing is implicit (we have no+special combinator to express sharing but use Haskell's sharing+directly). In case we introduce such a combinator, the following tests+are interesting.++> noDemandOnSharedVar :: Assertion+> noDemandOnSharedVar = assertResults comp [False]+>  where+>   comp cs _ = null (two (error "illegal demand")) 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+something that is shared.++> sharedCompoundTerms :: Assertion+> sharedCompoundTerms = assertResults comp [[True,False],[False,True]]+>  where+>   comp cs u = negHeads (unknown u) cs+>+> negHeads :: CFLP cs m => Nondet m [Bool] -> cs -> Nondet 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+terms even if they are consumed. In this example, the variable `l` is+shared, so the heads that are computed twice must be equal and the+negated head must be different from the head.+
+ src/Control/Monad/Constraint.lhs view
@@ -0,0 +1,171 @@+% Constraint Collecting Monads+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++We define type classes and instances for monads that can collect+constraints. 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.++> {-# LANGUAGE +>       MultiParamTypeClasses,+>       FlexibleInstances,+>       ExistentialQuantification+>   #-}+>+> module Control.Monad.Constraint (+>+>   -- type classes+>   ConstraintStore(..), MonadConstr(..), MonadSolve(..),+>+>   -- monad transformer+>   ConstrT+>+> ) where+> +> import Control.Monad+> import Control.Monad.State+> import Control.Monad.Trans+>+> class ConstraintStore c cs+>  where+>   assert :: (MonadState cs m, MonadPlus m) => c -> m ()++Constraint Stores provide an operation to assert a constraint into a+store. The constraint store is manipulated in an instance of+`MonadState`. The `assert` operation may fail or branch depending on+the given constraint or the current store and is, hence, performed in+an instance of `MonadPlus`.++A constraint store may support different types of constraints and a+constraint may be supported by different constraint stores.++> class MonadPlus m => MonadConstr c m+>  where+>   constr :: c -> m ()++A monad that supports collecting constraints is an instance of the+class `MonadConstr` that provides an operation to associate a+constraint of type `c` to monadic computations. One monad may support+different types of constraints and the same constraint type may be+supported by different monads.++> instance (MonadPlus m, ConstraintStore c cs) => MonadConstr c (StateT cs m)+>  where+>   constr = assert++An instance of `MonadPlus` that threads a constraint store can be+constrained with constraints that are supported by the threaded store.++> class (MonadPlus m, MonadPlus m') => MonadSolve cs m m'+>  where+>   solve :: m a -> StateT cs m' a++We also define an interface for monads that can solve associated+constraints by threading a constraint store through a (possibly, but+not necessarily different) monad.++We use the state monad transformer `StateT` to thread the constraint+store through the monad that returns the results.++> instance MonadPlus m => MonadSolve cs (StateT cs m) m+>  where+>   solve = id++Again, a state threading monad gives rise to a natural instance, where+results are returned in the base monad.++State monads are a natural choice for a constraint monad, 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 `ConstrT` that adds the capability of+collecting and solving constraints 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 ConstrT cs m a = ConstrT { unConstrT :: m (WithConstr cs m a) }+> data WithConstr cs m a+>   = Return a+>   | forall c . ConstraintStore c cs => Constr c (ConstrT cs m a)++The type `c` of collected constraints is existentially quantified in+order to allow different types of constraints in the same monadic+action. All types of constraints that are collected in a monadic+action need to be supported by the constraint store of type `cs`.++> instance (MonadPlus m, ConstraintStore c cs) => MonadConstr c (ConstrT cs m)+>  where+>   constr c = ConstrT (return (Constr c (return ())))++A transformed instance of `MonadPlus` is an instance of `MonadConstr`.++> instance MonadPlus m => MonadSolve cs (ConstrT cs m) m+>  where+>   solve = run+>    where+>     run :: MonadPlus m => ConstrT cs m a -> StateT cs m a+>     run x = lift (unConstrT x) >>= constrain+>+>     constrain (Return a)   = return a+>     constrain (Constr c y) = do constr c; run y++It is also an instance of `MonadSolve` where results are returned in+the base monad. In order to eliminate stored constraints, we thread a+constraint store through the monadic value and assert the associated+constraints into the store.++> instance MonadPlus m => MonadSolve cs (ConstrT cs m) (ConstrT cs m)+>  where+>   solve = run+>    where+>     run :: MonadPlus m => ConstrT cs m a -> StateT cs (ConstrT cs m) a+>     run x = lift (lift (unConstrT x)) >>= constrain+>+>     constrain (Return a)   = return a+>     constrain (Constr c y) = do lift (constr c); constr c; run y++We define another instance of `MonadSolve` 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 constraint store. All constraints are kept in+the monadic values and threaded additionally.++> instance Monad m => Monad (ConstrT cs m)+>  where+>   return = ConstrT . return . Return+>+>   x >>= f = ConstrT (unConstrT x >>= g)+>    where g (Return a)   = unConstrT (f a)+>          g (Constr c y) = return (Constr c (y >>= f))+>+> instance MonadPlus m => MonadPlus (ConstrT cs m)+>  where+>   mzero       = ConstrT mzero+>   x `mplus` y = ConstrT (unConstrT x `mplus` unConstrT y)+>+> instance MonadTrans (ConstrT cs)+>  where+>   lift x = ConstrT (x >>= return . 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, `ConstrT`+(with an arbitrary constraint store `cs`) is a monad transformer.++> instance Show a => Show (ConstrT cs [] a)+>  where+>   show (ConstrT x) = show x+>+> instance Show a => Show (WithConstr cs [] a)+>  where+>   show (Return x) = "(Return "++show x++")"+>   show (Constr _ (ConstrT x)) = "(Constr _ "++show x++")"++To simplify debugging, we define `Show` instances for transformed list+monads. Unfortunately, I don't know an easy way to show collected+constraints, because their type is not determined by the constraint+store and not mentioned in the signature of the instances.+
+ src/Control/Monad/Constraint/Choice.lhs view
@@ -0,0 +1,64 @@+% Sharing Choices with Constraints+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++We define a constraint store that stores choice constraints which+ensure that shared non-deterministic choices evaluate to the same+values when translating lazy functional logic programs.++Based on this constraint store, we provide a function `choice` that+can be used to generate choices that are constrained to evaluate to+the same value if they are shared.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts+>   #-}+>+> module Control.Monad.Constraint.Choice (+>+>   Choice, ChoiceStore, noChoices, choice+>+> ) where+>+> import Control.Monad+> import Control.Monad.State+> import Control.Monad.Constraint+>+> import Unique+> import UniqSupply+> import UniqFM++We borrow unique identifiers from the package `ghc` which is hidden by+default.++> newtype Choice = Choice (Unique,Int)+> newtype ChoiceStore = ChoiceStore (UniqFM Int)+>+> noChoices :: ChoiceStore+> noChoices = ChoiceStore emptyUFM+>+> instance ConstraintStore Choice ChoiceStore+>  where+>   assert (Choice (u,x)) = do+>     ChoiceStore cs <- get+>     maybe (put (ChoiceStore (addToUFM_Directly cs u x)))+>           (guard . (x==))+>           (lookupUFM_Directly cs u)++Choices are labeled with a `Unique`, so we can store them in a+`UniqFM` making it an instance of `ConstraintStore`.++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)..]+>  where constrain n = (constr (Choice (u,n))>>)++The operation `choice` takes a unique label and a list of monadic+values that can be constrained with choice constraints. The result is+a single monadic action combining the alternatives with `mplus`. If it+occurs more than once in a bigger monadic action, the result is+constrained to take the same alternative everywhere when collecting+constraints.+
+ src/Data/LazyNondet.lhs view
@@ -0,0 +1,219 @@+% Lazy Non-Deterministic Data+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides a datatype with operations for lazy+non-deterministic programming.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleInstances,+>       FlexibleContexts,+>       TypeFamilies+>   #-}+>+> module Data.LazyNondet (+>+>   NormalForm, HeadNormalForm(..), mkHNF, Nondet(..),+>+>   ID, initID, WithUnique(..), +>+>   Unknown(..), failure, oneOf, caseOf,+>+>   Data, normalForm+>+> ) where+>+> import Data.Data+> import Data.Generics.Twins ( gmapAccumT )+>+> import Control.Monad+> import Control.Monad.State+> import Control.Monad.Trans+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> import Unique+> import UniqSupply+> import UniqFM++We borrow unique identifiers from the package `ghc` which is hidden by+default.++> 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.++> type ID = UniqSupply+>+> initID :: IO ID+> initID = mkSplitUniqSupply 'x'+>+> class WithUnique a+>  where+>   type Mon a :: * -> *+>   type Typ a+>+>   withUnique :: a -> ID -> Nondet (Mon a) (Typ a)+>+> instance WithUnique (Nondet m a)+>  where+>   type Mon (Nondet m a) = m+>   type Typ (Nondet m a) = a+>+>   withUnique = const+>+> instance WithUnique a => WithUnique (ID -> a)+>  where+>   type Mon (ID -> a) = Mon a+>   type Typ (ID -> a) = Typ a+>+>   withUnique f us = withUnique (f vs) ws+>    where (vs,ws) = splitUniqSupply us++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+once:++    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 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.++> caseOf :: (Monad m, MonadSolve cs m m)+>        => Nondet m a+>        -> (HeadNormalForm m -> cs -> Nondet m b)+>        -> cs -> Nondet m b+> caseOf x branch cs = Typed (do+>   (hnf,cs') <- runStateT (solve (untyped x)) cs+>   untyped (branch hnf cs'))++The `caseOf` operation is 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.++Converting Between Primitive and Non-Deterministic Data+-------------------------------------------------------++> prim :: Data a => NormalForm -> a+> prim (NormalForm con args) =+>   snd (gmapAccumT perkid args (fromConstr con))+>  where+>   perkid (t:ts) _ = (ts, prim t)+>+> generic :: Data a => a -> NormalForm+> generic x = NormalForm (toConstr x) (gmapQ generic x)+>+> hnf :: Monad m => NormalForm -> Untyped m+> hnf (NormalForm con args) = return (mkHNF con (map hnf args))+>+> nondet :: (Monad m, Data a) => a -> Nondet m a+> nondet = Typed . hnf . 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.++> 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.+
+ src/Data/LazyNondet/Bool.lhs view
@@ -0,0 +1,39 @@+% Lazy Non-Deterministic Bools+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides non-deterministic booleans.++> {-# LANGUAGE+>       MultiParamTypeClasses,+>       FlexibleContexts+>   #-}+>+> module Data.LazyNondet.Bool where+>+> import Data.Data+> import Data.LazyNondet+>+> import Control.Monad.Constraint+> import Control.Monad.Constraint.Choice+>+> true :: Monad m => Nondet m Bool+> true = Typed (return (mkHNF (toConstr True) []))+>+> false :: Monad m => Nondet m Bool+> false = Typed (return (mkHNF (toConstr 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 on `Bool`s:++> not :: MonadSolve cs m m => Nondet m Bool -> cs -> Nondet m Bool+> not x = +>   caseOf x $ \x' _ ->+>   case x' of+>     Cons _ 1 _ -> true+>     Cons _ 2 _ -> false
+ src/Data/LazyNondet/List.lhs view
@@ -0,0 +1,53 @@+% Lazy Non-Deterministic Lists+% Sebastian Fischer (sebf@informatik.uni-kiel.de)++This module provides non-deterministic lists.++> module Data.LazyNondet.List where+>+> import Data.Data+> import Data.LazyNondet+> import Data.LazyNondet.Bool+>+> import Control.Monad.Constraint+>+> nil :: Monad m => Nondet m [a]+> nil = Typed (return (mkHNF (toConstr ([]::[()])) []))+>+> infixr 5 ^:+> (^:) :: Monad m => Nondet m a -> Nondet m [a] -> Nondet m [a]+> x^:xs = Typed (return (mkHNF (toConstr [()]) [untyped x, untyped xs]))+>+> 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 $ \xs' _ ->+>   case xs' of+>     Cons _ 1 _ -> true+>     _ -> false+>+> head :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m a+> head l =+>   caseOf l $ \l' cs ->+>   case l' of+>     Cons _ 1 _ -> failure+>     Cons _ 2 [x',_] -> Typed x'+>+> tail :: MonadSolve cs m m => Nondet m [a] -> cs -> Nondet m [a]+> tail l =+>   caseOf l $ \l' cs ->+>   case l' of+>     Cons _ 1 _ -> failure+>     Cons _ 2 [_,xs'] -> Typed xs'