diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,28 @@
+Copyright (c) 2008 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,16 @@
+module Main (main) where
+
+import Distribution.Simple
+import System.Cmd (system)
+import System.FilePath ((</>))
+import System.Directory (doesDirectoryExist, removeDirectoryRecursive)
+
+main :: IO ()
+main = defaultMainWithHooks hooks where
+  hooks = simpleUserHooks { runTests = runTests' }
+
+runTests' _ _ _ _ = system cmd >> return ()
+  where testdir = "dist" </> "build" </> "test"
+        testcmd = "." </> "test"
+        cmd = "cd " ++ testdir ++ " && " ++ testcmd
+
diff --git a/rewriting.cabal b/rewriting.cabal
new file mode 100644
--- /dev/null
+++ b/rewriting.cabal
@@ -0,0 +1,66 @@
+name:                   rewriting
+version:                0.1
+synopsis:               Generic rewriting library for regular datatypes.
+description:
+
+  This package provides rewriting functionality for regular datatypes.
+  Regular datatypes are recursive datatypes such as lists, binary trees,
+  etc. This library cannot be used with mutually recursive datatypes or
+  with nested datatypes.
+  . 
+  This library has been described in the paper:
+  .
+  *  /A Lightweight Approach to Datatype-Generic Rewriting./
+     Thomas van Noort, Alexey Rodriguez, Stefan Holdermans, Johan Jeuring, Bastiaan Heeren.
+     ACM SIGPLAN Workshop on Generic Programming 2008.
+  .
+  More information about this library can be found at
+  <http://www.cs.uu.nl/wiki/GenericProgramming/Rewriting>.
+
+category:               Generics
+copyright:              (c) 2008 Universiteit Utrecht
+license:                BSD3
+license-file:           LICENSE
+author:                 Thomas van Noort,
+                        Alexey Rodriguez,
+                        Stefan Holdermans,
+                        Johan Jeuring,
+                        Bastiaan Heeren
+maintainer:             generics@haskell.org
+stability:              experimental
+build-type:             Custom
+cabal-version:          >= 1.2.1
+tested-with:            GHC == 6.10.0.20081007
+
+-- Disabled the test flag for the moment since not all
+-- modules from the tests directory are properly included
+-- in the distribution generated by the sdist target
+--
+-- flag test
+--  description:          Enable the test configuration
+--  default:              False
+
+library
+  buildable:            True
+  hs-source-dirs:       src
+  exposed-modules:      Generics.Regular.Rewriting
+                        Generics.Regular.Rewriting.Base
+                        Generics.Regular.Rewriting.Representations
+                        Generics.Regular.Rewriting.Machinery
+                        Generics.Regular.Rewriting.Rules
+                        Generics.Regular.Rewriting.Strategies
+
+  build-depends:        base >= 3.0, containers >= 0.1
+
+-- Disabled the test flag for the moment since not all
+-- modules from the tests directory are properly included
+-- in the distribution generated by the sdist target
+--
+--executable test
+--  hs-source-dirs:       src, tests
+--  main-is:              Main.hs
+--  
+--  if flag (test)
+--    build-depends:      QuickCheck >= 2.1.0.1
+
+
diff --git a/src/Generics/Regular/Rewriting.hs b/src/Generics/Regular/Rewriting.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Regular/Rewriting.hs
@@ -0,0 +1,98 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Regular.Rewriting
+-- Copyright   :  (c) 2008 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- By importing this module, the user is able to use all the rewriting
+-- machinery. The user is only required to provide an instance of 
+-- @Regular@ and @Rewrite@ for his datatype.
+--
+-- Consider a datatype representing logical propositions:
+--
+-- @
+--   data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show
+-- @
+--
+-- An instance of @Regular@ would look like:
+--
+-- @
+--   instance Regular Expr where
+--     type PF Expr = K Int :+: Id :*: Id :+: Id :*: Id
+--     from (Const n)    = L (K n)
+--     from (e1 :++: e2) = R (L  $ (Id e1) :*: (Id e2))
+--     from (e1 :**: e2) = R (R  $ (Id e1) :*: (Id e2))
+--     to (L (K n))                     = Const n
+--     to (R (L ((Id r1) :*: (Id r2)))) = r1 :++: r2
+--     to (R (R ((Id r1) :*: (Id r2)))) = r1 :**: r2
+-- @
+--
+-- Additionally, the instance @Rewrite@ would look like:
+--
+-- @
+--   instance Rewrite Expr
+-- @
+--
+-- Build rules like this:
+--
+-- @
+--   rule1 :: Rule Expr
+--   rule1 = 
+--     rule $ \x -> x :++: Const 0 :~>
+--                 x
+--   rule5 :: Rule Expr
+--   rule5 = 
+--     rule $ \x y z -> x :**: (y :++: z) :~>  
+--                     (x :**: y) :++: (x :**: z) 
+-- @
+--
+-- And apply them as follows:
+--
+-- @
+--   test1 :: Maybe Expr
+--   test1 = rewriteM rule1 (Const 2 :++: Const 0)
+--   test10 :: Maybe Expr
+--   test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))
+-- @
+--
+-- You may also wish to add constructor names in the representation to use
+-- generic show. However, constructor names are not yet a stable feature
+-- and will probably change in future versions of this library.
+--
+-- @
+--   instance Regular Expr where
+--     type PF Expr = Con (K Int) :+: Con (Id :*: Id) :+: Con (Id :*: Id)
+--     from (Const n)    = L (Con \"Const\" (K n))
+--     from (e1 :++: e2) = R (L (Con \"(:++:)\" $ (Id e1) :*: (Id e2)))
+--     from (e1 :**: e2) = R (R (Con \"(:**:)\" $ (Id e1) :*: (Id e2)))
+--     to (L (Con _ (K n)))                        = Const n
+--     to (R (L (Con _ ((Id r1) :*: (Id r2))))) = r1 :++: r2
+--     to (R (R (Con _ ((Id r1) :*: (Id r2))))) = r1 :**: r2
+-- @
+--
+
+-----------------------------------------------------------------------------
+
+module Generics.Regular.Rewriting (
+
+  module Generics.Regular.Rewriting.Base,
+
+  module Generics.Regular.Rewriting.Machinery,
+
+  module Generics.Regular.Rewriting.Representations,
+
+  module Generics.Regular.Rewriting.Rules,
+
+  module Generics.Regular.Rewriting.Strategies
+
+) where
+
+import Generics.Regular.Rewriting.Base
+import Generics.Regular.Rewriting.Machinery
+import Generics.Regular.Rewriting.Representations
+import Generics.Regular.Rewriting.Rules
+import Generics.Regular.Rewriting.Strategies
diff --git a/src/Generics/Regular/Rewriting/Base.hs b/src/Generics/Regular/Rewriting/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Regular/Rewriting/Base.hs
@@ -0,0 +1,279 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators    #-}
+{-# LANGUAGE TypeFamilies     #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Regular.Rewriting.Base
+-- Copyright   :  (c) 2008 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Summary: Base generic functions that are used for generic rewriting.
+-----------------------------------------------------------------------------
+
+module Generics.Regular.Rewriting.Base (
+
+  -- * Functorial map function.
+  Functor (..),
+  
+  -- * Monadic functorial map function.
+  GMap (..),
+  
+  -- * Crush functions.
+  Crush (..),
+  flatten,
+
+  -- * Zip functions.
+  Zip (..),
+  fzip,
+  fzip',
+
+  -- * Equality function.
+  geq,
+
+  -- * Show function.
+  GShow (..),
+  
+  -- * Functions for generating values that are different on top-level.
+  LRBase (..),
+  LR (..),
+  left,
+  right  
+
+) where
+
+import Control.Monad
+
+import Generics.Regular.Rewriting.Representations
+
+
+-----------------------------------------------------------------------------
+-- Functorial map function.
+-----------------------------------------------------------------------------
+
+instance Functor Id where
+  fmap f (Id r) = Id (f r)
+
+instance Functor (K a) where
+  fmap _ (K a) = K a
+
+instance Functor Unit where
+  fmap _ Unit = Unit
+
+instance (Functor f, Functor g) => Functor (f :+: g) where
+  fmap f (L x) = L (fmap f x)
+  fmap f (R y) = R (fmap f y)
+
+instance (Functor f, Functor g) => Functor (f :*: g) where
+  fmap f (x :*: y) = fmap f x :*: fmap f y
+
+instance Functor f => Functor (Con f) where
+  fmap f (Con con r) = Con con (fmap f r)
+
+
+-----------------------------------------------------------------------------
+-- Monadic functorial map function.
+-----------------------------------------------------------------------------
+
+-- | The @GMap@ class defines a monadic functorial map.
+class GMap f where
+  fmapM :: Monad m => (a -> m b) -> f a -> m (f b)
+
+instance GMap Id where
+  fmapM f (Id r) = liftM Id (f r)
+
+instance GMap (K a) where
+  fmapM _ (K x)  = return (K x)
+
+instance GMap Unit where
+  fmapM _ Unit = return Unit
+
+instance (GMap f, GMap g) => GMap (f :+: g) where
+  fmapM f (L x) = liftM L (fmapM f x)
+  fmapM f (R x) = liftM R (fmapM f x)
+
+instance (GMap f, GMap g) => GMap (f :*: g) where
+  fmapM f (x :*: y) = liftM2 (:*:) (fmapM f x) (fmapM f y)
+
+instance GMap f => GMap (Con f) where
+  fmapM f (Con c x) = liftM (Con c) (fmapM f x)
+
+
+-----------------------------------------------------------------------------
+-- Crush functions.
+-----------------------------------------------------------------------------
+
+-- | The @Crush@ class defines a crush on functorial values. In fact,
+-- @crush@ is a generalized @foldr@.
+class Crush f where
+  crush :: (a -> b -> b) -> b -> f a -> b
+
+instance Crush Id where
+  crush op e (Id x) = x `op` e
+
+instance Crush (K a) where
+  crush _ e _ = e
+
+instance Crush Unit where
+  crush _ e _ = e
+
+instance (Crush f, Crush g) => Crush (f :+: g) where
+  crush op e (L x) = crush op e x
+  crush op e (R y) = crush op e y
+
+instance (Crush f, Crush g) => Crush (f :*: g) where
+  crush op e (x :*: y) = crush op (crush op e y) x
+
+instance Crush f => Crush (Con f) where
+  crush op e (Con _c x) = crush op e x
+
+-- | Flatten a structure by collecting all the elements present.
+flatten :: Crush f => f a -> [a]
+flatten = crush (:) []
+
+
+-----------------------------------------------------------------------------
+-- Zip functions.
+-----------------------------------------------------------------------------
+
+-- | The @Zip@ class defines a monadic zip on functorial values.
+class Zip f where
+  fzipM :: Monad m => (a -> b -> m c) -> f a -> f b -> m (f c)
+
+instance Zip Id where
+  fzipM f (Id x) (Id y) = liftM Id (f x y)
+
+instance Eq a => Zip (K a) where
+  fzipM _ (K x) (K y) 
+    | x == y    = return (K x)
+    | otherwise = fail "fzipM: structure mismatch"
+
+instance Zip Unit where
+  fzipM _ Unit Unit = return Unit
+
+instance (Zip f, Zip g) => Zip (f :+: g) where
+  fzipM f (L x) (L y) = liftM L (fzipM f x y)
+  fzipM f (R x) (R y) = liftM R (fzipM f x y)
+  fzipM _ _       _       = fail "fzipM: structure mismatch"
+
+instance (Zip f, Zip g) => Zip (f :*: g) where
+  fzipM f (x1 :*: y1) (x2 :*: y2) = 
+    liftM2 (:*:) (fzipM f x1 x2)
+                 (fzipM f y1 y2)
+
+instance Zip f => Zip (Con f) where
+  fzipM f (Con c1 x) (Con _c2 y) = liftM (Con c1) (fzipM f x y)
+
+-- | Functorial zip with a non-monadic function, resulting in a monadic value.
+fzip  :: (Zip f, Monad m) => (a -> b -> c) -> f a -> f b -> m (f c)
+fzip f = fzipM (\x y -> return (f x y))
+
+-- | Partial functorial zip with a non-monadic function.
+fzip' :: Zip f => (a -> b -> c) -> f a -> f b -> f c
+fzip' f x y = maybe (error "fzip': structure mismatch") id (fzip f x y)
+
+
+-----------------------------------------------------------------------------
+-- Equality function.
+-----------------------------------------------------------------------------
+
+-- | Equality on values based on their structural representation.
+geq :: (b ~ PF a, Regular a, Crush b, Zip b) => a -> a -> Bool
+geq x y = maybe False (crush (&&) True) (fzip geq (from x) (from y))
+
+
+-----------------------------------------------------------------------------
+-- Show function.
+-----------------------------------------------------------------------------
+
+-- | The @GShow@ class defines a show on values.
+class GShow f where
+  gshow :: (a -> ShowS) -> f a -> ShowS
+
+instance GShow Id where
+  gshow f (Id r) = f r
+
+instance Show a => GShow (K a) where
+  gshow _ (K x) = shows x
+
+instance GShow Unit where
+  gshow _ Unit = id
+
+instance (GShow f, GShow g) => GShow (f :+: g) where
+  gshow f (L x) = gshow f x
+  gshow f (R x) = gshow f x
+
+instance (GShow f, GShow g) => GShow (f :*: g) where
+  gshow f (x :*: y) = gshow f x . showChar ' ' . gshow f y
+
+instance GShow f => GShow (Con f) where
+  gshow f (Con c x) = showParen True (showString c . showChar ' ' . gshow f x)
+
+
+-----------------------------------------------------------------------------
+-- Functions for generating values that are different on top-level.
+-----------------------------------------------------------------------------
+
+-- | The @LRBase@ class defines two functions, @leftb@ and @rightb@, which 
+-- should produce different values.
+class LRBase a where
+  leftb  :: a
+  rightb :: a
+
+instance LRBase Int where
+  leftb  = 0
+  rightb = 1
+
+instance LRBase Char where
+  leftb  = 'L'
+  rightb = 'R'
+ 
+instance LRBase a => LRBase [a] where
+  leftb  = []
+  rightb = [error "Should never be inspected"]
+
+-- | The @LR@ class defines two functions, @leftf@ and @rightf@, which should 
+-- produce different functorial values.
+class LR f where
+  leftf  :: a -> f a
+  rightf :: a -> f a
+
+instance LR Id where
+  leftf  x = Id x
+  rightf x = Id x
+
+instance LRBase a => LR (K a) where
+  leftf  _ = K leftb
+  rightf _ = K rightb
+
+instance LR Unit where
+  leftf  _ = Unit
+  rightf _ = Unit
+
+instance (LR f, LR g) => LR (f :+: g)  where
+  leftf  x = L (leftf x)
+  rightf x = R (rightf x)
+
+instance (LR f, LR g) => LR (f :*: g)  where
+  leftf  x = leftf x :*: leftf x
+  rightf x = rightf x :*: rightf x
+
+instance LR f => LR (Con f) where
+  leftf  x = Con (error "Should never be inspected") (leftf x)
+  rightf x = Con (error "Should never be inspected") (rightf x)
+
+-- | Produces a value which should be different from the value returned by 
+-- @right@.
+left :: (Regular a, LR (PF a)) => a
+left = to (leftf left)
+
+-- | Produces a value which should be different from the value returned by 
+-- @left@.
+right :: (Regular a, LR (PF a)) => a
+right = to (rightf right)
diff --git a/src/Generics/Regular/Rewriting/Machinery.hs b/src/Generics/Regular/Rewriting/Machinery.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Regular/Rewriting/Machinery.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Regular.Rewriting.Machinery
+-- Copyright   :  (c) 2008 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Summary: Core machinery for rewriting terms.
+-----------------------------------------------------------------------------
+
+module Generics.Regular.Rewriting.Machinery (
+
+  -- * Type class synonym summarizing generic functions
+  Rewrite,
+
+  -- * Applying a rule specification to a term.
+  applyRuleM,
+  applyRule,
+
+  -- * Rewriting a term.
+  rewriteM,
+  rewrite,
+
+)  where
+
+import Control.Monad
+import qualified Data.Map as M
+import Data.Maybe
+
+import Generics.Regular.Rewriting.Base
+import Generics.Regular.Rewriting.Representations
+import Generics.Regular.Rewriting.Rules
+
+
+-----------------------------------------------------------------------------
+-- Type class synonym summarizing generic functions
+-----------------------------------------------------------------------------
+-- | The @Rewrite@ is a type class synonym, hiding some of the implementation
+-- details.
+--
+-- To be able to use the rewriting functions, the user is required to provide
+-- an instance of this type class.
+class (Regular a, Crush (PF a), GMap (PF a), GShow (PF a), Zip (PF a), LR (PF a)) => Rewrite a
+
+
+-----------------------------------------------------------------------------
+-- Applying a rule to a term.
+-----------------------------------------------------------------------------
+
+{-# INLINE applyRuleM #-}
+-- | Applies a rule specification to a term, obtaining a monadic value.
+applyRuleM :: (Builder r, Rewrite (Target r), Monad m) => r -> Target r -> m (Target r)
+applyRuleM = rewriteM . rule
+
+{-# INLINE applyRule #-}
+-- | Applies a rule specification to a term, obtaining the original term 
+-- when rewriting fails.
+applyRule :: (Builder r, Rewrite (Target r)) => r -> Target r -> Target r
+applyRule = rewrite . rule
+
+
+-----------------------------------------------------------------------------
+-- Rewriting a term.
+-----------------------------------------------------------------------------
+
+{-# INLINE rewriteM #-}
+-- | Rewrites a term, obtaining a monadic value.
+rewriteM :: (Rewrite a, Monad m) => Rule a -> a -> m a 
+rewriteM f term = 
+  do subst <- match (lhsR f) term
+     return (inst subst (rhsR f))
+
+{-# INLINE rewrite #-}
+-- | Rewrites a term, obtaining the original term when rewriting fails.
+rewrite :: Rewrite a => Rule a -> a -> a
+rewrite f term = maybe term id (rewriteM f term)
+
+
+-----------------------------------------------------------------------------
+-- Matching a term.
+-----------------------------------------------------------------------------
+
+-- | A substitution maps a metavariable to a pair of the original term
+-- and the converted term. Both are stored to improve efficiency, since
+-- the right-hand side of a term may caontain multiple occurrences of the
+-- same metavariable.
+type Subst a = M.Map Metavar (a, SchemeOf a)
+
+-- | Matches a term to the left-hand side of a rule.
+match :: (Rewrite a, Monad m) => SchemeOf a -> a -> m (Subst a)
+match scheme term = 
+  case schemeView scheme of
+    Metavar x -> return (M.singleton x (term, toScheme term))
+    PF r      ->
+      fzip (,) r (from term) >>=
+      crush matchOne (return M.empty)
+  where
+    matchOne (term1, term2) msubst = 
+      do subst1 <- msubst
+         subst2 <- match (apply subst1 term1) term2
+         return (M.union subst1 subst2)
+
+
+-----------------------------------------------------------------------------
+-- Building a term.
+-----------------------------------------------------------------------------
+
+-- | Applies a substitution to a term.
+apply :: Regular a => Subst a -> SchemeOf a -> SchemeOf a
+apply subst = foldScheme findMetavar pf
+  where
+    findMetavar x = maybe (metavar x) snd (M.lookup x subst)
+
+-- | Instantiates all the metavariables in a term, assuming that there are no
+-- unbound metavariables in the term.
+inst :: Regular a => Subst a -> SchemeOf a -> a
+inst subst = foldScheme findMetavar to
+  where
+    findMetavar x = 
+      maybe undefined fst (M.lookup x subst)
diff --git a/src/Generics/Regular/Rewriting/Representations.hs b/src/Generics/Regular/Rewriting/Representations.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Regular/Rewriting/Representations.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE FlexibleContexts   #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies       #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Regular.Rewriting.Representations
+-- Copyright   :  (c) 2008 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Summary: Types for structural representation.
+-----------------------------------------------------------------------------
+
+module Generics.Regular.Rewriting.Representations (
+
+  -- * Functorial structural representation types.
+  K (..),
+  Id (..),
+  Unit (..),
+  (:+:) (..),
+  (:*:) (..),
+  Con (..),
+
+  -- * Fixed-point type.
+  Fix (..),
+
+  -- * Type class capturing the structural representation of a type and the
+  -- | corresponding embedding-projection pairs.
+  Regular (..)
+  
+) where
+
+
+-----------------------------------------------------------------------------
+-- Functorial structural representation types.
+-----------------------------------------------------------------------------
+
+-- | Structure type for constant values.
+data K a r      = K a
+
+-- | Structure type for recursive values.
+data Id r       = Id r
+
+-- | Structure type for empty constructors.
+data Unit r     = Unit
+
+-- | Structure type for alternatives in a type.
+data (f :+: g) r  = L (f r) | R (g r)
+
+-- | Structure type for fields of a constructor.
+data (f :*: g) r = f r :*: g r
+
+-- | Structure type to store the name of a constructor.
+data Con f r    = Con String (f r)
+
+infixr 6 :+:
+infixr 7 :*:
+
+-----------------------------------------------------------------------------
+-- Fixed-point type.
+-----------------------------------------------------------------------------
+
+-- | The well-known fixed-point type.
+newtype Fix f = In (f (Fix f))
+
+
+-----------------------------------------------------------------------------
+-- Type class capturing the structural representation of a type and the
+-- | corresponding embedding-projection pairs.
+-----------------------------------------------------------------------------
+
+-- | The type class @Regular@ captures the structural representation of a 
+-- type and the corresponding embedding-projection pairs.
+--
+-- To be able to use the rewriting functions, the user is required to provide
+-- an instance of this type class.
+class Functor (PF a) => Regular a where
+  type PF a :: * -> *
+  from      :: a -> PF a a
+  to        :: PF a a -> a
+
+
diff --git a/src/Generics/Regular/Rewriting/Rules.hs b/src/Generics/Regular/Rewriting/Rules.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Regular/Rewriting/Rules.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies     #-}
+{-# LANGUAGE TypeOperators    #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Regular.Rewriting.Rules
+-- Copyright   :  (c) 2008 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Summary: Functions for transforming a rule specification to a rule.
+--
+
+
+-----------------------------------------------------------------------------
+
+module Generics.Regular.Rewriting.Rules (
+
+  -- * Rule specification.
+  RuleSpec (..),
+  lhsR,
+  rhsR,
+  
+  -- * Representation of a rule.
+  Rule,
+  SchemeOf,
+  Metavar,
+  metavar,
+  pf, 
+  toScheme,
+  SchemeView (..),
+  schemeView,
+  foldScheme,
+
+  -- * Builder for transforming a rule specification to a rule.
+  Builder (..),
+  ruleM, 
+  rule
+
+) where
+
+import Data.List
+
+import Generics.Regular.Rewriting.Base
+import Generics.Regular.Rewriting.Representations
+
+
+-----------------------------------------------------------------------------
+-- Rule specification.
+-----------------------------------------------------------------------------
+
+-- | Specifies a rule as a value of a datatype.
+infix 5 :~>
+data RuleSpec a = a :~> a
+
+-- | Returns the left-hand side of a rule.
+lhsR :: RuleSpec a -> a
+lhsR (x :~> _) = x
+
+-- | Returns the right-hand side of a rule.
+rhsR :: RuleSpec a -> a
+rhsR (_ :~> y) = y
+
+
+-----------------------------------------------------------------------------
+-- Representation of a rule.
+-----------------------------------------------------------------------------
+
+-- | Extends a pattern functor with a case for a metavariable.
+type Ext f    = K Metavar :+: f
+type Metavar  = Int
+
+-- | Recursively extends a type with a case for a metavariable.
+type Scheme f = Fix (Ext f)
+
+-- | Extends the pattern functor of a value.
+type SchemeOf a = Scheme (PF a)
+
+-- | Allows metavariables on either side of a rule.
+type Rule a = RuleSpec (SchemeOf a)
+
+-- | Constructs a metavariable.
+metavar :: Metavar -> Scheme f
+metavar = In . L . K
+
+-- | Constructs a pattern functor value.
+pf :: f (Scheme f) -> Scheme f
+pf = In . R
+
+-- | A view on schemes to easily distinguish metavariables from
+-- pattern functor values.
+data SchemeView f = Metavar Metavar | PF (f (Scheme f))
+
+-- | Returns the value corresponding to the @SchemeView@.
+schemeView :: Scheme f -> SchemeView f
+schemeView (In (L (K x))) = Metavar x
+schemeView (In (R r))     = PF r
+
+-- | Recursively converts a value to a @SchemeOf@ value.
+toScheme :: Regular a => a -> SchemeOf a
+toScheme = pf . fmap toScheme . from
+
+-- | Folds a @Scheme@ value given a function to apply to metavariables and a
+-- function to apply to a pattern functor value.
+foldScheme :: Functor f => (Metavar -> a) -> (f a -> a) -> Scheme f -> a
+foldScheme f g scheme =
+  case schemeView scheme of
+    Metavar x -> f x
+    PF r      -> g (fmap (foldScheme f g) r)
+
+
+-----------------------------------------------------------------------------
+-- Builder for transforming a rule specification to a rule.
+-----------------------------------------------------------------------------
+
+-- | The type class @Builder@ captures the functions, that are defined by
+-- induction on the type argument, that construct appropriate @left@ and 
+-- @right@ values. These values are used to transform a rule specification
+-- to a rule.
+class Regular (Target a) => Builder a where
+  type Target a :: *
+  base          :: a -> RuleSpec (Target a)
+  diag          :: a -> [RuleSpec (Target a)]
+
+instance Regular a => Builder (RuleSpec a) where
+  type Target (RuleSpec a) = a
+  base x                   = x
+  diag x                   = [x]
+
+instance (Builder a, Regular b, LR (PF b)) => Builder (b -> a) where
+  type Target (b -> a) = Target a
+  base f               = base (f left)
+  
+  -- Since mergeSchemes prefers metavariables in the first argument, it
+  -- suffices to provide undefined to f in the recursive call to diag:
+  --
+  -- f left left to f right left, and
+  -- f left left to f undefined right
+  -- 
+  -- The first hole of the first instance of f is filled with a metavariable, 
+  -- after which mergeSchemes does not care any more about the first hole
+  -- of the second instance of f.
+  diag f               = base (f right) : diag (f left)
+
+-- | Transforms a rule specification to a rule and throws a runtime error if
+-- an unbound metavariable occurs in the right-hand side of the rule.
+rule :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Rule (Target r)
+rule = maybe (error "rule: unbound metavariable") id . ruleM
+
+-- | Transforms a rule specification to a rule and returns @Nothing@ if
+-- an unbound metavariable occurs in the right-hand side of the rule.
+ruleM :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Maybe (Rule (Target r))
+ruleM f = checkMetavars $ foldr1 mergeRules rules
+  where
+    checkMetavars r 
+      | allElem rMetavars lMetavars = Just r
+      | otherwise                   = Nothing
+      where 
+        allElem xs ys = all (`elem` ys) xs
+        lMetavars = collectMetavars (lhsR r) [] 
+        rMetavars = collectMetavars (rhsR r) []
+        collectMetavars = foldScheme (:) (crush (.) id)
+    mergeRules x y = 
+      mergeSchemes (lhsR x) (lhsR y) :~>
+      mergeSchemes (rhsR x) (rhsR y)
+    rules          = zipWith (ins (base f)) (diag f) [0..]   
+    ins x y v      = 
+      insertMetavar v (lhsR x) (lhsR y) :~>
+      insertMetavar v (rhsR x) (rhsR y)
+
+-- | Merges two schemes by preferring the metavariables that occur in either
+-- of the two arguments.
+mergeSchemes :: Zip f => Scheme f -> Scheme f -> Scheme f
+mergeSchemes p@(In x) q@(In y) =
+  case (schemeView p, schemeView q) of
+    (Metavar _, _)  ->  p
+    (_, Metavar _)  ->  q 
+    _               ->  In (fzip' mergeSchemes x y)
+
+-- | Inserts a metavariable in the right place by zipping two instances of
+-- the function that are applied to different values. These values ensure
+-- that the zipping process fails exactly at the point where a metavariable
+-- is required to be inserted.
+insertMetavar :: (Regular a, Zip (PF a)) => Metavar -> a -> a -> SchemeOf a
+insertMetavar v x y =
+  case fzip (insertMetavar v) (from x) (from y) of
+    Just str -> pf str
+    Nothing  -> metavar v
diff --git a/src/Generics/Regular/Rewriting/Strategies.hs b/src/Generics/Regular/Rewriting/Strategies.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Regular/Rewriting/Strategies.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Regular.Rewriting.Strategies
+-- Copyright   :  (c) 2008 Universiteit Utrecht
+-- License     :  BSD3
+--
+-- Maintainer  :  generics@haskell.org
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Summary: Generic functions for traversal strategies.
+-----------------------------------------------------------------------------
+
+module Generics.Regular.Rewriting.Strategies (
+
+  -- * Apply a function to the children of a value
+  once,
+  one,
+
+  -- * Apply a (monadic) function exhaustively top-down
+  topdownM,
+  topdown,
+
+  -- * Apply a (monadic) function exhaustively bottom-up
+  bottomupM,
+  bottomup,
+
+  -- * Apply a (monadic) function to immediate children
+  composM,
+  compos
+
+) where
+
+import Control.Monad
+
+import Generics.Regular.Rewriting.Base
+import Generics.Regular.Rewriting.Representations
+
+
+-----------------------------------------------------------------------------
+-- Functions to apply a function to the children of a value
+-----------------------------------------------------------------------------
+
+{-# INLINE once #-}
+-- | Applies a function to the first subtree (possibly the tree itself) on which
+-- it succeeds, using a preorder traversal.
+once :: (Regular a, GMap (PF a), Functor m, MonadPlus m) => (a -> m a) -> a -> m a
+once f x = f x `mplus` one (once f) x
+
+{-# INLINE one #-}
+-- | Applies a function to the first immediate child of a value on which it succeeds.
+one :: (Regular a, GMap (PF a), Functor m, MonadPlus m) => (a -> m a) -> a -> m a
+one f x = fmap to rs
+  where 
+    S _ rs = fmapM try (from x)
+    try x' = S x' (f x')
+
+-- | Same monad to that in the SYB3 paper. It is used as follows: the first 
+-- argument contains the original value, and the second arguments contain 
+-- the transformed values.
+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 (rs2 `mplus` rs1)
+    where 
+      S r rs1 = k x
+      rs2     = 
+        do x' <- xs
+           let S r' _ = k x'
+           return r'
+
+
+-----------------------------------------------------------------------------
+-- Apply a (monadic) function exhaustively top-down
+-----------------------------------------------------------------------------
+
+{-# INLINE topdownM #-}
+-- | Applies a monadic function exhaustively in a top-down fashion.
+topdownM :: (Regular a, GMap (PF a), Functor m, Monad m) => (a -> m a) -> a -> m a
+topdownM f x = f x >>= composM (topdownM f)
+
+{-# INLINE topdown #-}
+-- | Applies a function exhaustively in a top-down fashion
+topdown :: Regular a => (a -> a) -> a -> a
+topdown f x = compos (topdown f) (f x)
+
+
+-----------------------------------------------------------------------------
+-- Apply a (monadic) function exhaustively bottom-up
+-----------------------------------------------------------------------------
+
+{-# INLINE bottomupM #-}
+-- | Applies a monadic function exhaustively in a bottom-up fashion.
+bottomupM :: (Regular a, GMap (PF a), Functor m, Monad m) => (a -> m a) -> a -> m a
+bottomupM f x = composM (bottomupM f) x >>= f
+
+{-# INLINE bottomup #-}
+-- | Applies a function exhaustively in a bottom-up fashion
+bottomup :: Regular a => (a -> a) -> a -> a
+bottomup f x = f (compos (bottomup f) x)
+
+
+-----------------------------------------------------------------------------
+-- Apply a (monadic) function to immediate children
+-----------------------------------------------------------------------------
+
+{-# INLINE composM #-}
+-- | Applies a monadic function to all the immediate children of a value.
+composM :: (Regular a, GMap (PF a), Functor m, Monad m) => (a -> m a) -> a -> m a
+composM f = fmap to . fmapM f . from
+
+{-# INLINE compos #-}
+-- | Applies a function to all the immediate children of a value.
+compos :: Regular a => (a -> a) -> a -> a
+compos f = to . fmap f . from