diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+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.
+
+The names of its contributors may not 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 COPYRIGHT OWNER 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/Language/CP/ComposableTransformers.hs b/Language/CP/ComposableTransformers.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/ComposableTransformers.hs
@@ -0,0 +1,274 @@
+{- 
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Language.CP.ComposableTransformers where 
+
+import Language.CP.Transformers
+import Language.CP.SearchTree
+import Language.CP.Solver
+import Language.CP.Queue
+
+import System.Random (mkStdGen, randoms)
+
+--------------------------------------------------------------------------------
+-- EVALUATION
+--------------------------------------------------------------------------------
+
+solve :: (Queue q, Solver solver, CTransformer c, CForSolver c ~ solver,
+          Elem q ~ (Label solver,Tree solver (CForResult c),CTreeState c)) 
+      => q -> c -> Tree solver (CForResult c) -> (Int,[CForResult c])
+solve q c model = runSM $ eval model q (TStack c)
+
+--------------------------------------------------------------------------------
+-- COMPOSABLE TRANSFORMERS
+--------------------------------------------------------------------------------
+
+data TStack es ts (solver :: * -> *) a where
+   TStack :: (CTransformer c, CForSolver c ~ solver, CForResult c ~ a) 
+          => c -> TStack (CEvalState c) (CTreeState c) solver a
+
+instance Solver solver => Transformer (TStack es ts solver a) where
+  type EvalState (TStack es ts solver a) = es
+  type TreeState (TStack es ts solver a) = ts
+  type ForSolver (TStack es ts solver a) = solver
+  type ForResult (TStack es ts solver a) = a
+  initT  (TStack c) _  = return $ initCT c
+  leftT  (TStack c) _  = leftCT c
+  rightT (TStack c) _  = rightCT c
+  nextT = nextTStack 
+  returnT i wl t@(TStack c) es = returnCT c es (\es' -> continue i wl t es') (\es' -> endT i wl t es')
+
+nextTStack :: 
+     (Solver solver, Queue q, Elem q ~ (Label solver,Tree solver a,ts))
+     => Int -> Tree solver a -> q -> (TStack es ts solver a) -> es -> ts -> solver (Int,[a])
+nextTStack i tree q t es ts =
+    case t of
+      TStack c ->
+        nextCT tree c es ts (\tree' es' ts' -> eval' i tree' q t es' ts') 
+                            (\es'       -> continue i q t es')
+			    (\es' -> endT i q t es')
+
+--------------------------------------------------------------------------------
+type CSearchSig c a =
+     (Solver (CForSolver c), CTransformer c) 
+     => Tree (CForSolver c) a -> c -> CEvalState c -> CTreeState c -> (EVAL c a) -> (CONTINUE c a) -> (EXIT c a) -> (CForSolver c) (Int,[a])
+
+type CContinueSig c a =
+     (Solver (CForSolver c), CTransformer c) 
+     => c -> CEvalState c -> (CONTINUE c a) -> (EXIT c a) -> (CForSolver c) (Int,[a])
+
+type EVAL     c a = (Tree (CForSolver c) a -> CEvalState c -> CTreeState c-> (CForSolver c) (Int,[a]))
+type CONTINUE c a = (CEvalState c -> (CForSolver c) (Int,[a]))
+type EXIT     c a = (CEvalState c) -> (CForSolver c) (Int,[a]) 
+
+class Solver (CForSolver c) => CTransformer c where
+  type CEvalState c :: *
+  type CTreeState c :: *
+  type CForSolver c :: (* -> *)
+  type CForResult c :: *
+  initCT :: c -> (CEvalState c, CTreeState c)
+  leftCT, rightCT :: c -> CTreeState c -> CTreeState c
+  leftCT  _  = id
+  rightCT    = leftCT
+  nextCT :: CSearchSig c (CForResult c)
+  nextCT   = evalCT
+  returnCT :: CContinueSig c (CForResult c) 
+  returnCT = continueCT
+  completeCT :: c -> CEvalState c -> Bool
+  completeCT _ _ = True
+
+evalCT :: CSearchSig c a
+evalCT tree c es ts eval continue exit =
+  eval tree es ts
+
+continueCT :: CContinueSig c a
+continueCT c es continue exit =
+  continue es
+
+exitCT :: CContinueSig c a
+exitCT c es continue exit =
+  exit es
+
+newtype CNodeBoundedST (solver :: * -> *) a = CNBST Int
+
+instance Solver solver => CTransformer (CNodeBoundedST solver a) where
+  type CEvalState (CNodeBoundedST solver a) = Int
+  type CTreeState (CNodeBoundedST solver a) = ()
+  type CForSolver (CNodeBoundedST solver a) = solver
+  type CForResult (CNodeBoundedST solver a) = a
+  initCT (CNBST n)  = (n,())  
+  nextCT tree c es ts eval' continue exit
+    | es == 0    = exit es
+    | otherwise  = eval' tree (es - 1) ts
+
+newtype CDepthBoundedST (solver :: * -> *) a = CDBST Int
+
+instance Solver solver => CTransformer (CDepthBoundedST solver a) where
+  type CEvalState (CDepthBoundedST solver a)  = Bool
+  type CTreeState (CDepthBoundedST solver a)  = Int
+  type CForSolver (CDepthBoundedST solver a)  = solver
+  type CForResult (CDepthBoundedST solver a)  = a
+  initCT (CDBST n)  = (True,n)
+  leftCT _ ts      = ts - 1
+  nextCT tree c es ts eval' continue exit
+    | ts == 0    = continue False
+    | otherwise  = eval' tree es ts
+  completeCT _ es  = es
+
+newtype CLimitedDiscrepancyST (solver :: * -> *) a = CLDST Int
+
+instance Solver solver => CTransformer (CLimitedDiscrepancyST solver a) where
+  type CEvalState (CLimitedDiscrepancyST solver a) = ()
+  type CTreeState (CLimitedDiscrepancyST solver a) = Int
+  type CForSolver (CLimitedDiscrepancyST solver a) = solver
+  type CForResult (CLimitedDiscrepancyST solver a) = a
+  initCT (CLDST n)  = ((),n)
+  rightCT _ n  = n - 1
+  nextCT tree c es ts eval' continue exit
+    | ts == 0    = continue es
+    | otherwise  = eval' tree es ts
+
+newtype CRandomST (solver :: * -> *) a  = CRST Int
+
+instance Solver solver => CTransformer (CRandomST solver a) where
+  type CEvalState (CRandomST solver a) = [Bool]
+  type CTreeState (CRandomST solver a) = ()
+  type CForSolver (CRandomST solver a) = solver
+  type CForResult (CRandomST solver a) = a
+  initCT (CRST n)  = (randoms $ mkStdGen n,())
+  nextCT tree@(Try l r) c (switch:es)
+    | switch        = evalCT (Try r l) c es
+    | otherwise     = evalCT tree      c es
+  nextCT tree@(Add d (Try l r)) c (switch:es)
+    | switch        = evalCT (Add d (Try r l)) c es
+    | otherwise     = evalCT tree      c es
+  nextCT tree c es  = evalCT tree      c es
+
+data CIdentityCST (solver :: * -> *) a  = CIST
+
+instance Solver solver => CTransformer (CIdentityCST solver a) where
+  type CEvalState (CIdentityCST solver a)  = ()
+  type CTreeState (CIdentityCST solver a)  = ()
+  type CForSolver (CIdentityCST solver a)  = solver
+  type CForResult (CIdentityCST solver a)  = a
+  initCT _  = ((),())
+
+data CFirstSolutionST (solver :: * -> *) a  = CFSST
+
+instance Solver solver => CTransformer (CFirstSolutionST solver a) where
+  type CEvalState (CFirstSolutionST solver a)  = Bool
+  type CTreeState (CFirstSolutionST solver a)  = ()
+  type CForSolver (CFirstSolutionST solver a)  = solver
+  type CForResult (CFirstSolutionST solver a)  = a
+  initCT _  = (True,())
+  returnCT _ es continue exit =
+    exit False
+  completeCT _ es = es 
+
+
+--------------------------------------------------------------------------------
+data Composition es ts solver a where
+  (:-) :: (CTransformer c1, CTransformer c2,
+           CForSolver c1 ~ solver, CForSolver c2 ~ solver,
+           CForResult c1 ~ a,      CForResult c2 ~ a
+          ) 
+       => c1 -> c2 -> Composition (CEvalState c1,CEvalState c2) (CTreeState c1,CTreeState c2) solver a
+
+instance Solver solver => CTransformer (Composition es ts solver a) where
+  type CEvalState (Composition es ts solver a) = es
+  type CTreeState (Composition es ts solver a) = ts
+  type CForSolver (Composition es ts solver a) = solver
+  type CForResult (Composition es ts solver a) = a
+  initCT (c1 :- c2)       = let (es1,ts1) = initCT c1 
+                                (es2,ts2) = initCT c2 
+                            in ((es1,es2),(ts1,ts2))
+  leftCT (c1 :- c2) (ts1,ts2)   = (leftCT c1 ts1,leftCT c2 ts2)
+  rightCT (c1 :- c2) (ts1,ts2)  = (rightCT c1 ts1,rightCT c2 ts2)
+  nextCT tree (c1 :- c2) (es1,es2) (ts1,ts2) eval' continue exit  =
+    nextCT tree c1 es1 ts1 
+           (\tree' es1' ts1' -> nextCT tree' c2 es2 ts2 
+                                   (\tree'' es2' ts2' -> eval' tree'' (es1',es2') (ts1',ts2'))
+                                   (\es2' -> continue (es1',es2'))
+				   (\es2' -> exit (es1',es2')) ) 
+           (\es1' -> continue (es1',es2))
+           (\es1' -> exit (es1',es2))
+  returnCT (c1 :- c2) (es1,es2) continue exit =
+    returnCT c1 es1 (\es1' -> returnCT c2 es2 (\es2' -> continue (es1',es2')) (\es2' -> exit (es1',es2'))) 
+		    (\es1' -> exit (es1',es2))
+  completeCT (c1 :- c2) (es1,es2)  = completeCT c1 es1 && completeCT c2 es2
+
+--------------------------------------------------------------------------------
+-- BRANCH & BOUND
+--------------------------------------------------------------------------------
+
+newtype CBranchBoundST (solver :: * -> *) a = CBBST (NewBound solver) 
+data    BBEvalState solver  = BBP Int (Bound solver)
+
+type Bound    solver  = forall a. Tree solver a -> Tree solver a
+type NewBound solver  = solver (Bound solver)
+
+instance Solver solver => CTransformer (CBranchBoundST solver a) where
+  type CEvalState (CBranchBoundST solver a) = BBEvalState solver
+  type CTreeState (CBranchBoundST solver a) = Int
+  type CForSolver (CBranchBoundST solver a) = solver
+  type CForResult (CBranchBoundST solver a) = a
+  initCT _  = (BBP 0 id,0)
+  nextCT tree c es@(BBP nv bound) v eval continue exit
+    | nv > v        = eval (bound tree) es nv
+    | otherwise     = eval tree         es v
+  returnCT (CBBST newBound) (BBP v bound) continue exit =
+    do bound' <- newBound
+       continue $ BBP (v + 1) bound' 
+
+--------------------------------------------------------------------------------
+-- RESTARTING
+--------------------------------------------------------------------------------
+
+data SealedCST es ts solver a where
+  Seal :: CTransformer c => c -> SealedCST (CEvalState c) (CTreeState c) (CForSolver c) (CForResult c)
+
+instance Solver solver => CTransformer (SealedCST es ts solver a) where
+  type CEvalState (SealedCST es ts solver a) = es
+  type CTreeState (SealedCST es ts solver a) = ts
+  type CForSolver (SealedCST es ts solver a) = solver
+  type CForResult (SealedCST es ts solver a) = a
+  leftCT (Seal c) 	= leftCT c
+  rightCT (Seal c)	= rightCT c
+  initCT (Seal c)       = initCT c
+  nextCT tree (Seal c)  = nextCT tree c
+  returnCT (Seal c)     = returnCT c
+  completeCT (Seal c)   = completeCT c
+
+data RestartST es ts (solver :: * -> *) a = RestartST [SealedCST es ts solver a] (Tree solver a -> solver (Tree solver a))
+
+instance Solver solver => Transformer (RestartST es ts solver a) where
+  type EvalState (RestartST es ts solver a) = (SealedCST es ts solver a,[SealedCST es ts solver a],es,Label solver,Tree solver a)
+  type TreeState (RestartST es ts solver a) = ts
+  type ForSolver (RestartST es ts solver a) = solver
+  type ForResult (RestartST es ts solver a) = a
+  initT  (RestartST (c:cs) _) tree  = 
+ 	let (es,ts) = initCT c
+        in do l <-  markSM
+	      return ((c,cs,es,l,tree),ts)
+  leftT  _ (c,_,_,_,_)      = leftCT c
+  rightT _ (c,_,_,_,_)      = rightCT c
+  nextT i tree q t es@(c,cs,es_c,l,tree0) ts = 
+        nextCT tree c es_c ts (\tree' es_c' ts' -> eval' i tree' q t (c,cs,es_c',l,tree0) ts') 
+                              (\es_c'       -> continue i q t (c,cs,es_c',l,tree0))
+			      (\es_c' -> endT i q t (c,cs,es_c',l,tree0))
+  returnT i wl t es@(c,cs,es_c,l,tree0)  = returnCT c es_c (\es_c' -> continue i wl t (c,cs,es_c',l,tree0)) (\es_c' -> endT i wl t (c,cs,es_c',l,tree0))
+  endT i wl t es@(_,[],_,_,_)      = return (i,[])
+  endT i wl t@(RestartST _ f) es@(c0,(c:cs),es_c0,l,tree0)   
+    | completeCT c0 es_c0  = return (i,[])
+    | otherwise            = let (es,ts) = initCT c
+                             in  do tree' <- f tree0
+                                    continue i (pushQ (l,tree',ts) $ emptyQ wl) t (c,cs,es,l,tree0)
+ 
diff --git a/Language/CP/Domain.hs b/Language/CP/Domain.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/Domain.hs
@@ -0,0 +1,167 @@
+{- 
+ - Origin:
+ - 	Constraint Programming in Haskell 
+ - 	http://overtond.blogspot.com/2008/07/pre.html
+ - 	author: David Overton, Melbourne Australia
+ -
+ - Modifications:
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -} 
+
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE IncoherentInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Language.CP.Domain (
+    Domain,
+    ToDomain,
+    toDomain,
+    member,
+    isSubsetOf,
+    elems,
+    intersection,
+    difference,
+    union,
+    empty,
+    null,
+    singleton,
+    isSingleton,
+    filterLessThan,
+    filterGreaterThan,
+    findMax,
+    findMin,
+    size,
+    shiftDomain
+) where
+
+import qualified Data.IntSet as IntSet
+import Data.IntSet (IntSet)
+import Prelude hiding (null)
+
+data Domain
+    = Set IntSet
+    | Range Int Int
+    deriving Show
+
+size :: Domain -> Int
+size (Range l u) = u - l + 1
+size (Set set)   = IntSet.size set
+
+-- Domain constructors
+class ToDomain a where
+    toDomain :: a -> Domain
+
+instance ToDomain Domain where
+    toDomain = id
+
+instance ToDomain IntSet where
+    toDomain = Set
+
+instance Integral a => ToDomain [a] where
+    toDomain = toDomain . IntSet.fromList . map fromIntegral
+
+instance (Integral a, Integral b) => ToDomain (a, b) where
+    toDomain (a, b) = Range (fromIntegral a) (fromIntegral b)
+
+instance ToDomain () where
+    toDomain () = Range minBound maxBound
+
+instance Integral a => ToDomain a where
+    toDomain a = toDomain (a, a)
+
+-- Operations on Domains
+instance Eq Domain where
+    (Range xl xh) == (Range yl yh) = xl == yl && xh == yh
+    xs == ys = elems xs == elems ys
+
+member :: Int -> Domain -> Bool
+member n (Set xs) = n `IntSet.member` xs
+member n (Range xl xh) = n >= xl && n <= xh
+
+isSubsetOf :: Domain -> Domain -> Bool
+isSubsetOf (Set xs) (Set ys) = xs `IntSet.isSubsetOf` ys
+isSubsetOf (Range xl xh) (Range yl yh) = xl >= yl && xh <= yh
+isSubsetOf (Set xs) yd@(Range yl yh) =
+    isSubsetOf (Range xl xh) yd where
+        xl = IntSet.findMin xs
+        xh = IntSet.findMax xs
+isSubsetOf (Range xl xh) (Set ys) =
+    all (`IntSet.member` ys) [xl..xh]
+
+elems :: Domain -> [Int]
+elems (Set xs) = IntSet.elems xs
+elems (Range xl xh) = [xl..xh]
+
+intersection :: Domain -> Domain -> Domain
+intersection (Set xs) (Set ys) = Set (xs `IntSet.intersection` ys)
+intersection (Range xl xh) (Range yl yh) = Range (max xl yl) (min xh yh)
+intersection (Set xs) (Range yl yh) =
+    Set $ IntSet.filter (\x -> x >= yl && x <= yh) xs
+intersection x y = intersection y x
+
+union :: Domain -> Domain -> Domain
+union (Set xs) (Set ys) = Set (xs `IntSet.union` ys)
+union (Range xl xh) (Range yl yh) 
+      | xh + 1 >= yl || yh+1 >= xl = Range (min xl yl) (max xh yh)
+      | otherwise = union (Set $ IntSet.fromList [xl..xh]) 
+                          (Set $ IntSet.fromList [yl..yh]) 
+union x@(Set xs) y@(Range yl yh) =
+      if null x then y 
+      else
+      let xmin = IntSet.findMin xs
+          xmax = IntSet.findMax xs
+      in 
+      if (xmin + 1 >= yl && xmax - 1 <= yh) 
+         then Range (min xmin yl) (max xmax yh)
+         else union (Set xs) (Set $ IntSet.fromList [yl..yh])
+union x y = union y x
+
+difference :: Domain -> Domain -> Domain
+difference (Set xs) (Set ys) = Set (xs `IntSet.difference` ys)
+difference xd@(Range xl xh) (Range yl yh)
+    | yl > xh || yh < xl = xd
+    | otherwise = Set $ IntSet.fromList [x | x <- [xl..xh], x < yl || x > yh]
+difference (Set xs) (Range yl yh) =
+    Set $ IntSet.filter (\x -> x < yl || x > yh) xs
+difference (Range xl xh) (Set ys)
+    | IntSet.findMin ys > xh || IntSet.findMax ys < xl = Range xl xh
+    | otherwise = Set $
+        IntSet.fromList [x | x <- [xl..xh], not (x `IntSet.member` ys)]
+
+null :: Domain -> Bool
+null (Set xs) = IntSet.null xs
+null (Range xl xh) = xl > xh
+
+singleton :: Int -> Domain
+singleton x = Set (IntSet.singleton x)
+
+isSingleton :: Domain -> Bool
+isSingleton (Set xs) = case IntSet.elems xs of
+    [x] -> True
+    _   -> False
+isSingleton (Range xl xh) = xl == xh
+
+filterLessThan :: Int -> Domain -> Domain
+filterLessThan n (Set xs) = Set $ IntSet.filter (< n) xs
+filterLessThan n (Range xl xh) = Range xl (min (n-1) xh)
+
+filterGreaterThan :: Int -> Domain -> Domain
+filterGreaterThan n (Set xs) = Set $ IntSet.filter (> n) xs
+filterGreaterThan n (Range xl xh) = Range (max (n+1) xl) xh
+
+findMax :: Domain -> Int
+findMax (Set xs) = IntSet.findMax xs
+findMax (Range xl xh) = xh
+
+findMin :: Domain -> Int
+findMin (Set xs) = IntSet.findMin xs
+findMin (Range xl xh) = xl
+
+empty :: Domain
+empty = Range 1 0
+
+shiftDomain :: Domain -> Int -> Domain
+shiftDomain (Range l u) d = Range (l + d) (u + d)
+shiftDomain (Set xs) d = Set $ IntSet.fromList $ map (+d) (IntSet.elems xs)
diff --git a/Language/CP/FD.hs b/Language/CP/FD.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/FD.hs
@@ -0,0 +1,412 @@
+{- 
+ - Origin:
+ - 	Constraint Programming in Haskell 
+ - 	http://overtond.blogspot.com/2008/07/pre.html
+ - 	author: David Overton, Melbourne Australia
+ -
+ - Modifications:
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -} 
+
+{-# OPTIONS_GHC -fglasgow-exts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE OverlappingInstances #-}
+module Language.CP.FD where 
+
+import Prelude hiding (lookup)
+import Maybe (fromJust,isJust)
+import Control.Monad.State.Lazy
+import Control.Monad.Trans
+import qualified Data.Map as Map
+import Data.Map ((!), Map)
+import Control.Monad (liftM,(<=<))
+
+import Language.CP.Domain as Domain
+
+import Language.CP.Solver
+
+-- import Debug.Trace
+trace = flip const
+--------------------------------------------------------------------------------
+-- Solver instance -------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+instance Solver FD where
+  type Constraint FD  = FD_Constraint
+  type Term       FD  = FD_Term
+  type Label      FD  = FDState
+
+  newvarSM 	= newVar () >>= return . FD_Var 
+  addSM    	= addFD
+  storeSM  	= undefined
+  runSM p   	= runFD p
+
+  markSM	= get
+  gotoSM	= put 
+
+data FD_Term where
+  FD_Var :: FDVar -> FD_Term
+  deriving Show
+
+un_fd (FD_Var v) = v
+
+data FD_Constraint where
+  FD_Diff :: FD_Term -> FD_Term -> FD_Constraint
+  FD_Same :: FD_Term -> FD_Term -> FD_Constraint
+  FD_Less :: FD_Term  -> FD_Term -> FD_Constraint
+  FD_LT   :: FD_Term -> Int -> FD_Constraint
+  FD_GT   :: FD_Term -> Int -> FD_Constraint
+  FD_HasValue :: FD_Term -> Int -> FD_Constraint
+  FD_Eq   :: (ToExpr a, ToExpr b) => a -> b -> FD_Constraint
+  FD_NEq   :: (ToExpr a, ToExpr b) => a -> b -> FD_Constraint
+  FD_AllDiff :: [FD_Term] -> FD_Constraint
+  FD_Dom     :: FD_Term -> (Int,Int) -> FD_Constraint
+
+addFD (FD_Diff (FD_Var v1) (FD_Var v2)) = different v1 v2
+addFD (FD_Same (FD_Var v1) (FD_Var v2)) = same      v1 v2
+addFD (FD_Less (FD_Var v1) (FD_Var v2)) = v1 .<. v2     
+addFD (FD_HasValue (FD_Var v1) i)       = hasValue v1  i
+addFD (FD_Eq e1 e2)                     = e1 .==. e2
+addFD (FD_NEq e1 e2)                    = e1 ./=. e2 
+-- addFD (FD_AllDiff vs)                   = allDifferent (map un_fd vs)
+addFD (FD_Dom v (l,u))                  = v `in_range` (l-1,u+1)
+addFD (FD_LT (FD_Var v) i)              = do iv <- exprVar $ toExpr i
+                                             v .<. iv
+addFD (FD_GT (FD_Var v) i)              = do iv <- exprVar $ toExpr i
+                                             iv .<. v
+
+
+(#<) :: (To_FD_Term a, To_FD_Term b) => a -> b -> FD Bool
+x #< y =
+  do xt <- to_fd_term x
+     yt <- to_fd_term y
+     addFD (FD_Less xt yt)
+
+in_range :: FD_Term -> (Int,Int) -> FD Bool
+in_range x (l,u) =
+  do l #< x
+     x #< u
+
+all_different = addFD . FD_AllDiff
+
+instance ToExpr FD_Term where
+  toExpr (FD_Var v) = toExpr v
+
+fd_domain :: FD_Term -> FD [Int]
+fd_domain (FD_Var v)  = do d <- lookup v
+                           return $ elems d
+
+fd_objective :: FD FD_Term
+fd_objective =
+  do s <- get
+     return $ FD_Var $ objective s
+
+class To_FD_Term a where
+  to_fd_term :: a -> FD FD_Term
+
+instance To_FD_Term FD_Term where
+  to_fd_term = return . id
+
+instance To_FD_Term Int where
+  to_fd_term i =  newVar i >>= return . FD_Var
+
+instance To_FD_Term Expr  where
+  to_fd_term e = unExpr e >>= return . FD_Var
+
+--------------------------------------------------------------------------------
+
+-- The FD monad
+newtype FD a = FD { unFD :: StateT FDState Maybe a }
+    deriving (Monad, MonadState FDState, MonadPlus)
+
+-- FD variables
+newtype FDVar = FDVar { unFDVar :: Int } deriving (Ord, Eq, Show)
+
+type VarSupply = FDVar
+
+data VarInfo = VarInfo
+     { delayedConstraints :: FD Bool, domain :: Domain }
+
+instance Show VarInfo where
+  show x = show $ domain x
+
+type VarMap = Map FDVar VarInfo
+
+data FDState = FDState
+     { varSupply :: VarSupply, varMap :: VarMap, objective :: FDVar }
+     deriving Show
+
+instance Eq FDState where
+  s1 == s2 = f s1 == f s2
+           where f s = head $ elems $ domain $ varMap s ! (objective s) 
+
+instance Ord FDState where
+  compare s1 s2  = compare (f s1) (f s2)
+           where f s = head $ elems $  domain $ varMap s ! (objective s) 
+
+  -- TOM: inconsistency is not observable within the FD monad
+consistentFD :: FD Bool
+consistentFD = return True
+
+-- Run the FD monad and produce a lazy list of possible solutions.
+runFD :: FD a -> a
+runFD fd = fromJust $ evalStateT (unFD fd') initState
+           where fd' = fd -- fd' = newVar () >> fd
+
+initState :: FDState
+initState = FDState { varSupply = FDVar 0, varMap = Map.empty, objective = FDVar 0 }
+
+-- Get a new FDVar
+newVar :: ToDomain a => a -> FD FDVar
+newVar d = do
+    s <- get
+    let v = varSupply s
+    put $ s { varSupply = FDVar (unFDVar v + 1) }
+    modify $ \s ->
+        let vm = varMap s
+            vi = VarInfo {
+                delayedConstraints = return True,
+                domain = toDomain d}
+        in
+        s { varMap = Map.insert v vi vm }
+    return v
+
+newVars :: ToDomain a => Int -> a -> FD [FDVar]
+newVars n d = replicateM n (newVar d)
+
+-- Lookup the current domain of a variable.
+lookup :: FDVar -> FD Domain
+lookup x = do
+    s <- get
+    return . domain $ varMap s ! x
+
+-- Update the domain of a variable and fire all delayed constraints
+-- associated with that variable.
+update :: FDVar -> Domain -> FD Bool
+update x i = do
+    trace (show x ++ " <- " ++ show i)  (return ())
+    s <- get
+    let vm = varMap s
+    let vi = vm ! x
+    trace ("where old domain = " ++ show (domain vi)) (return ())
+    put $ s { varMap = Map.insert x (vi { domain = i}) vm }
+    delayedConstraints vi
+
+-- Add a new constraint for a variable to the constraint store.
+addConstraint :: FDVar -> FD Bool -> FD ()
+addConstraint x constraint = do
+    s <- get
+    let vm = varMap s
+    let vi = vm ! x
+    let cs = delayedConstraints vi
+    put $ s { varMap =
+        Map.insert x (vi { delayedConstraints = do b <- cs 
+                                                   if b then constraint
+                                                        else return False}) vm }
+ 
+-- Useful helper function for adding binary constraints between FDVars.
+type BinaryConstraint = FDVar -> FDVar -> FD Bool
+addBinaryConstraint :: BinaryConstraint -> BinaryConstraint 
+addBinaryConstraint f x y = do
+    let constraint  = f x y
+    b <- constraint 
+    when b $ (do addConstraint x constraint
+                 addConstraint y constraint)
+    return b
+
+-- Constrain a variable to a particular value.
+hasValue :: FDVar -> Int -> FD Bool
+var `hasValue` val = do
+    vals <- lookup var
+    if val `member` vals
+       then do let i = singleton val
+               if (i /= vals) 
+                  then update var i
+                  else return True
+       else return False
+
+-- Constrain two variables to have the same value.
+same :: FDVar -> FDVar -> FD Bool
+same = addBinaryConstraint $ \x y -> do
+    xv <- lookup x
+    yv <- lookup y
+    let i = xv `intersection` yv
+    if not $ Domain.null i
+       then whenwhen (i /= xv)  (i /= yv) (update x i) (update y i)
+       else return False
+
+whenwhen c1 c2 a1 a2  =
+  if c1
+     then do b1 <- a1
+             if b1 
+                then if c2
+                        then a2
+                        else return True
+                else return False 
+     else if c2
+             then a2
+             else return True
+
+-- Constrain two variables to have different values.
+different :: FDVar  -> FDVar  -> FD Bool
+different = addBinaryConstraint $ \x y -> do
+    xv <- lookup x
+    yv <- lookup y
+    if not (isSingleton xv) || not (isSingleton yv) || xv /= yv
+       then whenwhen (isSingleton xv && xv `isSubsetOf` yv)
+                     (isSingleton yv && yv `isSubsetOf` xv)
+                     (update y (yv `difference` xv))
+                     (update x (xv `difference` yv))
+       else return False
+
+-- Constrain a list of variables to all have different values.
+allDifferent :: [FDVar ] -> FD  ()
+allDifferent (x:xs) = do
+    mapM_ (different x) xs
+    allDifferent xs
+allDifferent _ = return ()
+
+-- Constrain one variable to have a value less than the value of another
+-- variable.
+infix 4 .<.
+(.<.) :: FDVar -> FDVar -> FD Bool
+(.<.) = addBinaryConstraint $ \x y -> do
+    xv <- lookup x
+    yv <- lookup y
+    let xv' = filterLessThan (findMax yv) xv
+    let yv' = filterGreaterThan (findMin xv) yv
+    if  not $ Domain.null xv'
+        then if not $ Domain.null yv'
+                then whenwhen (xv /= xv') (yv /= yv') (update x xv') (update y yv')
+	        else return False
+        else return False
+
+{-
+-- Get all solutions for a constraint without actually updating the
+-- constraint store.
+solutions :: FD s a -> FD s [a]
+solutions constraint = do
+    s <- get
+    return $ evalStateT (unFD constraint) s
+
+-- Label variables using a depth-first left-to-right search.
+labelling :: [FDVar s] -> FD s [Int]
+labelling = mapM label where
+    label var = do
+        vals <- lookup var
+        val <- FD . lift $ elems vals
+        var `hasValue` val
+        return val
+-}
+
+dump :: [FDVar] -> FD [Domain]
+dump = mapM lookup
+
+newtype Expr = Expr { unExpr :: FD (FDVar) }
+
+class ToExpr a where
+    toExpr :: a -> Expr
+
+instance ToExpr FDVar where
+    toExpr = Expr . return
+
+instance ToExpr Expr where
+    toExpr = id
+
+instance Integral i => ToExpr i where
+    toExpr n = Expr $ newVar n
+
+exprVar :: ToExpr a => a -> FD FDVar
+exprVar = unExpr . toExpr
+
+-- Add constraint (z = x `op` y) for new var z
+addArithmeticConstraint :: (ToExpr a, ToExpr b) =>
+    (Domain -> Domain -> Domain) ->
+    (Domain -> Domain -> Domain) ->
+    (Domain -> Domain -> Domain) ->
+    a -> b -> Expr
+addArithmeticConstraint getZDomain getXDomain getYDomain xexpr yexpr = Expr $ do
+    x <- exprVar xexpr
+    y <- exprVar yexpr
+    xv <- lookup x
+    yv <- lookup y
+    z <- newVar (getZDomain xv yv)
+    let constraint z x y getDomain = do
+        xv <- lookup x
+        yv <- lookup y
+        zv <- lookup z
+        let znew = zv `intersection` (getDomain xv yv)
+	trace (show z ++ " before: "  ++ show zv ++ show "; after: " ++ show znew) (return ())
+        if not $ Domain.null znew
+           then if (znew /= zv) 
+                   then update z znew
+                   else return True
+           else return False
+    let zConstraint = constraint z x y getZDomain
+        xConstraint = constraint x z y getXDomain
+        yConstraint = constraint y z x getYDomain
+    addConstraint z xConstraint
+    addConstraint z yConstraint
+    addConstraint x zConstraint
+    addConstraint x yConstraint
+    addConstraint y zConstraint
+    addConstraint y xConstraint
+    return z
+
+infixl 6 .+.
+(.+.) :: (ToExpr a, ToExpr b) => a -> b -> Expr
+(.+.) = addArithmeticConstraint getDomainPlus getDomainMinus getDomainMinus
+
+infixl 6 .-.
+(.-.) :: (ToExpr a, ToExpr b) => a -> b -> Expr
+(.-.) = addArithmeticConstraint getDomainMinus getDomainPlus
+    (flip getDomainMinus)
+
+infixl 7 .*.
+(.*.) :: (ToExpr a, ToExpr b) => a -> b -> Expr
+(.*.) = addArithmeticConstraint getDomainMult getDomainDiv getDomainDiv
+
+getDomainPlus :: Domain -> Domain -> Domain
+getDomainPlus xs ys = toDomain (zl, zh) where
+    zl = findMin xs + findMin ys
+    zh = findMax xs + findMax ys
+
+getDomainMinus :: Domain -> Domain -> Domain
+getDomainMinus xs ys = toDomain (zl, zh) where
+    zl = findMin xs - findMax ys
+    zh = findMax xs - findMin ys
+
+getDomainMult :: Domain -> Domain -> Domain
+getDomainMult xs ys = toDomain (zl, zh) where
+    zl = minimum products
+    zh = maximum products
+    products = [x * y |
+        x <- [findMin xs, findMax xs],
+        y <- [findMin ys, findMax ys]]
+
+getDomainDiv :: Domain -> Domain -> Domain
+getDomainDiv xs ys = toDomain (zl, zh) where
+    zl = minimum quotientsl
+    zh = maximum quotientsh
+    quotientsl = [if y /= 0 then x `div` y else minBound |
+        x <- [findMin xs, findMax xs],
+        y <- [findMin ys, findMax ys]]
+    quotientsh = [if y /= 0 then x `div` y else maxBound |
+        x <- [findMin xs, findMax xs],
+        y <- [findMin ys, findMax ys]]
+
+infix 4 .==.
+(.==.) :: (ToExpr a, ToExpr b) => a -> b -> FD Bool
+xexpr .==. yexpr = do
+    x <- exprVar xexpr
+    y <- exprVar yexpr
+    x `same` y
+
+infix 4 ./=.
+(./=.) :: (ToExpr a, ToExpr b) => a -> b -> FD Bool
+xexpr ./=. yexpr = do
+    x <- exprVar xexpr
+    y <- exprVar yexpr
+    x `different` y
diff --git a/Language/CP/FDSugar.hs b/Language/CP/FDSugar.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/FDSugar.hs
@@ -0,0 +1,129 @@
+{- 
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+{-# LANGUAGE TransformListComp #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Language.CP.FDSugar where 
+
+import Language.CP.SearchTree hiding (label)
+import Language.CP.Transformers
+import Language.CP.ComposableTransformers
+import Language.CP.Queue
+import Language.CP.Solver
+
+import GHC.Exts (sortWith)
+import qualified Language.CP.PriorityQueue as PriorityQueue
+import qualified Data.Sequence
+import Language.CP.FD
+
+dfs = []
+bfs = Data.Sequence.empty
+pfs :: Ord a => PriorityQueue.PriorityQueue a (a,b,c)
+pfs = PriorityQueue.empty
+
+nb :: Int -> CNodeBoundedST FD a
+nb = CNBST
+db :: Int -> CDepthBoundedST FD a
+db = CDBST
+bb :: NewBound FD -> CBranchBoundST FD a
+bb = CBBST
+fs :: CFirstSolutionST FD a
+fs = CFSST
+it :: CIdentityCST FD a
+it = CIST
+ra :: Int -> CRandomST FD a
+ra = CRST
+ld :: Int -> CLimitedDiscrepancyST FD a
+ld = CLDST
+
+newBound :: NewBound FD
+newBound = do obj <- fd_objective
+              (val:_) <- fd_domain obj 
+	      l <- markSM
+              return ((\tree -> tree `insertTree` (obj @< val)) :: forall b . Tree FD b -> Tree FD b)
+
+newBoundBis :: NewBound FD 
+newBoundBis = do obj <- fd_objective
+                 (val:_) <- fd_domain obj 
+                 let m = val `div` 2
+                 return ((\tree -> (obj @< (m + 1) \/ ( obj @> m /\ obj @< val)) /\ tree) :: forall b . Tree FD b -> Tree FD b)
+
+restart :: (Queue q, Solver solver, CTransformer c, CForSolver c ~ solver,
+          Elem q ~ (Label solver,Tree solver (CForResult c),CTreeState c)) 
+      => q -> [c] -> Tree solver (CForResult c) -> (Int,[CForResult c])
+restart q cs model = runSM $ eval model q (RestartST (map Seal cs) return)
+
+restartOpt :: (Queue q, CTransformer c, CForSolver c ~ FD,
+          Elem q ~ (Label FD,Tree FD (CForResult c),CTreeState c)) 
+      => q -> [c] -> Tree FD (CForResult c) -> (Int,[CForResult c])
+restartOpt q cs model = runSM $ eval model q (RestartST (map Seal cs) opt)
+	where opt tree = newBound >>= \f -> return (f tree)
+
+--------------------------------------------------------------------------------
+-- ENUMERATION
+--------------------------------------------------------------------------------
+
+enumerate = Label . (label in_order) 
+-- enumerate = Label . (label firstfail) 
+
+label sel qs  = do qs' <- sel qs 
+                   label' qs' 
+  where label' []      = return true
+        label' (q:qs)  = do d <- fd_domain q 
+--                            return $ enum q (middleout d) /\ enumerate qs
+                            return $ enum q d /\ enumerate qs
+
+in_order :: Monad m => a -> m a
+in_order = return 
+
+firstfail qs = do ds <- mapM fd_domain qs 
+                  return [ q | (d,q) <- zip ds qs 
+                             , then sortWith by (length d) ] 
+enum queen values = 
+  disj [ queen @= value 
+       | value <- values 
+       ] 
+
+value var = do [val] <- fd_domain var
+               return val
+
+middleout l = let n = (length l) `div` 2 in
+              interleave (drop n l) (reverse $ take n l)
+
+endsout  l = let n = (length l) `div` 2 in
+              interleave (reverse $ drop n l) (take n l)
+
+interleave []     ys = ys
+interleave (x:xs) ys = x:interleave ys xs
+--------------------------------------------------------------------------------
+-- RESULT
+--------------------------------------------------------------------------------
+
+assignments = mapM assignment 
+assignment q = Label $ value q >>= (return . Return)
+--------------------------------------------------------------------------------
+-- SYNTACTIC SUGAR
+--------------------------------------------------------------------------------
+
+in_domain v (l,u)  = Add (FD_Dom v (l,u)) true
+(@\=) :: FD_Term -> FD_Term -> Tree FD ()
+v1 @\= v2  = Add (FD_NEq v1 v2) true
+
+(@=) :: FD_Term -> Int -> Tree FD ()
+v1 @= v2  = Add (FD_Eq v1 v2) true
+
+data Plus  = FD_Term :+ Int 
+(@+) = (:+)
+
+(@\==) :: FD_Term -> Plus -> Tree FD ()
+v1 @\== (v2 :+ i)  = Add (FD_NEq v1 (v2 .+. i))  true
+
+(@<) :: FD_Term -> Int -> Tree FD ()
+v @< i  = Add (FD_LT v i) true
+
+(@>) :: FD_Term -> Int -> Tree FD ()
+v @> i  = Add (FD_GT v i) true
diff --git a/Language/CP/Main.hs b/Language/CP/Main.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/Main.hs
@@ -0,0 +1,90 @@
+{- 
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+module Language.CP.Main where
+
+import Language.CP.ComposableTransformers
+import Language.CP.FD
+import Language.CP.FDSugar
+import List (tails)
+import Language.CP.SearchTree hiding (label)
+import System (getArgs)
+
+--------------------------------------------------------------------------------
+-- MAIN FUNCTIONS
+--------------------------------------------------------------------------------
+
+main = main1
+
+
+main1 = getArgs >>= print . solve dfs it . nqueens . read . head
+main2 = getArgs >>= print . solve dfs (nb 100 :- db  25 :- bb newBound)  . nqueens . read . head
+
+main3 = getArgs >>= print . solve dfs (db 9) . nqueens . read . head
+
+main4 = do (n1:_) <- getArgs 
+           let n = read n1
+           loop 1 n
+  where loop i n
+          | i > n     = return ()
+          | otherwise =
+              do -- print . (\(i,l) -> (i,not $ Prelude.null l)) . solve dfs (it :- fs :- ra 13 :- ld l) . nqueens $ i
+                 print . (\(i,l) -> (i, {- not $ Prelude.null-}  l)) . restart dfs (map db [3..10]) . nqueens $ i
+                 -- print . (\(i,l) -> (i, {- not $ Prelude.null-}  l)) . restartOpt dfs (replicate 10 fs) . nqueens $ i
+                 loop (i+1) n
+
+main5 = getArgs >>= loop 1 . read . head
+  where loop i n
+          | i > n     = return ()
+          | otherwise =
+              do print . (\(i,l) -> (i,minimum l)) . solve dfs (ld 5 :- bb newBoundBis) . gmodel $ i
+                 loop (i+1) n
+
+--------------------------------------------------------------------------------
+-- PATH MODEL
+--------------------------------------------------------------------------------
+
+gmodel n = NewVar $ \_ -> path 1 n 0
+
+path :: Int -> Int -> Int -> Tree FD Int
+path x y d = if x == y 
+               then Return d
+               else disj [ Label (fd_objective >>= \o -> return (o @> (d+d' - 1) /\ (path z y (d+d')))) 
+                         | (z,d') <- edge x
+                         ]
+
+edge i | i < 20     = [ (i+1,4), (i+2,1) ]
+       | otherwise  = []
+
+--------------------------------------------------------------------------------
+-- N QUEENS MODEL
+--------------------------------------------------------------------------------
+
+nqueens n = 
+  exist n $ \queens -> queens `allin` (1,n) /\ 
+                       alldifferent queens  /\ 
+                       diagonals queens     /\
+                       -- enumerate ({- middleout -} endsout queens) /\
+                       -- enumerate (middleout queens) /\
+                       enumerate (queens) /\
+		       assignments queens
+
+allin queens range  =  
+  conj [q `in_domain` range 
+       | q <- queens 
+       ] 
+
+alldifferent :: [ FD_Term ] -> Tree FD ()
+alldifferent queens =
+  conj [ qi @\= qj 
+       | qi:qjs <- tails queens 
+       , qj <- qjs 
+       ]
+ 
+diagonals queens = 
+  conj [ qi @\== (qj @+ d) /\ qj @\== (qi @+ d) 
+       | qi:qjs <- tails queens 
+       , (qj,d) <- zip qjs [1..] 
+       ]
diff --git a/Language/CP/PriorityQueue.hs b/Language/CP/PriorityQueue.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/PriorityQueue.hs
@@ -0,0 +1,110 @@
+{- Copyright (c) 2008 the authors listed at the following URL, and/or
+the authors of referenced articles or incorporated external code:
+http://en.literateprograms.org/Priority_Queue_(Haskell)?action=history&offset=20080608152146
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+Retrieved from: http://en.literateprograms.org/Priority_Queue_(Haskell)?oldid=13634
+-}
+
+module Language.CP.PriorityQueue (
+    PriorityQueue,
+    empty,
+    is_empty,
+    minKey,
+    minKeyValue,
+    insert,
+    deleteMin,
+    deleteMinAndInsert
+) where
+
+ 
+import Prelude
+
+
+-- Declare the data type constructors.
+
+data Ord k => PriorityQueue k a = Nil | Branch k a (PriorityQueue k a) (PriorityQueue k a)
+ 
+
+-- Declare the exported interface functions.
+
+-- Return an empty priority queue.
+
+is_empty Nil = True
+is_empty _   = False
+
+empty :: Ord k => PriorityQueue k a
+empty = Nil
+
+
+-- Return the highest-priority key.
+
+minKey :: Ord k => PriorityQueue k a -> k
+minKey = fst . minKeyValue
+
+
+-- Return the highest-priority key plus its associated value.
+
+minKeyValue :: Ord k => PriorityQueue k a -> (k, a)
+minKeyValue Nil              = error "empty queue"
+minKeyValue (Branch k a _ _) = (k, a)
+
+
+-- Insert a key/value pair into a queue.
+
+insert :: Ord k => k -> a -> PriorityQueue k a -> PriorityQueue k a
+insert k a q = union (singleton k a) q
+
+deleteMin :: Ord k => PriorityQueue k a -> ((k,a), PriorityQueue k a)
+deleteMin(Branch k a l r) = ((k,a),union l r)
+
+-- Delete the highest-priority key/value pair and insert a new key/value pair into the queue.
+
+deleteMinAndInsert :: Ord k => k -> a -> PriorityQueue k a -> PriorityQueue k a
+deleteMinAndInsert k a Nil              = singleton k a
+deleteMinAndInsert k a (Branch _ _ l r) = union (insert k a l) r
+
+
+
+-- Declare the private helper functions.
+
+-- Join two queues in sorted order.
+
+union :: Ord k => PriorityQueue k a -> PriorityQueue k a -> PriorityQueue k a
+union l Nil = l
+union Nil r = r
+union l@(Branch kl _ _ _) r@(Branch kr _ _ _)
+    | kl <= kr  = link l r
+    | otherwise = link r l
+
+
+-- Join two queues without regard to order.
+
+-- (This is a helper to the union helper.)
+
+link (Branch k a Nil m) r = Branch k a r m
+link (Branch k a ll lr) r = Branch k a lr (union ll r)
+
+
+-- Return a queue with a single item from a key/value pair.
+
+singleton :: Ord k => k -> a -> PriorityQueue k a
+singleton k a = Branch k a Nil Nil
diff --git a/Language/CP/Queue.hs b/Language/CP/Queue.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/Queue.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-
+ - The Queue data type, a worklist data type for search.
+ -
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+
+module Language.CP.Queue where
+
+import qualified Data.Sequence
+import qualified Language.CP.PriorityQueue as PriorityQueue
+
+class Queue q where   
+  type Elem q :: *
+  emptyQ   :: q -> q
+  isEmptyQ :: q -> Bool
+  popQ     :: q -> (Elem q,q)
+  pushQ    :: Elem q -> q -> q
+
+instance Queue [a] where
+  type Elem [a] = a
+  emptyQ _     = []
+  isEmptyQ     = Prelude.null
+  popQ (x:xs)  = (x,xs)
+  pushQ        = (:)
+
+instance Queue (Data.Sequence.Seq a) where
+  type Elem (Data.Sequence.Seq a)  = a
+  emptyQ _                   = Data.Sequence.empty
+  isEmptyQ                   = Data.Sequence.null 
+  popQ (Data.Sequence.viewl -> x Data.Sequence.:< xs)  = (x,xs)
+  pushQ                      = flip (Data.Sequence.|>)
+
+instance Ord a => Queue (PriorityQueue.PriorityQueue a (a,b,c)) where
+  type Elem (PriorityQueue.PriorityQueue a (a,b,c)) = (a,b,c)
+  emptyQ _ = PriorityQueue.empty
+  isEmptyQ = PriorityQueue.is_empty 
+  pushQ x@(k,_,_)  = PriorityQueue.insert k x
+  popQ q   = let ((_,x),q') = PriorityQueue.deleteMin q
+             in (x,q')
diff --git a/Language/CP/SearchTree.hs b/Language/CP/SearchTree.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/SearchTree.hs
@@ -0,0 +1,175 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+{-
+ - The Tree data type, a generic modelling language for constraint solvers.
+ -
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+
+module Language.CP.SearchTree  where
+
+import Monad
+import Language.CP.Solver
+
+-------------------------------------------------------------------------------
+----------------------------------- Tree --------------------------------------
+-------------------------------------------------------------------------------
+
+data Tree s a
+ 		= Fail                          -- failure
+                | Return a                      -- finished
+                | Try (Tree s a) (Tree s a)     -- disjunction
+                | Add (Constraint s) (Tree s a) -- sequentially adding a constraint to a tree
+                | NewVar (Term s -> Tree s a)   -- add a new variable to a tree
+	        | Label (s (Tree s a))      	-- label with a strategy
+
+instance Show (Tree s a)  where
+  show Fail 		= "Fail"
+  show (Return _) 	= "Return"
+  show (Try l r)        = "Try (" ++ show l ++ ") (" ++ show r ++ ")"
+  show (Add _ t)        = "Add (" ++ show t ++ ")"
+  show (NewVar _)       = "NewVar"
+  show (Label _)        = "Label"
+
+instance Solver s => Functor (Tree s) where
+	fmap  = liftM 
+ 
+instance Solver s => Monad (Tree s) where
+  return = Return
+  (>>=)  = bindTree
+  
+
+bindTree     :: Solver s => Tree s a -> (a -> Tree s b) -> Tree s b
+Fail           `bindTree` k  = Fail
+(Return x)     `bindTree` k  = k x
+(Try m n)      `bindTree` k  = Try (m `bindTree` k) (n `bindTree` k)
+(Add c m)      `bindTree` k  = Add c (m `bindTree` k)
+(NewVar f)     `bindTree` k  = NewVar (\x -> f x `bindTree` k)    
+(Label m)      `bindTree` k  = Label (m >>= \t -> return (t `bindTree` k))
+
+insertTree     :: Solver s => Tree s a -> Tree s () -> Tree s a
+(NewVar f)     `insertTree` t  = NewVar (\x -> f x `insertTree` t)    
+(Add c  o)     `insertTree` t  = Add c (o `insertTree` t)
+other 	       `insertTree` t  = t /\ other
+
+
+{- Monad laws:
+ -
+ - 1. return x >>= f  ==  f x
+ -
+ -    return a >>= f  
+ -    == Return a >>= f		(return def)
+ -    == f x			(bind def) 
+ -
+ - 2. m >>= return  =  m
+ -
+ -   By induction
+ -     case m of
+ -     1) Return x -> 
+ -          Return x >>= return
+ -          == return x			(bind def)
+ -          == Return x        		(return def)
+ -     2) Fail ->
+ -          Fail >>= return
+ -          == Fail			(bind def)
+ -     3)  Try l r >>= return
+ -         == Try (l >>= return) (r >>= return) (bind def)
+ -         == Try l r				(induction)
+ -      4) Add c m >>= return
+ -         == Add c (m >>= return) 	(bind def)
+ -         == Add c m 			(induction) 
+ - 	5) NewVar f >>= return
+ - 	   == NewVar (\v -> f v >>= return) 	(bind def) 
+ - 	   == NewVar (\v -> f v)		((co)-induction?)
+ - 	   == NewVar f				(eta reduction)
+ - 	6) Label sm >>= return
+ - 	   == Label (sm >>= \m -> return (m >>= return))	(bind def)
+ - 	   == Label (sm >>= \m -> return m)			(co-induction)
+ - 	   == Label (sm >>= return)				(eta reduction)
+ - 	   == Label sm						(2nd monad law for Monad s)
+ -
+ - 3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)
+ - 
+ -   By induction
+ -     case m of
+ -     1) (Return y >>= f) >>= g 
+ -	  == f y >>= g					(bind def)
+ -	  == (\x -> f x >>= g) y			(beta expansion)
+ -	  == Return y >>= (\x -> f x >>= g)		(bind def)
+ -     2) (Fail >>= f) >>= g
+ -        == Fail >>= g					(bind def)
+ -        == Fail					(bind def)
+ -        == Fail >>= (\x -> f x >>= g)			(bind def) 
+ -     3) (Try l r >>= f) >>= g
+ -        == Try (l >>= f) (r >>= f)) >>= g 				(bind def)
+ -        == Try ((l >>= f) >>= g) ((r >>= f) >>= g)			(bind def)
+ -        == Try (l >>= (\x -> f x >>= g)) (r >>= (\x -> f x >>= g)) 	(induction)
+ -        == Try l r >>= (\x -> f x >>= g)				(bind def)
+ -     4) (NewVar m >>= f) >>= g
+ -        == NewVar (\v -> m v >>= f) >>= g			(bind def)
+ -        == NewVar (\w -> (\v -> m v >>= f) w >>= g)		(bind def)
+ -        == NewVar (\w -> (m w >>= f) >>= g)			(beta reduction)  
+ -        == NewVar (\w -> m w >>= (\x -> f x >>= g))		(co-induction)
+ -        == NewVar m >>= (\x -> f x >>= g)			(bind def)
+ -     5) (Label sm >>= f) >>= g
+ -         == Label (sm >>= \m -> return (m >>= f)) >>= g 	(bind def) 
+ -         == Label ((sm >>= \m -> return (m >>= f)) >>= \m' -> return (m' >>= g))
+ -         == Label (sm >>= (\m -> return (m >>= f) >>= \m' -> return (m' >>= g)))
+ -         == Label (sm >>= \m -> return ((m >>= f) >>= g))
+ -         == Label (sm >>= \m -> return (m >>= (\x -> f x >>= g)))
+ -         == Label sm >>= (\x -> f x >>= g)
+ -
+ -}
+
+-------------------------------------------------------------------------------
+----------------------------------- Sugar -------------------------------------
+-------------------------------------------------------------------------------
+ 
+infixr 3 /\
+(/\) :: Solver s => Tree s a -> Tree s b -> Tree s b
+(/\) = (>>)
+ 
+infixl 2 \/
+(\/) :: Solver s => Tree s a -> Tree s a -> Tree s a
+(\/) = Try
+
+false :: Tree s a
+false = Fail
+ 
+true :: Tree s ()
+true = Return ()
+
+disj :: Solver s => [Tree s a] -> Tree s a
+disj = foldr (\/) false
+
+conj :: Solver s => [Tree s ()] -> Tree s ()
+conj = foldr (/\) true
+
+disj2 :: Solver s => [Tree s a] -> Tree s a
+disj2 (x:  [])  = x
+disj2 l        = let (xs,ys)      = split l
+                     split []     = ([],[])
+                     split (a:as) = let (bs,cs) = split as
+                                    in  (a:cs,bs)
+                 in  Try (disj2 xs) (disj2 ys)
+ 
+exists :: (Term s -> Tree s a) -> Tree s a
+exists f = NewVar f
+
+exist :: Solver s => Int -> ([Term s] -> Tree s a) -> Tree s a
+exist n ftree = f n []
+         where f 0 acc  = ftree acc
+               f n acc  = exists $ \v -> f (n-1) (v:acc)
+
+forall :: Solver s => [Term s] -> (Term s -> Tree s ()) -> Tree s ()
+forall list ftree = conj $ map ftree list
+ 
+label :: Solver s => s (Tree s a) -> Tree s a
+label = Label
+
+prim :: Solver s => (s a) -> Tree s a
+prim action = Label (action >>= return . return)
+
+add :: Solver s => Constraint s -> Tree s ()
+add c = Add c true
diff --git a/Language/CP/Solver.hs b/Language/CP/Solver.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/Solver.hs
@@ -0,0 +1,30 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+{-
+ - The Solver class, a generic interface for constraint solvers.
+ -
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+module Language.CP.Solver where 
+
+class Monad solver => Solver solver where
+	-- the constraints
+	type Constraint solver 	:: *
+	-- the terms
+	type Term solver 	:: *
+ 	-- the labels
+	type Label solver	:: *
+	-- produce a fresh constraint variable
+	newvarSM 	:: solver (Term solver)
+	-- add a constraint to the current state, and
+	-- return whethe the resulting state is consistent
+	addSM		:: Constraint solver -> solver Bool
+	-- reify the current state
+	storeSM		:: solver [Constraint solver]
+	-- run a computation
+	runSM		:: solver a -> a
+	-- mark the current state, and return its label
+	markSM		:: solver (Label solver)
+	-- go to the state with given label
+	gotoSM		:: Label solver -> solver ()
diff --git a/Language/CP/Transformers.hs b/Language/CP/Transformers.hs
new file mode 100644
--- /dev/null
+++ b/Language/CP/Transformers.hs
@@ -0,0 +1,104 @@
+{- 
+ - 	Monadic Constraint Programming
+ - 	http://www.cs.kuleuven.be/~toms/Haskell/
+ - 	Tom Schrijvers
+ -}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE Rank2Types #-}
+module Language.CP.Transformers where 
+
+import Language.CP.Solver
+import Language.CP.SearchTree
+import Language.CP.Queue
+
+--------------------------------------------------------------------------------
+-- EVALUATION
+--------------------------------------------------------------------------------
+
+eval :: (Solver solver, Queue q, Elem q ~ (Label solver,Tree solver (ForResult t),TreeState t), Transformer t,
+         ForSolver t ~ solver) 
+     => Tree solver (ForResult t) -> q -> t -> solver (Int,[ForResult t])
+eval tree q t  = do (es,ts) <- initT t tree
+                    eval' 0 tree q t es ts
+
+eval' :: SearchSig solver q t (ForResult t) 
+eval' i (Return x) wl t es ts  = do (j,xs) <- returnT (i+1) wl t es
+                                    return (j,(x:xs)) 
+eval' i (Add c k)  wl t es ts = do b <- addSM c 
+                                   if b then eval' (i+1) k wl t es ts
+                                        else continue (i+1) wl t es
+eval' i (NewVar f) wl t es ts = do v <- newvarSM 
+                                   eval' (i+1) (f v) wl t es ts
+eval' i (Try l r)  wl t es ts  = 
+  do now <- markSM 
+     let wl' = pushQ (now,l,leftT t es ts) $ pushQ (now,r,rightT t es ts) wl
+     continue (i+1) wl' t es
+eval' i Fail       wl t es ts  = continue (i+1) wl t es
+eval' i (Label m)  wl t es ts  = do tree <- m
+                                    eval' (i+1) tree wl t es ts
+ 
+continue :: ContinueSig solver q t (ForResult t) 
+continue i wl t es  
+	| isEmptyQ wl  = endT i wl t es -- return (i,[])
+        | otherwise    = let ((past,tree,ts),wl') = popQ wl
+                         in  do gotoSM past
+                                nextT i tree wl' t es ts 
+
+--------------------------------------------------------------------------------
+-- TRANSFORMER
+--------------------------------------------------------------------------------
+
+type SearchSig solver q t a =
+     (Solver solver, Queue q, Transformer t,   
+          Elem q ~ (Label solver,Tree solver a,TreeState t),
+	  ForSolver t ~ solver) 
+     => Int -> Tree solver a -> q -> t -> EvalState t -> TreeState t -> solver (Int,[a])
+
+type ContinueSig solver q t a =
+     (Solver solver, Queue q, Transformer t,   
+          Elem q ~ (Label solver,Tree solver a,TreeState t),
+	  ForSolver t ~ solver) 
+     => Int -> q -> t -> EvalState t -> solver (Int,[a])
+
+class Transformer t where
+  type EvalState t :: *
+  type TreeState t :: *
+  type ForSolver t :: (* -> *)
+  type ForResult t :: *
+  leftT, rightT :: t -> EvalState t -> TreeState t -> TreeState t
+  leftT  _ _ = id
+  rightT    = leftT
+  nextT :: SearchSig (ForSolver t) q t (ForResult t)
+  nextT  = eval'
+  initT :: t -> Tree (ForSolver t) (ForResult t) -> (ForSolver t) (EvalState t,TreeState t)
+  returnT :: ContinueSig solver q t (ForResult t) 
+  returnT i wl t es  = continue i wl t es
+  endT  :: ContinueSig solver q t (ForResult t)
+  endT i wl t es     = return (i,[])
+
+newtype DepthBoundedST (solver :: * -> *) a = DBST Int
+
+instance Solver solver => Transformer (DepthBoundedST solver a) where
+  type EvalState (DepthBoundedST solver a)  = ()
+  type TreeState (DepthBoundedST solver a)  = Int
+  type ForSolver (DepthBoundedST solver a)  = solver
+  type ForResult (DepthBoundedST solver a)  = a
+  initT (DBST n) _  = return ((),n)
+  leftT _ _ ts      = ts - 1
+  nextT i tree q t es ts
+    | ts == 0    = continue i q t es
+    | otherwise  = eval' i tree q t es ts
+
+newtype NodeBoundedST (solver :: * -> *) a = NBST Int
+
+instance Solver solver => Transformer (NodeBoundedST solver a)  where
+  type EvalState (NodeBoundedST solver a) = Int
+  type TreeState (NodeBoundedST solver a) = ()
+  type ForSolver (NodeBoundedST solver a) = solver
+  type ForResult (NodeBoundedST solver a) = a
+  initT (NBST n) _  = return (n,())
+  nextT i tree q t es ts
+    | es == 0    = return (i,[])
+    | otherwise  = eval' i tree q t (es - 1) ts
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+#! /usr/bin/env runhaskell
+ 
+import Distribution.Simple
+main = defaultMain
diff --git a/monadiccp.cabal b/monadiccp.cabal
new file mode 100644
--- /dev/null
+++ b/monadiccp.cabal
@@ -0,0 +1,13 @@
+Name:                monadiccp
+Version:             0.1
+Description:         Monadic Constraint Programming framework
+License:             BSD3
+License-file:        LICENSE
+Author:              Tom Schrijvers 
+Maintainer:          tom.schrijvers@cs.kuleuven.be
+Build-Depends:       base, containers, mtl, haskell98, random
+Build-Type:          Simple
+Exposed-modules:     Language.CP.Solver Language.CP.FD Language.CP.Domain Language.CP.FDSugar Language.CP.PriorityQueue Language.CP.SearchTree Language.CP.Transformers
+ghc-options:         
+Category:            control
+Synopsis:	     Package for Constraint Programming