diff --git a/INSTALL b/INSTALL
--- a/INSTALL
+++ b/INSTALL
@@ -1,17 +1,16 @@
 # Installation Instructions
 
-## Installation with Cabal
-
-You can install the `cflp` package using Cabal as follows.
+You can install the `cflp` package 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.
+ 2. Run configure, build, test, and install.
 
-        > ./Setup.lhs configure --user
-        > ./Setup.lhs build
-        > ./Setup.lhs install
+        > runhaskell Setup.lhs configure --user
+        > runhaskell Setup.lhs build
+        > runhaskell Setup.lhs test
+        > runhaskell Setup.lhs install
 
diff --git a/README b/README
--- a/README
+++ b/README
@@ -2,9 +2,9 @@
 
 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.
+combinators might later 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
diff --git a/Test.lhs b/Test.lhs
new file mode 100644
--- /dev/null
+++ b/Test.lhs
@@ -0,0 +1,15 @@
+% Testing the `cflp` Package
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+% November, 2008
+
+This module is used in the hook that runs the tests for the `cflp`
+package.
+
+> import Test.HUnit
+> import Control.CFLP.Tests.CallTimeChoice as CTC
+>
+> main :: IO ()
+> main = do
+>  runTestTT $ test [CTC.tests]
+>  return ()
+
diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,12 +1,13 @@
 Name:          cflp
-Version:       0.0.2.1
+Version:       0.1
 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.
+               combinators might later 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
@@ -16,7 +17,7 @@
 Build-Type:    Custom
 Stability:     alpha
 
-Extra-Source-Files: README, INSTALL
+Extra-Source-Files: README, INSTALL, Test.lhs
 
 Library
   Build-Depends:    base >= 4, ghc, mtl, syb, HUnit
@@ -35,8 +36,8 @@
                     FlexibleContexts,
                     TypeFamilies,
                     RankNTypes
+  Ghc-Options:      -O2 -Wall -fno-warn-orphans
 
 Source-Repository head
   type:     git
   location: git://github.com/sebfisch/cflp.git
-
diff --git a/src/Control/CFLP.lhs b/src/Control/CFLP.lhs
--- a/src/Control/CFLP.lhs
+++ b/src/Control/CFLP.lhs
@@ -13,7 +13,7 @@
 >
 > module Control.CFLP (
 >
->   CFLP, EvalStore, eval, evalPrint,
+>   CFLP, Computation, eval, evalPrint,
 >
 >   Strategy, depthFirst,
 >
@@ -37,7 +37,9 @@
 >  => CFLP cs m
 
 The type class `CFLP` is a shortcut for the type-class constraints on
-constraint functional-logic operations.
+constraint functional-logic computations that are parameterized over a
+constraint store and a constraint monad. Hence, such computations can
+be executed with different constraint stores and search strategies.
 
 > instance CFLP ChoiceStore (ConstrT ChoiceStore [])
 
@@ -48,6 +50,8 @@
 >
 > noConstraints :: EvalStore
 > noConstraints = noChoices
+>
+> type Computation m a = EvalStore -> ID -> Nondet (ConstrT EvalStore m) a
 
 Currently, the constraint store used to evaluate constraint
 functional-logic programs is simply a `ChoiceStore`. It will be a
@@ -83,9 +87,13 @@
 > printSols []     = putStrLn "No more solutions."
 > printSols (x:xs) = do
 >   print x
->   putStr "more? [Y|n]: "
+>   putStr "more? [Y(es)|n(o)|a(ll)]: "
 >   s <- getLine
->   if s `elem` ["n","no"] then return () else printSols xs
+>   if s `elem` ["n","no"] then
+>     return ()
+>    else if s `elem` ["a","all"]
+>     then mapM_ print xs
+>     else printSols xs
 
 For convenience, we provide an `evalPrint` operation that
 interactively shows solutions of a constraint functional-logic
diff --git a/src/Control/CFLP/Tests.lhs b/src/Control/CFLP/Tests.lhs
--- a/src/Control/CFLP/Tests.lhs
+++ b/src/Control/CFLP/Tests.lhs
@@ -1,34 +1,26 @@
 % Testing the `cflp` Package
 % Sebastian Fischer (sebf@informatik.uni-kiel.de)
 
-This module defines auxiiary functions for the test suite.
+This module defines auxiliary 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
+>               => (Computation [] a) -> [a] -> Assertion
 > assertResults = assertResultsLimit Nothing
 >
-> assertResultsN 
->   :: (Data a, Show a, Eq a)
->   => Int
->   -> (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)
->   -> [a] -> Assertion
+> assertResultsN :: (Data a, Show a, Eq a)
+>                => Int -> (Computation [] a) -> [a] -> Assertion
 > assertResultsN = assertResultsLimit . Just
 >
-> assertResultsLimit 
->   :: (Data a, Show a, Eq a)
->   => Maybe Int
->   -> (EvalStore -> ID -> Nondet (ConstrT EvalStore []) a)
->   -> [a] -> Assertion
+> assertResultsLimit :: (Data a, Show a, Eq a)
+>                    => Maybe Int -> (Computation [] a) -> [a] -> Assertion
 > assertResultsLimit limit op expected = do
 >   actual <- eval depthFirst op
 >   maybe id take limit actual @?= expected
diff --git a/src/Control/CFLP/Tests/CallTimeChoice.lhs b/src/Control/CFLP/Tests/CallTimeChoice.lhs
--- a/src/Control/CFLP/Tests/CallTimeChoice.lhs
+++ b/src/Control/CFLP/Tests/CallTimeChoice.lhs
@@ -13,7 +13,6 @@
 > import Test.HUnit
 >
 > import Control.CFLP
-> import Control.Monad.Constraint
 >
 > import Prelude hiding ( not, null, head )
 >
diff --git a/src/Control/Monad/Constraint.lhs b/src/Control/Monad/Constraint.lhs
--- a/src/Control/Monad/Constraint.lhs
+++ b/src/Control/Monad/Constraint.lhs
@@ -22,7 +22,6 @@
 >
 > ) where
 > 
