diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2008 Universiteit Utrecht
+Copyright (c) 2009 Universiteit Utrecht
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without modification,
diff --git a/examples/expr/Expr.expected b/examples/expr/Expr.expected
new file mode 100644
--- /dev/null
+++ b/examples/expr/Expr.expected
@@ -0,0 +1,11 @@
+test1: Just (Const 2)
+test2: Nothing
+test3: Nothing
+test4: Just (Const 2 :*: Const 4)
+test5: Just (Const 4 :*: Const 2)
+test6: Nothing
+test7: Just (Const 4 :*: Const 2 :+: Const 7)
+test8: Just (Const 2 :+: Const 1)
+test9: Just (Const 2 :*: Const 3 :+: Const 2 :*: Const 4)
+test10: Just (Const 1 :*: Const 2 :+: Const 1 :*: Const 3)
+test11: Just (Const 2)
diff --git a/examples/expr/Expr.hs b/examples/expr/Expr.hs
new file mode 100644
--- /dev/null
+++ b/examples/expr/Expr.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE TypeFamilies  #-}
+{-# LANGUAGE TypeOperators #-}
+
+import Generics.Regular.Rewriting
+
+
+-----------------------------------------------------------------------------
+-- Types and conversions
+-----------------------------------------------------------------------------
+
+infixl 7 :**:
+infixl 6 :++:
+
+data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show
+
+type instance PF Expr = K Int :+: I :*: I :+: I :*: I
+instance Regular Expr where
+  from (Const n)    = L (K n)
+  from (e1 :++: e2) = R (L  $ (I e1) :*: (I e2))
+  from (e1 :**: e2) = R (R  $ (I e1) :*: (I e2))
+
+  to (L (K n))                     = Const n
+  to (R (L ((I r1) :*: (I r2)))) = r1 :++: r2
+  to (R (R ((I r1) :*: (I r2)))) = r1 :**: r2
+
+{-
+ -- with Con type constructors to specify constructor names.
+instance Regular Expr where
+  type PF Expr = Con (K Int) :+: Con (I :*: I) :+: Con (I :*: I)
+
+  from (Const n)    = L (Con "Const" (K n))
+  from (e1 :++: e2) = R (L (Con "(:++:)" $ (I e1) :*: (I e2)))
+  from (e1 :**: e2) = R (R (Con "(:**:)" $ (I e1) :*: (I e2)))
+
+  to (L (Con _ (K n)))                     = Const n
+  to (R (L (Con _ ((I r1) :*: (I r2))))) = r1 :++: r2
+  to (R (R (Con _ ((I r1) :*: (I r2))))) = r1 :**: r2
+-}
+
+instance Rewrite Expr
+
+-----------------------------------------------------------------------------
+-- Example rules
+-----------------------------------------------------------------------------
+
+rule1 :: Rule Expr
+rule1 = 
+  rule $ \x -> x :++: Const 0 :~>
+               x
+
+rule2 :: Rule Expr
+rule2 = 
+  rule $ \x -> x :++: x :~> 
+               Const 2 :**: x
+
+rule3 :: Rule Expr
+rule3 =
+  rule $ \x y -> x :++: y :~> 
+                 y :++: x
+
+rule4 :: Rule Expr
+rule4 =  
+  rule $ \x y -> Const 2 :**: (x :++: y) :~>
+                 (Const 2 :**: x) :++: (Const 2 :**: y)
+
+rule5 :: Rule Expr
+rule5 = 
+  rule $ \x y z -> x :**: (y :++: z) :~>  
+                   (x :**: y) :++: (x :**: z) 
+
+rule6 :: Rule Expr
+rule6 = 
+  rule $ Const 1 :++: Const 1 :~>
+         Const 2
+
+
+-----------------------------------------------------------------------------
+-- Tests
+-----------------------------------------------------------------------------
+
+test1 :: Maybe Expr
+test1 = rewriteM rule1 (Const 2 :++: Const 0)
+
+test2 :: Maybe Expr
+test2 = rewriteM rule1 (Const 2 :++: Const 3)
+
+test3 :: Maybe Expr
+test3 = rewriteM rule2 (Const 4 :++: Const 3)
+
+test4 :: Maybe Expr
+test4 = rewriteM rule2 (Const 4 :++: Const 4)
+
+test5 :: Maybe Expr
+test5 = one (rewriteM rule1) ((Const 4 :++: Const 0) :**: Const 2)
+
+-- This does not work because the optimisation target is not
+-- an immediate child.
+test6 :: Maybe Expr
+test6 = one (rewriteM rule1) (((Const 4 :++: Const 0) :**: Const 2) :++: Const 7)
+
+-- This works well, because once applies the rule to the optimisation
+-- target exactly once.
+test7 :: Maybe Expr
+test7 = once (rewriteM rule1) (((Const 4 :++: Const 0) :**: Const 2) :++: Const 7)
+
+test8 :: Maybe Expr
+test8 = rewriteM rule3 ((Const 1) :++: (Const 2))
+
+test9 :: Maybe Expr
+test9 = rewriteM rule4 ((Const 2) :**: ((Const 3) :++: (Const 4)))
+
+test10 :: Maybe Expr
+test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))
+
+test11 :: Maybe Expr
+test11 = rewriteM rule6 (Const 1 :++: Const 1)
+
+allTests :: [Maybe Expr]
+allTests = [ test1
+           , test2
+           , test3
+           , test4
+           , test5
+           , test6
+           , test7
+           , test8
+           , test9
+           , test10
+           , test11
+           ]
+
+
+-----------------------------------------------------------------------------
+-- Running all the tests
+-----------------------------------------------------------------------------
+
+-- This main function is defined to solve a bug in GHC
+main :: IO ()
+main = do let resultsPP         = zipWith resultPP [1..] allTests
+              resultPP n result = "test" ++ show n ++ ": " ++ show result
+          putStr (unlines resultsPP)
diff --git a/examples/expr/run b/examples/expr/run
new file mode 100644
--- /dev/null
+++ b/examples/expr/run
@@ -0,0 +1,1 @@
+ghci Expr.hs -i../../src/
diff --git a/examples/logic/Logic.hs b/examples/logic/Logic.hs
new file mode 100644
--- /dev/null
+++ b/examples/logic/Logic.hs
@@ -0,0 +1,310 @@
+{-# LANGUAGE TypeFamilies  #-}
+{-# LANGUAGE TypeOperators #-}
+
+-----------------------------------------------------------------------------
+-- Copyright 2008, Open Universiteit Nederland. This file is distributed 
+-- under the terms of the GNU General Public License. For more information, 
+-- see the file "LICENSE.txt", which is included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+module Logic (Logic(..), isDNF, foldLogic, size, height, metaVars, matchLogic, (|->)) where
+
+import Data.List
+import Data.Maybe
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Test.QuickCheck
+import Control.Monad
+import Data.Char
+
+import Generics.Regular.Rewriting
+
+infixr 1 :<->:
+infixr 2 :->: 
+infixr 3 :||: 
+infixr 4 :&&:
+
+-- | The data type Logic is the abstract syntax for the domain
+-- | of logic expressions.
+data Logic = Var String
+           | Logic :->:  Logic            -- implication
+           | Logic :<->: Logic            -- equivalence
+           | Logic :&&:  Logic            -- and (conjunction)
+           | Logic :||:  Logic            -- or (disjunction)
+           | Not Logic                    -- not
+           | T                            -- true
+           | F                            -- false
+ deriving (Show, Eq, Ord)
+
+-- | The type LogicAlg is the algebra for the data type Logic
+-- | Used in the fold for Logic.
+type LogicAlg a = (String -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a, a)
+
+-- | foldLogic is the standard fold for Logic.
+foldLogic :: LogicAlg a -> Logic -> a
+foldLogic (var, impl, equiv, and, or, not, true, false) = rec
+ where
+   rec logic = 
+      case logic of
+         Var x     -> var x
+         p :->: q  -> rec p `impl`  rec q
+         p :<->: q -> rec p `equiv` rec q
+         p :&&: q  -> rec p `and`   rec q
+         p :||: q  -> rec p `or`    rec q
+         Not p     -> not (rec p)
+         T         -> true 
+         F         -> false
+              
+-- | evalLogic takes a function that gives a logic value to a variable,
+-- | and a Logic expression, and evaluates the boolean expression.
+evalLogic :: (String -> Bool) -> Logic -> Bool
+evalLogic env = foldLogic (env, impl, (==), (&&), (||), not, True, False)
+ where
+   impl p q = not p || q
+
+-- | eqLogic determines whether or not two Logic expression are logically 
+-- | equal, by evaluating the logic expressions on all valuations.
+eqLogic p q = all (\f -> evalLogic f p == evalLogic f q) fs
+ where 
+   xs = varsLogic p `union` varsLogic q
+   fs = map (flip elem) (subsets xs) 
+
+   subsets :: [a] -> [[a]]
+   subsets = foldr op [[]]
+    where op a list = list ++ map (a:) list
+
+-- | Functions noNot, noOr, and noAnd determine whether or not a Logic 
+-- | expression contains a not, or, and and constructor, respectively.
+noNot, noOr, noAnd :: Logic -> Bool
+noNot = foldLogic (const True, (&&), (&&), (&&), (&&), const False, True, True)
+noOr  = foldLogic (const True, (&&), (&&), (&&), \_ _ -> False, id, True, True)
+noAnd = foldLogic (const True, (&&), (&&), \_ _ -> False, (&&), id, True, True)
+
+-- | A Logic expression is atomic if it is a variable or a constant True or False.
+isAtomic :: Logic -> Bool
+isAtomic logic = 
+   case logic of
+      Var _       -> True
+      Not (Var _) -> True
+      _           -> False
+
+-- | Functions isDNF, and isCNF determine whether or not a Logix expression
+-- | is in disjunctive normal form, or conjunctive normal form, respectively. 
+isDNF, isCNF :: Logic -> Bool
+isDNF = all isAtomic . concatMap conjunctions . disjunctions
+isCNF = all isAtomic . concatMap disjunctions . conjunctions
+
+-- | Function disjunctions returns all Logic expressions separated by an or
+-- | operator at the top level.
+disjunctions :: Logic -> [Logic]
+disjunctions F          = []
+disjunctions (p :||: q) = disjunctions p ++ disjunctions q
+disjunctions logic      = [logic]
+
+-- | Function conjunctions returns all Logic expressions separated by an and
+-- | operator at the top level.
+conjunctions :: Logic -> [Logic]
+conjunctions T          = []
+conjunctions (p :&&: q) = conjunctions p ++ conjunctions q
+conjunctions logic      = [logic]
+
+size :: Logic -> Int
+size = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)
+ where bin x y = x+y+1
+
+height :: Logic -> Int
+height = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)
+ where bin x y = 1 + (x `max` y)
+ 
+-- | Count the number of implicationsations :: Logic -> Int
+countImplications :: Logic -> Int
+countImplications = foldLogic (const 0, \x y -> x+y+1, (+), (+), (+), id, 0, 0)
+ 
+-- | Count the number of equivalences
+countEquivalences :: Logic -> Int
+countEquivalences = foldLogic (const 0, (+), \x y -> x+y+1, (+), (+), id, 0, 0)
+
+-- | Count the number of binary operators
+countBinaryOperators :: Logic -> Int
+countBinaryOperators = foldLogic (const 0, binop, binop, binop, binop, id, 0, 0)
+ where binop x y = x + y + 1
+
+-- | Count the number of double negations 
+countDoubleNegations :: Logic -> Int
+countDoubleNegations = fst . foldLogic (const zero, bin, bin, bin, bin, notf, zero, zero)
+ where
+   zero = (0, False)
+   bin (n, _) (m, _) = (n+m, False)
+   notf (n, b) = if b then (n+1, False) else (n, True)
+
+-- | Function varsLogic returns the variables that appear in a Logic expression.
+varsLogic :: Logic -> [String]
+varsLogic = foldLogic (return, union, union, union, union, id, [], [])      
+
+test = associativityAnd $ (Var "a" :||: Var "b") :||: (Var "c" :||: Var "d" :||: Var "e")
+
+associativityAnd, associativityOr :: Logic -> [Logic]
+associativityAnd = associativity conjunctions (:&&:) [T]
+associativityOr  = associativity disjunctions (:||:) [F]
+
+-- Helper function (polymorphic, domain independent)
+associativity :: (a -> [a]) -> (a -> a -> a) -> [a] -> a -> [a]
+associativity f op nil = rec . f
+ where
+   rec ps
+      | n == 0    = nil
+      | n == 1    = ps
+      | otherwise = concatMap f [1 .. n-1]
+    where
+      n = length ps
+      f i = let (xs, ys) = splitAt i ps
+            in [ x `op` y | x <- rec xs, y <- rec ys ]
+
+eqAssociative :: Logic -> Logic -> Bool
+eqAssociative p q =
+   case (p, q) of
+      (Var x, Var y)             -> x==y
+      (p1 :->: p2,  q1 :->:  q2) -> eqAssociative p1 q1 && eqAssociative p2 q2
+      (p1 :<->: p2, q1 :<->: q2) -> eqAssociative p1 q1 && eqAssociative p2 q2
+      (_ :&&: _,  _ :&&:  _) -> and $ zipWith eqAssociative (conjunctions p) (conjunctions q)
+      (_ :||: _,  _ :||:  _) -> and $ zipWith eqAssociative (disjunctions p) (disjunctions q)
+      (Not p1,      Not q1     ) -> eqAssociative p1 q1
+      (T,           T          ) -> True
+      (F,           F          ) -> True
+      _ -> False
+
+-- sized, no nested equivalences
+-- arbLogic :: Bool -> Int -> Gen Logic
+arbLogic b n
+   | n <= 1 = frequency
+        [ (1, oneof $ map return [F, T])
+        , (3, oneof $ map (return . Var) ["p", "q", "r"])
+        ]
+   | otherwise = frequency
+        [ (4, arbLogic b 0)
+        , (2, bin (:->:))
+        , (i, liftM2 (:<->:) recF recF)
+        , (3, bin (:&&:))
+        , (3, bin (:||:))
+        , (3, liftM Not rec)
+        ]
+ where
+   i     = if b then 1 else 0
+   rec   = arbLogic b (n `div` 2)
+   recF  = arbLogic False (n `div` 2)
+   bin f = liftM2 f rec rec
+
+-----------------------------------------------------------
+--- Unification
+
+type Substitution = M.Map Char Logic
+
+isMetaVar :: Logic -> Maybe Char
+isMetaVar (Var ['_', c]) = Just c
+isMetaVar _ = Nothing
+
+metaVars :: [Logic]
+metaVars = [ Var ['_', c] | c <- ['a' .. 'z'] ]
+
+(|->) :: Substitution -> Logic -> Logic
+(|->) sub = foldLogic (var, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)
+ where 
+   var s = case isMetaVar (Var s) of
+              Just i -> fromMaybe (Var s) (M.lookup i sub)
+              _      -> Var s
+
+matchLogic :: Logic -> Logic -> Maybe Substitution
+matchLogic p q =
+   case isMetaVar p of
+      Just i  -> return (M.singleton i q)
+      Nothing ->
+         case (p, q) of
+            (Var x, Var y) | x==y      -> return M.empty
+            (p1 :->: p2,  q1 :->:  q2) -> matchPairs (p1, p2) (q1, q2)
+            (p1 :<->: p2, q1 :<->: q2) -> matchPairs (p1, p2) (q1, q2)
+            (p1 :&&: p2,  q1 :&&: q2 ) -> matchPairs (p1, p2) (q1, q2)
+            (p1 :||: p2,  q1 :||: q2 ) -> matchPairs (p1, p2) (q1, q2)
+            (Not p1,      Not q1     ) -> matchLogic p1 q1
+            (T,           T          ) -> return M.empty
+            (F,           F          ) -> return M.empty
+            _ -> Nothing
+ where
+  matchPairs :: (Logic, Logic) -> (Logic, Logic) -> Maybe Substitution
+  matchPairs (x1, x2) (y1, y2) = do
+     s1 <- matchLogic x1 y1
+     s2 <- matchLogic (s1 |-> x2) y2
+     return (M.union s1 s2)
+
+
+-----------------------------------------------------------
+--- QuickCheck generator
+
+instance Arbitrary Logic where
+   arbitrary = sized (arbLogic True)
+   coarbitrary logic = 
+      case logic of
+         Var x     -> variant 0 . coarbitrary (map ord x)
+         p :->: q  -> variant 1 . coarbitrary p . coarbitrary q
+         p :<->: q -> variant 2 . coarbitrary p . coarbitrary q
+         p :&&: q  -> variant 3 . coarbitrary p . coarbitrary q
+         p :||: q  -> variant 4 . coarbitrary p . coarbitrary q
+         Not p     -> variant 5 . coarbitrary p
+         T         -> variant 6  
+         F         -> variant 7
+
+#ifdef FixView
+type instance PF Logic =
+    (((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))
+    :+:
+    ((I :*: I :+: I) :+: (U :+: U))
+
+instance Regular Logic where
+  from (Var x)     = L (L (L (K x)))
+  from (p :<->: q) = L (L (R ((I (from p)) :*: (I (from q)))))
+  from (p :->: q)  = L (R (L ((I (from p)) :*: (I (from q)))))
+  from (p :&&: q)  = L (R (R ((I (from p)) :*: (I (from q)))))
+  from (p :||: q)  = R (L (L ((I (from p)) :*: (I (from q)))))
+  from (Not p)     = R (L (R (I (from p))))
+  from T           = R (R (L U))
+  from F           = R (R (R U))
+
+  to (L (L (L (K x))))               = Var x
+  to (L (L (R ((I p) :*: (I q))))) = to p :<->: to q
+  to (L (R (L ((I p) :*: (I q))))) = to p :->: to q
+  to (L (R (R ((I p) :*: (I q))))) = to p :&&: to q
+  to (R (L (L ((I p) :*: (I q))))) = to p :||: to q
+  to (R (L (R (I p))))              = Not (to p)
+  to (R (R (L U)))                = T
+  to (R (R (R U)))                = F
+#else
+type instance PF Logic =
+    (((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))
+    :+:
+    ((I :*: I :+: I) :+: (U :+: U))
+
+instance Regular Logic where
+  from (Var x)     = L (L (L (K x)))
+  from (p :<->: q) = L (L (R ((I p) :*: (I q))))
+  from (p :->: q)  = L (R (L ((I p) :*: (I q))))
+  from (p :&&: q)  = L (R (R ((I p) :*: (I q))))
+  from (p :||: q)  = R (L (L ((I p) :*: (I q))))
+  from (Not p)     = R (L (R (I p)))
+  from T           = R (R (L U))
+  from F           = R (R (R U))
+
+  to (L (L (L (K x))))               = Var x
+  to (L (L (R ((I p) :*: (I q))))) = p :<->: q
+  to (L (R (L ((I p) :*: (I q))))) = p :->: q
+  to (L (R (R ((I p) :*: (I q))))) = p :&&: q
+  to (R (L (L ((I p) :*: (I q))))) = p :||: q
+  to (R (L (R (I p))))              = Not p
+  to (R (R (L U)))                = T
+  to (R (R (R U)))                = F
+#endif
+
+instance Rewrite Logic
diff --git a/examples/logic/LogicGenerator.hs b/examples/logic/LogicGenerator.hs
new file mode 100644
--- /dev/null
+++ b/examples/logic/LogicGenerator.hs
@@ -0,0 +1,9 @@
+module LogicGenerator () where
+
+import Control.Monad
+import Data.Char
+import System.Random
+import Test.QuickCheck hiding (defaultConfig)
+
+import Logic
+
diff --git a/examples/logic/LogicRules.hs b/examples/logic/LogicRules.hs
new file mode 100644
--- /dev/null
+++ b/examples/logic/LogicRules.hs
@@ -0,0 +1,237 @@
+-----------------------------------------------------------------------------
+-- Copyright 2008, Open Universiteit Nederland. This file is distributed 
+-- under the terms of the GNU General Public License. For more information, 
+-- see the file "LICENSE.txt", which is included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+module LogicRules where
+
+import qualified Data.Set as S
+import Logic
+import Generics.Regular.Rewriting
+
+p |- q = p :~> q
+makeRuleList _ = map rule
+buggyRule = id
+makeRule _ = rule
+
+{- 
+logicRules :: [LogicRule]
+logicRules = [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
+             , ruleFalseZeroAnd, ruleDeMorganOr, ruleDeMorganAnd
+             , ruleNotBoolConst, ruleNotNot, ruleAndOverOr, ruleOrOverAnd
+             , ruleDefImpl, ruleDefEquiv
+             , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl
+             , ruleTrueInImpl
+	     , ruleComplOr, ruleComplAnd
+	     , ruleIdempOr, ruleIdempAnd
+	     , ruleAbsorpOr, ruleAbsorpAnd
+	     , ruleCommOr, ruleCommAnd
+             ] 
+
+logicBuggyRules :: [LogicRule]
+logicBuggyRules = [ buggyRuleCommImp, buggyRuleAssImp] 
+-}
+
+-- This main function is defined to solve a bug in GHC
+main :: IO ()
+main = do let resultsPP = zipWith undefined [1..] ([] :: [Logic])
+          putStr (unlines resultsPP)   
+     
+ruleComplOr :: [Rule Logic]
+ruleComplOr = makeRuleList "ComplOr"
+   [ \x -> (x :||: Not x)  |-  T
+   , \x -> (Not x :||: x)  |-  T
+   ]
+
+ruleComplAnd :: [Rule Logic]
+ruleComplAnd = makeRuleList "ComplAnd"
+   [ \x -> (x :&&: Not x)  |-  F
+   , \x -> (Not x :&&: x)  |-  F
+   ]
+
+ruleDefImpl :: Rule Logic
+ruleDefImpl = makeRule "DefImpl" $
+   \x y -> (x :->: y)  |-  (Not x :||: y)
+
+ruleDefEquiv :: Rule Logic
+ruleDefEquiv = makeRule "DefEquiv" $
+   \x y -> (x :<->: y)  |-  ((x :&&: y) :||: (Not x :&&: Not y))
+   
+ruleFalseInEquiv :: [Rule Logic]
+ruleFalseInEquiv = makeRuleList "FalseInEquiv"
+   [ \x -> (F :<->: x)  |-  (Not x)
+   , \x -> (x :<->: F)  |-  (Not x)
+   ]
+
+ruleTrueInEquiv :: [Rule Logic]
+ruleTrueInEquiv = makeRuleList "TrueInEquiv"
+   [ \x -> (T :<->: x)  |-  x
+   , \x -> (x :<->: T)  |-  x
+   ]
+
+ruleFalseInImpl :: [Rule Logic]
+ruleFalseInImpl = makeRuleList "FalseInImpl"
+   [ \x -> (F :->: x)  |-  T
+   , \x -> (x :->: F)  |- (Not x)
+   ]
+ 
+ruleTrueInImpl :: [Rule Logic]
+ruleTrueInImpl = makeRuleList "TrueInImpl"
+   [  \x -> (T :->: x)  |-  x
+   ,  \x -> (x :->: T)  |-  T
+   ]
+        
+ruleFalseZeroOr :: [Rule Logic]
+ruleFalseZeroOr = makeRuleList "FalseZeroOr"
+   [ \x -> (F :||: x)  |-  x
+   , \x -> (x :||: F)  |-  x
+   ]
+
+ruleTrueZeroOr :: [Rule Logic]
+ruleTrueZeroOr = makeRuleList "TrueZeroOr"
+   [ \x -> (T :||: x)  |-  T
+   , \x -> (x :||: T)  |-  T
+   ]
+
+ruleTrueZeroAnd :: [Rule Logic]
+ruleTrueZeroAnd = makeRuleList "TrueZeroAnd"
+   [ \x -> (T :&&: x)  |-  x
+   , \x -> (x :&&: T)  |-  x
+   ]
+
+ruleFalseZeroAnd :: [Rule Logic]
+ruleFalseZeroAnd = makeRuleList "FalseZeroAnd"
+   [ \x -> (F :&&: x)  |-  F
+   , \x -> (x :&&: F)  |-  F
+   ]
+
+ruleDeMorganOr :: Rule Logic
+ruleDeMorganOr = makeRule "DeMorganOr" $
+   \x y -> (Not (x :||: y))  |-  (Not x :&&: Not y)
+
+ruleDeMorganAnd :: Rule Logic
+ruleDeMorganAnd = makeRule "DeMorganAnd" $
+   \x y -> (Not (x :&&: y))  |-  (Not x :||: Not y)
+
+ruleNotBoolConst :: [Rule Logic]
+ruleNotBoolConst = makeRuleList "NotBoolConst"
+   [ (Not T)  |-  F
+   , (Not F)  |-  T
+   ]
+
+ruleNotNot :: Rule Logic
+ruleNotNot = makeRule "NotNot" $ 
+   \x -> (Not (Not x))  |-  x
+
+ruleAndOverOr :: [Rule Logic]
+ruleAndOverOr = makeRuleList "AndOverOr"
+   [ \x y z -> (x :&&: (y :||: z))  |-  ((x :&&: y) :||: (x :&&: z))
+   , \x y z -> ((x :||: y) :&&: z)  |-  ((x :&&: z) :||: (y :&&: z))
+   ]
+
+ruleOrOverAnd :: [Rule Logic]
+ruleOrOverAnd = makeRuleList "OrOverAnd"
+   [ \x y z -> (x :||: (y :&&: z))  |-  ((x :||: y) :&&: (x :||: z))
+   , \x y z -> ((x :&&: y) :||: z)  |-  ((x :||: z) :&&: (y :||: z))
+   ]
+ 
+ruleIdempOr :: Rule Logic
+ruleIdempOr = makeRule "IdempOr" $
+    \x -> (x :||: x)  |-  x
+   
+    
+ruleIdempAnd :: Rule Logic
+ruleIdempAnd = makeRule "IdempAnd" $
+    \x -> (x :&&: x)  |-  x
+    
+    
+ruleAbsorpOr :: Rule Logic
+ruleAbsorpOr = makeRule "AbsorpOr" $
+    \x y -> (x :||: (x :&&: y))  |-  x
+    
+    
+ruleAbsorpAnd :: Rule Logic
+ruleAbsorpAnd = makeRule "AbsorpAnd" $
+    \x y -> (x :&&: (x :||: y))  |-  x 
+    
+ruleCommOr :: Rule Logic
+ruleCommOr = makeRule "CommOr" $
+    \x y -> (x :||: y)  |-  (y :||: x) 
+    
+    
+ruleCommAnd :: Rule Logic
+ruleCommAnd = makeRule "CommAnd" $
+    \x y -> (x :&&: y)  |-  (y :&&: x)
+    
+
+-- Buggy rules:
+
+buggyRuleCommImp :: Rule Logic
+buggyRuleCommImp = buggyRule $ makeRule "CommImp" $
+    \x y -> (x :->: y)  |-  (y :->: x) --this does not hold: T->T => T->x
+
+    
+buggyRuleAssImp :: [Rule Logic]
+buggyRuleAssImp = buggyRule $ makeRuleList "AssImp"
+   [ \x y z -> (x :->: (y :->: z))  |-  ((x :->: y) :->: z)
+   , \x y z -> ((x :->: y) :->: z)  |-  (x :->: (y :->: z))
+   ]
+    
+buggyRuleIdemImp :: Rule Logic
+buggyRuleIdemImp = buggyRule $ makeRule "IdemImp" $
+    \x -> (x :->: x)  |-  x 
+    
+buggyRuleIdemEqui :: Rule Logic
+buggyRuleIdemEqui = buggyRule $ makeRule "IdemEqui" $
+    \x -> (x :<->: x)  |-  x 
+    
+buggyRuleEquivElim :: [Rule Logic]
+buggyRuleEquivElim = buggyRule $ makeRuleList "BuggyEquivElim"
+    [ \x y -> (x :<->: y) |- ((x :&&: y) :||: Not (x :&&: y))
+    , \x y -> (x :<->: y) |- ((x :||: y) :&&: (Not x :||: Not y))
+    , \x y -> (x :<->: y) |- ((x :&&: y) :||: (Not x :&&:  y))
+    , \x y -> (x :<->: y) |- ((x :&&: y) :||: ( x :&&: Not y))
+    , \x y -> (x :<->: y) |- ((x :&&: y) :&&: (Not x :&&: Not y))
+    ]
+    
+buggyRuleImplElim :: Rule Logic
+buggyRuleImplElim = buggyRule $ makeRule "BuggyImplElim" $
+    \x y -> (x :->: y) |- Not (x :||: y) 
+    
+buggyRuleDeMorgan :: [Rule Logic]
+buggyRuleDeMorgan = buggyRule $ makeRuleList "BuggyDeMorgan"
+    [ \x y -> (Not (x :&&: y)) |-  (Not x :||: y)
+    , \x y -> (Not (x :&&: y)) |-  (x :||: Not y)
+    , \x y -> (Not (x :&&: y)) |- (Not (Not x :||: Not y))
+    , \x y -> (Not (x :||: y)) |-  (Not x :&&: y)
+    , \x y -> (Not (x :||: y)) |-  (x :&&: Not y)
+    , \x y -> (Not (x :||: y)) |- (Not (Not x :&&: Not y))
+    ]
+buggyRuleNotOverImpl :: Rule Logic
+buggyRuleNotOverImpl = buggyRule $ makeRule "BuggyNotOverImpl" $
+    \x y -> (Not(x :->: y)) |- (Not x :->: Not y)   
+    
+buggyRuleParenth :: [Rule Logic]
+buggyRuleParenth = buggyRule $ makeRuleList "BuggyParenth"
+    [ \x y -> (Not (x :&&: y)) |-  (Not x :&&: y)
+    , \x y -> (Not (x :||: y)) |-  (Not x :||: y)
+    , \x y -> (Not (x :<->: y)) |- (Not(x :&&: y) :||: (Not x :&&: Not y))
+    , \x y -> (Not(Not x :&&: y)) |- (x :&&: y) 
+    , \x y -> (Not(Not x :||: y)) |- (x :||: y)
+    , \x y -> (Not(Not x :->: y)) |- (x :->: y)
+    , \x y -> (Not(Not x :<->: y)) |- (x :<->: y)
+    ]
+    
+buggyRuleAssoc :: [Rule Logic]
+buggyRuleAssoc = buggyRule $ makeRuleList "BuggyAssoc"
+    [ \x y z -> (x :||: (y :&&: z)) |- ((x :||: y) :&&: z)
+    , \x y z -> ((x :||: y) :&&: z) |- (x :||: (y :&&: z))
+    , \x y z -> ((x :&&: y) :||: z) |- (x :&&: (y :||: z))
+    , \x y z -> (x :&&: (y :||: z)) |- ((x :&&: y) :||: z)
+    ]
diff --git a/examples/logic/LogicStrategies.hs b/examples/logic/LogicStrategies.hs
new file mode 100644
--- /dev/null
+++ b/examples/logic/LogicStrategies.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- Copyright 2008, Open Universiteit Nederland. This file is distributed 
+-- under the terms of the GNU General Public License. For more information, 
+-- see the file "LICENSE.txt", which is included in the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+module LogicStrategies where
+
+import Prelude hiding (repeat)
+import Logic
+import LogicRules hiding (main)
+import System.Random
+import Test.QuickCheck hiding (label)
+
+import Generics.Regular.Rewriting
+
+
+type Strategy a = a -> [a]
+
+label _ = id
+(s <*> t) a = [c | b <- s a, c <- t b]
+(s <|> t) a = s a ++ t a
+many s = return <|> (s <*> many s)
+repeat s = many s <*> notS s
+alternatives = foldr (<|>) (const [])
+notS s a = if null (s a) then [a] else []
+
+rewriteMl :: Rewrite a => [Rule a] -> Strategy a 
+rewriteMl = alternatives . map rewriteM
+
+eliminateConstants :: Strategy (Logic)
+eliminateConstants = repeat $ once $
+   alternatives $
+      [ rewriteMl ruleFalseZeroOr
+      , rewriteMl ruleTrueZeroOr
+      , rewriteMl ruleTrueZeroAnd
+      , rewriteMl ruleFalseZeroAnd
+      , rewriteMl ruleNotBoolConst
+      , rewriteMl ruleFalseInEquiv
+      , rewriteMl ruleTrueInEquiv
+      , rewriteMl ruleFalseInImpl
+      , rewriteMl ruleTrueInImpl
+      ]
+
+eliminateImplEquiv :: Strategy (Logic)
+eliminateImplEquiv = repeat $ once $
+          rewriteM ruleDefImpl
+      <|> rewriteM ruleDefEquiv
+      
+eliminateNots :: Strategy (Logic)
+eliminateNots = repeat $ once $ 
+          rewriteM ruleDeMorganAnd
+      <|> rewriteM ruleDeMorganOr
+      <|> rewriteM ruleNotNot
+      
+orToTop :: Strategy (Logic)
+orToTop = repeat $ once $ rewriteMl ruleAndOverOr
+
+toDNF :: Strategy (Logic)
+toDNF =  label "Bring to dnf"
+      $  label "Eliminate constants"                 eliminateConstants
+     <*> label "Eliminate implications/equivalences" eliminateImplEquiv
+     <*> label "Eliminate nots"                      eliminateNots 
+     <*> label "Move ors to top"                     orToTop
+     
+propSound :: Logic -> Bool
+propSound p = 
+   case toDNF p of
+      x:_ -> isDNF x
+      _   -> False
+      
+propView :: Logic -> Bool
+propView p = p == to (from p)
+
+checks :: IO ()
+checks = do
+   quickCheck propView
+   quickCheck propSound
+
+main :: IO ()
+main = print $ all checkOne [0..250]
+ where
+   checkOne n =
+      propSound (generate n (mkStdGen n) arbitrary)
diff --git a/examples/logic/run b/examples/logic/run
new file mode 100644
--- /dev/null
+++ b/examples/logic/run
@@ -0,0 +1,1 @@
+ghci -cpp LogicStrategies.hs LogicRules.hs LogicGenerator.hs Logic.hs -i../../src/ -package QuickCheck-1.2.0.0
diff --git a/rewriting.cabal b/rewriting.cabal
--- a/rewriting.cabal
+++ b/rewriting.cabal
@@ -1,5 +1,5 @@
 name:                   rewriting
-version:                0.1
+version:                0.2
 synopsis:               Generic rewriting library for regular datatypes.
 description:
 
@@ -18,7 +18,7 @@
   <http://www.cs.uu.nl/wiki/GenericProgramming/Rewriting>.
 
 category:               Generics
-copyright:              (c) 2008 Universiteit Utrecht
+copyright:              (c) 2009 Universiteit Utrecht
 license:                BSD3
 license-file:           LICENSE
 author:                 Thomas van Noort,
@@ -30,8 +30,17 @@
 stability:              experimental
 build-type:             Custom
 cabal-version:          >= 1.2.1
-tested-with:            GHC == 6.10.0.20081007
+tested-with:            GHC == 6.10.1
+extra-source-files:     examples/expr/run
+                        examples/expr/Expr.hs
+                        examples/expr/Expr.expected
+                        examples/logic/Logic.hs
+                        examples/logic/LogicGenerator.hs
+                        examples/logic/LogicRules.hs
+                        examples/logic/LogicStrategies.hs
+                        examples/logic/run
 
+
 -- Disabled the test flag for the moment since not all
 -- modules from the tests directory are properly included
 -- in the distribution generated by the sdist target
@@ -50,7 +59,7 @@
                         Generics.Regular.Rewriting.Rules
                         Generics.Regular.Rewriting.Strategies
 
-  build-depends:        base >= 3.0, containers >= 0.1
+  build-depends:        base >= 4.0 && < 5, containers >= 0.1, regular >= 0.1
 
 -- Disabled the test flag for the moment since not all
 -- modules from the tests directory are properly included
diff --git a/src/Generics/Regular/Rewriting.hs b/src/Generics/Regular/Rewriting.hs
--- a/src/Generics/Regular/Rewriting.hs
+++ b/src/Generics/Regular/Rewriting.hs
@@ -10,89 +10,88 @@
 --
 -- By importing this module, the user is able to use all the rewriting
 -- machinery. The user is only required to provide an instance of 
--- @Regular@ and @Rewrite@ for his datatype.
+-- @Regular@ and @Rewrite@ for the datatype.
 --
 -- Consider a datatype representing logical propositions:
 --
--- @
---   data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show
--- @
+-- > data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show
+-- >
+-- > infixr 5 :++:
+-- > infixr 6 :**:
 --
 -- An instance of @Regular@ would look like:
 --
--- @
---   instance Regular Expr where
---     type PF Expr = K Int :+: Id :*: Id :+: Id :*: Id
---     from (Const n)    = L (K n)
---     from (e1 :++: e2) = R (L  $ (Id e1) :*: (Id e2))
---     from (e1 :**: e2) = R (R  $ (Id e1) :*: (Id e2))
---     to (L (K n))                     = Const n
---     to (R (L ((Id r1) :*: (Id r2)))) = r1 :++: r2
---     to (R (R ((Id r1) :*: (Id r2)))) = r1 :**: r2
--- @
+-- > data Const
+-- > data Plus
+-- > data Times
+-- >
+-- > instance Constructor Const where conName _ = "Const"
+-- > instance Constructor Plus where 
+-- >   conName _   = "(:++:)"
+-- >   conFixity _ = Infix RightAssociative 5
+-- > instance Constructor Times where 
+-- >   conName _   = "(:**:)"
+-- >   conFixity _ = Infix RightAssociative 6
+-- >
+-- > type instance PF Expr =  C Const (K Int) 
+-- >                      :+: C Plus  (I :*: I) 
+-- >                      :+: C Times (I :*: I)
+-- >
+-- > instance Regular Expr where
+-- >   from (Const n)    = L (C (K n))
+-- >   from (e1 :++: e2) = R (L (C $ (I e1) :*: (I e2)))
+-- >   from (e1 :**: e2) = R (R (C $ (I e1) :*: (I e2)))
+-- >   to (L (C (K n)))                   = Const n
+-- >   to (R (L (C ((I r1) :*: (I r2))))) = r1 :++: r2
+-- >   to (R (R (C ((I r1) :*: (I r2))))) = r1 :**: r2
 --
--- Additionally, the instance @Rewrite@ would look like:
+-- Alternatively, the above code could be derived using Template Haskell:
 --
--- @
---   instance Rewrite Expr
--- @
+-- > $(deriveConstructors ''Expr)
+-- > $(deriveRegular ''Expr "PFExpr")
+-- > type instance PF Expr = PFExpr
 --
--- Build rules like this:
+-- Additionally, the instance @Rewrite@ would look like:
 --
--- @
---   rule1 :: Rule Expr
---   rule1 = 
---     rule $ \x -> x :++: Const 0 :~>
---                 x
---   rule5 :: Rule Expr
---   rule5 = 
---     rule $ \x y z -> x :**: (y :++: z) :~>  
---                     (x :**: y) :++: (x :**: z) 
--- @
+-- > instance Rewrite Expr
 --
--- And apply them as follows:
+-- Rules are built like this:
 --
--- @
---   test1 :: Maybe Expr
---   test1 = rewriteM rule1 (Const 2 :++: Const 0)
---   test10 :: Maybe Expr
---   test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))
--- @
+-- > rule1 :: Rule Expr
+-- > rule1 = 
+-- >   rule $ \x -> x :++: Const 0 :~>
+-- >               x
+-- > rule5 :: Rule Expr
+-- > rule5 = 
+-- >   rule $ \x y z -> x :**: (y :++: z) :~>
+-- >                   (x :**: y) :++: (x :**: z)
 --
