rewriting-0.2.1: Generic rewriting library for regular datatypes.

Portabilitynon-portable
Stabilityexperimental
Maintainergenerics@haskell.org

Generics.Regular.Rewriting

Description

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)))

Documentation