-> import Control.Monad
 > import Control.Monad.State
 > import Control.Monad.Trans
 >
diff --git a/src/Control/Monad/Constraint/Choice.lhs b/src/Control/Monad/Constraint/Choice.lhs
--- a/src/Control/Monad/Constraint/Choice.lhs
+++ b/src/Control/Monad/Constraint/Choice.lhs
@@ -21,12 +21,10 @@
 >
 > ) 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
diff --git a/src/Data/LazyNondet.lhs b/src/Data/LazyNondet.lhs
--- a/src/Data/LazyNondet.lhs
+++ b/src/Data/LazyNondet.lhs
@@ -5,36 +5,38 @@
 non-deterministic programming.
 
 > {-# LANGUAGE
+>       ExistentialQuantification,
 >       MultiParamTypeClasses,
 >       FlexibleInstances,
 >       FlexibleContexts,
->       TypeFamilies
+>       TypeFamilies,
+>       FunctionalDependencies
 >   #-}
 >
 > module Data.LazyNondet (
 >
 >   NormalForm, HeadNormalForm(..), mkHNF, Nondet(..),
 >
->   ID, initID, WithUnique(..), 
+>   ID, initID, withUnique,
 >
->   Unknown(..), failure, oneOf, caseOf,
+>   Unknown(..), failure, oneOf, withHNF, caseOf, caseOf_, Match,
 >
->   Data, normalForm
+>   Data, nondet, normalForm,
 >
+>   ConsRep(..), cons, match,
+>
+>   prim_eq
+>
 > ) 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.
@@ -75,32 +77,35 @@
 Non-deterministic computations need a supply of unique identifiers in
 order to constrain shared choices.
 
-> type ID = UniqSupply
+> newtype ID = ID UniqSupply
 >
 > initID :: IO ID
-> initID = mkSplitUniqSupply 'x'
+> initID = liftM ID $ mkSplitUniqSupply 'x'
 >
-> class WithUnique a
+> class With x a
 >  where
->   type Mon a :: * -> *
->   type Typ a
+>   type Mon x a :: * -> *
+>   type Typ x a
 >
->   withUnique :: a -> ID -> Nondet (Mon a) (Typ a)
+>   with :: a -> x -> Nondet (Mon x a) (Typ x a)
 >
-> instance WithUnique (Nondet m a)
+> instance With x (Nondet m a)
 >  where
->   type Mon (Nondet m a) = m
->   type Typ (Nondet m a) = a
+>   type Mon x (Nondet m a) = m
+>   type Typ x (Nondet m a) = a
 >
->   withUnique = const
+>   with = const
 >
-> instance WithUnique a => WithUnique (ID -> a)
+> instance With ID a => With ID (ID -> a)
 >  where
->   type Mon (ID -> a) = Mon a
->   type Typ (ID -> a) = Typ a
+>   type Mon ID (ID -> a) = Mon ID a
+>   type Typ ID (ID -> a) = Typ ID a
 >
->   withUnique f us = withUnique (f vs) ws
+>   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
@@ -108,7 +113,7 @@
 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:
+the same time:
 
     Nondet m a -> ID -> Nondet m a
     (ID -> Nondet m a) -> ID -> Nondet m a
@@ -131,7 +136,7 @@
 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))
