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