diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,28 @@
+Copyright (c) 2009 Universiteit Utrecht
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of Universiteit Utrecht nor the names of its contributors
+   may be used to endorse or promote products derived from this software without
+   specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE 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/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/examples/BadRules.hs b/examples/BadRules.hs
new file mode 100644
--- /dev/null
+++ b/examples/BadRules.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE TypeFamilies       #-}
+{-# LANGUAGE TypeOperators      #-}
+
+module BadRules where
+
+import Generics.Instant.Rewriting
+import Generics.Instant
+
+-- Test datatypes
+data Term = Val Int | Add Term Term | Mul Term Term
+  deriving (Show, Typeable, Eq)
+
+data RecTerm = Branch Int RecTerm RecTerm
+  deriving (Show, Typeable, Eq)
+
+-- SPVIew instances
+instance Representable Term where
+  type Rep Term = Var Int :+: Rec Term :*: Rec Term :+: Rec Term :*: Rec Term
+
+  from (Val i)   = L (Var i)
+  from (Add x y) = R (L (Rec x :*: Rec y))
+  from (Mul x y) = R (R (Rec x :*: Rec y))
+
+  to (L (Var i))               = Val i
+  to (R (L (Rec x :*: Rec y))) = Add x y
+  to (R (R (Rec x :*: Rec y))) = Mul x y
+
+instance Representable RecTerm where
+  type Rep RecTerm = Var Int :*: Rec RecTerm :*: Rec RecTerm
+  from (Branch i x y)            = Var i :*: Rec x :*: Rec y
+  to (Var i :*: Rec x :*: Rec y) = Branch i x y
+
+-- Rewritable instances
+instance Rewritable Term
+instance Rewritable RecTerm
+
+
+-- Superfluous metavariable
+-- Result: *** Exception: invalid rule
+badApplication1 :: Rule Term
+badApplication1 = synthesise badApplication1Template
+    where badApplication1Template :: Term -> Term -> Term -> Template Term
+          badApplication1Template x y z = Add x y +-> Add y x
+
+-- Unbound metavariable in right-hand side
+-- Result: *** Exception: user error (merging failure)
+badApplication2 :: Rule Term
+badApplication2 = synthesise badApplication2Template
+    where badApplication2Template x y = Add x x +-> Add y x
+
+-- Unbound metavariable in guard
+-- Result: *** Exception: user error (merging failure)
+badApplication3 :: Rule Term
+badApplication3 = synthesise badApplication3Template
+    where badApplication3Template x y = Add x x +-> Add y x // const True y
+
+
+-- Metavariable has no possible finite values
+-- Result: would loop, but it is rejected at the type level
+{-
+badApplication4 :: Rule RecTerm
+badApplication4 = synthesise badApplication4Template
+    where badApplication4Template i x y = Branch i x y +-> Branch i y x
+-}
+
+main = (map validate [badApplication1, badApplication2, badApplication3])
diff --git a/examples/Test.hs b/examples/Test.hs
new file mode 100644
--- /dev/null
+++ b/examples/Test.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE DeriveDataTypeable     #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE FlexibleInstances      #-}
+
+module Test where
+
+import Generics.Instant
+import Generics.Instant.Rewriting
+
+-------------------------------------------------------------------------------
+-- Simple Datatype
+-------------------------------------------------------------------------------
+
+-- Example datatype
+data Exp = Const Int | Plus Exp Exp deriving (Show, Typeable, Eq)
+
+-- Representable instance
+instance Representable Exp where
+  type Rep Exp = Var Int :+: Rec Exp :*: Rec Exp
+
+  from (Const n)   = L (Var n)
+  from (Plus e e') = R (Rec e :*: Rec e')
+
+  to (L (Var n))            = Const n
+  to (R (Rec e :*: Rec e')) = Plus e e'
+
+-- Required Rewritable instance
+instance Rewritable Exp
+
+-- An example rule
+silly :: Rule Exp
+silly = synthesise $ \e n ->
+           Plus e (Const n)  +->  e    // n == 0
+
+-- Applying the rewriting mechanism
+test1 :: String
+test1 = show $ rewrite silly (Plus (Const 2) (Const 0))
+
+-------------------------------------------------------------------------------
+-- Mutually recursive datatypes
+-------------------------------------------------------------------------------
+
+data Decl = None | Seq Decl Decl | Assign String Expr
+  deriving (Show, Typeable, Eq)
+
+data Expr = V String | Lam String Expr | App Expr Expr | Let Decl Expr
+  deriving (Show, Typeable, Eq)
+
+instance Representable Decl where
+  type Rep Decl = U :+: Rec Decl :*: Rec Decl :+: Var String :*: Rec Expr
+
+  from None         = L U
+  from (Seq d1 d2)  = R (L (Rec d1 :*: Rec d2))
+  from (Assign v e) = R (R (Var v :*: Rec e))
+
+  to (L U)                       = None
+  to (R (L (Rec d1 :*: Rec d2))) = Seq d1 d2
+  to (R (R (Var v :*: Rec e)))   = Assign v e
+
+instance Representable Expr where
+  type Rep Expr =     Var String :+: Var String :*: Rec Expr
+                 :+: Rec Expr :*: Rec Expr :+: Rec Decl :*: Rec Expr
+
+  from (V x)     = L (Var x)
+  from (Lam v e) = R (L (Var v :*: Rec e))
+  from (App f e) = R (R (L (Rec f :*: Rec e)))
+  from (Let d e) = R (R (R (Rec d :*: Rec e)))
+
+  to (L (Var x))                   = V x
+  to (R (L (Var v :*: Rec e)))     = Lam v e
+  to (R (R (L (Rec f :*: Rec e)))) = App f e
+  to (R (R (R (Rec d :*: Rec e)))) = Let d e
+              
+instance Rewritable Decl
+instance Rewritable Expr
+instance Rewritable [Char]
+
+remLet :: Rule Expr
+remLet = synthesise $ \x e -> Let (Assign x e) (V x) +-> e
+
+remX :: Rule Decl
+remX = synthesise $ \v e -> Assign v e +-> None // v == "x"
+
+test2 :: String
+test2 = show $ rewrite remLet (Let (Assign "x" (V "y")) (V "x"))
+
+test3 :: String
+test3 = show $ rewrite remX (Assign "x" (V "y"))
+
+
+main = print [test1, test2, test3]
diff --git a/guarded-rewriting.cabal b/guarded-rewriting.cabal
new file mode 100644
--- /dev/null
+++ b/guarded-rewriting.cabal
@@ -0,0 +1,62 @@
+category:               Generics
+copyright:              (c) 2010 Universiteit Utrecht
+name:                   guarded-rewriting
+version:                0.1
+license:                BSD3
+license-file:           LICENSE
+author:                 Thomas van Noort, Alexey Rodriguez Yakushev,
+                        Stefan Holdermans, Johan Jeuring, Bastiaan Heeren,
+                        Jose Pedro Magalhaes
+maintainer:             generics@haskell.org
+homepage:               http://www.cs.uu.nl/wiki/GenericProgramming/GuardedRewriting
+synopsis:               Datatype-generic rewriting with preconditions
+description:               
+
+  This package provides rewriting functionality for datatypes. Most forms of 
+  datatypes are supported, including parametrized and mutually-recursive.
+  .
+  This library has been described in the paper:
+  .
+  *  Thomas van Noort, Alexey Rodriguez Yakushev, Stefan Holdermans, 
+     Johan Jeuring, Bastiaan Heeren, Jose Pedro Magalhaes.
+     /A Lightweight Approach to Datatype-Generic Rewriting./
+     Journal of Functional Programming, Special Issue on Generic Programming, 
+     2010.
+  .
+  More information about this library can be found at
+  <http://www.cs.uu.nl/wiki/GenericProgramming/GuardedRewriting>.
+
+stability:              provisional
+build-type:             Simple
+cabal-version:          >= 1.6
+tested-with:            GHC == 6.10.4, GHC == 6.12.1
+extra-source-files:     examples/BadRules.hs,
+                        examples/Test.hs,
+                        performance/Main.hs,
+                        performance/Makefile,
+                        performance/Common/*.hs,
+                        performance/Gen/Rules.hs,
+                        performance/Gen/Arith/*.hs,
+                        performance/Gen/DNF1/*.hs,
+                        performance/Gen/DNF2/*.hs,
+                        performance/Gen/DNF3/*.hs,
+                        performance/Gen/DNF4/*.hs,
+                        performance/PM/Rules.hs,
+                        performance/PM/Arith/*.hs,
+                        performance/PM/DNF1/*.hs,
+                        performance/PM/DNF2/*.hs,
+                        performance/PM/DNF3/*.hs,
+                        performance/PM/DNF4/*.hs,
+                        performance/Uni/Rules.hs,
+                        performance/Uni/DNF1/*.hs,
+                        performance/Uni/DNF2/*.hs,
+                        performance/Uni/DNF3/*.hs,
+                        performance/Uni/DNF4/*.hs,
+                        performance/out/description.txt,
+                        performance/bin/description.txt
+
+library
+  ghc-options:            -Wall
+  build-depends:          base >= 3.0 && < 5, instant-generics >= 0.1 && < 1.0
+  exposed-modules:        Generics.Instant.Rewriting
+  hs-source-dirs:         src
diff --git a/performance/Common/Arith.hs b/performance/Common/Arith.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/Arith.hs
@@ -0,0 +1,303 @@
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Common.Arith where
+
+import Control.Monad
+import Data.Ratio
+import Data.Maybe
+import Data.Typeable
+import Test.QuickCheck
+import System.Random
+import Common.GuardedRewriting
+
+propGen :: Int -> Gen (Prop (Equation Expr))
+propGen n
+   | n == 0 = frequency 
+        [ (5, liftM VarP (sized eqGen))
+        , (1, return T)
+        , (1, return F)
+        ]
+   | otherwise = oneof 
+        [ propGen 0
+        , liftM2 (:\/:) rec rec
+        , liftM2 (:/\:) rec rec
+        , liftM  Not    rec 
+        ]
+ where
+   rec = propGen (n `div` 2)
+
+eqGen :: Int -> Gen (Equation Expr)
+eqGen n = liftM2 (:==:) (exprGen n) constGen
+
+-- Expression with exactly one variable
+exprGen :: Int -> Gen Expr
+exprGen 0 = return (Varia "x")
+exprGen n = oneof
+   [ return (Varia "x")
+   , liftM2 (:+:) rec constGen, liftM2 (:+:) constGen rec
+   , liftM2 (:-:) rec constGen, liftM2 (:-:) constGen rec
+   , liftM2 (:**:) rec constGen, liftM2 (:**:) constGen rec
+   , liftM2 (:/:) rec constGen, liftM2 (:/:) constGen rec
+   , liftM2 (\a n -> a :^: Const (fromInteger (succ $ abs n))) rec arbitrary
+   ]
+ where
+   rec = exprGen (n `div` 2)
+   
+constGen :: Gen Expr
+constGen = liftM (Const . fromInteger) arbitrary
+
+isSolved :: Prop (Equation Expr) -> Bool
+isSolved prop =
+   case prop of
+      p :\/: q -> isSolved p && isSolved q
+      p :/\: q -> isSolved p && isSolved q
+      Not p    -> isSolved p
+      VarP p    -> isSolvedEq p 
+      _        -> True
+
+isSolvedEq :: Equation Expr -> Bool
+isSolvedEq (Varia _ :==: b) = noVaria b
+isSolvedEq (a       :==: b) = noVaria a && noVaria b
+
+repeatM :: Monad m => m a -> m [a]
+repeatM m = liftM2 (:) m (repeatM m)
+
+formula :: [Prop (Equation Expr)]
+formula = generate 100 (mkStdGen 280578) (repeatM (sized propGen))
+
+formulas :: [Prop (Equation Expr)]
+formulas = take 10000 formula
+
+-----------------------------------
+
+data Prop a = VarP a | T | F 
+            | Prop a :\/: Prop a 
+            | Prop a :/\: Prop a 
+            | Not (Prop a)
+   deriving (Show, Typeable, Eq)
+
+data Equation a = a :==: a
+   deriving (Show, Typeable, Eq)
+
+infix  2 :==: 
+infixl 6 :+:, :-: 
+infixl 7 :**:, :/: 
+infixr 8 :^:
+
+data Expr = Const Rational
+          | Varia String
+          | Expr :+: Expr
+          | Expr :-: Expr
+          | Expr :**: Expr
+          | Expr :/: Expr
+          | Expr :^: Expr
+   deriving (Eq, Show, Typeable)
+
+instance Functor Prop where
+   fmap f (VarP a)    = VarP (f a)
+   fmap f T          = T
+   fmap f F          = F
+   fmap f (p :\/: q) = fmap f p :\/: fmap f q
+   fmap f (p :/\: q) = fmap f p :/\: fmap f q
+   fmap f (Not p)    = Not (fmap f p)
+   
+instance Functor Equation where
+   fmap f (a :==: b) = f a :==: f b
+
+
+isEven, isOdd :: Rational -> Bool
+isEven r = denominator r == 1 && even (numerator r)
+isOdd  r = denominator r == 1 && odd  (numerator r)
+
+hasDivisionByZero :: Expr -> Bool
+hasDivisionByZero expr =
+   case expr of
+      _ :/: Const 0 -> True
+      a :+: b  -> hasDivisionByZero a || hasDivisionByZero b
+      a :-: b  -> hasDivisionByZero a || hasDivisionByZero b
+      a :**: b -> hasDivisionByZero a || hasDivisionByZero b
+      a :/: b  -> hasDivisionByZero a || hasDivisionByZero b
+      a :^: b  -> hasDivisionByZero a || hasDivisionByZero b
+      _ -> False
+
+noVaria, hasVaria :: Expr -> Bool
+noVaria = not . hasVaria
+hasVaria expr = 
+   case expr of
+      Const _  -> False
+      Varia _  -> True
+      a :+: b  -> hasVaria a || hasVaria b
+      a :-: b  -> hasVaria a || hasVaria b
+      a :**: b -> hasVaria a || hasVaria b
+      a :/: b  -> hasVaria a || hasVaria b
+      a :^: b  -> hasVaria a || hasVaria b
+
+applyD :: (a -> Maybe a) -> a -> a
+applyD f a = fromMaybe a (f a)
+
+applyOne :: [a -> Maybe a] -> a -> Maybe a
+applyOne fs a = case mapMaybe ($ a) fs of
+                   hd:_ -> Just hd
+                   _    -> Nothing
+                   
+
+applyBin :: (a -> Maybe a) -> (a -> a -> b) -> a -> a -> Maybe b
+applyBin rec op a b = 
+   case (rec a, rec b) of
+      (Nothing, Nothing) -> Nothing
+      (ma, mb) -> Just (fromMaybe a ma `op` fromMaybe b mb)
+
+somewhereProp :: (Prop a -> Maybe (Prop a)) -> Prop a -> Maybe (Prop a)
+somewhereProp f = rec
+ where
+   rec prop = 
+      let make op a b = case applyBin rec op a b of
+                           Just c  -> Just (applyD f c)
+                           Nothing -> f prop
+      in case prop of
+            p :\/: q -> make (:\/:) p q
+            p :/\: q -> make (:/\:) p q
+            Not p    -> case rec p of
+                           Just p2 -> Just $ applyD f p2
+                           Nothing -> f prop
+            _        -> f prop
+
+somewhereExpr :: (Expr -> Maybe Expr) -> Expr -> Maybe Expr
+somewhereExpr f = rec 
+ where
+   rec expr = 
+      let make2 op a b = case applyBin rec op a b of
+                           Just c  -> Just (applyD f c)
+                           Nothing -> f expr
+      in case expr of
+            a :+: b  -> make2 (:+:) a b
+            a :-: b  -> make2 (:-:) a b
+            a :**: b -> make2 (:**:) a b
+            a :/: b  -> make2 (:/:) a b
+            a :^: b  -> make2 (:^:) a b
+            _        -> f expr
+
+liftToEq :: (a -> Maybe a) -> Equation a -> Maybe (Equation a)
+liftToEq f (a :==: b) =
+   case (f a, f b) of
+      (Nothing, Nothing) -> Nothing
+      (ma, mb) -> Just $ fromMaybe a ma :==: fromMaybe b mb
+
+liftToProp :: (a -> Maybe a) -> Prop a -> Maybe (Prop a)
+liftToProp f = rec 
+ where
+   rec prop =
+      case prop of
+         p :\/: q  -> applyBin rec (:\/:) p q
+         p :/\: q  -> applyBin rec (:/\:) p q
+         Not p     -> liftM Not (rec p)
+         VarP a    -> liftM VarP (f a)
+         _         -> Nothing
+
+transformExpr :: (Expr -> Expr) -> Expr -> Expr
+transformExpr f = rec 
+ where
+   rec expr = f $
+      case expr of
+         a :+: b  -> rec a :+: rec b
+         a :-: b  -> rec a :-: rec b
+         a :**: b -> rec a :**: rec b
+         a :/: b  -> rec a :/: rec b
+         a :^: b  -> rec a :^: rec b
+         _        -> expr
+
+simplify :: Expr -> Expr
+simplify = transformExpr f
+ where
+   f (Const a :+: Const b)  = Const (a+b)
+   f (Const a :-: Const b)  = Const (a-b)
+   f (Const a :**: Const b) = Const (a*b)
+   f (Const a :/: Const b)  = Const (a/b)
+   f (Const a :^: Const b) | denominator b == 1 
+      = Const (a^numerator b)
+   f a = a
+
+-- Also counts the number of rules that hvae been applied (successfully)
+solve :: [Prop (Equation Expr) -> Maybe (Prop (Equation Expr))]
+         -> Prop (Equation Expr) -> Prop (Equation Expr)
+solve rules = rec where
+   rec p = 
+      case applyOne rules p of
+         Just a  -> rec a
+         Nothing -> p
+
+-- Examples
+ex :: Prop (Equation Expr)
+ex = VarP p :\/: VarP q
+ where
+   x = Varia "x"
+   p = (((x :-: Const 3) :^: Const 2) :/: Const 4) :==: Const 25
+   q = (Const 1 :-: (Const 2 :/: (Const 1 :+: (x :**: Const 5)))) :==: Const 4 
+ex2 = ((VarP (Const (5 % 1) :/: Varia "x" :==: Const (4 % 1)) :\/: VarP ((Const (6 % 1)
+ :/: (Const ((-4) % 1) :+: Varia "x")) :^: Const (3 % 1) :==: Const ((-6) % 1)))
+ :\/: VarP (Const ((-7) % 1) :**: (Const ((-5) % 1) :**: Varia "x") :==: Const (4 %
+ 1))) :\/: (VarP (Varia "x" :==: Const ((-7) % 1)) :\/: VarP (Const (0 % 1) :/: ((Varia "x" :-: Const (0 % 1)) :+: Const (2 % 1)) :==: Const ((-3) % 1)))
+ 
+-- Generic representation
+instance (Representable a) => Representable (Prop a) where
+  type Rep (Prop a) =      Var a
+                      :+: U
+                      :+: U
+                      :+: Rec (Prop a) :*: Rec (Prop a)
+                      :+: Rec (Prop a) :*: Rec (Prop a)
+                      :+: Rec (Prop a)
+  
+  from (VarP x)   = L (Var x)
+  from T          = R (L U)
+  from F          = R (R (L U))
+  from (p :\/: q) = R (R (R (L (Rec p :*: Rec q))))
+  from (p :/\: q) = R (R (R (R (L (Rec p :*: Rec q)))))
+  from (Not p)    = R (R (R (R (R (Rec p)))))
+  
+  to (L (Var x))                           = VarP x
+  to (R (L U))                             = T
+  to (R (R (L U)))                         = F
+  to (R (R (R (L (Rec p :*: Rec q)))))     = p :\/: q
+  to (R (R (R (R (L (Rec p :*: Rec q)))))) = p :/\: q
+  to (R (R (R (R (R (Rec p))))))           = p
+
+instance (Representable a) => Representable (Equation a) where
+  type Rep (Equation a) = Var a :*: Var a
+  
+  from (x :==: y) = Var x :*: Var y
+  to (Var x :*: Var y) = x :==: y
+
+instance Representable Expr where
+  type Rep Expr =      Var Rational
+                  :+: Var String
+                  :+: Rec Expr :*: Rec Expr
+                  :+: Rec Expr :*: Rec Expr
+                  :+: Rec Expr :*: Rec Expr
+                  :+: Rec Expr :*: Rec Expr
+                  :+: Rec Expr :*: Rec Expr
+  
+  from (Const r) = L (Var r)
+  from (Varia s) = R (L (Var s))
+  from (e1 :+: e2)  = R (R (L (Rec e1 :*: Rec e2)))
+  from (e1 :-: e2)  = R (R (R (L (Rec e1 :*: Rec e2))))
+  from (e1 :**: e2) = R (R (R (R (L (Rec e1 :*: Rec e2)))))
+  from (e1 :/: e2)  = R (R (R (R (R (L (Rec e1 :*: Rec e2))))))
+  from (e1 :^: e2)  = R (R (R (R (R (R (Rec e1 :*: Rec e2))))))
+  
+  to (L (Var r)) = Const r
+  to (R (L (Var s))) = Varia s
+  to (R (R (L (Rec e1 :*: Rec e2)))) = e1 :+: e2
+  to (R (R (R (L (Rec e1 :*: Rec e2))))) = e1 :-: e2
+  to (R (R (R (R (L (Rec e1 :*: Rec e2)))))) = e1 :**: e2
+  to (R (R (R (R (R (L (Rec e1 :*: Rec e2))))))) = e1 :/: e2
+  to (R (R (R (R (R (R (Rec e1 :*: Rec e2))))))) = e1 :^: e2
+
+ 
+instance (Rewritable a) => Rewritable (Prop a)
+instance (Rewritable a) => Rewritable (Equation a)
+instance Rewritable Expr
+instance Rewritable String
diff --git a/performance/Common/DNF.hs b/performance/Common/DNF.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/DNF.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -cpp #-}
+
+module Common.DNF (runStrategy, dnf1, dnf2, dnf3, dnf4, reportTick) where
+
+import Prelude hiding (repeat)
+import Common.LogicRules()
+import Common.Logic
+import System.IO.Unsafe
+import Data.IORef
+
+{- Which rules -}
+#ifdef __PM
+import PM.Rules
+#endif
+#ifdef __Uni
+import Uni.Rules
+#endif
+#ifdef __Gen
+import Gen.Rules
+#endif
+
+
+import Common.Once
+
+counting = False
+
+
+type Strategy a = a -> [a]
+
+somewhere s = once s
+(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
+try s = s <|> (notS s)
+alternatives = foldr (<|>) (const [])
+notS s a = if null (s a) then [a] else []
+
+runStrategy :: Strategy a -> a -> a
+runStrategy s p = case s p of
+                     hd:_ -> hd
+                     _    -> p      
+
+data Count = C !Integer !Integer deriving Show
+
+tickRef :: IORef Count
+tickRef = unsafePerformIO (newIORef (C 0 0))
+
+reportTick :: IO ()
+reportTick = if counting then readIORef tickRef >>= print else return ()
+
+tick :: (a -> [b]) -> a -> [b]
+tick r a = if not counting then r a else unsafePerformIO $ do
+   xs <- return (r a)
+   c  <- readIORef tickRef
+   seq c (writeIORef tickRef (update (null xs) c))
+   return xs
+
+update :: Bool -> Count -> Count
+update b (C x y)
+   | b         = C (x+1) y
+   | otherwise = C x (y+1)
+
+---------------------------------------------------------------
+
+allRules = conRules ++ defRules ++ notRules ++ disRules
+conRules = map tick [ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd, ruleFalseZeroAnd, ruleNotBoolConst, ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl]
+defRules = map tick [ruleDefImpl, ruleDefEquiv]
+notRules = map tick [ruleDeMorganAnd, ruleDeMorganOr, ruleNotNot]
+disRules = map tick [ruleAndOverOr]
+
+eliminateConstants :: Strategy (Logic)
+eliminateConstants = repeat $ somewhere $ alternatives conRules
+
+eliminateImplEquiv :: Strategy (Logic)
+eliminateImplEquiv = repeat $ somewhere $ alternatives defRules
+
+eliminateNots :: Strategy (Logic)
+eliminateNots = repeat $ somewhere $ alternatives notRules
+
+
+dnf1 :: Strategy (Logic)
+dnf1 =  repeat (somewhere (alternatives allRules))
+
+dnf2 :: Strategy (Logic)
+dnf2 =  repeat (somewhere (alternatives conRules))
+     <*> repeat (somewhere (alternatives defRules))
+     <*> repeat (somewhere (alternatives notRules))
+     <*> repeat (somewhere (alternatives disRules))
+
+dnf3 :: Strategy (Logic)
+dnf3 =  repeat (oneTD (alternatives conRules))
+     <*> repeat (oneBU (alternatives defRules))
+     <*> repeat (oneTD (alternatives notRules))
+     <*> repeat (somewhere (alternatives disRules))
+
+dnf4 :: Strategy (Logic)
+dnf4 =   fullBU (repeat (alternatives (conRules ++ defRules)))
+     <*> fullTD (repeat (alternatives notRules))
+     <*> fullBU (try (alternatives disRules <*> fullTD (try (alternatives disRules))))
diff --git a/performance/Common/GuardedRewriting.hs b/performance/Common/GuardedRewriting.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/GuardedRewriting.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Common.GuardedRewriting (
+    module Generics.Instant.Rewriting,
+    module Generics.Instant
+  ) where
+
+import Data.Ratio
+
+import Generics.Instant.Rewriting
+import Generics.Instant
+
+
+instance Extensible Rational where
+  newtype Ext Rational gam = ExtRational Rational
+  toExt = ExtRational
+
+instance Matchable Rational where
+  match' (ExtRational r) r' | r == r'   = return empty
+                            | otherwise = fail "structure mismatch"
+
+instance Substitutable Rational where
+  subst' _ (ExtRational r) = return r
+
+instance Sampleable Rational where
+  left'  = 1
+  right' = 2
+
+instance Empty Rational where
+  empty' = 1
+
+instance Diffable Rational where
+  diff' (ExtRational r) (ExtRational r') | r == r'   = Just (ExtRational r)
+                                         | otherwise = Nothing
+
+instance Validatable Rational
+
+type instance Finite Rational = True
+
+instance Rewritable Rational
+
+instance Representable Rational where
+  type Rep Rational = Rational
+  from = id
+  to = id
diff --git a/performance/Common/Logic.hs b/performance/Common/Logic.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/Logic.hs
@@ -0,0 +1,245 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE TypeFamilies       #-}
+{-# LANGUAGE TypeOperators      #-}
+{-# LANGUAGE FlexibleInstances  #-}
+
+-----------------------------------------------------------------------------
+-- 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 Common.Logic where
+
+import Data.List
+import Data.Maybe
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Data.Typeable
+import Data.Data
+import Common.GuardedRewriting
+
+infixr 1 :<->:
+infixr 2 :->: 
+infixr 3 :||: 
+infixr 4 :&&:
+
+-- | The data type Logic is the abstract syntax for the domain
+-- | of logic expressions.
+data Logic = VarL 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, Typeable, Data)
+
+-- | 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
+         VarL 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
+      VarL _       -> True
+      Not (VarL _) -> 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]
+
+-- | 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 $ (VarL "a" :||: VarL "b") :||: (VarL "c" :||: VarL "d" :||: VarL "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
+      (VarL x, VarL 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
+
+-----------------------------------------------------------
+--- Unification
+
+type Substitution = M.Map Char Logic
+
+isMetaVar :: Logic -> Maybe Char
+isMetaVar (VarL ['_', c]) = Just c
+isMetaVar _ = Nothing
+
+metaVars :: [Logic]
+metaVars = [ VarL ['_', c] | c <- ['a' .. 'z'] ]
+
+(|->) :: Substitution -> Logic -> Logic
+(|->) sub = foldLogic (var, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)
+ where 
+   var s = case isMetaVar (VarL s) of
+              Just i -> fromMaybe (VarL s) (M.lookup i sub)
+              _      -> VarL 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
+            (VarL x, VarL 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)
+
+
+instance Rewritable Logic
+instance Rewritable [Char]
+
+instance Representable Logic where
+  type Rep Logic =
+        Var String
+    :+: Rec Logic :*: Rec Logic
+    :+: Rec Logic :*: Rec Logic
+    :+: Rec Logic :*: Rec Logic
+    :+: Rec Logic :*: Rec Logic
+    :+: Rec Logic
+    :+: U
+    :+: U
+
+  from (VarL x)    = L (Var x)
+  from (p :<->: q) = R (L (Rec p :*: Rec q))
+  from (p :->: q)  = R (R (L (Rec p :*: Rec q)))
+  from (p :&&: q)  = R (R (R (L (Rec p :*: Rec q))))
+  from (p :||: q)  = R (R (R (R (L (Rec p :*: Rec q)))))
+  from (Not p)     = R (R (R (R (R (L (Rec p))))))
+  from T           = R (R (R (R (R (R (L U))))))
+  from F           = R (R (R (R (R (R (R U))))))
+
+  to (L (Var x))                           = VarL x
+  to (R (L (Rec p :*: Rec q)))             = p :<->: q
+  to (R (R (L (Rec p :*: Rec q))))         = p :->: q
+  to (R (R (R (L (Rec p :*: Rec q)))))     = p :&&: q
+  to (R (R (R (R (L (Rec p :*: Rec q)))))) = p :||: q
+  to (R (R (R (R (R (L (Rec p)))))))       = Not p
+  to (R (R (R (R (R (R (L U)))))))         = T
+  to (R (R (R (R (R (R (R U)))))))         = F
diff --git a/performance/Common/LogicGenerator.hs b/performance/Common/LogicGenerator.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/LogicGenerator.hs
@@ -0,0 +1,61 @@
+-----------------------------------------------------------------------------
+-- 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 Common.LogicGenerator where
+
+import Common.Logic
+import Control.Monad
+import Data.Char
+import Test.QuickCheck hiding (defaultConfig)
+import System.Random
+
+-----------------------------------------------------------
+--- QuickCheck generator
+
+-- 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 . VarL) ["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
+
+instance Arbitrary Logic where
+   arbitrary = sized (arbLogic True)
+   coarbitrary logic = 
+      case logic of
+         VarL 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
+
+repeatM :: Monad m => m a -> m [a]
+repeatM m = liftM2 (:) m (repeatM m)
+
+formula :: [Logic]
+formula = generate 100 (mkStdGen 280578) (repeatM arbitrary)
diff --git a/performance/Common/LogicRules.hs b/performance/Common/LogicRules.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/LogicRules.hs
@@ -0,0 +1,231 @@
+{-# OPTIONS -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- 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 the distribution.
+-----------------------------------------------------------------------------
+-- |
+-- Maintainer  :  bastiaan.heeren@ou.nl
+-- Stability   :  provisional
+-- Portability :  portable (depends on ghc)
+--
+-----------------------------------------------------------------------------
+module Common.LogicRules where
+
+import qualified Data.Set as S
+import Common.Logic
+import Common.GuardedRewriting
+
+
+p |- q = p +-> q
+makeRuleList _ = map synthesise
+buggyRule = id
+makeRule _ = synthesise
+
+{- 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
+                  ] -}
+                  
+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)) --note the firstNot both formulas!  
+    ]
+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/performance/Common/LogicStrategies.hs b/performance/Common/LogicStrategies.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/LogicStrategies.hs
@@ -0,0 +1,124 @@
+-----------------------------------------------------------------------------
+-- 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 Common.LogicStrategies where
+
+import Prelude hiding (repeat)
+import Common.LogicRules
+import Common.Logic
+import Common.LogicGenerator
+import Test.QuickCheck hiding (label)
+import System.Random
+import Common.GuardedRewriting
+import Control.Monad
+
+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 []
+
+-- --------------------------------------
+-- Strategies
+-- --------------------------------------
+-- Same monad to that in the SYB3 paper
+data S m a = S a (m a)
+
+instance MonadPlus m => Monad (S m) where
+  return x = S x mzero
+  (S x xs) >>= k
+    = S r (rs1 `mplus` rs2)
+      where
+        S r rs1 = k x
+        rs2 = do x <- xs
+                 let S r _ = k x
+                 return r
+
+-- This is like Stratego's one.
+-- It applies f to one of the immediate children of x.
+{-
+one :: (Rewritable a, MonadPlus m, Functor m) => (a -> m a) -> a -> m a
+one f x = fmap (from . In) rs
+  where
+    S _ rs = fmapM try_f $ out $ to x
+    try_f x = S x (f_str x)
+    f_str = fmap to . f . from
+-}
+
+-- Apply f once to one of the nodes of x
+-- Mirrors the corresponding definition in Stratego
+once :: (Rewritable a, MonadPlus m, Functor m) => (a -> m a) -> a -> m a
+once f x = f x `mplus` one (once f) x
+
+
+-- applies a strategy at one location
+-- see http://ideas.cs.uu.nl/trac/browser/Feedback/trunk/src/Common/Strategy.hs
+somewhere :: Rewritable a => Strategy a -> Strategy a
+somewhere = once
+
+lift :: Rewritable a => Rule' a -> Strategy a
+lift r = (:[]) . rewrite' r
+
+liftl :: Rewritable a => [Rule' a] -> Strategy a
+liftl = alternatives . map lift
+
+eliminateConstants :: Strategy (Logic)
+eliminateConstants = repeat $ somewhere $
+   alternatives $
+      [ liftl ruleFalseZeroOr, liftl ruleTrueZeroOr, liftl ruleTrueZeroAnd
+      , liftl ruleFalseZeroAnd, liftl ruleNotBoolConst, liftl ruleFalseInEquiv
+      , liftl ruleTrueInEquiv, liftl ruleFalseInImpl, liftl ruleTrueInImpl
+      ]
+
+eliminateImplEquiv :: Strategy (Logic)
+eliminateImplEquiv = repeat $ somewhere $
+          lift ruleDefImpl
+      <|> lift ruleDefEquiv
+      
+eliminateNots :: Strategy (Logic)
+eliminateNots = repeat $ somewhere $ 
+          lift ruleDeMorganAnd
+      <|> lift ruleDeMorganOr
+      <|> lift ruleNotNot
+      
+orToTop :: Strategy (Logic)
+orToTop = repeat $ somewhere $ liftl 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 == from (to p)
+
+checks :: IO ()
+checks = do
+   quickCheck propView
+   quickCheck propSound
+
+main :: IO ()
+main = print $ all checkOne [0..1000]
+ where
+   checkOne n = 
+      propSound (generate n (mkStdGen n) generateLogic)
diff --git a/performance/Common/Once.hs b/performance/Common/Once.hs
new file mode 100644
--- /dev/null
+++ b/performance/Common/Once.hs
@@ -0,0 +1,47 @@
+module Common.Once (once, oneTD, oneBU, fullTD, fullBU) where
+
+import Common.Logic
+
+once = somewhere
+
+somewhere :: (Logic -> [Logic]) -> Logic -> [Logic]
+somewhere f p = f p ++ one (somewhere f) p
+
+oneTD :: (Logic -> [Logic]) -> Logic -> [Logic]
+oneTD f p = f p +> one (oneTD f) p
+
+oneBU :: (Logic -> [Logic]) -> Logic -> [Logic]
+oneBU f p = one (oneBU f) p +> f p
+
+fullTD :: (Logic -> [Logic]) -> Logic -> [Logic]
+fullTD f p = [ p'' | p' <- f p, p'' <- full (fullTD f) p' ]
+
+fullBU :: (Logic -> [Logic]) -> Logic -> [Logic]
+fullBU f p = [ p'' | p' <- full (fullBU f) p, p'' <- f p' ] 
+
+one :: (Logic -> [Logic]) -> Logic -> [Logic]
+one f p = 
+   case p of
+      p :->:  q -> make (:->:  q) p ++ make (p :->:)  q
+      p :<->: q -> make (:<->: q) p ++ make (p :<->:) q
+      p :&&:  q -> make (:&&:  q) p ++ make (p :&&:)  q
+      p :||:  q -> make (:||:  q) p ++ make (p :||:)  q
+      Not p     -> make Not p
+      _ -> []
+ where
+   make :: (Logic -> Logic) -> Logic -> [Logic]
+   make g = map g . f
+
+full :: (Logic -> [Logic]) -> Logic -> [Logic]
+full f p = 
+   case p of
+      p :->:  q -> [ p' :->:  q' | p' <- f p, q' <- f q ] 
+      p :<->: q -> [ p' :<->: q' | p' <- f p, q' <- f q ] 
+      p :&&:  q -> [ p' :&&:  q' | p' <- f p, q' <- f q ] 
+      p :||:  q -> [ p' :||:  q' | p' <- f p, q' <- f q ] 
+      Not p     -> [ Not p'      | p' <- f p ] 
+      _ -> [p]
+
+(+>) :: [a] -> [a] -> [a]
+[] +> ys = ys
+xs +> _  = xs
diff --git a/performance/Gen/Arith/Rules.hs b/performance/Gen/Arith/Rules.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/Arith/Rules.hs
@@ -0,0 +1,148 @@
+module Gen.Arith.Rules where
+
+import Common.Arith
+import Common.GuardedRewriting
+import Test.QuickCheck
+import Data.Maybe (isJust, fromJust, catMaybes)
+
+type PropRule = Rule (Prop (Equation Expr))
+type EqRule   = Rule (Equation Expr)
+type ExprRule = Rule Expr
+
+
+go = quickCheck $ forAll (sized propGen) (isSolved . solve rules)
+
+rules :: [Prop (Equation Expr) -> Maybe (Prop (Equation Expr))]
+rules = [ somewhereProp $ applyOne (map rewriteM propRules)
+        , liftToProp $ applyOne (map rewriteM eqRules)
+        , liftToProp $ liftToEq $ somewhereExpr $ applyOne (map rewriteM exprRules)
+        ]
+ where
+   propRules :: [PropRule]
+   propRules = 
+      [ coverPowerEven, divisionByZero
+      , eqSame, eqDifferent
+      , andTrueLeft, andTrueRight, andFalseLeft, andFalseRight
+      , orTrueLeft, orTrueRight, orFalseLeft, orFalseRight
+      , notTrue, notFalse
+      ]
+
+   eqRules :: [EqRule]
+   eqRules = 
+      [ coverPlusLeft, coverPlusRight, coverMinLeft, coverMinRight
+      , coverTimesLeft, coverTimesRight, coverDivLeft, coverDivRight
+      , coverPowerOdd
+      ]
+
+   exprRules :: [ExprRule]
+   exprRules = [timesZeroLeft, timesZeroRight]
+
+
+-- Rules
+coverPlusLeft :: Rule (Equation Expr)
+coverPlusLeft = synthesise $ \a b c -> 
+  a :+: b :==: c +->
+    a :==: c :-: b // hasVaria a && noVaria b
+
+coverPlusRight = synthesise $ \a b c -> 
+  a :+: b :==: c +->
+    b :==: c :-: a // noVaria a && hasVaria b
+
+coverMinLeft = synthesise $ \a b c ->
+  a :-: b :==: c +-> 
+    a :==: c :+: b // hasVaria a && noVaria b
+
+coverMinRight = synthesise $ \a b c ->
+  a :-: b :==: c +->
+    b :==: a :-: c // noVaria a && hasVaria b
+   
+coverTimesLeft = synthesise $ \a b c -> 
+  a :**: Const b :==: c +->
+    a :==: c :/: Const b // hasVaria a && b /= 0
+   
+coverTimesRight = synthesise $ \a b c ->
+  Const a :**: b :==: c +->
+    b :==: c :/: Const a // a /= 0 && hasVaria b
+   
+coverDivLeft = synthesise $ \a b c ->
+  a :/: Const b :==: c +->
+    a :==: c :**: Const b // hasVaria a && b /= 0
+   
+coverDivRight = synthesise $ \a b c ->
+  Const a :/: b :==: c +->
+    b :==: Const a :/: c // hasVaria b -- and b should not be zero here!
+
+coverPowerEven = synthesise $ \a n b -> let new = b :^: Const (1/n) in
+  VarP (a :^: Const n :==: b) +->
+    VarP (a :==: new) :\/: VarP (a :==: Const 0 :-: new)
+      // hasVaria a && n > 0 && isEven n
+
+coverPowerOdd = synthesise $ \a n b ->
+  a :^: Const n :==: b +->
+    a :==: b :^: Const (1/n) // hasVaria a && n > 0 && isOdd n
+
+timesZeroLeft = synthesise $ \x ->
+  Const 0 :**: x +->
+    Const 0
+
+timesZeroRight = synthesise $ \x -> 
+  x :**: Const 0 +->
+    Const 0
+
+divisionByZero = synthesise $ \a b -> 
+  VarP (a :==: b) +->
+    F // hasDivisionByZero a || hasDivisionByZero b
+
+--------------------------------------------------------
+-- Rules for comparing the two sides of an equation
+      
+eqSame = synthesise $ \a b ->
+  VarP (a :==: b) +->
+    T // a == b
+
+eqDifferent = synthesise $ \a b ->
+  VarP (Const a :==: Const b) +->
+    F // a /= b
+
+----------------------------------
+-- Propagating boolean constants
+
+andTrueLeft = synthesise $ \p ->
+  T :/\: p +->
+    p
+
+andTrueRight = synthesise $ \p ->
+  p :/\: T +->
+    p
+
+andFalseLeft = synthesise $ \p ->
+  F :/\: p +->
+    F
+
+andFalseRight = synthesise $ \p ->
+  p :/\: F +->
+    F
+
+orTrueLeft = synthesise $ \p ->
+  T :\/: p +->
+    T
+
+orTrueRight = synthesise $ \p ->
+  p :\/: T +->
+    T
+
+orFalseLeft = synthesise $ \p ->
+  F :\/: p +->
+    p
+
+orFalseRight = synthesise $ \p ->
+  p :\/: F +->
+    p
+
+notTrue = synthesise $ 
+  Not T +->
+    F
+
+notFalse = synthesise $ 
+  Not F +->
+    T
diff --git a/performance/Gen/Arith/Test.hs b/performance/Gen/Arith/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/Arith/Test.hs
@@ -0,0 +1,15 @@
+module Gen.Arith.Test (main) where
+
+import Common.Arith
+import Gen.Arith.Rules
+import System.CPUTime (getCPUTime)
+import Common.GuardedRewriting
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p e = if isSolved (solve rules e) then True else error (show e)
+   if all p formulas then (return ()) else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Gen/DNF1/Test.hs b/performance/Gen/DNF1/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/DNF1/Test.hs
@@ -0,0 +1,19 @@
+module Gen.DNF1.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf1
+nr = 10000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Gen/DNF2/Test.hs b/performance/Gen/DNF2/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/DNF2/Test.hs
@@ -0,0 +1,19 @@
+module Gen.DNF2.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf2
+nr = 50000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Gen/DNF3/Test.hs b/performance/Gen/DNF3/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/DNF3/Test.hs
@@ -0,0 +1,19 @@
+module Gen.DNF3.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf3
+nr = 50000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Gen/DNF4/Test.hs b/performance/Gen/DNF4/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/DNF4/Test.hs
@@ -0,0 +1,19 @@
+module Gen.DNF4.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf4
+nr = 100000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Gen/Rules.hs b/performance/Gen/Rules.hs
new file mode 100644
--- /dev/null
+++ b/performance/Gen/Rules.hs
@@ -0,0 +1,89 @@
+module Gen.Rules where
+
+import Data.Maybe
+import Common.Logic
+import Common.GuardedRewriting
+
+
+(|-) :: Logic -> Logic -> Template Logic
+p |- q = p +-> q // True
+
+makeRuleList _ = rewriteMl . map synthesise
+makeRule s x = makeRuleList s [x]
+
+--rewriteMl :: [Rule (Pat (PF Logic))] -> Logic -> [Logic]
+rewriteMl rs p = take 1 $ catMaybes $ map (`rewriteM` p) rs
+
+-- This main function is defined to solve a bug in GHC
+main :: IO ()
+main = do let resultsPP = zipWith undefined [1..] ([] :: [Logic])
+          putStr (unlines resultsPP)   
+
+ruleDefImpl = makeRule "DefImpl" $
+   \x y -> (x :->: y)  |-  (Not x :||: y)
+
+ruleDefEquiv = makeRule "DefEquiv" $
+   \x y -> (x :<->: y)  |-  ((x :&&: y) :||: (Not x :&&: Not y))
+   
+ruleFalseInEquiv = makeRuleList "FalseInEquiv"
+   [ \x -> (F :<->: x)  |-  (Not x)
+   , \x -> (x :<->: F)  |-  (Not x)
+   ]
+
+ruleTrueInEquiv = makeRuleList "TrueInEquiv"
+   [ \x -> (T :<->: x)  |-  x
+   , \x -> (x :<->: T)  |-  x
+   ]
+
+ruleFalseInImpl = makeRuleList "FalseInImpl"
+   [ \x -> (F :->: x)  |-  T
+   , \x -> (x :->: F)  |- (Not x)
+   ]
+ 
+ruleTrueInImpl = makeRuleList "TrueInImpl"
+   [  \x -> (T :->: x)  |-  x
+   ,  \x -> (x :->: T)  |-  T
+   ]
+        
+ruleFalseZeroOr = makeRuleList "FalseZeroOr"
+   [ \x -> (F :||: x)  |-  x
+   , \x -> (x :||: F)  |-  x
+   ]
+ruleTrueZeroOr = makeRuleList "TrueZeroOr"
+   [ \x -> (T :||: x)  |-  T
+   , \x -> (x :||: T)  |-  T
+   ]
+
+ruleTrueZeroAnd = makeRuleList "TrueZeroAnd"
+   [ \x -> (T :&&: x)  |-  x
+   , \x -> (x :&&: T)  |-  x
+   ]
+
+ruleFalseZeroAnd = makeRuleList "FalseZeroAnd"
+   [ \x -> (F :&&: x)  |-  F
+   , \x -> (x :&&: F)  |-  F
+   ]
+
+ruleDeMorganOr = makeRule "DeMorganOr" $
+   \x y -> (Not (x :||: y))  |-  (Not x :&&: Not y)
+
+ruleDeMorganAnd = makeRule "DeMorganAnd" $
+   \x y -> (Not (x :&&: y))  |-  (Not x :||: Not y)
+
+ruleNotBoolConst = makeRuleList "NotBoolConst"
+   [ (Not T)  |-  F
+   , (Not F)  |-  T
+   ]
+
+ruleNotNot = makeRule "NotNot" $ 
+   \x -> (Not (Not x))  |-  x
+
+ruleAndOverOr = makeRuleList "AndOverOr"
+   [ \x y z -> (x :&&: (y :||: z))  |-  ((x :&&: y) :||: (x :&&: z))
+   , \x y z -> ((x :||: y) :&&: z)  |-  ((x :&&: z) :||: (y :&&: z))
+   ]
+
+ruleOrOverAnd = makeRuleList "OrOverAnd"
+   [ \x y z -> (x :||: (y :&&: z))  |-  ((x :||: y) :&&: (x :||: z))
+   , \x y z -> ((x :&&: y) :||: z)  |-  ((x :||: z) :&&: (y :||: z))
+   ]
diff --git a/performance/Main.hs b/performance/Main.hs
new file mode 100644
--- /dev/null
+++ b/performance/Main.hs
@@ -0,0 +1,193 @@
+module Main where
+
+
+-- ParseArgs library
+import System.Console.ParseArgs
+
+import System.CPUTime (cpuTimePrecision)
+import Data.List (groupBy, sortBy, intersperse)
+import System.FilePath ((</>))
+import System.Cmd (system)
+import System.IO 
+    (Handle, openFile, IOMode(..), stdout, hFlush, hIsEOF, hGetChar, hClose, hPutStrLn)
+import System.Exit (ExitCode(..))
+import System.Info (os, arch, compilerVersion)
+
+data Mode = PM | Uni | Gen deriving (Eq, Ord, Show)
+data Strategy = DNF1 | DNF2 | DNF3 | DNF4 | Arith deriving (Eq, Ord, Show)
+data Test = Test { mode :: Mode, strategy :: Strategy} deriving (Eq, Ord)
+
+instance Show Test where
+  show t = show (mode t) ++ "-" ++ show (strategy t)
+
+tests = [Test PM DNF1,
+         Test PM DNF2,
+         Test PM DNF3,
+         Test PM DNF4,
+         Test PM Arith,
+         
+         Test Uni DNF1,
+         Test Uni DNF2,
+         Test Uni DNF3,
+         Test Uni DNF4,
+         
+         Test Gen DNF1,
+         Test Gen DNF2,
+         Test Gen DNF3,
+         Test Gen DNF4,
+         Test Gen Arith]
+
+inCommas :: [String] -> String
+inCommas = concat . intersperse ","
+
+
+printGroupStats :: (Enum a, Fractional a, Floating a, Num a)
+                => Handle -> IO [(Test, Int, a)] -> IO ()
+printGroupStats h l = do
+                        l' <- l
+                        let --group1 :: [[(Test, Int, a)]]
+                            group1 = groupBy g (sortBy f l')
+                            f (t1,_,_) (t2,_,_) = compare t1 t2
+                            g (t1,_,_) (t2,_,_) = t1 == t2
+                            --calcAvgStdDev :: [(Test, Int, a)] -> (Test, a, a)
+                            calcAvgStdDev x = let avg l = sum' l / toEnum (length l)
+                                                  stddev a = sqrt (avg [ (t,d,y - a) | (t,d,y) <- x ])
+                                              in (fst' (head x), avg x, stddev (avg x))
+                            fst' (a,_,_) = a
+                            --sum' :: [(Test, Int, a)] -> a
+                            sum' [] = 0
+                            sum' ((_,_,d):ts) = d + sum' ts
+                            sort2 l = sortBy f' l
+                            f' (t1,_,_) (t2,_,_) = compare (strategy t1, mode t1)
+                                                           (strategy t2, mode t2)
+                        printTests h $ sort2 $ map calcAvgStdDev group1
+
+printTests :: (Show a) => Handle -> [(Test, a, a)] -> IO ()
+printTests h l = sequence_ $ map (hPutStrLn h) [ inCommas [show t, show a, show d] | (t,a,d) <- l ]
+
+-- Arguments
+data MyArgs = N | O | F | P deriving (Eq, Ord, Show)
+
+myArgs :: [Arg MyArgs]
+myArgs = [
+          Arg { argIndex = N,
+                argAbbr = Just 'n',
+                argName = Just "number-times",
+                argData = argDataDefaulted "int" ArgtypeInt 1,
+                argDesc = "Number of times to run the benchmark"
+              },
+          Arg { argIndex = O,
+                argAbbr = Just 'o',
+                argName = Just "output",
+                argData = argDataOptional "file" ArgtypeString,
+                argDesc = "Output report file"
+              },
+          Arg { argIndex = F,
+                argAbbr = Just 'f',
+                argName = Just "flags",
+                argData = argDataDefaulted "string" ArgtypeString "",
+                argDesc = "Extra flags to pass to the compiler"
+              },
+          Arg { argIndex = P,
+                argAbbr = Just 'p',
+                argName = Just "profiling",
+                argData = Nothing,
+                argDesc = "Profile, do not benchmark"
+              }
+         ]
+
+sequenceProgress_ :: [IO ExitCode] -> IO ()
+sequenceProgress_ [] = return ()
+sequenceProgress_ l  = do
+  let seq :: [IO ExitCode] -> Int -> IO ()
+      seq []    _ = putStrLn "done."
+      seq (h:t) n = do
+                      putStr ((show n) ++ " ") >> hFlush stdout
+                      sequenceError_ [h]
+                      seq t (n + 1)
+  putStr ("Total number of elements: " ++ show (length l) ++ ". ")
+  seq l 1
+
+-- sequence_ accounting for errors
+sequenceError_ :: [IO ExitCode] -> IO ()
+sequenceError_ []    = return ()
+sequenceError_ (h:t) = do
+                         e <- h
+                         case e of
+                           ExitSuccess   -> sequenceError_ t
+                           ExitFailure n -> error ("Execution returned exit code "
+                                                    ++ show n ++ ", aborted.")
+
+-- Stricter readFile
+hGetContents' hdl = do e <- hIsEOF hdl
+                       if e then return []
+                         else do c <- hGetChar hdl
+                                 cs <- hGetContents' hdl
+                                 return (c:cs)
+
+readFile' fn = do hdl <- openFile fn ReadMode
+                  xs <- hGetContents' hdl
+                  hClose hdl
+                  return xs
+
+
+main :: IO ()
+main = do
+        args <- parseArgsIO ArgsComplete myArgs
+        
+        -- Some variables
+        let profiling = gotArg args P
+            n :: Int
+            n = if profiling then 1 else (getRequiredArg args N)
+            extraFlags = getRequiredArg args F
+            flags t = "-fforce-recomp --make -iCommon -D__" ++ show (mode t)
+                      ++ " -o bin" </> path t
+                      ++ " -main-is " ++ show (mode t) ++ "." 
+                                      ++ show (strategy t) ++ ".Test.main "
+                      ++ (if profiling then " -prof -auto-all " else "")
+                      ++ " -outputdir out "
+                      ++ extraFlags ++ " "
+            path t = "Test" ++ show t
+            out t = "out" </> "Test" ++ show t ++ ".compile.out"
+            redirect t = " > " ++ out t ++ " 2>&1 "
+            cmd t = "ghc " ++ show (mode t) ++ "." ++ show (strategy t) 
+                           ++ ".Test " ++ flags t ++ redirect t
+        
+        -- Compilation
+        putStrLn "Compiling..." >> hFlush stdout
+        --sequence_ [ putStrLn (cmd t) | t <- tests ]
+        sequenceProgress_ [ system (cmd t) | t <- tests ]
+        
+        -- Running tests
+        let newout t m = "out" </> "Test" ++ show t ++ "." ++ show m ++ ".out"
+            newpath t  = "bin" </> "Test" ++ show t
+            run t m    = newpath t 
+                          ++ if profiling then " +RTS -p -RTS" else ""
+                          ++ " > " ++ newout t m
+        do
+          putStrLn ("-------------------------------------")
+          putStrLn "Running tests..." >> hFlush stdout
+          --sequence_ [ putStrLn (run t m) | t <- tests, m <- [1..n]]
+          sequenceProgress_ [ system (run t m) | t <- tests, m <- [1..n]]
+        
+        -- Results output
+        h <- getArgStdio args O WriteMode
+        hPutStrLn h ("-------------------------------------")
+        hPutStrLn h "\nResults:"
+        hPutStrLn h ("Number of repetitions: " ++ show n)
+        hPutStrLn h ("Flags to the compiler: " ++ extraFlags)
+        hPutStrLn h ("Environment: " ++ inCommas [os, arch, show compilerVersion])
+        hPutStrLn h ("CPU time precision: " ++ show (fromInteger cpuTimePrecision / (1000000000 :: Double)) ++ " (ms)")
+        hPutStrLn h ""
+        let parse :: Test -> Int -> IO Double
+            parse t m = readFile' (newout t m) >>= return . read . tail . dropWhile (/= '\t')
+            liftIOList :: [(a, b, IO c)] -> IO [(a, b, c)]
+            liftIOList [] = return []
+            liftIOList ((a,b,c):t) = do  c' <- c
+                                         t' <- liftIOList t
+                                         return ((a,b,c'):t')
+        if profiling
+          then hPutStrLn h ("Profiling run, no benchmarking results.")
+          else printGroupStats h (liftIOList [ (t, m, parse t m) | t <- tests, m <- [1..n]])
+        hPutStrLn h ("-------------------------------------")
+        hClose h
diff --git a/performance/Makefile b/performance/Makefile
new file mode 100644
--- /dev/null
+++ b/performance/Makefile
@@ -0,0 +1,14 @@
+GHC=ghc
+
+.default=PHONY
+
+all: compile run
+
+compile:
+	$(GHC) --make -O1 Main
+
+run:
+	./Main -n 5 -f "-O1 -package QuickCheck-1.2.0.0"
+
+clean: 
+	rm -rf bin/* out/*
diff --git a/performance/PM/Arith/Rules.hs b/performance/PM/Arith/Rules.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/Arith/Rules.hs
@@ -0,0 +1,169 @@
+module PM.Arith.Rules where
+
+import Common.Arith
+import Test.QuickCheck
+import Data.Ratio
+
+type Rule a   = a -> Maybe a
+type PropRule = Rule (Prop (Equation Expr))
+type EqRule   = Rule (Equation Expr)
+type ExprRule = Rule Expr
+
+rules :: [PropRule]
+rules = [ somewhereProp $ applyOne propRules
+        , liftToProp $ applyOne eqRules
+        , liftToProp $ liftToEq $ somewhereExpr $ applyOne exprRules
+        ]
+ where
+   propRules :: [PropRule]
+   propRules = 
+      [ coverPowerEven, divisionByZero
+      , eqSame, eqDifferent
+      , andTrueLeft, andTrueRight, andFalseLeft, andFalseRight
+      , orTrueLeft, orTrueRight, orFalseLeft, orFalseRight
+      , notTrue, notFalse
+      ]
+
+   eqRules :: [EqRule]
+   eqRules = 
+      [ coverPlusLeft, coverPlusRight, coverMinLeft, coverMinRight
+      , coverTimesLeft, coverTimesRight, coverDivLeft, coverDivRight
+      , coverPowerOdd
+      ]
+
+   exprRules :: [ExprRule]
+   exprRules = [timesZeroLeft, timesZeroRight]
+   
+go = quickCheck $ forAll (sized propGen) (isSolved . solve rules)
+
+-- Rules
+coverPlusLeft :: EqRule
+coverPlusLeft (a :+: b :==: c)
+   | hasVaria a && noVaria b = 
+        Just (a :==: c :-: b)
+coverPlusLeft _ = Nothing
+
+coverPlusRight :: EqRule
+coverPlusRight (a :+: b :==: c)
+   | noVaria a && hasVaria b =
+        Just (b :==: c :-: a)
+coverPlusRight _ = Nothing
+
+coverMinLeft :: EqRule
+coverMinLeft (a :-: b :==: c)
+   | hasVaria a && noVaria b = 
+        Just (a :==: c :+: b)
+coverMinLeft _ = Nothing
+
+coverMinRight :: EqRule
+coverMinRight (a :-: b :==: c)
+   | noVaria a && hasVaria b =
+        Just (b :==: a :-: c)
+coverMinRight _ = Nothing
+   
+coverTimesLeft :: EqRule
+coverTimesLeft (a :**: Const b :==: c) 
+   | hasVaria a && b /= 0 =
+        Just (a :==: c :/: Const b)
+coverTimesLeft _ = Nothing
+   
+coverTimesRight :: EqRule
+coverTimesRight (Const a :**: b :==: c) 
+   | a /= 0 && hasVaria b =
+        Just (b :==: c :/: Const a)
+coverTimesRight _ = Nothing
+   
+coverDivLeft :: EqRule
+coverDivLeft (a :/: Const b :==: c) 
+   | hasVaria a && b /= 0 =
+        Just (a :==: c :**: Const b)
+coverDivLeft _ = Nothing
+   
+coverDivRight :: EqRule
+coverDivRight (Const a :/: b :==: c) 
+   | hasVaria b =
+        Just (b :==: Const a :/: c) -- and b should not be zero here!
+coverDivRight _ = Nothing
+
+coverPowerEven :: PropRule
+coverPowerEven (VarP (a :^: Const n :==: b)) 
+   | hasVaria a && n > 0 && isEven n =
+        let new = b :^: Const (1/n) in
+        Just (VarP (a :==: new) :\/: VarP (a :==: Const 0 :-: new))
+coverPowerEven _ = Nothing
+
+coverPowerOdd :: EqRule
+coverPowerOdd (a :^: Const n :==: b)
+   | hasVaria a && n > 0 && isOdd n =
+        Just (a :==: b :^: Const (1/n))
+coverPowerOdd _ = Nothing
+
+timesZeroLeft :: ExprRule
+timesZeroLeft (Const 0 :**: _) =
+   Just (Const 0)
+timesZeroLeft _ = Nothing
+
+timesZeroRight :: ExprRule
+timesZeroRight (_ :**: Const 0) =
+   Just (Const 0)
+timesZeroRight _ = Nothing
+
+divisionByZero :: PropRule
+divisionByZero (VarP (a :==: b)) 
+   | hasDivisionByZero a || hasDivisionByZero b =
+        Just F
+divisionByZero _ = Nothing
+
+--------------------------------------------------------
+-- Rules for comparing the two sides of an equation
+      
+eqSame :: PropRule
+eqSame (VarP (a :==: b)) | a == b = Just T
+eqSame _ = Nothing 
+
+eqDifferent :: PropRule
+eqDifferent (VarP (Const a :==: Const b)) | a /= b = Just F
+eqDifferent _ = Nothing 
+
+----------------------------------
+-- Propagating boolean constants
+
+andTrueLeft :: PropRule 
+andTrueLeft (T :/\: p) = Just p
+andTrueLeft _ = Nothing
+
+andTrueRight :: PropRule 
+andTrueRight (p :/\: T) = Just p
+andTrueRight _ = Nothing
+
+andFalseLeft :: PropRule 
+andFalseLeft (F :/\: _) = Just F
+andFalseLeft _ = Nothing
+
+andFalseRight :: PropRule 
+andFalseRight (_ :/\: F) = Just F
+andFalseRight _ = Nothing
+
+orTrueLeft :: PropRule 
+orTrueLeft (T :\/: _) = Just T
+orTrueLeft _ = Nothing
+
+orTrueRight :: PropRule 
+orTrueRight (_ :\/: T) = Just T
+orTrueRight _ = Nothing
+
+orFalseLeft :: PropRule 
+orFalseLeft (F :\/: p) = Just p
+orFalseLeft _ = Nothing
+
+orFalseRight :: PropRule 
+orFalseRight (p :\/: F) = Just p
+orFalseRight _ = Nothing
+
+notTrue :: PropRule
+notTrue (Not T) = Just F
+notTrue _ = Nothing
+
+notFalse :: PropRule
+notFalse (Not F) = Just T
+notFalse _ = Nothing
diff --git a/performance/PM/Arith/Test.hs b/performance/PM/Arith/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/Arith/Test.hs
@@ -0,0 +1,14 @@
+module PM.Arith.Test (main) where
+
+import Common.Arith
+import PM.Arith.Rules
+import System.CPUTime (getCPUTime)
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p e = if isSolved (solve rules e) then True else error (show e)
+   if all p formulas then (return ()) else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/PM/DNF1/Test.hs b/performance/PM/DNF1/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/DNF1/Test.hs
@@ -0,0 +1,19 @@
+module PM.DNF1.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf1
+nr = 10000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/PM/DNF2/Test.hs b/performance/PM/DNF2/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/DNF2/Test.hs
@@ -0,0 +1,19 @@
+module PM.DNF2.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf2
+nr = 50000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/PM/DNF3/Test.hs b/performance/PM/DNF3/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/DNF3/Test.hs
@@ -0,0 +1,19 @@
+module PM.DNF3.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf3
+nr = 50000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/PM/DNF4/Test.hs b/performance/PM/DNF4/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/DNF4/Test.hs
@@ -0,0 +1,19 @@
+module PM.DNF4.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf4
+nr = 100000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/PM/Rules.hs b/performance/PM/Rules.hs
new file mode 100644
--- /dev/null
+++ b/performance/PM/Rules.hs
@@ -0,0 +1,62 @@
+module PM.Rules where
+
+import Common.Logic
+
+ruleDefImpl (x :->: y) = [Not x :||: y]
+ruleDefImpl _ = []
+
+ruleDefEquiv (x :<->: y) = [(x :&&: y) :||: (Not x :&&: Not y)]
+ruleDefEquiv _ = []
+   
+ruleFalseInEquiv (F :<->: x) = [Not x]
+ruleFalseInEquiv (x :<->: F) = [Not x]
+ruleFalseInEquiv _ = []
+
+ruleTrueInEquiv (T :<->: x) = [x]
+ruleTrueInEquiv (x :<->: T) = [x]
+ruleTrueInEquiv _ = []
+
+ruleFalseInImpl (F :->: x)  = [T]
+ruleFalseInImpl (x :->: F)  = [Not x]
+ruleFalseInImpl _ = []
+ 
+ruleTrueInImpl (T :->: x) = [x]
+ruleTrueInImpl (x :->: T) = [T]
+ruleTrueInImpl _ = []
+        
+ruleFalseZeroOr (F :||: x) = [x]
+ruleFalseZeroOr (x :||: F) = [x]
+ruleFalseZeroOr _ = []
+
+ruleTrueZeroOr (T :||: x) = [T]
+ruleTrueZeroOr (x :||: T) = [T]
+ruleTrueZeroOr _  = []
+
+ruleTrueZeroAnd (T :&&: x) = [x]
+ruleTrueZeroAnd (x :&&: T) = [x]
+ruleTrueZeroAnd _ = []
+
+ruleFalseZeroAnd (F :&&: x) = [F]
+ruleFalseZeroAnd (x :&&: F) = [F]
+ruleFalseZeroAnd _ = []
+
+ruleDeMorganOr (Not (x :||: y)) = [Not x :&&: Not y]
+ruleDeMorganOr _ = []
+
+ruleDeMorganAnd (Not (x :&&: y))  = [ Not x :||: Not y ]
+ruleDeMorganAnd _ = []
+
+ruleNotBoolConst (Not T)  = [ F ]
+ruleNotBoolConst (Not F)  = [ T ]
+ruleNotBoolConst _ = []
+
+ruleNotNot (Not (Not x)) = [x]
+ruleNotNot _ = []
+
+ruleAndOverOr (x :&&: (y :||: z))  = [ (x :&&: y) :||: (x :&&: z) ]
+ruleAndOverOr ((x :||: y) :&&: z)  = [ (x :&&: z) :||: (y :&&: z) ]
+ruleAndOverOr _ = []
+
+ruleOrOverAnd (x :||: (y :&&: z))  =  [ (x :||: y) :&&: (x :||: z) ]
+ruleOrOverAnd ((x :&&: y) :||: z)  =  [ (x :||: z) :&&: (y :||: z) ]
+ruleOrOverAnd _ = []
diff --git a/performance/Uni/DNF1/Test.hs b/performance/Uni/DNF1/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Uni/DNF1/Test.hs
@@ -0,0 +1,19 @@
+module Uni.DNF1.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf1
+nr = 10000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Uni/DNF2/Test.hs b/performance/Uni/DNF2/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Uni/DNF2/Test.hs
@@ -0,0 +1,19 @@
+module Uni.DNF2.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf2
+nr = 50000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Uni/DNF3/Test.hs b/performance/Uni/DNF3/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Uni/DNF3/Test.hs
@@ -0,0 +1,19 @@
+module Uni.DNF3.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf3
+nr = 50000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Uni/DNF4/Test.hs b/performance/Uni/DNF4/Test.hs
new file mode 100644
--- /dev/null
+++ b/performance/Uni/DNF4/Test.hs
@@ -0,0 +1,19 @@
+module Uni.DNF4.Test (main) where
+
+import Common.LogicGenerator
+import Common.Logic
+import Common.DNF
+import System.CPUTime (getCPUTime)
+
+
+dnf = dnf4
+nr = 100000
+
+main :: IO ()
+main = do
+   t1 <- getCPUTime
+   let p l = if isDNF (runStrategy dnf l) then True else error (show l)
+   if all p $ take nr formula then reportTick else error "ERROR!"
+   t2 <- getCPUTime
+   let diff = fromInteger (t2 - t1) / (1000000000 :: Double)
+   putStrLn ("\t" ++ show diff)
diff --git a/performance/Uni/Rules.hs b/performance/Uni/Rules.hs
new file mode 100644
--- /dev/null
+++ b/performance/Uni/Rules.hs
@@ -0,0 +1,82 @@
+module Uni.Rules where
+
+import Common.Logic
+
+x:y:z:_ = metaVars
+
+(|-) :: Logic -> Logic -> (Logic -> [Logic]) 
+(lhs |- rhs) a = case matchLogic lhs a of 
+                    Just s  -> [s |-> rhs]
+                    Nothing -> []
+
+makeRuleList _ fs a = take 1 $ concatMap ($ a) fs
+makeRule _ = id
+
+ruleDefImpl = makeRule "DefImpl" $
+   (x :->: y)  |-  (Not x :||: y)
+
+ruleDefEquiv = makeRule "DefEquiv" $
+   (x :<->: y)  |-  ((x :&&: y) :||: (Not x :&&: Not y))
+   
+ruleFalseInEquiv = makeRuleList "FalseInEquiv"
+   [ (F :<->: x)  |-  (Not x)
+   , (x :<->: F)  |-  (Not x)
+   ]
+
+ruleTrueInEquiv = makeRuleList "TrueInEquiv"
+   [ (T :<->: x)  |-  x
+   , (x :<->: T)  |-  x
+   ]
+
+ruleFalseInImpl = makeRuleList "FalseInImpl"
+   [ (F :->: x)  |-  T
+   , (x :->: F)  |- (Not x)
+   ]
+ 
+ruleTrueInImpl = makeRuleList "TrueInImpl"
+   [  (T :->: x)  |-  x
+   ,  (x :->: T)  |-  T
+   ]
+        
+ruleFalseZeroOr = makeRuleList "FalseZeroOr"
+   [ (F :||: x)  |-  x
+   , (x :||: F)  |-  x
+   ]
+ruleTrueZeroOr = makeRuleList "TrueZeroOr"
+   [ (T :||: x)  |-  T
+   , (x :||: T)  |-  T
+   ]
+
+ruleTrueZeroAnd = makeRuleList "TrueZeroAnd"
+   [ (T :&&: x)  |-  x
+   , (x :&&: T)  |-  x
+   ]
+
+ruleFalseZeroAnd = makeRuleList "FalseZeroAnd"
+   [ (F :&&: x)  |-  F
+   , (x :&&: F)  |-  F
+   ]
+
+ruleDeMorganOr = makeRule "DeMorganOr" $
+   (Not (x :||: y))  |-  (Not x :&&: Not y)
+
+ruleDeMorganAnd = makeRule "DeMorganAnd" $
+   (Not (x :&&: y))  |-  (Not x :||: Not y)
+
+ruleNotBoolConst = makeRuleList "NotBoolConst"
+   [ (Not T)  |-  F
+   , (Not F)  |-  T
+   ]
+
+ruleNotNot = makeRule "NotNot" $ 
+   (Not (Not x))  |-  x
+
+ruleAndOverOr = makeRuleList "AndOverOr"
+   [ (x :&&: (y :||: z))  |-  ((x :&&: y) :||: (x :&&: z))
+   , ((x :||: y) :&&: z)  |-  ((x :&&: z) :||: (y :&&: z))
+   ]
+
+ruleOrOverAnd = makeRuleList "OrOverAnd"
+   [ (x :||: (y :&&: z))  |-  ((x :||: y) :&&: (x :||: z))
+   , ((x :&&: y) :||: z)  |-  ((x :||: z) :&&: (y :||: z))
+   ]
diff --git a/performance/bin/description.txt b/performance/bin/description.txt
new file mode 100644
--- /dev/null
+++ b/performance/bin/description.txt
@@ -0,0 +1,1 @@
+Binaries will be placed here.
diff --git a/performance/out/description.txt b/performance/out/description.txt
new file mode 100644
--- /dev/null
+++ b/performance/out/description.txt
@@ -0,0 +1,1 @@
+Output files will be placed here.
diff --git a/src/Generics/Instant/Rewriting.hs b/src/Generics/Instant/Rewriting.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Instant/Rewriting.hs
@@ -0,0 +1,606 @@
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE EmptyDataDecls       #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE OverlappingInstances #-}
+
+{-# OPTIONS_GHC -Wall             #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Instant.Rewriting
+-- Copyright   :  (c) 2010, Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This is the top module for the rewriting library. All functionality is
+-- implemented in this module. For examples of how to use the library, see
+-- the included files in the directory examples, or the benchmark in the
+-- directory performance.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Instant.Rewriting (
+    
+    -- * The class to signal availability of rewriting for a type
+    Rewritable,
+  
+    -- * Top-level functions
+    rewrite, rewriteM, validate, synthesise,
+
+    -- * Building rewrite rules
+    Template(..), (+->), (//), Rule,
+    
+    -- * Internal classes: might be necessary to add new base types
+    Extensible(..),
+    Matchable(..),
+    Substitutable(..),
+    Sampleable(..), Empty(..), HasRec(..), Finite, True, False,
+    Diffable(..),
+    Validatable(..),
+    Nillable(..),
+
+    -- * Re-exported for convenience
+    Typeable
+    
+  ) where
+
+import Control.Monad  (join, liftM, liftM2)
+import Data.Maybe     (fromJust, fromMaybe)
+import Data.Typeable  (Typeable, gcast)
+
+import Generics.Instant.Base
+import Generics.Instant.Instances ()
+
+-------------------------------------------------------------------------------
+-- | Typed references
+-------------------------------------------------------------------------------
+
+data Ref :: * -> * -> * where
+  Rz :: Ref a (a :*: gam)
+  Rs :: Ref a gam -> Ref a (b :*: gam)
+
+instance Eq (Ref a gam) where
+  Rz   == Rz    = True
+  Rs r == Rs r' = r == r'
+  _    == _     = False
+
+-------------------------------------------------------------------------------
+-- | The 'Rewritable' class is used to signal types that can be rewritten and 
+-- to ``tie the recursive knot'' of the generic functions.
+-------------------------------------------------------------------------------
+
+class (Representable a, Typeable a, Eq a, Empty (Rep a),
+       Extensible (Rep a), Matchable (Rep a), Substitutable (Rep a),
+       Sampleable (Rep a), Diffable (Rep a), Validatable (Rep a)) =>
+  Rewritable a
+
+instance Rewritable Int
+instance Rewritable Float
+instance Rewritable Char
+
+-------------------------------------------------------------------------------
+-- Rewrite rules
+-------------------------------------------------------------------------------
+
+-- Metavariables
+type Metavar a gam = Ref a gam
+
+-- | Schemes
+class Extensible a where
+  data Ext a :: * -> *
+  toExt :: a -> Ext a U
+
+type Scheme a gam = Ext (Rep a) gam :+: Metavar a gam
+
+toScheme :: Rewritable a => a -> Scheme a U
+toScheme = L . toExt . from
+
+instance Extensible Int where
+  newtype Ext Int gam = ExtInt Int
+  toExt = ExtInt
+
+instance Extensible Float where
+  newtype Ext Float gam = ExtFloat Float
+  toExt = ExtFloat
+
+instance Extensible Char where
+  newtype Ext Char gam = ExtChar Char
+  toExt = ExtChar
+
+instance (Extensible a, Extensible b) => Extensible (a :+: b) where
+  newtype Ext (a :+: b) gam = ExtSum (Ext a gam :+: Ext b gam)
+
+  toExt (L x) = ExtSum (L (toExt x))
+  toExt (R y) = ExtSum (R (toExt y))
+
+instance (Extensible a, Extensible b) => Extensible (a :*: b) where
+  newtype Ext (a :*: b) gam = ExtCons (Ext a gam :*: Ext b gam)
+  toExt (x :*: y) = ExtCons (toExt x :*: toExt y)
+
+instance Extensible U where
+  newtype Ext U gam = ExtNil U
+  toExt = ExtNil
+
+instance (Rewritable a) => Extensible (Rec a) where
+  newtype Ext (Rec a) gam = ExtRec (Rec (Scheme a gam))
+  toExt (Rec a) = ExtRec (Rec (toScheme a))
+
+instance (Rewritable a) => Extensible (Var a) where
+  newtype Ext (Var a) gam = ExtVar (Var (Scheme a gam))
+  toExt (Var a) = ExtVar (Var (toScheme a))
+
+instance (Extensible a) => Extensible (C c a) where
+  newtype Ext (C c a) gam = ExtC (C c (Ext a gam))
+  toExt (C a) = ExtC (C (toExt a))
+
+-- Guards
+type family Guard gam :: *
+type instance Guard U         = Bool
+type instance Guard (a :*: gam) = a -> Guard gam
+
+-- Rules
+data Rule' a gam =
+  Rule' { lhs :: Scheme a gam, rhs :: Scheme a gam, guard :: Guard gam }
+
+-------------------------------------------------------------------------------
+-- Rewriting
+-------------------------------------------------------------------------------
+
+-- Substitutions
+data Subst :: * -> * where
+  Sz :: Subst U
+  Ss :: Rewritable a => Maybe a -> Subst gam -> Subst (a :*: gam)
+
+(!!!) :: Subst gam -> Ref a gam -> Maybe a
+Ss mb _ !!! Rz   = mb
+Ss _  s !!! Rs r = s !!! r
+_       !!! _    = error "(!!!) failure"
+
+total :: Monad m => Subst gam -> Ref a gam -> m a
+total s r = maybe (fail "metavariable unbound") return (s !!! r)
+
+class Nillable gam where
+  empty :: Subst gam
+
+instance Nillable U where
+  empty = Sz
+
+instance (Rewritable a, Nillable gam) => Nillable (a :*: gam) where
+  empty = Ss Nothing empty
+
+singleton :: Nillable gam => Ref a gam -> a -> Subst gam
+singleton r x = update r x empty
+
+update :: Ref a gam -> a -> Subst gam -> Subst gam
+update Rz     x (Ss _ s)  = Ss (Just x) s
+update (Rs r) x (Ss mb s) = Ss mb (update r x s)
+update _      _ _         = error "update failure"
+
+(+++) :: Monad m => Subst gam -> Subst gam -> m (Subst gam)
+Sz               +++ Sz                          = return Sz
+Ss mb@(Just x) s +++ Ss (Just x') s' | x == x'   = liftM (Ss mb) (s +++ s')
+                                     | otherwise = fail "merging failure"
+Ss mb@(Just _) s +++ Ss Nothing s'               = liftM (Ss mb) (s +++ s')
+Ss Nothing s     +++ Ss mb s'                    = liftM (Ss mb) (s +++ s')
+_                +++ _                           = error "(+++) failure"
+
+-- | Matching
+class Matchable a where
+  match' :: (Nillable gam, Monad m) => Ext a gam -> a -> m (Subst gam)
+
+match :: (Rewritable a, Nillable gam, Monad m) =>
+         Scheme a gam -> a -> m (Subst gam)
+match (L ext) x = match' ext (from x)
+match (R r) x   = return (singleton r x)
+
+instance Matchable Int where
+  match' (ExtInt n) n' | n == n'   = return empty
+                       | otherwise = fail "structure mismatch"
+
+instance Matchable Char where
+  match' (ExtChar c) c' | c == c'   = return empty
+                        | otherwise = fail "structure mismatch"
+
+instance Matchable Float where
+  match' (ExtFloat f) f' | f == f'   = return empty
+                         | otherwise = fail "structure mismatch"
+
+instance (Matchable a, Matchable b) => Matchable (a :+: b) where
+  match' (ExtSum (L ext)) (L x) = match' ext x
+  match' (ExtSum (R ext)) (R y) = match' ext y
+  match' _                  _       = fail "structure mismatch"
+
+instance (Matchable a, Matchable b) => Matchable (a :*: b) where
+  match' (ExtCons (ext :*: ext')) (x :*: y) =
+    join (liftM2 (+++) (match' ext x) (match' ext' y))
+
+instance Matchable U where
+  match' (ExtNil U) U = return empty
+
+instance (Rewritable a) => Matchable (Var a) where
+  match' (ExtVar (Var e)) (Var a) = match e a
+
+instance (Rewritable a) => Matchable (Rec a) where
+  match' (ExtRec (Rec e)) (Rec a) = match e a
+
+instance (Matchable a) => Matchable (C c a) where
+  match' (ExtC (C e)) (C a) = match' e a
+
+-- | Substituting
+class Substitutable a where
+  subst' :: Monad m => Subst gam -> Ext a gam -> m a
+
+subst :: (Rewritable a, Monad m) => Subst gam -> Scheme a gam -> m a
+subst s (L ext) = liftM to (subst' s ext)
+subst s (R r)   = total s r
+
+instance Substitutable Int where
+  subst' _ (ExtInt n) = return n
+
+instance Substitutable Char where
+  subst' _ (ExtChar c) = return c
+
+instance Substitutable Float where
+  subst' _ (ExtFloat f) = return f
+
+instance (Substitutable a, Substitutable b) => Substitutable (a :+: b) where
+  subst' s (ExtSum (L ext)) = liftM L (subst' s ext)
+  subst' s (ExtSum (R ext)) = liftM R (subst' s ext)
+
+instance (Substitutable a, Substitutable b) => Substitutable (a :*: b) where
+  subst' s (ExtCons (ext :*: ext')) = liftM2 (:*:) (subst' s ext) (subst' s ext')
+
+instance Substitutable U where
+  subst' _ (ExtNil U) = return U
+
+instance (Rewritable a) => Substitutable (Rec a) where
+  subst' s (ExtRec (Rec scheme)) = liftM Rec (subst s scheme)
+
+instance (Rewritable a) => Substitutable (Var a) where
+  subst' s (ExtVar (Var scheme)) = liftM Var (subst s scheme)
+
+instance (Substitutable a) => Substitutable (C c a) where
+  subst' s (ExtC (C ext)) = liftM C (subst' s ext)
+
+-- | Testing preconditions
+class Testable gam where
+  test :: Subst gam -> Guard gam -> Bool
+
+instance Testable U where
+  test Sz b = b
+
+instance Testable gam => Testable (a :*: gam) where
+  test (Ss (Just x) s) f = test s (f x)
+  test (Ss Nothing _)  _ = error "invalid rule"
+
+-- Rewriting
+rewrite' :: (Rewritable a, Nillable gam, Testable gam) => Rule' a gam -> a -> a
+rewrite' rule x = fromMaybe x (rewriteM' rule x)
+
+rewriteM' :: (Rewritable a, Nillable gam, Testable gam, Monad m) 
+         => Rule' a gam -> a -> m a
+rewriteM' rule x =
+  do s <- match (lhs rule) x
+     if (test s (guard rule)) then subst s (rhs rule) else fail "guard failed"
+
+-------------------------------------------------------------------------------
+-- Synthesising rules
+-------------------------------------------------------------------------------
+
+-- | Sampling
+class Sampleable a where
+  left'  :: a
+  right' :: a
+
+left, right :: Rewritable a => a
+left  = to left'
+right = to right'
+
+instance (Bounded a) => Sampleable a where
+  left'  = minBound
+  right' = maxBound
+
+instance Sampleable Float where
+  left'  = 0
+  right' = 1
+
+instance (Representable a, Empty (Rep a), Representable b, Empty (Rep b)) => Sampleable (a :+: b) where
+  left'  = L gempty
+  right' = R gempty
+
+instance (Sampleable a, Sampleable b) => Sampleable (a :*: b) where
+  left'  = left'  :*: left'
+  right' = right' :*: right'
+
+instance Sampleable U where
+  left'  = U
+  right' = U
+
+instance (Rewritable a) => Sampleable (Rec a) where
+  left'  = Rec left
+  right' = Rec right
+
+instance (Rewritable a) => Sampleable (Var a) where
+  left'  = Var left
+  right' = Var right
+
+instance (Sampleable a) => Sampleable (C c a) where
+  left'  = C left' 
+  right' = C right'
+
+-- | Diff
+
+class Diffable a where
+  diff' :: Typeable b => Ext a gam -> Ext a gam -> Maybe (Ext a (b :*: gam))
+
+diff :: (Rewritable a, Typeable b) =>
+        Scheme a gam -> Scheme a gam -> Maybe (Scheme a (b :*: gam))
+diff (L ext) (L ext')         = 
+  maybe (scast (R Rz)) (Just . L) (diff' ext ext')
+diff (R r)   (R r') | r == r' = Just (R (Rs r))
+diff _       _                = Nothing
+
+newtype FlipScheme gam a = Flip {unFlip :: Scheme a gam}
+
+scast :: (Typeable a, Typeable b) =>
+  Scheme b (b :*: gam) -> Maybe (Scheme a (b :*: gam))
+scast = fmap unFlip . gcast . Flip
+
+(><) :: (Rewritable a, Typeable b) =>
+        Scheme a gam -> Scheme a gam -> (Scheme a (b :*: gam))
+scheme >< scheme' = fromJust (diff scheme scheme')
+
+instance Diffable Int where
+  diff' (ExtInt n) (ExtInt n') | n == n'   = Just (ExtInt n)
+                               | otherwise = Nothing
+
+instance Diffable Char where
+  diff' (ExtChar c) (ExtChar c') | c == c'   = Just (ExtChar c)
+                                 | otherwise = Nothing
+
+instance Diffable Float where
+  diff' (ExtFloat f) (ExtFloat f') | f == f'   = Just (ExtFloat f)
+                                   | otherwise = Nothing
+
+instance (Diffable a, Diffable b) => Diffable (a :+: b) where
+  diff' (ExtSum (L ext)) (ExtSum (L ext')) =
+    fmap (ExtSum . L) (diff' ext ext')
+  diff' (ExtSum (R ext)) (ExtSum (R ext')) =
+    fmap (ExtSum . R) (diff' ext ext')
+  diff' _ _ = Nothing
+
+instance (Diffable a, Diffable b) => Diffable (a :*: b) where
+  diff' (ExtCons (a :*: ext)) (ExtCons (b :*: ext')) =
+    fmap ExtCons (liftM2 (:*:) (diff' a b) (diff' ext ext'))
+
+instance Diffable U where
+  diff' (ExtNil U) (ExtNil U) = Just (ExtNil U)
+
+instance (Rewritable a) => Diffable (Rec a) where
+  diff' (ExtRec (Rec s)) (ExtRec (Rec s')) = fmap ExtRec (liftM Rec (diff s s'))
+
+instance (Rewritable a) => Diffable (Var a) where
+  diff' (ExtVar (Var s)) (ExtVar (Var s')) = fmap ExtVar (liftM Var (diff s s'))
+
+instance (Diffable a) => Diffable (C c a) where
+  diff' (ExtC (C a)) (ExtC (C b)) = fmap ExtC (liftM C (diff' a b))
+
+-- | Templates
+data Template a = Template a a Bool
+
+infix 0 //
+infix 1 +->
+
+(+->) :: a -> a -> Template a
+l +-> r = Template l r True
+
+(//) :: Template a -> Bool -> Template a
+Template l r _ // g = Template l r g
+
+-- | Synthesising rules from metasyntax specifications
+class (Rewritable (Obj a)) => IsRule a where
+  type Obj a :: *
+  type Env a :: *
+
+  synthesise' :: a -> Rule' (Obj a) (Env a)
+
+instance (Rewritable a) => IsRule (Template a) where
+  type Obj (Template a) = a
+  type Env (Template a) = U
+
+  synthesise' (Template l r g) =
+    Rule' {lhs = toScheme l, rhs = toScheme r, guard = g}
+
+instance (Rewritable a, IsRule b) => IsRule (a -> b) where
+  type Obj (a -> b) = Obj b
+  type Env (a -> b) = a :*: Env b
+
+  synthesise' f = Rule'
+    { lhs = lhs l >< lhs r
+    , rhs = rhs l >< rhs r
+    , guard = guard . synthesise' . f
+    }
+    where
+      l = synthesise' (f left)
+      r = synthesise' (f right)
+
+-- | Validating synthesised rules
+class Validatable a where
+  record :: Ext a gam -> Record gam -> Record gam
+  record _ = id
+
+data Record :: * -> * where
+  RNil  :: Record U
+  RCons :: Bool -> Record gam -> Record (a :*: gam)
+
+class Recordable gam where
+  blank :: Record gam
+
+instance Recordable U where
+  blank = RNil
+
+instance Recordable gam => Recordable (a :*: gam) where
+  blank = RCons False blank
+
+record' :: Rewritable a => Scheme a gam -> Record gam -> Record gam
+record' (L e)      rec           = record e rec
+record' (R Rz)     (RCons _ rec) = RCons True rec
+record' (R (Rs r)) (RCons b rec) = RCons b (record' (R r) rec)
+record' _          _             = error "record' failure"
+
+instance Validatable Int
+instance Validatable Float
+instance Validatable Char
+instance Validatable U
+
+instance (Validatable a, Validatable b) => Validatable (a :+: b) where
+  record (ExtSum (L e)) = record e
+  record (ExtSum (R e)) = record e
+
+instance (Validatable a, Validatable b) => Validatable (a :*: b) where
+  record (ExtCons (e :*: es)) = record e . record es
+
+instance (Rewritable a) => Validatable (Rec a) where
+  record (ExtRec (Rec e)) = record' e
+
+instance (Rewritable a) => Validatable (Var a) where
+  record (ExtVar (Var e)) = record' e
+
+instance (Validatable a) => Validatable (C c a) where
+  record (ExtC (C e)) = record e
+
+validate' :: forall a gam. (Rewritable a, Recordable gam)
+          => Rule' a gam -> Bool
+validate' r = conj (record' (lhs r) blank)
+  where
+    conj :: forall gam'. Record gam' -> Bool
+    conj RNil          = True
+    conj (RCons b rec) = b && conj rec
+
+-------------------------------------------------------------------------------
+-- | Type level validation for the datatypes to be rewritten: there can be no
+-- recursive calls on the leftmost constructor
+-------------------------------------------------------------------------------
+
+class Empty a where
+  empty' :: a
+
+instance Empty U where empty' = U
+  
+instance (HasRec a, Empty a, Empty b) => Empty (a :+: b) where
+  empty' = if hasRec' (empty' :: a) then R empty' else L empty'
+  
+instance (Empty a, Empty b) => Empty (a :*: b) where
+  empty' = empty' :*: empty'
+  
+instance (Empty a) => Empty (C c a) where
+  empty' = C empty'
+
+instance (Rewritable a) => Empty (Var a) where
+  empty' = Var gempty
+
+instance (Rewritable a) => Empty (Rec a) where
+  empty' = Rec gempty
+
+instance Empty Int   where empty' = 0
+instance Empty Float where empty' = 0
+instance Empty Char  where empty' = '\NUL'
+
+
+-- Dispatcher
+gempty :: (Representable a, Empty (Rep a)) => a
+gempty = to empty'
+
+
+-- Used to avoid producing infinite values
+class HasRec a where
+  hasRec' :: a -> Bool
+  hasRec' _ = False
+  
+instance HasRec U
+instance HasRec (Var a)
+
+instance (HasRec a, HasRec b) => HasRec (a :*: b) where
+  hasRec' (a :*: b) = hasRec' a || hasRec' b
+  
+instance (HasRec a, HasRec b) => HasRec (a :+: b) where
+  hasRec' (L x) = hasRec' x
+  hasRec' (R x) = hasRec' x
+
+instance (HasRec a) => HasRec (C c a) where
+  hasRec' (C x) = hasRec' x
+  
+instance HasRec (Rec a) where
+  hasRec' _ = True
+  
+instance HasRec Int
+instance HasRec Float
+instance HasRec Char
+
+type family Finite a :: *
+type instance Finite Int       = True
+type instance Finite Float     = True
+type instance Finite Char      = True
+type instance Finite U         = True
+type instance Finite (a :+: b) = Or (Finite a) (Finite b)
+type instance Finite (a :*: b) = And (Finite a) (Finite b)
+type instance Finite (Rec a)   = False
+type instance Finite (Var a)   = True
+type instance Finite (C c a)   = Finite a
+
+data True
+data False
+
+type family And p q
+type instance And True  True  = True
+type instance And True  False = False
+type instance And False True  = False
+type instance And False False = False
+
+type family Or p q
+type instance Or True  True  = True
+type instance Or True  False = True
+type instance Or False True  = True
+type instance Or False False = False
+
+type family FiniteEnv gam
+type instance FiniteEnv U = True
+type instance FiniteEnv (a :*: gam) = And (Finite (Rep a)) (FiniteEnv gam)
+
+-------------------------------------------------------------------------------
+-- Convenience: hiding the environment to the user Rule' type
+-------------------------------------------------------------------------------
+
+-- | Rules
+data Rule a where
+  Rule :: (Nillable gam, Recordable gam, Testable gam)
+       => Rule' a gam -> Rule a
+
+-- | Validate a rewrite rule
+validate :: Rewritable a => Rule a -> Bool
+validate (Rule rule) = validate' rule
+
+-- | Synthesise a function into a rewrite rule
+synthesise :: (IsRule a, Nillable (Env a), Recordable (Env a), 
+               Testable (Env a), FiniteEnv (Env a) ~ True)
+           => a -> Rule (Obj a)
+synthesise r = Rule (synthesise' r)
+
+-- | Rewrite a term. The term is unchanged if the rule cannot be applied.
+rewrite :: Rewritable a => Rule a -> a -> a
+rewrite (Rule rule) x = rewrite' rule x
+
+-- | Rewrite a term. Monad 'fail' is used if the rule cannot be applied.
+rewriteM :: (Rewritable a, Monad m) => Rule a -> a -> m a
+rewriteM (Rule rule) x = rewriteM' rule x