diff --git a/INSTALL b/INSTALL
new file mode 100644
--- /dev/null
+++ b/INSTALL
@@ -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
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
+
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -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
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -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
+
+
diff --git a/cflp.cabal b/cflp.cabal
new file mode 100644
--- /dev/null
+++ b/cflp.cabal
@@ -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
+
diff --git a/src/Control/CFLP.lhs b/src/Control/CFLP.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/CFLP.lhs
@@ -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.
+
diff --git a/src/Control/CFLP/Tests.lhs b/src/Control/CFLP/Tests.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/CFLP/Tests.lhs
@@ -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.
+
diff --git a/src/Control/CFLP/Tests/CallTimeChoice.lhs b/src/Control/CFLP/Tests/CallTimeChoice.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/CFLP/Tests/CallTimeChoice.lhs
@@ -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.
+
diff --git a/src/Control/Monad/Constraint.lhs b/src/Control/Monad/Constraint.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Constraint.lhs
@@ -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.
+
diff --git a/src/Control/Monad/Constraint/Choice.lhs b/src/Control/Monad/Constraint/Choice.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Constraint/Choice.lhs
@@ -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.
+
diff --git a/src/Data/LazyNondet.lhs b/src/Data/LazyNondet.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet.lhs
@@ -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.
+
diff --git a/src/Data/LazyNondet/Bool.lhs b/src/Data/LazyNondet/Bool.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/Bool.lhs
@@ -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
diff --git a/src/Data/LazyNondet/List.lhs b/src/Data/LazyNondet/List.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/List.lhs
@@ -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'