--- You may also wish to add constructor names in the representation to use
--- generic show. However, constructor names are not yet a stable feature
--- and will probably change in future versions of this library.
+-- And applied as follows:
 --
--- @
---   instance Regular Expr where
---     type PF Expr = Con (K Int) :+: Con (Id :*: Id) :+: Con (Id :*: Id)
---     from (Const n)    = L (Con \"Const\" (K n))
---     from (e1 :++: e2) = R (L (Con \"(:++:)\" $ (Id e1) :*: (Id e2)))
---     from (e1 :**: e2) = R (R (Con \"(:**:)\" $ (Id e1) :*: (Id e2)))
---     to (L (Con _ (K n)))                        = Const n
---     to (R (L (Con _ ((Id r1) :*: (Id r2))))) = r1 :++: r2
---     to (R (R (Con _ ((Id r1) :*: (Id r2))))) = r1 :**: r2
--- @
+-- > test1 :: Maybe Expr
+-- > test1 = rewriteM rule1 (Const 2 :++: Const 0)
+-- > test10 :: Maybe Expr
+-- > test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))
 --
 
 -----------------------------------------------------------------------------
 
 module Generics.Regular.Rewriting (
 
-  module Generics.Regular.Rewriting.Base,
+  module Generics.Regular.Base,
+  
+  module Generics.Regular.Functions,
 
   module Generics.Regular.Rewriting.Machinery,
 
-  module Generics.Regular.Rewriting.Representations,
-
   module Generics.Regular.Rewriting.Rules,
 
   module Generics.Regular.Rewriting.Strategies
 
 ) where
 
-import Generics.Regular.Rewriting.Base
+import Generics.Regular.Base
+import Generics.Regular.Functions
 import Generics.Regular.Rewriting.Machinery
-import Generics.Regular.Rewriting.Representations
 import Generics.Regular.Rewriting.Rules
 import Generics.Regular.Rewriting.Strategies
diff --git a/src/Generics/Regular/Rewriting/Base.hs b/src/Generics/Regular/Rewriting/Base.hs
--- a/src/Generics/Regular/Rewriting/Base.hs
+++ b/src/Generics/Regular/Rewriting/Base.hs
@@ -2,8 +2,6 @@
 {-# LANGUAGE TypeOperators    #-}
 {-# LANGUAGE TypeFamilies     #-}
 
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.Regular.Rewriting.Base
@@ -15,265 +13,12 @@
 -- Portability :  non-portable
 --
 -- Summary: Base generic functions that are used for generic rewriting.
+-- This module simply reexports "Generics.Regular.Functions", and is provided
+-- for backwards-compatibility only.
 -----------------------------------------------------------------------------
 
 module Generics.Regular.Rewriting.Base (
-
-  -- * Functorial map function.
-  Functor (..),
-  
-  -- * Monadic functorial map function.
-  GMap (..),
-  
-  -- * Crush functions.
-  Crush (..),
-  flatten,
-
-  -- * Zip functions.
-  Zip (..),
-  fzip,
-  fzip',
-
-  -- * Equality function.
-  geq,
-
-  -- * Show function.
-  GShow (..),
-  
-  -- * Functions for generating values that are different on top-level.
-  LRBase (..),
-  LR (..),
-  left,
-  right  
-
-) where
-
-import Control.Monad
-
-import Generics.Regular.Rewriting.Representations
-
-
------------------------------------------------------------------------------
--- Functorial map function.
------------------------------------------------------------------------------
-
-instance Functor Id where
-  fmap f (Id r) = Id (f r)
-
-instance Functor (K a) where
-  fmap _ (K a) = K a
-
-instance Functor Unit where
-  fmap _ Unit = Unit
-
-instance (Functor f, Functor g) => Functor (f :+: g) where
-  fmap f (L x) = L (fmap f x)
-  fmap f (R y) = R (fmap f y)
-
-instance (Functor f, Functor g) => Functor (f :*: g) where
-  fmap f (x :*: y) = fmap f x :*: fmap f y
-
-instance Functor f => Functor (Con f) where
-  fmap f (Con con r) = Con con (fmap f r)
-
-
------------------------------------------------------------------------------
--- Monadic functorial map function.
------------------------------------------------------------------------------
-
--- | The @GMap@ class defines a monadic functorial map.
-class GMap f where
-  fmapM :: Monad m => (a -> m b) -> f a -> m (f b)
-
-instance GMap Id where
-  fmapM f (Id r) = liftM Id (f r)
-
-instance GMap (K a) where
-  fmapM _ (K x)  = return (K x)
-
-instance GMap Unit where
-  fmapM _ Unit = return Unit
-
-instance (GMap f, GMap g) => GMap (f :+: g) where
-  fmapM f (L x) = liftM L (fmapM f x)
-  fmapM f (R x) = liftM R (fmapM f x)
-
-instance (GMap f, GMap g) => GMap (f :*: g) where
-  fmapM f (x :*: y) = liftM2 (:*:) (fmapM f x) (fmapM f y)
-
-instance GMap f => GMap (Con f) where
-  fmapM f (Con c x) = liftM (Con c) (fmapM f x)
-
-
------------------------------------------------------------------------------
--- Crush functions.
------------------------------------------------------------------------------
-
--- | The @Crush@ class defines a crush on functorial values. In fact,
--- @crush@ is a generalized @foldr@.
-class Crush f where
-  crush :: (a -> b -> b) -> b -> f a -> b
-
-instance Crush Id where
-  crush op e (Id x) = x `op` e
-
-instance Crush (K a) where
-  crush _ e _ = e
-
-instance Crush Unit where
-  crush _ e _ = e
-
-instance (Crush f, Crush g) => Crush (f :+: g) where
-  crush op e (L x) = crush op e x
-  crush op e (R y) = crush op e y
-
-instance (Crush f, Crush g) => Crush (f :*: g) where
-  crush op e (x :*: y) = crush op (crush op e y) x
-
-instance Crush f => Crush (Con f) where
-  crush op e (Con _c x) = crush op e x
-
--- | Flatten a structure by collecting all the elements present.
-flatten :: Crush f => f a -> [a]
-flatten = crush (:) []
-
-
------------------------------------------------------------------------------
--- Zip functions.
------------------------------------------------------------------------------
-
--- | The @Zip@ class defines a monadic zip on functorial values.
-class Zip f where
-  fzipM :: Monad m => (a -> b -> m c) -> f a -> f b -> m (f c)
-
-instance Zip Id where
-  fzipM f (Id x) (Id y) = liftM Id (f x y)
-
-instance Eq a => Zip (K a) where
-  fzipM _ (K x) (K y) 
-    | x == y    = return (K x)
-    | otherwise = fail "fzipM: structure mismatch"
-
-instance Zip Unit where
-  fzipM _ Unit Unit = return Unit
-
-instance (Zip f, Zip g) => Zip (f :+: g) where
-  fzipM f (L x) (L y) = liftM L (fzipM f x y)
-  fzipM f (R x) (R y) = liftM R (fzipM f x y)
-  fzipM _ _       _       = fail "fzipM: structure mismatch"
-
-instance (Zip f, Zip g) => Zip (f :*: g) where
-  fzipM f (x1 :*: y1) (x2 :*: y2) = 
-    liftM2 (:*:) (fzipM f x1 x2)
-                 (fzipM f y1 y2)
-
-instance Zip f => Zip (Con f) where
-  fzipM f (Con c1 x) (Con _c2 y) = liftM (Con c1) (fzipM f x y)
-
--- | Functorial zip with a non-monadic function, resulting in a monadic value.
-fzip  :: (Zip f, Monad m) => (a -> b -> c) -> f a -> f b -> m (f c)
-fzip f = fzipM (\x y -> return (f x y))
-
--- | Partial functorial zip with a non-monadic function.
-fzip' :: Zip f => (a -> b -> c) -> f a -> f b -> f c
-fzip' f x y = maybe (error "fzip': structure mismatch") id (fzip f x y)
-
-
------------------------------------------------------------------------------
--- Equality function.
------------------------------------------------------------------------------
-
--- | Equality on values based on their structural representation.
-geq :: (b ~ PF a, Regular a, Crush b, Zip b) => a -> a -> Bool
-geq x y = maybe False (crush (&&) True) (fzip geq (from x) (from y))
-
-
------------------------------------------------------------------------------
--- Show function.
------------------------------------------------------------------------------
-
--- | The @GShow@ class defines a show on values.
-class GShow f where
-  gshow :: (a -> ShowS) -> f a -> ShowS
-
-instance GShow Id where
-  gshow f (Id r) = f r
-
-instance Show a => GShow (K a) where
-  gshow _ (K x) = shows x
-
-instance GShow Unit where
-  gshow _ Unit = id
-
-instance (GShow f, GShow g) => GShow (f :+: g) where
-  gshow f (L x) = gshow f x
-  gshow f (R x) = gshow f x
-
-instance (GShow f, GShow g) => GShow (f :*: g) where
-  gshow f (x :*: y) = gshow f x . showChar ' ' . gshow f y
-
-instance GShow f => GShow (Con f) where
-  gshow f (Con c x) = showParen True (showString c . showChar ' ' . gshow f x)
-
-
------------------------------------------------------------------------------
--- Functions for generating values that are different on top-level.
------------------------------------------------------------------------------
-
--- | The @LRBase@ class defines two functions, @leftb@ and @rightb@, which 
--- should produce different values.
-class LRBase a where
-  leftb  :: a
-  rightb :: a
-
-instance LRBase Int where
-  leftb  = 0
-  rightb = 1
-
-instance LRBase Char where
-  leftb  = 'L'
-  rightb = 'R'
- 
-instance LRBase a => LRBase [a] where
-  leftb  = []
-  rightb = [error "Should never be inspected"]
-
--- | The @LR@ class defines two functions, @leftf@ and @rightf@, which should 
--- produce different functorial values.
-class LR f where
-  leftf  :: a -> f a
-  rightf :: a -> f a
-
-instance LR Id where
-  leftf  x = Id x
-  rightf x = Id x
-
-instance LRBase a => LR (K a) where
-  leftf  _ = K leftb
-  rightf _ = K rightb
-
-instance LR Unit where
-  leftf  _ = Unit
-  rightf _ = Unit
-
-instance (LR f, LR g) => LR (f :+: g)  where
-  leftf  x = L (leftf x)
-  rightf x = R (rightf x)
-
-instance (LR f, LR g) => LR (f :*: g)  where
-  leftf  x = leftf x :*: leftf x
-  rightf x = rightf x :*: rightf x
-
-instance LR f => LR (Con f) where
-  leftf  x = Con (error "Should never be inspected") (leftf x)
-  rightf x = Con (error "Should never be inspected") (rightf x)
-
--- | Produces a value which should be different from the value returned by 
--- @right@.
-left :: (Regular a, LR (PF a)) => a
-left = to (leftf left)
+    module Generics.Regular.Functions
+  ) where
 
--- | Produces a value which should be different from the value returned by 
--- @left@.
-right :: (Regular a, LR (PF a)) => a
-right = to (rightf right)
+import Generics.Regular.Functions
diff --git a/src/Generics/Regular/Rewriting/Machinery.hs b/src/Generics/Regular/Rewriting/Machinery.hs
--- a/src/Generics/Regular/Rewriting/Machinery.hs
+++ b/src/Generics/Regular/Rewriting/Machinery.hs
@@ -15,7 +15,7 @@
 
 module Generics.Regular.Rewriting.Machinery (
 
-  -- * Type class synonym summarizing generic functions
+  -- * Type class synonym summarizing generic functions.
   Rewrite,
 
   -- * Applying a rule specification to a term.
@@ -32,20 +32,21 @@
 import qualified Data.Map as M
 import Data.Maybe
 
-import Generics.Regular.Rewriting.Base
-import Generics.Regular.Rewriting.Representations
+import Generics.Regular.Base
+import Generics.Regular.Functions
 import Generics.Regular.Rewriting.Rules
 
 
 -----------------------------------------------------------------------------
--- Type class synonym summarizing generic functions
+-- Type class synonym summarizing generic functions.
 -----------------------------------------------------------------------------
 -- | The @Rewrite@ is a type class synonym, hiding some of the implementation
 -- details.
 --
 -- To be able to use the rewriting functions, the user is required to provide
 -- an instance of this type class.
-class (Regular a, Crush (PF a), GMap (PF a), GShow (PF a), Zip (PF a), LR (PF a)) => Rewrite a
+class (Regular a, CrushR (PF a), GMap (PF a), GShow (PF a)
+      , Zip (PF a), LR (PF a), Functor (PF a)) => Rewrite a
 
 
 -----------------------------------------------------------------------------
@@ -98,7 +99,7 @@
     Metavar x -> return (M.singleton x (term, toScheme term))
     PF r      ->
       fzip (,) r (from term) >>=
-      crush matchOne (return M.empty)
+      crushr matchOne (return M.empty)
   where
     matchOne (term1, term2) msubst = 
       do subst1 <- msubst
@@ -111,14 +112,14 @@
 -----------------------------------------------------------------------------
 
 -- | Applies a substitution to a term.
-apply :: Regular a => Subst a -> SchemeOf a -> SchemeOf a
+apply :: (Regular a, Functor (PF a)) => Subst a -> SchemeOf a -> SchemeOf a
 apply subst = foldScheme findMetavar pf
   where
     findMetavar x = maybe (metavar x) snd (M.lookup x subst)
 
 -- | Instantiates all the metavariables in a term, assuming that there are no
 -- unbound metavariables in the term.
-inst :: Regular a => Subst a -> SchemeOf a -> a
+inst :: (Regular a, Functor (PF a)) => Subst a -> SchemeOf a -> a
 inst subst = foldScheme findMetavar to
   where
     findMetavar x = 
diff --git a/src/Generics/Regular/Rewriting/Representations.hs b/src/Generics/Regular/Rewriting/Representations.hs
--- a/src/Generics/Regular/Rewriting/Representations.hs
+++ b/src/Generics/Regular/Rewriting/Representations.hs
@@ -12,75 +12,12 @@
 -- Stability   :  experimental
 -- Portability :  non-portable
 --
--- Summary: Types for structural representation.
+-- Summary: Types for structural representation. This module simply reexports
+-- "Generics.Regular.Base", and is provided for backwards-compatibility only.
 -----------------------------------------------------------------------------
 
 module Generics.Regular.Rewriting.Representations (
-
-  -- * Functorial structural representation types.
-  K (..),
-  Id (..),
-  Unit (..),
-  (:+:) (..),
-  (:*:) (..),
-  Con (..),
-
-  -- * Fixed-point type.
-  Fix (..),
-
-  -- * Type class capturing the structural representation of a type and the
-  -- | corresponding embedding-projection pairs.
-  Regular (..)
-  
-) where
-
-
------------------------------------------------------------------------------
--- Functorial structural representation types.
------------------------------------------------------------------------------
-
--- | Structure type for constant values.
-data K a r      = K a
-
--- | Structure type for recursive values.
-data Id r       = Id r
-
--- | Structure type for empty constructors.
-data Unit r     = Unit
-
--- | Structure type for alternatives in a type.
-data (f :+: g) r  = L (f r) | R (g r)
-
--- | Structure type for fields of a constructor.
-data (f :*: g) r = f r :*: g r
-
--- | Structure type to store the name of a constructor.
-data Con f r    = Con String (f r)
-
-infixr 6 :+:
-infixr 7 :*:
-
------------------------------------------------------------------------------
--- Fixed-point type.
------------------------------------------------------------------------------
-
--- | The well-known fixed-point type.
-newtype Fix f = In (f (Fix f))
-
-
------------------------------------------------------------------------------
--- Type class capturing the structural representation of a type and the
--- | corresponding embedding-projection pairs.
------------------------------------------------------------------------------
-
--- | The type class @Regular@ captures the structural representation of a 
--- type and the corresponding embedding-projection pairs.
---
--- To be able to use the rewriting functions, the user is required to provide
--- an instance of this type class.
-class Functor (PF a) => Regular a where
-  type PF a :: * -> *
-  from      :: a -> PF a a
-  to        :: PF a a -> a
-
+    module Generics.Regular.Base
+  ) where
 
+import Generics.Regular.Base
diff --git a/src/Generics/Regular/Rewriting/Rules.hs b/src/Generics/Regular/Rewriting/Rules.hs
--- a/src/Generics/Regular/Rewriting/Rules.hs
+++ b/src/Generics/Regular/Rewriting/Rules.hs
@@ -14,8 +14,6 @@
 --
 -- Summary: Functions for transforming a rule specification to a rule.
 --
-
-
 -----------------------------------------------------------------------------
 
 module Generics.Regular.Rewriting.Rules (
@@ -45,8 +43,8 @@
 
 import Data.List
 
-import Generics.Regular.Rewriting.Base
-import Generics.Regular.Rewriting.Representations
+import Generics.Regular.Base
+import Generics.Regular.Functions
 
 
 -----------------------------------------------------------------------------
@@ -101,7 +99,7 @@
 schemeView (In (R r))     = PF r
 
 -- | Recursively converts a value to a @SchemeOf@ value.
-toScheme :: Regular a => a -> SchemeOf a
+toScheme :: (Regular a, Functor (PF a)) => a -> SchemeOf a
 toScheme = pf . fmap toScheme . from
 
 -- | Folds a @Scheme@ value given a function to apply to metavariables and a
@@ -148,12 +146,16 @@
 
 -- | Transforms a rule specification to a rule and throws a runtime error if
 -- an unbound metavariable occurs in the right-hand side of the rule.
-rule :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Rule (Target r)
+rule :: ( Builder r, CrushR (PF (Target r))
+        , Functor (PF (Target r)), Zip (PF (Target r)))
+     => r -> Rule (Target r)
 rule = maybe (error "rule: unbound metavariable") id . ruleM
 
 -- | Transforms a rule specification to a rule and returns @Nothing@ if
 -- an unbound metavariable occurs in the right-hand side of the rule.
-ruleM :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Maybe (Rule (Target r))
+ruleM :: (  Builder r, CrushR (PF (Target r))
+          , Zip (PF (Target r)), Functor (PF (Target r)))
+      => r -> Maybe (Rule (Target r))
 ruleM f = checkMetavars $ foldr1 mergeRules rules
   where
     checkMetavars r 
@@ -163,7 +165,7 @@
         allElem xs ys = all (`elem` ys) xs
         lMetavars = collectMetavars (lhsR r) [] 
         rMetavars = collectMetavars (rhsR r) []
-        collectMetavars = foldScheme (:) (crush (.) id)
+        collectMetavars = foldScheme (:) (crushr (.) id)
     mergeRules x y = 
       mergeSchemes (lhsR x) (lhsR y) :~>
       mergeSchemes (rhsR x) (rhsR y)
diff --git a/src/Generics/Regular/Rewriting/Strategies.hs b/src/Generics/Regular/Rewriting/Strategies.hs
--- a/src/Generics/Regular/Rewriting/Strategies.hs
+++ b/src/Generics/Regular/Rewriting/Strategies.hs
@@ -15,19 +15,19 @@
 
 module Generics.Regular.Rewriting.Strategies (
 
-  -- * Apply a function to the children of a value
+  -- * Apply a function to the children of a value.
   once,
   one,
 
-  -- * Apply a (monadic) function exhaustively top-down
+  -- * Apply a (monadic) function exhaustively top-down.
   topdownM,
   topdown,
 
-  -- * Apply a (monadic) function exhaustively bottom-up
+  -- * Apply a (monadic) function exhaustively bottom-up.
   bottomupM,
   bottomup,
 
-  -- * Apply a (monadic) function to immediate children
+  -- * Apply a (monadic) function to immediate children.
   composM,
   compos
 
@@ -35,12 +35,12 @@
 
 import Control.Monad
 
-import Generics.Regular.Rewriting.Base
-import Generics.Regular.Rewriting.Representations
+import Generics.Regular.Base
+import Generics.Regular.Functions
 
 
 -----------------------------------------------------------------------------
--- Functions to apply a function to the children of a value
+-- Functions to apply a function to the children of a value.
 -----------------------------------------------------------------------------
 
 {-# INLINE once #-}
@@ -75,7 +75,7 @@
 
 
 -----------------------------------------------------------------------------
--- Apply a (monadic) function exhaustively top-down
+-- Apply a (monadic) function exhaustively top-down.
 -----------------------------------------------------------------------------
 
 {-# INLINE topdownM #-}
@@ -85,12 +85,12 @@
 
 {-# INLINE topdown #-}
 -- | Applies a function exhaustively in a top-down fashion
-topdown :: Regular a => (a -> a) -> a -> a
+topdown :: (Regular a, Functor (PF a)) => (a -> a) -> a -> a
 topdown f x = compos (topdown f) (f x)
 
 
 -----------------------------------------------------------------------------
--- Apply a (monadic) function exhaustively bottom-up
+-- Apply a (monadic) function exhaustively bottom-up.
 -----------------------------------------------------------------------------
 
 {-# INLINE bottomupM #-}
@@ -100,12 +100,12 @@
 
 {-# INLINE bottomup #-}
 -- | Applies a function exhaustively in a bottom-up fashion
-bottomup :: Regular a => (a -> a) -> a -> a
+bottomup :: (Regular a, Functor (PF a)) => (a -> a) -> a -> a
 bottomup f x = f (compos (bottomup f) x)
 
 
 -----------------------------------------------------------------------------
--- Apply a (monadic) function to immediate children
+-- Apply a (monadic) function to immediate children.
 -----------------------------------------------------------------------------
 
 {-# INLINE composM #-}
@@ -115,5 +115,5 @@
 
 {-# INLINE compos #-}
 -- | Applies a function to all the immediate children of a value.
-compos :: Regular a => (a -> a) -> a -> a
+compos :: (Regular a, Functor (PF a)) => (a -> a) -> a -> a
 compos f = to . fmap f . from