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 the datatype.

Consider a datatype representing logical propositions:

 data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show

 infixr 5 :++:
 infixr 6 :**:

An instance of Regular would look like:

 data Const
 data Plus
 data Times

 instance Constructor Const where conName _ = "Const"
 instance Constructor Plus where 
   conName _   = "(:++:)"
   conFixity _ = Infix RightAssociative 5
 instance Constructor Times where 
   conName _   = "(:**:)"
   conFixity _ = Infix RightAssociative 6

 type instance PF Expr =  C Const (K Int) 
                      :+: C Plus  (I :*: I) 
                      :+: C Times (I :*: I)

 instance Regular Expr where
   from (Const n)    = L (C (K n))
   from (e1 :++: e2) = R (L (C $ (I e1) :*: (I e2)))
   from (e1 :**: e2) = R (R (C $ (I e1) :*: (I e2)))
   to (L (C (K n)))                   = Const n
   to (R (L (C ((I r1) :*: (I r2))))) = r1 :++: r2
   to (R (R (C ((I r1) :*: (I r2))))) = r1 :**: r2

Alternatively, the above code could be derived using Template Haskell:

 $(deriveConstructors ''Expr)
 $(deriveRegular ''Expr "PFExpr")
 type instance PF Expr = PFExpr

Additionally, the instance Rewrite would look like:

 instance Rewrite Expr

Rules are built 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 applied as follows:

 test1 :: Maybe Expr
 test1 = rewriteM rule1 (Const 2 :++: Const 0)
 test10 :: Maybe Expr
 test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))