+> 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
@@ -143,21 +148,92 @@
 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
+> 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 (branch hnf cs'))
+>   untyped (b hnf cs'))
 
-The `caseOf` operation is used for pattern matching and solves
+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
 -------------------------------------------------------
 
@@ -165,16 +241,16 @@
 > prim (NormalForm con args) =
 >   snd (gmapAccumT perkid args (fromConstr con))
 >  where
->   perkid (t:ts) _ = (ts, prim t)
+>   perkid ts _ = (tail ts, prim (head ts))
 >
 > 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))
+> 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 . hnf . generic
+> nondet = Typed . nf2hnf . generic
 
 We provide generic operations to convert between instances of the
 `Data` class and non-deterministic data.
@@ -192,6 +268,77 @@
 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
diff --git a/src/Data/LazyNondet/Bool.lhs b/src/Data/LazyNondet/Bool.lhs
--- a/src/Data/LazyNondet/Bool.lhs
+++ b/src/Data/LazyNondet/Bool.lhs
@@ -3,24 +3,27 @@
 
 This module provides non-deterministic booleans.
 
-> {-# LANGUAGE
->       MultiParamTypeClasses,
->       FlexibleContexts
->   #-}
->
 > module Data.LazyNondet.Bool where
 >
 > import Data.Data
 > import Data.LazyNondet
 >
+> import Control.Monad.State
 > import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
 >
+> instance ConsRep Bool where consRep = toConstr
+>
 > true :: Monad m => Nondet m Bool
-> true = Typed (return (mkHNF (toConstr True) []))
+> true = cons True
 >
+> pTrue :: (cs -> Nondet m a) -> Match cs m a
+> pTrue = match True
+>
 > false :: Monad m => Nondet m Bool
-> false = Typed (return (mkHNF (toConstr False) []))
+> 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`.
@@ -29,11 +32,12 @@
 >  where
 >   unknown = oneOf [false,true]
 
-Some operations on `Bool`s:
+Some operations with `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
+> 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
diff --git a/src/Data/LazyNondet/List.lhs b/src/Data/LazyNondet/List.lhs
--- a/src/Data/LazyNondet/List.lhs
+++ b/src/Data/LazyNondet/List.lhs
@@ -3,6 +3,10 @@
 
 This module provides non-deterministic lists.
 
+> {-# LANGUAGE
+>       FlexibleInstances
+>   #-}
+>
 > module Data.LazyNondet.List where
 >
 > import Data.Data
@@ -11,13 +15,21 @@
 >
 > import Control.Monad.Constraint
 >
+> instance ConsRep [()] where consRep = toConstr
+>
 > nil :: Monad m => Nondet m [a]
-> nil = Typed (return (mkHNF (toConstr ([]::[()])) []))
+> 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]
-> x^:xs = Typed (return (mkHNF (toConstr [()]) [untyped x, untyped xs]))
+> (^:) = 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
 
@@ -32,22 +44,11 @@
 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
+> null xs = caseOf_ xs [pNil (\_ -> 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'
+> head l = caseOf l [pCons (\_ x _ -> 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'
+> tail l = caseOf l [pCons (\_ _ xs -> xs)]
+