transformations (empty) → 0.1.0.0

raw patch · 22 files changed

+3232/−0 lines, 22 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl, multirec, parsec, regular, rewriting, zipper

Files

• Generics/MultiRec/Any.hs +17/−0
• Generics/MultiRec/HZip.hs +76/−0
• Generics/MultiRec/LR.hs +94/−0
• Generics/MultiRec/Ord.hs +57/−0
• Generics/MultiRec/Rewriting.hs +7/−0
• Generics/MultiRec/Rewriting/Machinery.hs +66/−0
• Generics/MultiRec/Rewriting/Rules.hs +100/−0
• Generics/MultiRec/Transformations/Explicit.hs +413/−0
• Generics/MultiRec/Transformations/RewriteRules.hs +59/−0
• Generics/MultiRec/Transformations/ZipperState.hs +72/−0
• Generics/Regular/Functions/GOrd.hs +41/−0
• Generics/Regular/Transformations/Explicit.hs +329/−0
• Generics/Regular/Transformations/RewriteRules.hs +31/−0
• Generics/Regular/Transformations/ZipperState.hs +57/−0
• Generics/Regular/Zipper.hs +245/−0
• LICENSE +675/−0
• Setup.hs +2/−0
• examples/Datatypes.hs +81/−0
• examples/Lang.lhs +368/−0
• examples/MultiRec.hs +177/−0
• examples/Regular.hs +212/−0
• transformations.cabal +53/−0

@@ -0,0 +1,17 @@+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE GADTs                 #-}
+
+module Generics.MultiRec.Any where
+
+import Generics.MultiRec
+
+data Any phi where
+  Any :: phi ix -> ix -> Any phi
+
+-- | Unify an 'Any' with an @a@.
+matchAny :: forall phi ix. EqS phi => phi ix -> Any phi -> Maybe ix
+matchAny p (Any w x) = match' w x p where
+  match' :: EqS s => s b -> b -> s a -> Maybe a
+  match' w x w' = case eqS w w' of
+    Nothing -> Nothing
+    Just Refl -> Just x

@@ -0,0 +1,76 @@+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs                 #-}
+
+module Generics.MultiRec.HZip where
+
+import Generics.MultiRec
+import Control.Monad (liftM, liftM2, zipWithM)
+
+class HZip phi f where
+  hzipM :: Monad m =>
+           (forall ix. El phi ix => phi ix -> r ix -> r' ix -> m (r'' ix)) ->
+           f r ix -> f r' ix -> m (f r'' ix)
+
+instance El phi xi => HZip phi (I xi) where
+  hzipM f (I x) (I y) = liftM I (f proof x y)
+
+instance Eq a => HZip phi (K a) where
+  hzipM f (K x) (K y) | x == y    = return (K x)
+                      | otherwise = fail "zip failed in K"
+
+instance HZip phi U where
+  hzipM f U U = return U
+
+instance (HZip phi a, HZip phi b) => HZip phi (a :+: b) where
+  hzipM f (L x) (L y) = liftM L (hzipM f x y)
+  hzipM f (R x) (R y) = liftM R (hzipM f x y)
+  hzipM f _     _     = fail "zip failed"
+
+instance (HZip phi a, HZip phi b) => HZip phi (a :*: b) where
+  hzipM f (x1 :*: y1) (x2 :*: y2) = liftM2 (:*:) (hzipM f x1 x2) (hzipM f y1 y2)
+
+instance HZip phi f => HZip phi (f :>: xi) where
+  hzipM f (Tag x) (Tag y) = liftM Tag (hzipM f x y)
+
+instance HZip phi f => HZip phi (C c f) where
+  hzipM f (C x) (C y) = liftM C (hzipM f x y)
+
+instance HZip phi f => HZip phi ([] :.: f) where
+  hzipM f (D x) (D y) = liftM D (zipWithM (hzipM f) x y)
+
+-- | Monadic zip but argument is not monadic
+hzip :: (HZip phi f, Monad m) =>
+        (forall ix. El phi ix => phi ix -> r ix -> s ix -> t ix) ->
+        phi ix -> f r ix -> f s ix -> m (f t ix)
+hzip f p = hzipM (\w x y -> return (f w x y))
+
+-- | Unsafe zip
+hzip' :: (HZip phi f) =>
+         (forall ix. El phi ix => phi ix -> r ix -> s ix -> t ix) ->
+         phi ix -> f r ix -> f s ix -> f t ix
+hzip' f p a b = case hzip (\p x y -> f p x y) p a b of
+  Nothing  -> error "generic zip failed"
+  Just res -> res
+
+-- | Combine two structures monadically only
+combine :: forall phi f r r' m ix. (Monad m, HZip phi f) =>
+           (forall ix. El phi ix => phi ix -> r ix -> r' ix -> m ()) ->
+           phi ix -> f r ix -> f r' ix -> m ()
+combine f l x y = hzipM wrapf x y >> return ()
+  where
+    wrapf :: forall ix' b. El phi ix' => phi ix' -> r ix' -> r' ix' -> m (K0 () b)
+    wrapf ix x y = f ix x y >> return (K0 ())
+
+-- | Generic equality
+geq :: (Fam phi, HZip phi (PF phi)) => phi ix -> ix -> ix -> Bool
+geq ix x y = maybe False (const True) (geq' ix (I0 x) (I0 y))
+
+-- | Monadic generic equality (just for the sake of the monad!)
+geq' :: (Monad m, Fam phi, HZip phi (PF phi))
+        => phi ix -> I0 ix -> I0 ix -> m ()
+geq' p (I0 x) (I0 y) = combine geq' p (from p x) (from p y)

@@ -0,0 +1,94 @@+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs                 #-}
+
+module Generics.MultiRec.LR where
+
+import Generics.MultiRec
+
+-----------------------------------------------------------------------------
+-- 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 Integer where
+  leftb  = 0
+  rightb = 1
+
+instance LRBase Char where
+  leftb  = 'L'
+  rightb = 'R'
+ 
+instance LRBase Bool where
+  leftb  = True
+  rightb = False
+
+instance LRBase a => LRBase [a] where
+  leftb  = []
+  rightb = [rightb]
+
+-- | The @LR@ class defines two functions, @leftf@ and @rightf@, which should 
+-- produce different functorial values.
+class LR phi (f :: (* -> *) -> * -> *) where
+--    leftf  :: s ix -> (forall ix . Ix s ix => s ix -> r ix) -> [f s r ix]
+  leftf  :: phi ix -> (forall ix'. El phi ix' => phi ix' -> r ix') -> [f r ix]
+  rightf :: phi ix -> (forall ix'. El phi ix' => phi ix' -> r ix') -> [f r ix]
+ 
+instance El phi xi => LR phi (I xi) where
+  leftf  _ f = [I (f proof)]
+  rightf _ f = [I (f proof)]
+
+instance LRBase a => LR phi (K a) where
+  leftf  _ _ = [K leftb]
+  rightf _ _ = [K rightb]
+
+instance LR phi U where
+  leftf  _ _ = [U]
+  rightf _ _ = [U]
+
+instance (LR phi f, LR phi g) => LR phi (f :+: g) where
+  leftf  p f = map L (leftf  p f) ++ map R (leftf  p f)
+  rightf p f = map R (rightf p f) ++ map L (rightf p f)
+
+instance (LR phi f, LR phi g) => LR phi (f :*: g) where
+  leftf  p f = zipWith (:*:) (leftf  p f) (leftf  p f)
+  rightf p f = zipWith (:*:) (rightf p f) (rightf p f)
+
+instance LR phi f => LR phi (C c f) where
+  leftf  p f = map C (leftf  p f)
+  rightf p f = map C (rightf p f)
+
+instance (El phi ix, LR phi f, EqS phi) => LR phi (f :>: ix) where
+  leftf  p f = case eqS (proof :: phi ix) p of
+    Just Refl -> map Tag (leftf  p f)
+    Nothing   -> []
+  rightf p f = case eqS (proof :: phi ix) p of
+    Just Refl -> map Tag (rightf  p f)
+    Nothing   -> []
+
+instance LR phi f => LR phi ([] :.: f) where
+  leftf  p f = [D []]
+  rightf p f = map (\v -> D [v]) $ rightf p f
+
+left :: (Fam phi, LR phi (PF phi)) => phi ix -> ix
+left p = to p $ safeHead $ leftf p (I0 . left)
+
+right :: (Fam phi, LR phi (PF phi)) => phi ix -> ix
+right p = to p $ safeHead $ rightf p (I0 . right)
+
+safeHead [] = error "Internal error, left or right returned []"
+safeHead (x:xs) = x

@@ -0,0 +1,57 @@+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+
+module Generics.MultiRec.Ord where
+
+import Generics.MultiRec
+import Data.Monoid (mappend)
+
+--------------------------------------------------------------------------------
+-- Generic Ord
+--------------------------------------------------------------------------------
+class HOrd phi f where
+  hcompare :: (forall ix. phi ix -> r ix -> r ix -> Ordering) 
+              -> phi ix -> f r ix -> f r ix -> Ordering
+
+instance El phi xi => HOrd phi (I xi) where
+  hcompare f _ (I x) (I y) = f proof x y
+
+instance Ord a => HOrd phi (K a) where
+  hcompare _ _ (K x) (K y) = compare x y
+
+instance HOrd phi U where
+  hcompare _ _ U U = EQ
+
+instance (HOrd phi f, HOrd phi g) => HOrd phi (f :+: g) where
+  hcompare f p (L _) (R _) = LT
+  hcompare f p (R _) (L _) = GT
+  hcompare f p (L x) (L y) = hcompare f p x y
+  hcompare f p (R x) (R y) = hcompare f p x y
+
+instance (HOrd phi f, HOrd phi g) => HOrd phi (f :*: g) where
+  hcompare f p (v :*: x) (w :*: y) = hcompare f p v w `mappend` hcompare f p x y
+
+instance HOrd phi f => HOrd phi (C c f) where
+  hcompare f p (C x) (C y) = hcompare f p x y
+
+instance HOrd phi f => HOrd phi (f :>: ix) where
+  hcompare f p (Tag x) (Tag y) = hcompare f p x y
+
+instance (Ord1 f, HOrd phi g) => HOrd phi (f :.: g) where
+  hcompare f p (D x) (D y) = compare1 (hcompare f p) x y
+
+class Ord1 f where
+  compare1 :: (a -> a -> Ordering) -> f a -> f a -> Ordering
+
+instance Ord1 [] where
+  compare1 f [] [] = EQ
+  compare1 f [] _  = LT
+  compare1 f _  [] = GT
+  compare1 f (x:xs) (y:ys) = f x y `mappend` compare1 f xs ys
+
+gcompare :: (Fam phi, HOrd phi (PF phi)) => phi ix -> ix -> ix -> Ordering
+gcompare p x1 x2 = hcompare (\ p (I0 x1) (I0 x2) -> gcompare p x1 x2) p (from p x1) (from p x2)

@@ -0,0 +1,7 @@+module Generics.MultiRec.Rewriting (
+  module Generics.MultiRec.Rewriting.Machinery,
+  module Generics.MultiRec.Rewriting.Rules,
+) where
+
+import Generics.MultiRec.Rewriting.Machinery
+import Generics.MultiRec.Rewriting.Rules

@@ -0,0 +1,66 @@+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs                 #-}
+
+module Generics.MultiRec.Rewriting.Machinery where
+
+import Generics.MultiRec
+import Generics.MultiRec.HZip
+import Generics.MultiRec.Rewriting.Rules
+import Generics.MultiRec.Any
+
+import qualified Data.Map as M
+import Control.Monad.State
+
+-----------------------------------------------------------------------------
+-- Class synonym for shorter names
+-----------------------------------------------------------------------------
+class (Fam phi, EqS phi, HZip phi (PF phi), HFunctor phi (PF phi))
+      => Rewrite phi
+
+-----------------------------------------------------------------------------
+-- Actual rewriting
+-----------------------------------------------------------------------------
+rewriteM :: Rewrite phi => Rule phi a -> a -> Maybe a
+rewriteM (Rule p (lhs :~> rhs)) term = 
+  match p lhs term >>= return . (\s -> inst s p rhs)
+
+match :: (Monad m, Rewrite phi) => 
+         phi ix -> Scheme phi ix -> ix -> m (Subst phi)
+match p pat term = execStateT (matchM p pat (I0 term)) M.empty
+
+matchM :: (Monad m, Rewrite phi) 
+          => phi ix -> Scheme phi ix -> I0 ix -> StateT (Subst phi) m ()
+matchM p scheme (I0 e) = case scheme of
+  HIn (L (K var)) -> do 
+    subst <- get
+    case M.lookup var subst of
+      Nothing     -> put (M.insert var (Any p e) subst)
+      Just exTerm -> checkEqual p e exTerm
+  HIn (R r) -> combine matchM p r (from p e)
+
+checkEqual :: (Monad m, Rewrite phi)
+           => phi ix -> ix -> Any phi -> m ()
+checkEqual p e (Any p' e') = case eqS p p' of
+  Nothing   -> fail "checkEqual"
+  Just Refl -> geq' p (I0 e) (I0 e')
+
+inst :: Rewrite phi =>
+        Subst phi -> phi ix -> Scheme phi ix -> ix
+inst s ix p
+  = case p of
+     HIn (L (K x)) ->
+        case M.lookup x s of
+          Just (Any ix' e)
+            -> case eqS ix ix' of
+                 Just Refl -> e
+                 Nothing -> error "Coerce error in inst"
+     HIn (R r) -> to ix $ hmap (\ix' -> I0 . inst s ix') ix r
+
+type Subst phi = M.Map Metavar (Any phi)

@@ -0,0 +1,100 @@+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs                 #-}
+
+module Generics.MultiRec.Rewriting.Rules where
+
+import Generics.MultiRec
+import Generics.MultiRec.LR
+import Generics.MultiRec.HZip
+
+-----------------------------------------------------------------------------
+-- 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 phi  = K Metavar :+: PF phi
+type Metavar  = Int
+
+-- | Recursively extends a type with a case for a metavariable.
+type Scheme phi = HFix (Ext phi)
+
+-- | Allows metavariables on either side of a rule.
+data Rule phi a where 
+  Rule :: phi ix -> RuleSpec (Scheme phi ix) -> Rule phi ix
+
+-- | Constructs a metavariable.
+metavar :: phi ix -> Metavar -> Scheme phi ix
+metavar _ = HIn . L . K
+
+pf :: phi ix -> PF phi (Scheme phi) ix -> Scheme phi ix
+pf _ = HIn . R
+
+-----------------------------------------------------------------------------
+-- Builder for transforming a rule specification to a rule.
+-----------------------------------------------------------------------------
+
+class Builder phi a where
+  type Target a :: *
+  base          :: phi (Target a) -> a -> RuleSpec (Target a)
+  diag          :: phi (Target a) -> a -> [RuleSpec (Target a)]
+
+instance Builder phi (RuleSpec a) where
+  type Target (RuleSpec a) = a
+  base _ x                 = x
+  diag _ x                 = [x]
+
+instance (Builder phi a, Fam phi, LR phi (PF phi), El phi b)
+         => Builder phi (b -> a) where
+  type Target (b -> a) = Target a
+  base ix f            = base ix (f (left  (proof :: phi b)))
+  diag ix f            = base ix (f (right (proof :: phi b))) :
+                         diag ix (f (left  (proof :: phi b)))
+
+rule :: forall phi r. (Fam phi, Builder phi r, HZip phi (PF phi), 
+                       El phi (Target r), EqS phi, HFunctor phi (PF phi))
+        => r -> Rule phi (Target r)
+rule f = Rule ix $ foldr1 mergeRules rules
+  where
+    ix = proof :: phi (Target r)
+    mergeRules x y = 
+      mergeSchemes ix (lhsR x) (lhsR y) :~>
+      mergeSchemes ix (rhsR x) (rhsR y)
+    rules          = zipWith (ins (base ix f)) (diag ix f) [0..]   
+    ins x y v      = 
+      insertMVar v ix (I0 (lhsR x)) (I0 (lhsR y)) :~>
+      insertMVar v ix (I0 (rhsR x)) (I0 (rhsR y))
+
+mergeSchemes :: HZip phi (PF phi)
+                => phi ix -> Scheme phi ix -> Scheme phi ix -> Scheme phi ix
+mergeSchemes p a@(HIn x) b@(HIn y) = case (x,y) of
+  (L _,_) -> a
+  (_,L _) -> b
+  _       -> HIn (hzip' mergeSchemes p x y)
+
+insertMVar :: forall phi ix. (Fam phi, HZip phi (PF phi), El phi ix)
+              => Metavar -> phi ix -> I0 ix -> I0 ix -> Scheme phi ix
+insertMVar name p (I0 x) (I0 y) =
+  case hzip (insertMVar name) p (from p x) (from p y) of
+    Just struc -> pf p struc
+    Nothing    -> metavar p name

@@ -0,0 +1,413 @@+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE RankNTypes            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+
+module Generics.MultiRec.Transformations.Explicit (
+  diff, apply, Transformation, AnyInsert (..), WithRef (..), Path, 
+  Transform, OrdI (..)
+  ) where
+
+import Generics.MultiRec.Any
+import Generics.MultiRec.Eq
+import Generics.MultiRec.Ord
+
+import Generics.MultiRec hiding (show, foldM)
+import Control.Applicative ( (<|>) )
+import Control.Monad (foldM)
+import Control.Monad.State hiding (foldM)
+import Data.Monoid (mappend)
+import qualified Data.Map as Map
+import Data.Map (Map)
+
+--------------------------------------------------------------------------------
+-- Paths, annotations, edits and existentials
+--------------------------------------------------------------------------------
+data WithRef phi f a = InR (PF phi f a)
+                     | Ref Path
+
+type Path = [Int]
+
+data AnyInsert phi where
+  AnyInsert :: phi ix -> Path -> HFix (WithRef phi) ix -> AnyInsert phi
+
+type Transformation phi = [ AnyInsert phi]
+
+class (Fam phi, Children phi (PF phi), CountI phi (PF phi),
+       HFunctor phi (PF phi), SEq phi (PF phi), ExtractN phi (PF phi), 
+       MapN phi (PF phi), EqS phi, HEq phi (PF phi), HOrd phi (PF phi),
+       OrdI phi) => Transform phi
+
+--------------------------------------------------------------------------------
+-- Applying
+--------------------------------------------------------------------------------
+-- | Apply the transformation to the given tree
+apply :: forall phi ix. (Transform phi)
+         => phi ix -> ix -> Transformation phi -> Maybe ix
+apply p t = foldM (apply' p) t where
+  apply' :: forall ix. phi ix -> ix -> AnyInsert phi -> Maybe ix
+  apply' p' _ (AnyInsert p'' [] c) = case eqS p' p'' of 
+    Just Refl -> lookupRefs p t p' c
+    Nothing   -> Nothing
+  apply' p' a (AnyInsert p'' (i:is) c) =
+    liftM (to p') $ tmapN f p' $ from p' a where
+      f :: forall ix. Int -> phi ix -> I0 ix -> Maybe (I0 ix)
+      f j p''' x | i == j    = liftM I0 (apply' p''' (unI0 x) (AnyInsert p'' is c))
+                 | otherwise = return x
+
+-- | Look up the references using the original structure
+lookupRefs :: forall phi ix ix'. (Fam phi, HFunctor phi (PF phi), ExtractN phi (PF phi), EqS phi) 
+              => phi ix -> ix -> phi ix' -> HFix (WithRef phi) ix' -> Maybe ix'
+lookupRefs p r p' = build .  hout where
+  build :: WithRef phi (HFix (WithRef phi)) ix' -> Maybe ix'
+  build (InR x) = liftM (to p') (hmapM (\p'' -> liftM I0 . lookupRefs p r p'') p' x)
+  build (Ref l) = extract l p r >>= matchAny p'
+
+-- | Extract the subtree at the given path
+extract :: (Fam phi, ExtractN phi (PF phi)) => Path -> phi ix -> ix -> Maybe (Any phi)
+extract []     p a = return $ Any p a
+extract (i:is) p a = extractN i p a >>= \(Any p' x) -> extract is p' x
+
+--------------------------------------------------------------------------------
+-- Memoisation
+--------------------------------------------------------------------------------
+-- | Comparing index of different types
+class OrdI phi where
+  compareI :: phi ix -> phi ix' -> Ordering
+
+-- | Key used in memoisation table
+data MemoKey phi where
+  MemoKey :: phi ix -> Bool -> ix -> ix -> MemoKey phi
+
+instance (EqS phi, Fam phi, HEq phi (PF phi)) => Eq (MemoKey phi) where
+  (MemoKey p1 a1 b1 c1) == (MemoKey p2 a2 b2 c2) = case eqS p1 p2 of
+    Nothing   -> False
+    Just Refl -> a1 == a2 && eq p1 b1 b2 && eq p1 c1 c2
+
+instance (EqS phi, Fam phi, OrdI phi, HEq phi (PF phi), HOrd phi (PF phi))
+         => Ord (MemoKey phi) where
+  compare (MemoKey p1 a1 b1 c1) (MemoKey p2 a2 b2 c2) = case eqS p1 p2 of
+    Nothing   -> compareI p1 p2
+    Just Refl -> compare a1 a2 `mappend` gcompare p1 b1 b2 
+                               `mappend` gcompare p1 c1 c2
+
+-- | The type of the memo table
+type MemoTable phi = Map (MemoKey phi) (Transformation phi)
+type Memo phi a = State (MemoTable phi) a
+
+runMemo :: Memo phi a -> a
+runMemo = flip evalState Map.empty
+
+recMemo :: (Fam phi, HEq phi (PF phi), HOrd phi (PF phi), EqS phi, OrdI phi) => 
+           (forall ix. Bool -> phi ix -> ix -> ix -> Memo phi (Transformation phi))
+           -> Bool -> phi ix -> ix -> ix -> Memo phi (Transformation phi)
+recMemo f a p b c = do
+  mp <- get
+  let k = MemoKey p a b c
+  case Map.lookup k mp of
+    Just r -> return r
+    Nothing -> do
+      r <- f a p b c
+      modify (Map.insert k r)
+      return r
+
+--------------------------------------------------------------------------------
+-- Diffing
+--------------------------------------------------------------------------------
+-- | Find a set of insertions to transform the first into the second tree
+diff :: forall phi ix. (Transform phi)
+        => phi ix -> ix -> ix -> Transformation phi
+diff p a b = runMemo (build False p a b)
+  where
+    childPaths :: [(Any phi, Path)]
+    childPaths = childrenPaths p a
+    build :: forall ix. Bool -> phi ix -> ix -> ix -> Memo phi (Transformation phi)
+    build False p' a' b' | eq p' a' b' = return []
+    build ins   p' a' b' = case anyLookup p' b' childPaths of
+      Just l  -> return [ AnyInsert p' [] (HIn $ Ref l) ]
+      Nothing -> uses >>= maybe insert return -- Only insert when we cannot reuse
+        where
+          -- Construct the edits for the children based on a root
+          construct :: Bool -> ix -> Memo phi (Maybe (Transformation phi))
+          construct ins' c = 
+            if shallowEq p' (from p' c) (from p' b')
+            then do r <- zipWithM (\(Any p1 c1) (Any p2 c2) -> case eqS p1 p2 of
+                                      Just Refl -> recMemo build ins' p1 c1 c2)
+                         (imChildren p' c) (imChildren p' b')
+                    return $ Just $ concat $ updateChildPaths r
+            else return Nothing
+          -- Possible edits reusing the existing tree or using a part of
+          -- the original tree. The existing tree is only used if we didn't
+          -- just insert it, since we want to keep the inserts small
+          uses :: Memo phi (Maybe (Transformation phi))
+          uses = reuses >>= \re -> case re of
+              Just r | ins -> return re
+              _            -> construct ins a' >>= return . pickBest re
+          -- Possible edits that include reusing a part of the original tree
+          reuses :: Memo phi (Maybe (Transformation phi))
+          reuses = foldM f Nothing childPaths where
+            addRef :: Path -> Maybe (Transformation phi) 
+                       -> Maybe (Transformation phi)
+            addRef l = liftM ((AnyInsert p' [] (HIn $ Ref l)):)
+            f c (Any p'' x, l) = case eqS p' p'' of
+              Just Refl -> construct False x >>= return . pickBest c . addRef l
+              Nothing   -> return c
+          -- Best edit including insertion, only chosen if nothing can be reused
+          insert :: Memo phi (Transformation phi)
+          insert = do
+            Just r <- construct True b'
+            let (r',e')  = partialApply p' (annotate p' b') r
+            return $ (AnyInsert p' [] r') : e'
+
+-- | Pick the best edit
+pickBest :: Maybe (Transformation phi) -> Maybe (Transformation phi) -> Maybe (Transformation phi)
+pickBest e1 e2 = case (e1,e2) of
+  (Just e1', Just e2') -> Just (pickShortest e1' e2')
+  _                    -> e1 <|> e2
+
+-- | Pick the shortest of two lists lazily
+pickShortest :: [a] -> [a] -> [a]
+pickShortest a b = if f a b then a else b
+  where f []     _      = True
+        f _      []     = False
+        f (_:xs) (_:ys) = f xs ys
+
+-- | Lookup with a specific type
+anyLookup :: (Fam phi, EqS phi, HEq phi (PF phi))
+             => phi ix -> ix -> [(Any phi, a)] -> Maybe a
+anyLookup p _ [] = Nothing
+anyLookup p x ((Any p' y,r) : ys) = case eqS p p' of
+  Just Refl | eq p x y -> Just r
+  _                    -> anyLookup p x ys
+
+-- | Lift a tree to an edit structure
+annotate :: (Fam phi, HFunctor phi (PF phi)) => phi ix -> ix -> HFix (WithRef phi) ix
+annotate p = HIn . InR . hmap (\p' (I0 x) -> annotate p' x) p . from p
+
+-- | Extend the paths of edits for the children with the child number
+updateChildPaths :: [Transformation phi] -> [Transformation phi]
+updateChildPaths = zipWith (\n -> map (\(AnyInsert p l c) -> (AnyInsert p (n:l) c))) [0..]
+
+-- | Try to apply as much edits to the edit structure as possible
+--   to make the final edit smaller
+partialApply :: (Fam phi, CountI phi (PF phi), ExtractN phi (PF phi), MapN phi (PF phi), EqS phi)
+                => phi ix -> HFix (WithRef phi) ix -> Transformation phi -> (HFix (WithRef phi) ix, Transformation phi)
+partialApply _ a [] = (a, [])
+partialApply p a (AnyInsert p' l x : xs) = case replace p' l x p a of
+  Just a' -> partialApply p a' xs
+  Nothing -> let (a',xs') = partialApply p a xs in (a', AnyInsert p' l x : xs')
+
+-- | Replace a subtree in an edit structure
+replace :: forall phi ix ix'. (Fam phi, EqS phi, MapN phi (PF phi))
+           => phi ix -> Path -> HFix (WithRef phi) ix
+           -> phi ix' -> HFix (WithRef phi) ix' -> Maybe (HFix (WithRef phi) ix')
+replace p [] r p' _ = case eqS p p' of
+  Just Refl -> Just r
+  Nothing   -> Nothing
+replace p (i:is) r p' a = case hout a of
+  Ref _  -> Nothing
+  InR a' -> liftM HIn . liftM InR . tmapN f p' $ a'
+    where f :: forall ix. Int -> phi ix -> HFix (WithRef phi) ix -> Maybe (HFix (WithRef phi) ix)
+          f j p'' = if i == j then replace p is r p'' else Just
+
+--------------------------------------------------------------------------------
+-- Shallow equality
+--------------------------------------------------------------------------------
+
+class SEq phi (f :: (* -> *) -> * -> *) where
+  shallowEq :: phi ix -> f r ix  -> f r ix -> Bool
+
+instance El phi xi => SEq phi (I xi) where
+  shallowEq _ (I _) (I _) = True
+
+instance SEq phi U where
+  shallowEq _ U U = True
+
+instance Eq a => SEq phi (K a) where
+  shallowEq p (K a) (K b) = a == b
+
+instance (SEq phi f, SEq phi g) => SEq phi (f :+: g) where
+  shallowEq p (L a) (L b) = shallowEq p a b
+  shallowEq p (R a) (R b) = shallowEq p a b
+  shallowEq _ _     _     = False
+
+instance (SEq phi f, SEq phi g) => SEq phi (f :*: g) where
+  shallowEq p (a :*: b) (c :*: d) = shallowEq p a c && shallowEq p b d
+
+instance SEq phi f => SEq phi (f :>: ix) where
+  shallowEq p (Tag a) (Tag b) = shallowEq p a b
+
+instance SEq phi f => SEq phi (C c f) where
+  shallowEq p (C a) (C b) = shallowEq p a b
+
+-- Todo: is this the best choice?
+instance SEq phi ([] :.: ix) where
+  shallowEq p (D a) (D b) = length a == length b
+
+--------------------------------------------------------------------------------
+-- ExtractN
+--------------------------------------------------------------------------------
+
+extractN :: (Fam phi, ExtractN phi (PF phi), Monad m) 
+            => Int -> phi ix -> ix -> m (Any phi)
+extractN i p v = extractN' (\p (I0 v) -> Any p v) i p (from p v)
+
+class ExtractN phi (f :: (* -> *) -> * -> *) where
+  extractN' :: Monad m => (forall ix. phi ix -> r ix -> r')
+                          -> Int -> phi ix -> f r ix -> m r'
+
+instance El phi xi => ExtractN phi (I xi) where
+  extractN' mka 0 _ (I r) = return $ mka proof r
+  extractN' _   _ _ (I _) = fail "extractN"
+
+instance ExtractN phi (K a) where
+  extractN' mka _ _ (K _) = fail "extractN"
+
+instance ExtractN phi U where
+  extractN' mka _ _ U = fail "extractN"
+
+instance (ExtractN phi f, ExtractN phi g) => ExtractN phi (f :+: g) where
+  extractN' mka i p (L x) = extractN' mka i p x
+  extractN' mka i p (R x) = extractN' mka i p x
+
+instance (CountI phi f, ExtractN phi f, ExtractN phi g) => ExtractN phi (f :*: g) where
+  extractN' mka i p (x :*: y) = let n = countI p x
+                                in if i < n then extractN' mka i     p x
+                                            else extractN' mka (i-n) p y
+
+instance ExtractN phi f => ExtractN phi (f :>: ix) where
+  extractN' mka i p (Tag x) = extractN' mka i p x
+
+instance ExtractN phi f => ExtractN phi (C c f) where
+  extractN' mka i p (C x) = extractN' mka i p x
+
+-- Todo: is this the best choice?
+instance ExtractN phi f => ExtractN phi ([] :.: f) where
+  extractN' mka i p (D x) = extractN' mka 0 p (x !! i)
+
+--------------------------------------------------------------------------------
+-- MapN
+--------------------------------------------------------------------------------
+
+-- | Map a function with child index at a top-level structure
+tmapN :: (Fam phi, MapN phi f, Monad m)
+         => (forall ix. Int -> phi ix -> r ix -> m (r' ix))
+         -> phi ix -> f r ix -> m (f r' ix)
+tmapN = mapN 0
+
+class MapN phi (f :: (* -> *) -> * -> *) where
+  mapN :: Monad m => Int -> (forall ix. Int -> phi ix -> r ix -> m (r' ix))
+                           -> phi ix -> f r ix -> m (f r' ix)
+
+instance El phi xi => MapN phi (I xi) where
+  mapN i f p (I x) = liftM I (f i proof x)
+
+instance MapN phi (K a) where
+  mapN _ _ _ (K x)  = return $ K x
+
+instance MapN phi U where
+  mapN _ _ _ U = return U
+
+instance (MapN phi f, MapN phi g) => MapN phi (f :+: g) where
+  mapN i f p (L x) = liftM L (mapN i f p x)
+  mapN i f p (R x) = liftM R (mapN i f p x)
+
+-- Here we increment our parameter. Does not require right-nested products
+instance (CountI phi f, MapN phi f, MapN phi g) => MapN phi (f :*: g) where
+  mapN i f p (x :*: y) = liftM2 (:*:) (mapN i f p x) (mapN (i + countI p x) f p y)
+
+instance MapN phi f => MapN phi (f :>: ix) where
+  mapN i f p (Tag x) = liftM Tag (mapN i f p x)
+
+instance MapN phi f => MapN phi (C c f) where
+  mapN i f p (C x) = liftM C (mapN i f p x)
+
+-- Todo: is this the best choice?
+instance (CountI phi f, MapN phi f) => MapN phi ([] :.: f) where
+  mapN i f p (D [])     = return $ D []
+  mapN i f p (D (x:xs)) = do h <- mapN i f p x
+                             t <- mapN (i + countI p x) f p (D xs)
+                             return $ D (h : unD t)
+
+--------------------------------------------------------------------------------
+-- CountI
+--------------------------------------------------------------------------------
+
+class CountI phi (f :: (* -> *) -> * -> *) where
+  -- | Count the number of recursive occurrences
+  countI :: phi ix -> f r ix -> Int
+
+instance El phi xi => CountI phi (I xi) where
+  countI _ _ = 1
+
+instance CountI phi (K a) where
+  countI _ _ = 0
+
+instance CountI phi U where
+  countI _ _ = 0
+
+instance (CountI phi f, CountI phi g) => CountI phi (f :+: g) where
+  countI p (L x) = countI p x
+  countI p (R x) = countI p x
+
+instance (CountI phi f, CountI phi g) => CountI phi (f :*: g) where
+  countI p (x :*: y) = countI p x + countI p y
+
+instance CountI phi f => CountI phi (f :>: ix) where
+  countI p (Tag x) = countI p x
+
+instance CountI phi f => CountI phi (C c f) where
+  countI p (C x) = countI p x
+
+-- Todo: is this the best choice?
+instance CountI phi f => CountI phi ([] :.: f) where
+  countI p (D x) = sum (map (countI p) x)
+
+--------------------------------------------------------------------------------
+-- Children
+--------------------------------------------------------------------------------
+
+-- | Get the immediate children
+imChildren :: (Fam phi, Children phi (PF phi)) => phi ix -> ix -> [Any phi]
+imChildren p x = children (\p (I0 v) -> Any p v) p (from p x)
+
+-- | Get all children with their paths
+childrenPaths :: (Fam phi, Children phi (PF phi)) => phi ix -> ix -> [(Any phi, Path)]
+childrenPaths p a = (Any p a, []) : 
+                    [ (r, n : p)
+                    | (n, Any p' c) <- zip [0..] (imChildren p a)
+                    , (r, p) <- childrenPaths p' c ]
+
+class Children phi (f :: (* -> *) -> * -> *) where
+  children :: (forall ix. phi ix -> r ix -> Any phi) -> phi ix -> f r ix -> [Any phi]
+
+instance (Fam phi, El phi xi) => Children phi (I xi) where
+  children mka _ (I r) = [mka proof r]
+
+instance Children phi (K a) where
+  children _ _ (K _) = []
+
+instance Children phi U where
+  children _ _ U = []
+
+instance (Children phi f, Children phi g) => Children phi (f :+: g) where
+  children mka p (L x) = children mka p x
+  children mka p (R x) = children mka p x
+
+instance (Children phi f, Children phi g) => Children phi (f :*: g) where
+  children mka p (x :*: y) = children mka p x ++ children mka p y
+
+instance Children phi f => Children phi (C c f) where
+  children mka p (C x) = children mka p x
+
+instance Children phi f => Children phi (f :>: ix) where
+  children mka p (Tag x) = children mka p x
+
+-- Todo: is this the best choice?
+instance Children phi f => Children phi ([] :.: f) where
+  children mka p (D x) = concatMap (children mka p) x

@@ -0,0 +1,59 @@+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE UndecidableInstances       #-}
+{-# LANGUAGE TemplateHaskell            #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE EmptyDataDecls             #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE GADTs                      #-}
+
+module Generics.MultiRec.Transformations.RewriteRules (
+  Transformation, Transform, apply, insert, AnyInsert (..)
+  ) where
+
+import Generics.MultiRec hiding ( foldM )
+import Generics.MultiRec.Rewriting
+import Generics.MultiRec.Zipper (Zipper, Loc, leave, enter, update)
+
+import Data.Maybe ( fromJust )
+import Control.Monad ( (>=>), foldM )
+
+--------------------------------------------------------------------------------
+-- Patch
+--------------------------------------------------------------------------------
+-- Basically, a class synonym
+class (Zipper phi (PF phi), Rewrite phi) => Transform phi
+instance Transform phi => Rewrite phi
+
+-- An edit is a list of:
+type Transformation phi a = [ AnyInsert phi a ]
+
+-- Existential for insertion
+data AnyInsert phi a where 
+  AnyInsert ::
+    -- Proof
+    phi ix
+    -- A path to the location to edit
+    -> (Loc phi I0 a -> Maybe (Loc phi I0 a)) 
+    -- The rewrite rule to apply there
+    -> Rule phi ix
+    -> AnyInsert phi a
+
+insert :: El phi ix => (Loc phi I0 a -> Maybe (Loc phi I0 a)) -> Rule phi ix
+          -> AnyInsert phi a
+insert = AnyInsert proof
+
+-- Patching is terribly simple: at the given locations, apply all the rules,
+-- then exit the zipper.
+apply :: Transform phi => Transformation phi a -> phi a -> a -> Maybe a
+apply rs p x = fmap leave $ foldM appRule (enter p x) rs
+  where appRule a (AnyInsert p' l r) = l a >>=
+                            updateM (\p'' -> case eqS p' p'' of
+                                              Nothing   -> const Nothing
+                                              Just Refl -> rewriteM r)
+
+updateM :: (forall xi. phi xi -> xi -> Maybe xi)
+        -> Loc phi I0 ix -> Maybe (Loc phi I0 ix)
+-- updateM f (Loc p (I0 x) s) = f p x >>= \y -> Loc p (I0 y) s
+updateM f = Just . update (\p -> maybe (error "updateM") id . f p)

@@ -0,0 +1,72 @@+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE GADTs                      #-}
+
+module Generics.MultiRec.Transformations.ZipperState (
+  ZipperMonad, ZipperState, upMonad, downMonad, leftMonad, rightMonad, 
+  navigate, saveMonad, loadMonad, topMonad, updateMonad
+  ) where
+
+import Control.Monad
+import Control.Monad.State
+
+import Generics.MultiRec
+import Generics.MultiRec.Zipper
+import Generics.MultiRec.Any
+
+--------------------------------------------------------------------------------
+-- A zipper with state
+--------------------------------------------------------------------------------
+
+type ZipperState phi r a = ([Any phi], Loc phi r a)
+type ZipperMonad phi r a b = StateT (ZipperState phi r a) Maybe b
+
+enterMonad :: (El phi a, Fam phi, Zipper phi (PF phi))
+           => a -> ZipperMonad phi I0 a (Any phi)
+enterMonad x = put ([], enter proof x) >> return (Any proof x)
+
+moveMonad :: (EqS phi, El phi a)
+          => (Loc phi I0 a -> Maybe (Loc phi I0 a))
+          -> ZipperMonad phi I0 a (Any phi)
+moveMonad d = StateT (\(s,l) -> do l' <- d l
+                                   let a = on (\p (I0 x) -> Any p x) l'
+                                   return (a, (s,l')))
+
+upMonad, downMonad, leftMonad, rightMonad :: (EqS phi, El phi a)
+                                          => ZipperMonad phi I0 a (Any phi)
+upMonad    = moveMonad up
+downMonad  = moveMonad down
+leftMonad  = moveMonad left
+rightMonad = moveMonad right
+
+updateMonad :: (EqS phi, El phi a)
+            => (forall xi. phi xi -> xi -> Maybe xi) 
+               -> ZipperMonad phi I0 a (Any phi)
+updateMonad f = do (s,l) <- get
+                   let l' = update (\p -> maybe (error "updateMonad") id . f p) l
+                       a  = on (\p (I0 x) -> Any p x) l'
+                   put (s,l')
+                   return a
+saveMonad :: (EqS phi, El phi a) => ZipperMonad phi I0 a (Any phi)
+saveMonad = do (s,l) <- get
+               let a = on (\p (I0 x) -> Any p x) l
+               put (s++[a],l)
+               return a
+
+loadMonad :: (EqS phi, El phi a) => ZipperMonad phi I0 a (Any phi)
+loadMonad = do (s:ss,l) <- get
+               let l' = update (\p x -> maybe x id (matchAny p s)) l
+               put (ss,l')
+               return s
+
+topMonad :: (EqS phi, El phi a) => ZipperMonad phi I0 a (Any phi)
+topMonad = moveMonad goUp where
+  goUp l = maybe (Just l) goUp (up l)
+
+leaveMonad :: (EqS phi, El phi a) 
+              => Loc phi I0 a -> ZipperMonad phi I0 a b -> Maybe a
+leaveMonad s m = maybe Nothing (matchAny proof) $ evalStateT (m >> topMonad) ([],s)
+
+navigate :: (Fam phi, EqS phi, El phi a, Zipper phi (PF phi))
+            => phi a -> a -> ZipperMonad phi I0 a b -> Maybe a
+navigate p x = leaveMonad (enter p x)

@@ -0,0 +1,41 @@+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE FlexibleContexts           #-}
+
+module Generics.Regular.Functions.GOrd where
+
+import Generics.Regular
+import Data.Monoid (mappend)
+
+--------------------------------------------------------------------------------
+-- Generic Ord
+--------------------------------------------------------------------------------
+
+class GOrd f where
+  comparef :: (a -> a -> Ordering) -> f a -> f a -> Ordering
+
+instance GOrd I where
+  comparef f (I x) (I y) = f x y
+
+instance Ord a => GOrd (K a) where
+  comparef _ (K x) (K y) = compare x y
+
+instance GOrd U where
+  comparef _ U U = EQ
+
+instance (GOrd f, GOrd g) => GOrd (f :+: g) where
+  comparef _ (L _) (R _) = LT
+  comparef _ (R _) (L _) = GT
+  comparef f (L x) (L y) = comparef f x y
+  comparef f (R x) (R y) = comparef f x y
+
+instance (GOrd f, GOrd g) => GOrd (f :*: g) where
+  comparef f (x1 :*: y1) (x2 :*: y2) = comparef f x1 x2 `mappend` comparef f y1 y2
+
+instance GOrd f => GOrd (C c f) where
+  comparef f (C x) (C y) = comparef f x y
+
+instance GOrd f => GOrd (S s f) where
+  comparef f (S x) (S y) = comparef f x y
+
+gcompare :: (Regular a, GOrd (PF a)) => a -> a -> Ordering
+gcompare x y = comparef gcompare (from x) (from y)

@@ -0,0 +1,329 @@+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE UndecidableInstances       #-}
+
+module Generics.Regular.Transformations.Explicit (
+  diff, apply, Transformation, WithRef (..), Path, Transform
+  ) where
+
+import Generics.Regular
+import Generics.Regular.Functions.GOrd
+import Control.Applicative ( (<|>) )
+import Control.Monad (foldM, liftM, liftM2)
+import Control.Monad.State
+import Data.Monoid (mappend)
+import qualified Data.Map as Map
+import Data.Map (Map)
+import qualified Generics.Regular.Functions.Eq as GEq
+
+--------------------------------------------------------------------------------
+-- Paths, annotations and edits
+--------------------------------------------------------------------------------
+type Path             = [Int]
+data WithRef a b      = InR (PF a b)
+                      | Ref Path
+type Transformation a = [ (Path, Fix (WithRef a)) ]
+
+class (Regular a, Children (PF a), CountI (PF a), Functor (PF a),
+       SEq (PF a), ExtractN (PF a), MapN (PF a), GMap (PF a), GOrd (PF a),
+       GEq.Eq (PF a)) => Transform a
+
+--------------------------------------------------------------------------------
+-- Patching
+--------------------------------------------------------------------------------
+
+-- | Apply the edits to the given tree
+apply :: Transform a => Transformation a -> a -> Maybe a
+apply e t = foldM apply' t e where
+  apply' _ ([],   c) = lookupRefs t c
+  apply' a (i:is, c) = fmap to . tmapN f . from $ a where
+    f j x | i == j     = apply' x (is,c)
+          | otherwise  = Just x
+
+-- | Look up the references using the original structure
+lookupRefs :: Transform a => a -> Fix (WithRef a) -> Maybe a
+lookupRefs r (In (InR a)) = fmap to (fmapM (lookupRefs r) a)
+lookupRefs r (In (Ref p)) = extract p r
+
+-- | Extract the subtree at the given path
+extract :: Transform a => Path -> a -> Maybe a
+extract p a = foldM (\x i -> extractN i $ from x) a p
+
+--------------------------------------------------------------------------------
+-- Diffing
+--------------------------------------------------------------------------------
+data MemoKey a where
+  MemoKey :: Bool -> a -> a -> MemoKey a
+
+instance (Regular a, GEq.Eq (PF a)) => Eq (MemoKey a) where
+  (MemoKey a1 b1 c1) == (MemoKey a2 b2 c2) =
+    a1 == a2 && GEq.eq b1 b2 && GEq.eq c1 c2
+
+instance (Regular a, GEq.Eq (PF a), GOrd (PF a)) => Ord (MemoKey a) where
+  compare (MemoKey a1 b1 c1) (MemoKey a2 b2 c2) =
+    compare a1 a2 `mappend` gcompare b1 b2 `mappend` gcompare c1 c2
+
+type Memo a = Map (MemoKey a) (Transformation a)
+
+-- | Find a set of edits to transform the first into the second tree
+diff :: forall a. (Transform a) => a -> a -> Transformation a
+diff a b = evalState (build False a b) Map.empty
+  where
+    childPaths :: [(a,Path)]
+    childPaths = childrenPaths a
+    buildmem :: Bool -> a -> a -> State (Memo a) (Transformation a)
+    buildmem a b c = do
+      mp <- get
+      let k = MemoKey a b c
+      case Map.lookup k mp of
+        Just r  -> return r
+        Nothing -> do
+          r <- build a b c
+          modify (Map.insert k r)
+          return r
+    build :: Bool -> a -> a -> State (Memo a) (Transformation a)
+    build False a' b' | GEq.eq a' b' = return []
+    build ins a' b' = case lookupWith GEq.eq b' childPaths of
+      Just p  -> return [([], In (Ref p))]
+      Nothing -> uses >>= maybe insert return
+        where
+          -- Construct the edits for the children based on a root
+          construct :: Bool -> a -> State (Memo a) (Maybe (Transformation a))
+          construct ins' c =
+            if shallowEq (from c) (from b')
+            then do r <- zipWithM (buildmem ins') (imChildren c) (imChildren b')
+                    return $ Just $ concat $ updateChildPaths r
+            else return Nothing
+          -- Possible edits reusing the existing tree or using a part of
+          -- the original tree. The existing tree is only used if we didn't
+          -- just insert it, since we want to keep the inserts small
+          uses :: State (Memo a) (Maybe (Transformation a))
+          uses = reuses >>= \re -> case re of
+              Just r | ins -> return re
+              _            -> construct ins a' >>= return . best re
+          -- Possible edits that include reusing a part of the original tree
+          reuses :: State (Memo a) (Maybe (Transformation a))
+          reuses = foldM f Nothing childPaths where
+            addRef p = fmap (([], In (Ref p)):)
+            f c (x,p) = construct False x >>= return . best c . addRef p
+          -- Best edit including insertion, only chosen if nothing can be reused
+          insert :: State (Memo a) (Transformation a)
+          insert = do
+            Just r <- construct True b'
+            let (r', e') = partialApply (withRefs b') r
+            return $ ([], r') : e'
+
+-- | Helper function for lookup with provided compare function
+lookupWith :: (a -> a -> Bool) -> a -> [(a,b)] -> Maybe b
+lookupWith _ _ [] = Nothing
+lookupWith f a ((b,r):bs)
+  | f a b     = Just r
+  | otherwise = lookupWith f a bs
+
+-- | Pick the best edit
+best :: Maybe (Transformation a) -> Maybe (Transformation a) -> Maybe (Transformation a)
+best e1 e2 = case (e1,e2) of
+  (Just e1', Just e2') -> Just (pickShortest e1' e2')
+  _                    -> e1 <|> e2
+
+-- | Pick the shortest of two lists lazily
+pickShortest :: [a] -> [a] -> [a]
+pickShortest a b = if f a b then a else b
+  where f []     _      = True
+        f _      []     = False
+        f (_:xs) (_:ys) = f xs ys
+
+-- | Lift a tree to a tree with references
+withRefs :: Transform a => a -> Fix (WithRef a)
+withRefs = In . InR . fmap withRefs . from
+
+-- | Try to apply as much edits to the edit structure as possible
+--   to make the final edit smaller
+partialApply :: Transform a =>
+                Fix (WithRef a) -> Transformation a -> (Fix (WithRef a), Transformation a)
+partialApply a [] = (a, [])
+partialApply a ((p,r):xs) = case replace p r a of
+  Just a' -> partialApply a' xs
+  Nothing -> let (a',xs') = partialApply a xs in (a', (p,r) : xs')
+
+-- | Replace a subtree in an edit structure
+replace :: (Transform a, Monad m)
+           => Path -> Fix (WithRef a) -> Fix (WithRef a) -> m (Fix (WithRef a))
+replace []     r _ = return r
+replace (i:is) r a = case a of
+  In (Ref _) -> fail "Replace"
+  In (InR a') -> tmapN f a' >>= return . In . InR
+    where f j = if i == j then replace is r else return
+
+-- | Extend the paths of edits for the children with the child number
+updateChildPaths :: [Transformation a] -> [Transformation a]
+updateChildPaths = zipWith (\n -> map (\(p,c) -> (n:p,c))) [0..]
+
+--------------------------------------------------------------------------------
+-- Shallow equality
+--------------------------------------------------------------------------------
+
+class SEq f where
+  shallowEq :: f a -> f a -> Bool
+
+instance SEq I where
+  shallowEq (I _) (I _) = True
+
+instance SEq U where
+  shallowEq U U = True
+
+instance Eq a => SEq (K a) where
+  shallowEq (K a) (K b) = a == b
+
+instance (SEq f, SEq g) => SEq (f :+: g) where
+  shallowEq (L a) (L b) = shallowEq a b
+  shallowEq (R a) (R b) = shallowEq a b
+  shallowEq _     _     = False
+
+instance (SEq f, SEq g) => SEq (f :*: g) where
+  shallowEq (a :*: b) (c :*: d) = shallowEq a c && shallowEq b d
+
+instance SEq f => SEq (C c f) where
+  shallowEq (C a) (C b) = shallowEq a b
+
+instance SEq f => SEq (S s f) where
+  shallowEq (S a) (S b) = shallowEq a b
+
+--------------------------------------------------------------------------------
+-- ExtractN
+--------------------------------------------------------------------------------
+
+class ExtractN f where
+  extractN :: Monad m => Int -> f a -> m a
+
+instance ExtractN I where
+  extractN 0 (I r) = return r
+  extractN _ (I _) = fail "extractN"
+
+instance ExtractN (K a) where
+  extractN _ (K _) = fail "extractN"
+
+instance ExtractN U where
+  extractN _ U = fail "extractN"
+
+instance (ExtractN f, ExtractN g) => ExtractN (f :+: g) where
+  extractN i (L x) = extractN i x
+  extractN i (R x) = extractN i x
+
+-- Here we decrement our parameter. Does not require right-nested products
+instance (CountI f, ExtractN f, ExtractN g) => ExtractN (f :*: g) where
+  extractN i (x :*: y) = let n = countI x
+                          in if i < n then extractN i     x
+                                      else extractN (i-n) y
+
+instance ExtractN f => ExtractN (C c f) where
+  extractN i (C x) = extractN i x
+
+instance ExtractN f => ExtractN (S s f) where
+  extractN i (S x) = extractN i x
+
+--------------------------------------------------------------------------------
+-- MapN
+--------------------------------------------------------------------------------
+
+-- | Map a function with child index at a top-level structure
+tmapN :: (Monad m, MapN f) => (Int -> a -> m b) -> f a -> m (f b)
+tmapN = mapN 0
+
+class MapN f where
+  mapN :: Monad m => Int -> (Int -> a -> m b) -> f a -> m (f b)
+
+instance MapN I where
+  mapN i f (I r) = liftM I (f i r)
+
+instance MapN (K a) where
+  mapN _ _ (K x)  = liftM K (return x)
+
+instance MapN U where
+  mapN _ _ U = return U
+
+instance (MapN f, MapN g) => MapN (f :+: g) where
+  mapN i f (L x) = liftM L (mapN i f x)
+  mapN i f (R x) = liftM R (mapN i f x)
+
+-- Here we increment our parameter. Does not require right-nested products
+instance (CountI f, MapN f, MapN g) => MapN (f :*: g) where
+  mapN i f (x :*: y) = liftM2 (:*:) (mapN i f x) (mapN (i + countI x) f y)
+
+instance MapN f => MapN (C c f) where
+  mapN i f (C x) = liftM C (mapN i f x)
+
+instance MapN f => MapN (S s f) where
+  mapN i f (S x) = liftM S (mapN i f x)
+
+
+--------------------------------------------------------------------------------
+-- CountI
+--------------------------------------------------------------------------------
+
+class CountI f where
+  -- | Count the number of recursive occurrences
+  countI :: f a -> Int
+
+instance CountI I where
+  countI _ = 1
+
+instance CountI (K a) where
+  countI _ = 0
+
+instance CountI U where
+  countI _ = 0
+
+instance (CountI f, CountI g) => CountI (f :+: g) where
+  countI (L x) = countI x
+  countI (R x) = countI x
+
+instance (CountI f, CountI g) => CountI (f :*: g) where
+  countI (x :*: y) = countI x + countI y
+
+instance CountI f => CountI (C c f) where
+  countI (C x) = countI x
+
+instance CountI f => CountI (S s f) where
+  countI (S x) = countI x
+
+--------------------------------------------------------------------------------
+-- Children
+--------------------------------------------------------------------------------
+
+-- | Get the immediate children
+imChildren :: (Regular a, Children (PF a)) => a -> [a]
+imChildren = children . from
+
+-- | Get all children with their paths
+childrenPaths :: (Regular a, Children (PF a)) => a -> [(a,Path)]
+childrenPaths a = (a, []) : [ (r, n : p)
+                            | (n, c) <- zip [0..] (imChildren a)
+                            , (r, p) <- childrenPaths c ]
+
+class Children f where
+  children :: f a -> [a]
+
+instance Children I where
+  children (I r) = [r]
+
+instance Children (K a) where
+  children (K _) = []
+
+instance Children U where
+  children U = []
+
+instance (Children f, Children g) => Children (f :+: g) where
+  children (L x) = children x
+  children (R x) = children x
+
+instance (Children f, Children g) => Children (f :*: g) where
+  children (x :*: y) = children x ++ children y
+
+instance Children f => Children (C c f) where
+  children (C x) = children x
+
+instance Children f => Children (S s f) where
+  children (S x) = children x

@@ -0,0 +1,31 @@+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE UndecidableInstances       #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+
+module Generics.Regular.Transformations.RewriteRules (
+  Transform, Transformation, apply
+  ) where
+
+import Generics.Regular
+import Generics.Regular.Rewriting
+import Generics.Regular.Zipper
+
+import Control.Monad ( foldM )
+
+--------------------------------------------------------------------------------
+-- Patch
+--------------------------------------------------------------------------------
+-- Basically, a class synonym
+class (Regular a, Rewrite a, Zipper (PF a)) => Transform a
+instance Transform a => Rewrite a
+
+-- An edit is a list of:
+type Transformation a = [ ( Loc a -> Maybe (Loc a) -- A path to the location to edit
+                          , Rule a) ]              -- The rewrite rule to apply there
+
+-- Patching is terribly simple: at the given locations, apply all the rules,
+-- then exit the zipper.
+apply :: forall a. (Transform a) => Transformation a -> a -> Maybe a
+apply rs = fmap leave . flip (foldM appRule) rs . enter
+  where appRule a (l,r) = l a >>= updateM (rewriteM r)

@@ -0,0 +1,57 @@+{-# LANGUAGE FlexibleContexts           #-}
+
+module Generics.Regular.Transformations.ZipperState (
+  ZipperMonad, ZipperState, upMonad, downMonad, leftMonad, rightMonad, 
+  navigate, saveMonad, loadMonad, topMonad, updateMonad
+  ) where
+
+import Control.Monad.State (StateT (..), evalStateT, get, put)
+
+import Generics.Regular.Zipper
+import Generics.Regular ( Regular, PF )
+
+--------------------------------------------------------------------------------
+-- A zipper with state
+--------------------------------------------------------------------------------
+
+type ZipperState a = ([a], Loc a)
+type ZipperMonad a b = StateT (ZipperState a) Maybe b
+
+moveMonad :: (Loc a -> Maybe (Loc a)) -> ZipperMonad a a
+moveMonad m = StateT (\(s,l) -> m l >>= (\l' -> return (on l', (s,l'))))
+
+upMonad, downMonad, leftMonad, rightMonad :: ZipperMonad a a
+upMonad    = moveMonad up
+downMonad  = moveMonad down
+leftMonad  = moveMonad left
+rightMonad = moveMonad right
+
+updateMonad :: (a -> a) -> ZipperMonad a a
+updateMonad f = do (s,l) <- get
+                   let l' = update f l
+                   put (s,l')
+                   return (on l')
+
+saveMonad :: ZipperMonad a a
+saveMonad = do (s,l) <- get
+               let a = on l
+               put (s++[a],l)
+               return a
+
+loadMonad :: ZipperMonad a a
+loadMonad = do (s:ss,l) <- get
+               let l' = update (const s) l
+               put (ss,l')
+               return (on l')
+
+topMonad :: ZipperMonad a a
+topMonad = do (_, Loc x l) <- get
+              case l of
+                [] -> return x
+                _  -> upMonad >> topMonad
+
+leaveMonad :: Loc a -> ZipperMonad a b -> Maybe a
+leaveMonad s m = evalStateT (m >> topMonad) ([],s)
+
+navigate :: (Regular a, Zipper (PF a)) => a -> ZipperMonad a b -> Maybe a
+navigate x m = leaveMonad (enter x) m

@@ -0,0 +1,245 @@+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE KindSignatures             #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE EmptyDataDecls             #-}
+{-# LANGUAGE TupleSections              #-}
+
+module Generics.Regular.Zipper
+  (-- * Locations
+   Loc(..),
+   -- * Context frames
+   Ctx(),
+   -- * Generic zipper class
+   Zipper(..),
+   -- * Interface
+   enter,
+   down, down', up, right, left,
+   -- dfnext, dfprev,
+   leave, on, update, updateM
+
+  )
+  where
+
+import Prelude hiding (last)
+
+import Control.Monad
+import Control.Monad.State
+import Control.Applicative
+import Data.Maybe
+import Data.Traversable
+
+import Generics.Regular hiding (left, right)
+
+-- * Locations and context stacks
+
+-- | Abstract type of locations. A location contains the current focus
+-- and its context. A location is parameterized over the family of
+-- datatypes and over the type of the complete value.
+
+data Loc :: * -> * where
+  Loc :: (Regular a, Zipper (PF a)) => a -> [Ctx (PF a) a] -> Loc a
+
+-- * Context frames
+
+-- | Abstract type of context frames. Not required for the high-level
+-- navigation functions.
+
+data family Ctx (f :: * -> *) :: * -> *
+
+data instance Ctx (K a) r
+data instance Ctx U r
+data instance Ctx (f :+: g) r = CL (Ctx f r) | CR (Ctx g r)
+data instance Ctx (f :*: g) r = C1 (Ctx f r) (g r) | C2 (f r) (Ctx g r)
+data instance Ctx I r = CId
+data instance Ctx (C c f) r = CC (Ctx f r)
+data instance Ctx (S s f) r = CS (Ctx f r)
+
+-- * Contexts and locations are functors
+
+instance Zipper f => Functor (Ctx f) where
+  fmap = cmap
+
+-- instance Functor (Loc f) where
+  -- fmap f (Loc p x)  = Loc (f p) (map (fmap f) x)
+
+-- * Generic navigation functions
+
+-- | It is in general not necessary to use the generic navigation
+-- functions directly. The functions listed in the ``Interface'' section
+-- below are more user-friendly.
+--
+
+class Functor f => Zipper f where
+  cmap        :: (a -> b) -> Ctx f a -> Ctx f b
+  fill        :: Ctx f a -> a -> f a
+  first, last :: f a -> Maybe (a, Ctx f a)
+  next, prev  :: Ctx f a -> a -> Maybe (a, Ctx f a)
+
+instance Zipper I where
+  cmap  f CId = CId
+  fill  CId x = I x
+  first (I x) = Just (x, CId)
+  last  (I x) = Just (x, CId)
+  next  CId x = Nothing
+  prev  CId x = Nothing
+
+instance Zipper (K a) where
+  cmap f void = impossible void
+  fill void x = impossible void
+  first (K a) = Nothing
+  last  (K a) = Nothing
+  next  void x = impossible void
+  prev  void x = impossible void
+
+instance Zipper U where
+  cmap f void = impossible void
+  fill void x = impossible void
+  first U      = Nothing
+  last  U      = Nothing
+  next  void x = impossible void
+  prev  void x = impossible void
+
+instance (Zipper f, Zipper g) => Zipper (f :+: g) where
+  cmap f (CL c)   = CL (cmap f c)
+  cmap f (CR c)   = CR (cmap f c)
+  fill (CL c) x   = L (fill c x)
+  fill (CR c) y   = R (fill c y)
+  first (L x)     = first x >>= return . fmap CL
+  first (R x)     = first x >>= return . fmap CR
+  last  (L x)     = last x >>= return . fmap CL
+  last  (R x)     = last x >>= return . fmap CR
+  next  (CL c) x = next c x >>= return . fmap CL
+  next  (CR c) x = next c x >>= return . fmap CR
+  prev  (CL c) x = prev c x >>= return . fmap CL
+  prev  (CR c) x = prev c x >>= return . fmap CR
+
+instance (Zipper f, Zipper g) => Zipper (f :*: g) where
+  cmap f (C1 c y)   = C1 (cmap f c) (fmap f y)
+  cmap f (C2 x c)   = C2 (fmap f x) (cmap f c)
+  fill (C1 c y) x = fill c x :*: y
+  fill (C2 x c) y = x :*: fill c y
+  first (x :*: y) =         fmap (fmap (flip C1 y)) (first x)
+                    `mplus` fmap (fmap (C2 x))      (first y)
+  last  (x :*: y) =         fmap (fmap (C2 x))      (last  y)
+                    `mplus` fmap (fmap (flip C1 y)) (last  x)
+  next (C1 c y) z =         (fmap (flip C1 y)     <$> next c z)
+                    `mplus` (fmap (C2 (fill c z)) <$> first y)
+  next (C2 x c) z =          fmap (C2 x)          <$> next c z
+  prev (C1 c y) z =          fmap (flip C1 y)     <$> prev c z
+  prev (C2 x c) z =         (fmap (C2 x)               <$> prev c z)
+                    `mplus` (fmap (flip C1 (fill c z)) <$> last x)
+
+instance (Zipper f) => Zipper (C c f) where
+  cmap f (CC c)   = CC (cmap f c)
+  fill   (CC c) x = C (fill c x)
+  first  (C x)    = first  x >>= return . fmap CC
+  last   (C x)    = last   x >>= return . fmap CC
+  next   (CC c) x = next c x >>= return . fmap CC
+  prev   (CC c) x = prev c x >>= return . fmap CC
+
+instance (Zipper f) => Zipper (S s f) where
+  cmap f (CS c)   = CS (cmap f c)
+  fill   (CS c) x = S (fill c x)
+  first  (S x)    = first  x >>= return . fmap CS
+  last   (S x)    = last   x >>= return . fmap CS
+  next   (CS c) x = next c x >>= return . fmap CS
+  prev   (CS c) x = prev c x >>= return . fmap CS
+
+-- * Interface
+
+-- ** Introduction
+
+-- | Start navigating a datastructure. Returns a location that
+-- focuses the entire value and has an empty context.
+enter :: (Regular a, Zipper (PF a)) => a -> Loc a
+enter x = Loc x []
+
+-- ** Navigation
+
+-- | Move down to the leftmost child. Returns 'Nothing' if the
+-- current focus is a leaf.
+down :: Loc a -> Maybe (Loc a)
+down (Loc x cs) = first (from x) >>= \(a,c) -> return (Loc a (c:cs))
+
+-- | Move down to the rightmost child. Returns 'Nothing' if the
+-- current focus is a leaf.
+down' :: Loc a -> Maybe (Loc a)
+down' (Loc x cs) = last (from x) >>= \(a,c) -> return (Loc a (c:cs))
+
+-- | Move up to the parent. Returns 'Nothing' if the current
+-- focus is the root.
+up :: Loc a -> Maybe (Loc a)
+up (Loc x [])     = Nothing
+up (Loc x (c:cs)) = return (Loc (to (fill c x)) cs)
+
+-- | Move to the right sibling. Returns 'Nothing' if the current
+-- focus is the rightmost sibling.
+right :: Loc a -> Maybe (Loc a)
+right (Loc x []    ) = Nothing
+right (Loc x (c:cs)) = next c x >>= \(a,c') -> return (Loc a (c':cs))
+
+-- | Move to the left sibling. Returns 'Nothing' if the current
+-- focus is the leftmost sibling.
+left :: Loc a -> Maybe (Loc a)
+left (Loc x []    ) = Nothing
+left (Loc x (c:cs)) = prev c x >>= \(a,c') -> return (Loc a (c':cs))
+
+
+-- ** Derived navigation.
+{-
+df :: (a -> Maybe a) -> (a -> Maybe a) -> (a -> Maybe a) -> a -> Maybe a
+df d u lr l =
+  case d l of
+    Nothing -> df' l
+    r       -> r
+ where
+  df' l =
+    case lr l of
+      Nothing -> case u l of
+                   Nothing -> Nothing
+                   Just l' -> df' l'
+      r       -> r
+
+-- | Move through all positions in depth-first left-to-right order.
+dfnext :: Loc phi I0 ix -> Maybe (Loc phi I0 ix)
+dfnext = df down up right
+
+-- | Move through all positions in depth-first right-to-left order.
+dfprev :: Loc phi I0 ix -> Maybe (Loc phi I0 ix)
+dfprev = df down' up left
+-}
+
+-- | Utility
+-- navigate :: (Regular a, Zipper (PF a))
+         -- => a -> (Loc a -> Maybe (Loc a)) -> Loc a
+-- navigate a f = fromJust $ f (enter a)
+
+-- ** Elimination
+
+-- | Return the entire value, independent of the current focus.
+leave :: Loc a -> a
+leave (Loc x []) = x
+leave loc        = leave (fromJust (up loc))
+
+-- | Operate on the current focus. This function can be used to
+-- extract the current point of focus.
+on :: Loc a -> a
+on (Loc x _) = x
+
+-- | Update the current focus without changing its type.
+update :: (a -> a) -> Loc a -> Loc a
+update f (Loc x cs) = Loc (f x) cs
+
+-- | Update the current focus without changing its type.
+updateM :: Monad m => (a -> m a) -> Loc a -> m (Loc a)
+updateM f (Loc x cs) = f x >>= \y -> return (Loc y cs)
+
+-- * Internal functions
+
+impossible :: a -> b
+impossible x = x `seq` error "impossible"

@@ -0,0 +1,675 @@+              GNU GENERAL PUBLIC LICENSE
+                Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                     Preamble
+
+  The GNU General Public License is a free, copyleft license for
+software and other kinds of works.
+
+  The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works.  By contrast,
+the GNU General Public License is intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.  We, the Free Software Foundation, use the
+GNU General Public License for most of our software; it applies also to
+any other work released this way by its authors.  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+  To protect your rights, we need to prevent others from denying you
+these rights or asking you to surrender the rights.  Therefore, you have
+certain responsibilities if you distribute copies of the software, or if
+you modify it: responsibilities to respect the freedom of others.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must pass on to the recipients the same
+freedoms that you received.  You must make sure that they, too, receive
+or can get the source code.  And you must show them these terms so they
+know their rights.
+
+  Developers that use the GNU GPL protect your rights with two steps:
+(1) assert copyright on the software, and (2) offer you this License
+giving you legal permission to copy, distribute and/or modify it.
+
+  For the developers' and authors' protection, the GPL clearly explains
+that there is no warranty for this free software.  For both users' and
+authors' sake, the GPL requires that modified versions be marked as
+changed, so that their problems will not be attributed erroneously to
+authors of previous versions.
+
+  Some devices are designed to deny users access to install or run
+modified versions of the software inside them, although the manufacturer
+can do so.  This is fundamentally incompatible with the aim of
+protecting users' freedom to change the software.  The systematic
+pattern of such abuse occurs in the area of products for individuals to
+use, which is precisely where it is most unacceptable.  Therefore, we
+have designed this version of the GPL to prohibit the practice for those
+products.  If such problems arise substantially in other domains, we
+stand ready to extend this provision to those domains in future versions
+of the GPL, as needed to protect the freedom of users.
+
+  Finally, every program is threatened constantly by software patents.
+States should not allow patents to restrict development and use of
+software on general-purpose computers, but in those that do, we wish to
+avoid the special danger that patents applied to a free program could
+make it effectively proprietary.  To prevent this, the GPL assures that
+patents cannot be used to render the program non-free.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                TERMS AND CONDITIONS
+
+  0. Definitions.
+
+  "This License" refers to version 3 of the GNU General Public License.
+
+  "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+ 
+  "The Program" refers to any copyrightable work licensed under this
+License.  Each licensee is addressed as "you".  "Licensees" and
+"recipients" may be individuals or organizations.
+
+  To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy.  The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+  A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+  To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy.  Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+  To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies.  Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+  An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License.  If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+  1. Source Code.
+
+  The "source code" for a work means the preferred form of the work
+for making modifications to it.  "Object code" means any non-source
+form of a work.
+
+  A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+  The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form.  A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+  The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities.  However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work.  For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+  The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+  The Corresponding Source for a work in source code form is that
+same work.
+
+  2. Basic Permissions.
+
+  All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met.  This License explicitly affirms your unlimited
+permission to run the unmodified Program.  The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work.  This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+  You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force.  You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright.  Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+  Conveying under any other circumstances is permitted solely under
+the conditions stated below.  Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+  3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+  No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+  When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+  4. Conveying Verbatim Copies.
+
+  You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+  You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+  5. Conveying Modified Source Versions.
+
+  You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+    a) The work must carry prominent notices stating that you modified
+    it, and giving a relevant date.
+
+    b) The work must carry prominent notices stating that it is
+    released under this License and any conditions added under section
+    7.  This requirement modifies the requirement in section 4 to
+    "keep intact all notices".
+
+    c) You must license the entire work, as a whole, under this
+    License to anyone who comes into possession of a copy.  This
+    License will therefore apply, along with any applicable section 7
+    additional terms, to the whole of the work, and all its parts,
+    regardless of how they are packaged.  This License gives no
+    permission to license the work in any other way, but it does not
+    invalidate such permission if you have separately received it.
+
+    d) If the work has interactive user interfaces, each must display
+    Appropriate Legal Notices; however, if the Program has interactive
+    interfaces that do not display Appropriate Legal Notices, your
+    work need not make them do so.
+
+  A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit.  Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+  6. Conveying Non-Source Forms.
+
+  You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+    a) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by the
+    Corresponding Source fixed on a durable physical medium
+    customarily used for software interchange.
+
+    b) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by a
+    written offer, valid for at least three years and valid for as
+    long as you offer spare parts or customer support for that product
+    model, to give anyone who possesses the object code either (1) a
+    copy of the Corresponding Source for all the software in the
+    product that is covered by this License, on a durable physical
+    medium customarily used for software interchange, for a price no
+    more than your reasonable cost of physically performing this
+    conveying of source, or (2) access to copy the
+    Corresponding Source from a network server at no charge.
+
+    c) Convey individual copies of the object code with a copy of the
+    written offer to provide the Corresponding Source.  This
+    alternative is allowed only occasionally and noncommercially, and
+    only if you received the object code with such an offer, in accord
+    with subsection 6b.
+
+    d) Convey the object code by offering access from a designated
+    place (gratis or for a charge), and offer equivalent access to the
+    Corresponding Source in the same way through the same place at no
+    further charge.  You need not require recipients to copy the
+    Corresponding Source along with the object code.  If the place to
+    copy the object code is a network server, the Corresponding Source
+    may be on a different server (operated by you or a third party)
+    that supports equivalent copying facilities, provided you maintain
+    clear directions next to the object code saying where to find the
+    Corresponding Source.  Regardless of what server hosts the
+    Corresponding Source, you remain obligated to ensure that it is
+    available for as long as needed to satisfy these requirements.
+
+    e) Convey the object code using peer-to-peer transmission, provided
+    you inform other peers where the object code and Corresponding
+    Source of the work are being offered to the general public at no
+    charge under subsection 6d.
+
+  A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+  A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling.  In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage.  For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product.  A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+  "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source.  The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+  If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information.  But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+  The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed.  Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+  Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+  7. Additional Terms.
+
+  "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law.  If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+  When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it.  (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.)  You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+  Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+    a) Disclaiming warranty or limiting liability differently from the
+    terms of sections 15 and 16 of this License; or
+
+    b) Requiring preservation of specified reasonable legal notices or
+    author attributions in that material or in the Appropriate Legal
+    Notices displayed by works containing it; or
+
+    c) Prohibiting misrepresentation of the origin of that material, or
+    requiring that modified versions of such material be marked in
+    reasonable ways as different from the original version; or
+
+    d) Limiting the use for publicity purposes of names of licensors or
+    authors of the material; or
+
+    e) Declining to grant rights under trademark law for use of some
+    trade names, trademarks, or service marks; or
+
+    f) Requiring indemnification of licensors and authors of that
+    material by anyone who conveys the material (or modified versions of
+    it) with contractual assumptions of liability to the recipient, for
+    any liability that these contractual assumptions directly impose on
+    those licensors and authors.
+
+  All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10.  If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term.  If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+  If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+  Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+  8. Termination.
+
+  You may not propagate or modify a covered work except as expressly
+provided under this License.  Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+  However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+  Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+  Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License.  If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+  9. Acceptance Not Required for Having Copies.
+
+  You are not required to accept this License in order to receive or
+run a copy of the Program.  Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance.  However,
+nothing other than this License grants you permission to propagate or
+modify any covered work.  These actions infringe copyright if you do
+not accept this License.  Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+  10. Automatic Licensing of Downstream Recipients.
+
+  Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License.  You are not responsible
+for enforcing compliance by third parties with this License.
+
+  An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations.  If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+  You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License.  For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+  11. Patents.
+
+  A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based.  The
+work thus licensed is called the contributor's "contributor version".
+
+  A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version.  For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+  Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+  In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement).  To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+  If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients.  "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+  
+  If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+  A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License.  You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+  Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+  12. No Surrender of Others' Freedom.
+
+  If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all.  For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+  13. Use with the GNU Affero General Public License.
+
+  Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU Affero General Public License into a single
+combined work, and to convey the resulting work.  The terms of this
+License will continue to apply to the part which is the covered work,
+but the special requirements of the GNU Affero General Public License,
+section 13, concerning interaction through a network will apply to the
+combination as such.
+
+  14. Revised Versions of this License.
+
+  The Free Software Foundation may publish revised and/or new versions of
+the GNU General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+  Each version is given a distinguishing version number.  If the
+Program specifies that a certain numbered version of the GNU General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation.  If the Program does not specify a version number of the
+GNU General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+  If the Program specifies that a proxy can decide which future
+versions of the GNU General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+  Later license versions may give you additional or different
+permissions.  However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+  15. Disclaimer of Warranty.
+
+  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. Limitation of Liability.
+
+  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+  17. Interpretation of Sections 15 and 16.
+
+  If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+              END OF TERMS AND CONDITIONS
+
+     How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+Also add information on how to contact you by electronic and paper mail.
+
+  If the program does terminal interaction, make it output a short
+notice like this when it starts in an interactive mode:
+
+    <program>  Copyright (C) <year>  <name of author>
+    This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, your program's commands
+might be different; for a GUI interface, you would use an "about box".
+
+  You should also get your employer (if you work as a programmer) or school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.
+For more information on this, and how to apply and follow the GNU GPL, see
+<http://www.gnu.org/licenses/>.
+
+  The GNU General Public License does not permit incorporating your program
+into proprietary programs.  If your program is a subroutine library, you
+may consider it more useful to permit linking proprietary applications with
+the library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.  But first, please read
+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain

@@ -0,0 +1,81 @@+
+module Datatypes (
+  Tree (..), exTree1, exTree2, exTree3, exTree4, exTree5,
+  List (..), toL, fromL, exLst1, exLst2,
+  X (..), exX1, exX2,
+  Zig (..), Zag (..), zigzag, zigzag2,
+  Expr, prog1, prog2, prog3, prog4, prog5, prog6,
+  module Lang
+  ) where
+
+import Lang
+import Data.List ( unfoldr )
+
+--------------------------------------------------------------------------------
+-- Example datatypes
+--------------------------------------------------------------------------------
+
+--Trees
+data Tree = Leaf Int | Bin Tree Tree deriving (Show, Eq)
+
+exTree1, exTree2, exTree3, exTree4, exTree5 :: Tree
+exTree1 = Bin (Leaf 0) (Leaf 1)
+exTree2 = Bin (Leaf 1) (Leaf 0)
+exTree3 = Bin (Leaf 2) (Leaf 3)
+exTree4 = Bin exTree2 exTree3
+exTree5 = Bin exTree3 exTree4
+
+-- Lists
+data List a = Nil | Cons a (List a) deriving (Eq, Show)
+
+toL :: [a] -> List a
+toL = foldr Cons Nil
+
+fromL :: List a -> [a]
+fromL = unfoldr f where
+  f Nil        = Nothing
+  f (Cons h t) = Just (h,t)
+
+exLst1, exLst2 :: List Int
+exLst1 = Cons 1 $ Cons 2 $ Cons 3 $ Cons 4 Nil
+exLst2 = Cons 4 $ Cons 2 $ Cons 3 $ Cons 1 Nil
+
+-- Something more exotic
+data X = XA X | XB X | XC X X | XD Int deriving (Show, Eq)
+
+exX1, exX2 :: X
+exX1 = XA (XA (XA (XC (XD 1) (XD 2))))
+exX2 = XA (XB (XA (XA (XB (XC (XD 2) (XD 1))))))
+
+-- Mutually recursive
+data Zig = Zig1 Zig | Zig2 Zag | Zig3 deriving (Show, Eq)
+data Zag = Zag1 Zag | Zag2 Zig | Zag3 deriving (Show, Eq)
+
+zigzag :: Zig
+zigzag = Zig1 (Zig2 (Zag2 Zig3))
+
+zigzag2 :: Zig
+zigzag2 = Zig2 (Zag1 (Zag2 Zig3))
+
+-- Example from paper (imported from Lang)
+type Expr = AExpr
+
+progFragment1, progFragment2 :: String
+progFragment1 =     "a := 1;"
+                 ++ "b := a + 2;"
+                 ++ "if b > 3"
+                 ++ "then a := 2"
+                 ++ "else b := 1;"
+progFragment2 =     "a := 1;"
+                 ++ "b := a + 2;"
+                 ++ "if not b > 3"
+                 ++ "then b := 1"
+                 ++ "else a := 2;"
+
+prog1, prog2, prog3, prog4, prog5, prog6 :: Stmt
+prog1 = parseString . init . concat . replicate 1 $ progFragment1
+prog2 = parseString . init . concat . replicate 1 $ progFragment2
+prog3 = parseString . init . concat . replicate 4 $ progFragment1
+prog4 = parseString . init . concat . replicate 4 $ progFragment2
+prog5 = parseString . init . concat . replicate 5 $ progFragment1
+prog6 = parseString . init . concat . replicate 5 $ progFragment2

@@ -0,0 +1,368 @@+Source: http://www.haskell.org/haskellwiki/Parsing_a_simple_imperative_language
+
+This tutorial will present how to parse a subset of a simple imperative
+programming language called W<small>HILE</small> (introduced in a book
+"Principles of Program Analysis" by Nielson, Nielson and Hankin). It includes
+only a few statements and basic boolean/arithmetic expressions, which makes it
+a nice material for a tutorial.
+
+== Imports ==
+
+First let's specify the name of the module:
+
+<haskell>
+
+> module Lang where
+
+</haskell>
+
+And then import the necessary libraries:
+
+<haskell>
+
+> import System.IO
+> import Control.Monad
+> import Text.ParserCombinators.Parsec
+> import Text.ParserCombinators.Parsec.Expr
+> import Text.ParserCombinators.Parsec.Language
+> import qualified Text.ParserCombinators.Parsec.Token as Token
+
+</haskell>
+
+== The language ==
+
+The grammar for expressions is defined as follows:
+
+<tt>
+
+''a''   ::=  ''x'' | ''n'' | - ''a'' | ''a'' ''opa'' ''a''
+
+''b''   ::=  true | false | not ''b'' | ''b'' ''opb'' ''b'' | ''a'' ''opr'' ''a''
+
+''opa'' ::=  + | - | * | /
+
+''opb'' ::=  and | or
+
+''opr'' ::=  > | <
+
+</tt>
+
+Note that we have three groups of operators - arithmetic, booloan and
+relational ones.
+
+And now the definition of statements:
+
+<tt>
+
+''S''   ::=  x := ''a'' | skip | ''S1''; ''S2'' | ''( S )'' | if ''b'' then ''S1'' else ''S2'' | while ''b'' do ''S''
+
+</tt>
+
+We probably want to parse that into some internal representation of the
+language (abstract syntax tree). Therefore we need to define the data
+structures for the expressions and statements.
+
+== Data structures ==
+
+We need to take care of boolean and arithmetic expressions and the
+appropriate operators. First let's look at the boolean expressions:
+
+<haskell>
+
+> data BExpr = BConst Bool
+>            | Not BExpr
+>            | And BExpr BExpr
+>            | Greater AExpr AExpr
+>             deriving (Show, Eq)
+
+</haskell>
+
+Now we define the types for arithmetic expressions:
+
+<haskell>
+
+> data AExpr = Var String
+>            | Const Integer
+>            | Neg AExpr
+>            | Add AExpr AExpr
+>              deriving (Show, Eq)
+
+</haskell>
+
+Finally let's take care of the statements:
+
+<haskell>
+
+> data Stmt = Seq [Stmt]
+>           | Assign String AExpr
+>           | If BExpr Stmt Stmt
+>           | While BExpr Stmt
+>           | Skip
+>             deriving (Show, Eq)
+
+</haskell>
+
+== Lexer ==
+
+Having all the data structures we can go on with writing the code to do actual
+parsing. First of all we create the language definition using Haskell's record
+syntax and the constructor <hask>emptyDef</hask> (from
+<hask>Text.ParserCombinators.Parsec.Language</hask>):
+
+<haskell>
+
+> languageDef =
+>   emptyDef { Token.commentStart    = "/*"
+>            , Token.commentEnd      = "*/"
+>            , Token.commentLine     = "//"
+>            , Token.identStart      = letter
+>            , Token.identLetter     = alphaNum
+>            , Token.reservedNames   = [ "if"
+>                                      , "then"
+>                                      , "else"
+>                                      , "while"
+>                                      , "do"
+>                                      , "skip"
+>                                      , "true"
+>                                      , "false"
+>                                      , "not"
+>                                      , "and"
+>                                      , "or"
+>                                      ]
+>            , Token.reservedOpNames = ["+", "-", "*", "/", ":="
+>                                      , "<", ">", "and", "or", "not"
+>                                      ]
+>            }
+
+</haskell>
+
+This creates a language definition that accepts the C-style comments, requires
+that the identifiers start with a letter, and end with alphanumeric
+characters. Moreover there is a number of reserved names, that cannot be used
+by the identifiers.
+
+Having the above definition we can create a lexer:
+
+<haskell>
+
+> lexer = Token.makeTokenParser languageDef
+
+</haskell>
+
+<tt>lexer</tt> contains a number of lexical parsers, that we can us to parse
+identifiers, reserved words/operations, etc. Now we can select/extract them in
+the following way:
+
+<haskell>
+
+> identifier = Token.identifier lexer -- parses an identifier
+> reserved   = Token.reserved   lexer -- parses a reserved name
+> reservedOp = Token.reservedOp lexer -- parses an operator
+> parens     = Token.parens     lexer -- parses surrounding parenthesis:
+>                                     --   parens p
+>                                     -- takes care of the parenthesis and
+>                                     -- uses p to parse what's inside them
+> integer    = Token.integer    lexer -- parses an integer
+> semi       = Token.semi       lexer -- parses a semicolon
+> whiteSpace = Token.whiteSpace lexer -- parses whitespace
+
+</haskell>
+
+This isn't really necessary, but should make the code much more readable (also
+this is the reason why we used the qualified import of
+<hask>Text.ParserCombinators.Parsec.Token</hask>). Now we can use them to
+parse the source code at the token level. One of the nice features of these
+parsers is that they take care of all whitespace after the tokens.
+
+== Main parser ==
+
+As already mentioned a program in this language is simply a statement, so the
+main parser should basically only parse a statement. But remember to take care of
+initial whitespace - our parsers only get rid of whitespace after the tokens!
+
+<haskell>
+
+> whileParser :: Parser Stmt
+> whileParser = whiteSpace >> statement
+
+</haskell>
+
+Now because any statement might be actually a sequence of statements separated
+by semicolon, we use <hask>sepBy1</hask> to parse at least one statement. The
+result is a list of statements. We also allow grouping statements by the
+parenthesis, which is useful, for instance, in the <tt>while</tt> loop.
+
+<haskell>
+
+> statement :: Parser Stmt
+> statement =   parens statement
+>           <|> sequenceOfStmt
+
+> sequenceOfStmt =
+>   do list <- (sepBy1 statement' semi)
+>      -- If there's only one statement return it without using Seq.
+>      return $ if length list == 1 then head list else Seq list
+
+</haskell>
+
+Now a single statement is quite simple, it's either an if conditional, a while
+loop, an assignment or simply a skip statement. We use <hask><|></hask> to
+express choice. So <hask>a <|> b</hask> will first try parser <hask>a</hask>
+and if it fails (but without actually consuming any input) then parser
+<hask>b</hask> will be used. Note: this means that the order is important.
+
+<haskell>
+
+> statement' :: Parser Stmt
+> statement' =   ifStmt
+>            <|> whileStmt
+>            <|> skipStmt
+>            <|> assignStmt
+
+</haskell>
+
+If you have a parser that might fail after consuming some input, and you still
+want to try the next parser, you should look into <hask>try</hask> combinator.
+For instance <hask>try p <|> q</hask> will try parsing with <hask>p</hask> and
+if it fails, even after consuming the input, the <hask>q</hask> parser will be
+used as if nothing has been consumed by <hask>p</hask>.
+
+Now let's define the parsers for all the possible statements. This is quite
+straightforward as we just use the parsers from the lexer and then use all the
+necessary information to create appropriate data structures.
+
+<haskell>
+
+> ifStmt :: Parser Stmt
+> ifStmt =
+>   do reserved "if"
+>      cond  <- bExpression
+>      reserved "then"
+>      stmt1 <- statement
+>      reserved "else"
+>      stmt2 <- statement
+>      return $ If cond stmt1 stmt2
+
+> whileStmt :: Parser Stmt
+> whileStmt =
+>   do reserved "while"
+>      cond <- bExpression
+>      reserved "do"
+>      stmt <- statement
+>      return $ While cond stmt
+
+> assignStmt :: Parser Stmt
+> assignStmt =
+>   do var  <- identifier
+>      reservedOp ":="
+>      expr <- aExpression
+>      return $ Assign var expr
+
+> skipStmt :: Parser Stmt
+> skipStmt = reserved "skip" >> return Skip
+
+</haskell>
+
+== Expressions ==
+
+What's left is to parse the expressions. Fortunately Parsec provides a very
+easy way to do that. Let's define the arithmetic and boolean expressions:
+
+<haskell>
+
+> aExpression :: Parser AExpr
+> aExpression = buildExpressionParser aOperators aTerm
+
+> bExpression :: Parser BExpr
+> bExpression = buildExpressionParser bOperators bTerm
+
+</haskell>
+
+Now we have to define the lists with operator precedence, associativity and
+what constructors to use in each case.
+
+<haskell>
+
+> aOperators = [ [Prefix (reservedOp "-"   >> return (Neg             ))          ]
+>              , [Infix  (reservedOp "+"   >> return (Add             )) AssocLeft]
+>               ]
+
+> bOperators = [ [Prefix (reservedOp "not" >> return (Not             ))          ]
+>              , [Infix  (reservedOp "and" >> return (And             )) AssocLeft]
+>              ]
+
+</haskell>
+
+In case of Prefix operators it is enough to specify which one should be parsed
+and what is the associated data constructor. Infix operators are defined
+similarly, but it's necessary to add information about associativity. Note
+that the operator precedence depends only on the order of the elements in the
+list.
+
+Finally we have to define the terms. In case of arithmetic expressions, it is
+quite simple:
+
+<haskell>
+
+> aTerm =  parens aExpression
+>      <|> liftM Var identifier
+>      <|> liftM Const integer
+
+</haskell>
+
+However, the term in a boolean expression is a bit more tricky. In this case,
+a term can also be an expression with relational operator consisting of
+arithmetic expressions.
+
+<haskell>
+
+> bTerm =  parens bExpression
+>      <|> (reserved "true"  >> return (BConst True ))
+>      <|> (reserved "false" >> return (BConst False))
+>      <|> rExpression
+
+</haskell>
+
+Therefore we have to define a parser for relational expressions:
+
+<haskell>
+
+> rExpression =
+>   do a1 <- aExpression
+>      op <- reservedOp ">"
+>      a2 <- aExpression
+>      return $ Greater a1 a2
+
+</haskell>
+
+And that's it. We have a quite simple parser able to parse a few statements and
+arithmetic/boolean expressions.
+
+== Notes ==
+
+If you want to experiment with the parser inside ghci, these functions might be
+handy:
+
+<haskell>
+
+> parseString :: String -> Stmt
+> parseString str =
+>   case parse whileParser "" str of
+>     Left e  -> error $ show e
+>     Right r -> r
+
+> parseFile :: String -> IO Stmt
+> parseFile file =
+>   do program  <- readFile file
+>      case parse whileParser "" program of
+>        Left e  -> print e >> fail "parse error"
+>        Right r -> return r
+
+</haskell>
+
+Now you can simply load the module in ghci and then do
+<hask>ast <- parseFile "<filename>"</hask> to parse a file and get the
+result if parsing was successful. If you already have a string with
+the program, you can use <hask>parseString</hask>.
+
+[[Category:How to]]

@@ -0,0 +1,177 @@+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE TypeFamilies          #-}
+
+module MultiRec where
+
+import Datatypes
+import Generics.MultiRec.Any
+import Generics.MultiRec.Transformations.RewriteRules as RR
+import Generics.MultiRec.Transformations.ZipperState
+import Generics.MultiRec.Transformations.Explicit as Ex
+import Generics.MultiRec.Rewriting
+import Generics.MultiRec.Zipper
+
+import Generics.MultiRec hiding (show)
+import Generics.MultiRec.TH
+
+import Control.Monad ( (>=>) )
+
+--------------------------------------------------------------------------------
+-- Multirec representations for the example datatypes
+--------------------------------------------------------------------------------
+data TreeAST :: * -> * where
+  Tree :: TreeAST Tree
+
+$(deriveAll ''TreeAST)
+
+data ListAST :: * -> * -> * where
+  List :: ListAST a (List a)
+
+$(deriveAll ''ListAST)
+
+data XAST :: * -> * where
+  X :: XAST X
+
+$(deriveAll ''XAST)
+
+data ZigZag :: * -> * where
+  Zig :: ZigZag Zig
+  Zag :: ZigZag Zag
+
+$(deriveAll ''ZigZag)
+
+data AST i where
+  BExpr  :: AST BExpr
+  AExpr  :: AST AExpr
+  Stmt   :: AST Stmt
+
+$(deriveAll ''AST)
+
+--------------------------------------------------------------------------------
+-- Rewrite rules solution
+--------------------------------------------------------------------------------
+instance RR.Transform AST
+
+-- Now we can simply do the above transformation in a nice way!
+rr = RR.apply [insert (down >=> right >=> right) change] Stmt prog1 == Just prog2
+  where
+    change = rule $ \e a b -> If e a b :~> If (Not e) b a
+
+-- The same one in two steps, which illustrates that rules can be of different
+-- types
+rr2 = RR.apply [ insert (down >=> right >=> right) swap
+               , insert down addNot] Stmt prog1          == Just prog2
+  where
+    swap   :: Rule AST Stmt
+    swap   = rule $ \e a b -> If e a b :~> If e b a
+    addNot :: Rule AST BExpr
+    addNot = rule $ \e -> e :~> Not e
+
+--------------------------------------------------------------------------------
+-- Zipper with state
+--------------------------------------------------------------------------------
+zs = navigate Stmt prog1 $ do
+  downMonad >> rightMonad >> rightMonad
+  -- Swap
+  l <- downMonad >> rightMonad
+  r <- rightMonad
+  updateMonad (\p _ -> matchAny p l)
+  leftMonad
+  updateMonad (\p _ -> matchAny p r)
+  -- Add the not
+  leftMonad
+  updateMonad (\p e -> case p of
+                  BExpr -> Just (Not e)
+                  _     -> Nothing)
+
+--------------------------------------------------------------------------------
+-- Explicit
+--------------------------------------------------------------------------------
+instance Ex.Transform AST
+
+-- Ordering index of AST as AExpr < BExpr < Stmt
+instance OrdI AST where
+  compareI AExpr AExpr = EQ
+  compareI AExpr _     = LT
+  compareI BExpr AExpr = GT
+  compareI BExpr BExpr = EQ
+  compareI BExpr _     = LT
+  compareI Stmt  Stmt  = EQ
+  compareI Stmt  _     = GT
+
+-- Family with references
+class HasRef phi where
+  type RefRep phi ix
+  toRef   :: phi ix -> HFix (WithRef phi) ix -> RefRep phi ix
+  fromRef :: phi ix -> RefRep phi ix -> HFix (WithRef phi) ix
+
+data NiceInsert phi where
+  NiceInsert :: phi ix -> Path -> RefRep phi ix -> NiceInsert phi
+
+type NiceTransformation phi = [ NiceInsert phi]
+
+toNiceTransformation :: HasRef phi => Ex.Transformation phi -> NiceTransformation phi
+toNiceTransformation = map f
+  where f (Ex.AnyInsert p l x) = NiceInsert p l (toRef p x)
+
+-- Instances for example
+data AExprEH = VarEH String
+             | ConstEH Integer
+             | NegEH AExprEH
+             | AddEH AExprEH AExprEH
+             | AExprRef Path
+           deriving (Show, Eq)
+
+data BExprEH = BConstEH Bool
+             | NotEH BExprEH
+             | AndEH BExprEH BExprEH
+             | GreaterEH AExprEH AExprEH
+             | BExprRef Path
+             deriving (Show, Eq)
+
+data StmtEH = SeqEH [StmtEH]
+            | AssignEH String AExprEH
+            | IfEH BExpr StmtEH StmtEH
+            | WhileEH BExprEH StmtEH
+            | SkipEH
+            | StmtRef Path
+            deriving (Show, Eq)
+
+instance HasRef AST where
+  type RefRep AST AExpr = AExprEH
+  type RefRep AST BExpr = BExprEH
+  type RefRep AST Stmt  = StmtEH
+  
+  -- Not complete, but enough for example below
+  toRef AExpr (HIn (Ref p)) = AExprRef p
+  toRef BExpr (HIn (Ref p)) = BExprRef p
+  toRef BExpr (HIn (InR (L (Tag (R (L (C (I x)))))))) = NotEH (toRef BExpr x)
+  toRef Stmt (HIn (Ref p)) = StmtRef p
+
+  fromRef AExpr (AExprRef p) = HIn (Ref p)
+
+-- Show existentials
+instance Show (NiceInsert AST) where
+  show (NiceInsert AExpr x l) = "NiceInsert AExpr (" ++ show x ++ ") " ++ show l
+  show (NiceInsert BExpr x l) = "NiceInsert BExpr (" ++ show x ++ ") " ++ show l
+  show (NiceInsert Stmt x l)  = "NiceInsert Stmt (" ++ show x ++ ") " ++ show l
+
+-- Actual example
+{- This prints: (note the different reference types here)
+  [ NiceInsert BExpr (NotEH (BExprRef [2,0])) [2,0]
+  , NiceInsert Stmt (StmtRef [2,2]) [2,1]
+  , NiceInsert Stmt (StmtRef [2,1]) [2,2] ]
+-}
+expl1 = print $ toNiceTransformation $ diff Stmt prog1 prog2
+expl2 = print $ toNiceTransformation $ diff Stmt prog3 prog4
+expl3 = print $ toNiceTransformation $ diff Stmt prog5 prog6

@@ -0,0 +1,212 @@+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies      #-}
+{-# LANGUAGE TemplateHaskell   #-}
+{-# LANGUAGE TypeOperators     #-}
+{-# LANGUAGE EmptyDataDecls    #-}
+module Regular where
+
+import Datatypes
+import Generics.Regular hiding (right)
+import Generics.Regular.Transformations.Explicit as Ex
+import Generics.Regular.Transformations.RewriteRules as RR
+import Generics.Regular.Zipper
+import Generics.Regular.Transformations.ZipperState
+
+import Control.Monad ( (>=>) )
+import Generics.Regular.Rewriting hiding (left, right)
+import Data.Maybe (fromJust)
+
+--------------------------------------------------------------------------------
+-- Regular representations for the example datatypes
+--------------------------------------------------------------------------------
+--Trees
+$(deriveAll ''Tree "PFTree")
+type instance PF Tree = PFTree
+
+-- Lists
+$(deriveAll ''List "PFL")
+type instance PF (List a) = PFL a
+
+-- Something more exotic
+$(deriveAll ''X "PFX")
+type instance PF X = PFX
+
+-- Example for paper (do manual instance to avoid C's)
+type instance PF Expr = K String :+: K Integer :+: I :+: I :*: I
+
+instance Regular Expr where
+  from  (Var s)       = L (K s)
+  from  (Const i)     = R (L (K i))
+  from  (Neg e)       = R (R (L (I e)))
+  from  (Add e1 e2)   = R (R (R (I e1 :*: I e2)))
+
+  to (L (K s))                    = Var s
+  to (R (L (K i)))                = Const i
+  to (R (R (L (I e))))            = Neg e
+  to (R (R (R (I e1 :*: I e2))))  = Add e1 e2
+
+
+--------------------------------------------------------------------------------
+-- Examples for the paper
+--------------------------------------------------------------------------------
+-- Some example values
+expr1 :: Expr
+expr1 = Add (Const 1) (Var "a")
+
+expr2 :: Expr
+expr2 = Add (Const 1) (Neg (Var "a"))
+
+expr3 :: Expr
+expr3 = Add (Var "a") (Const 1)
+
+instance RR.Transform Expr
+instance Ex.Transform Expr
+
+instance Show (Fix (WithRef Expr)) where
+  show (In (Ref p)) = "Ref " ++ show p
+
+-- Insertion (expr1 => expr2)
+rewriteRulesIns :: Maybe Expr
+rewriteRulesIns = RR.apply [(down >=> right, rule1)] expr1
+  where rule1 :: Rule Expr
+        rule1 = rule $ \x -> x :~> Neg x
+
+zipperStateIns :: Maybe Expr
+zipperStateIns = navigate expr1 $ do
+  downMonad >> rightMonad
+  updateMonad Neg
+
+explicitIns :: Maybe Expr
+explicitIns = Ex.apply addNeg expr1
+  where addNeg :: Ex.Transformation Expr
+        addNeg = [ ([1], In . InR . R . R . L . I . In $ Ref [1]) ]
+
+-- Deletion (expr2 => expr1)
+
+rewriteRulesDel :: Maybe Expr
+rewriteRulesDel = RR.apply [(down >=> right, rule2)] expr2
+  where rule2 :: Rule Expr
+        rule2 = rule $ \x -> Neg x :~> x
+
+zipperStateDel :: Maybe Expr
+zipperStateDel = navigate expr2 $ do
+  r <- downMonad >> rightMonad >> downMonad
+  upMonad
+  updateMonad (const r)
+
+explicitDel :: Maybe Expr
+explicitDel = Ex.apply delNeg expr2
+  where delNeg :: Ex.Transformation Expr
+        delNeg = [ ([1], In (Ref [1,0])) ]
+
+-- Swapping (expr1 => expr3)
+rewriteRulesSwap :: Maybe Expr
+rewriteRulesSwap = RR.apply [(return, rule3)] expr1
+  where rule3 :: Rule Expr
+        rule3 = rule $ \l r -> Add l r :~> Add r l
+
+zipperStateSwap :: Maybe Expr
+zipperStateSwap = navigate expr1 $ do
+  l <- downMonad
+  r <- rightMonad
+  updateMonad (const l)
+  leftMonad
+  updateMonad (const r)
+
+explicitSwap :: Maybe Expr
+explicitSwap = Ex.apply swap' expr1
+  where swap' :: Ex.Transformation Expr
+        swap' = [ ([0], In $ Ref [1]) 
+                , ([1], In $ Ref [0])]
+
+-- Rotation
+rotate1 = Add (Var "a") (Add (Var "b") (Var "c"))
+rotate2 = Add (Add (Var "a") (Var "b")) (Var "c")
+rotate = diff rotate1 rotate2
+
+--------------------------------------------------------------------------------
+-- Other RewriteRules examples
+--------------------------------------------------------------------------------
+instance RR.Transform Tree
+instance RR.Transform X
+
+-- Test swapping two subtrees. Note the nice syntax!
+swap :: Rule Tree
+swap = rule $ \t1 t2 -> Bin t1 t2 :~> Bin t2 t1
+
+t1 = RR.apply [(return        , swap)]      exTree4
+t2 = RR.apply [(down          , swap)]      exTree4
+t3 = RR.apply [(down >=> right, swap)]      exTree4
+t4 = RR.apply [(down >=> right, swap), (return, swap)] exTree4 -- == id
+
+-- A tricky example
+ruleSwapC, ruleAddB :: Rule X
+ruleSwapC = rule $ \x y -> XC x y :~> XC y x
+ruleAddB  = rule $ \x   -> XA x   :~> XA (XB x)
+
+t6 = RR.apply [(down >=> down >=> down, ruleSwapC)] exX1
+t7 = RR.apply [(down >=> down,          ruleAddB)]  (fromJust t6)
+t8 = RR.apply [(return,                 ruleAddB)]  (fromJust t7)
+t9 = t8 == Just exX2 -- True
+
+--------------------------------------------------------------------------------
+-- Other ZipperState examples
+--------------------------------------------------------------------------------
+-- An example using a zipper with state
+t5 = navigate exTree4 $
+       do downMonad >> downMonad
+          saveMonad
+          upMonad >> rightMonad >> downMonad >> rightMonad
+          saveMonad
+          x1 <- loadMonad
+          updateMonad (const x1)
+          upMonad >> leftMonad >> downMonad
+          x2 <- loadMonad
+          updateMonad (const x2)
+
+--------------------------------------------------------------------------------
+-- A nicer interface for Expr, could be generated using Template Haskell
+--------------------------------------------------------------------------------
+data ExprEH
+  = VarEH String
+  | ConstEH Integer
+  | NegEH ExprEH
+  | AddEH ExprEH ExprEH
+  | RefEH Path
+  deriving Show
+
+class HasRef a where
+  type RefRep a
+  
+  toRef   :: Fix (WithRef a) -> RefRep a
+  fromRef :: RefRep a -> Fix (WithRef a)
+
+instance HasRef Expr where
+  type RefRep Expr = ExprEH
+  
+  toRef (In (Ref p))                           = RefEH p
+  toRef (In (InR (L (K s))))                   = VarEH s
+  toRef (In (InR (R (L (K i)))))               = ConstEH i
+  toRef (In (InR (R (R (L (I e))))))           = NegEH (toRef e)
+  toRef (In (InR (R (R (R (I e1 :*: I e2)))))) = AddEH (toRef e1) (toRef e2)
+  
+  fromRef (RefEH p)     = In (Ref p)
+  fromRef (VarEH s)      = In (InR (L (K s)))
+  fromRef (ConstEH i)    = In (InR (R (L (K i))))
+  fromRef (NegEH e)      = In (InR (R (R (L (I (fromRef e))))))
+  fromRef (AddEH e1 e2)  = In (InR (R (R (R (I (fromRef e1) :*: I (fromRef e2))))))
+
+
+-- Provide the interface
+type NiceTransformation a = [ (Path, RefRep a) ] 
+
+toNiceTransformation :: HasRef a => Ex.Transformation a -> NiceTransformation a
+toNiceTransformation = map (\(p,e) -> (p, toRef e))
+
+fromNiceTransformation :: HasRef a => NiceTransformation a -> Ex.Transformation a
+fromNiceTransformation = map (\(p,e) -> (p,fromRef e))
+
+explicitInsNice :: Maybe Expr
+explicitInsNice = Ex.apply (fromNiceTransformation addNeg) expr1
+  where addNeg :: NiceTransformation Expr
+        addNeg = [ ([1], NegEH (RefEH [1])) ]

@@ -0,0 +1,53 @@+name:                transformations
+version:             0.1.0.0
+synopsis:            Generic representation of tree transformations
+description:
+  This library is based on ideas described in the paper:
+  .
+  *  Jeroen Bransen and Jose Pedro Magalhaes.
+     /Generic Representations of Tree Transformations/.
+     <http://dreixel.net/research/pdf/grtt_draft.pdf>
+
+license:             GPL-3
+license-file:        LICENSE
+author:              Jeroen Bransen and Jose Pedro Magalhaes
+maintainer:          generics@haskell.org
+-- copyright:           
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.8
+
+
+extra-source-files:    examples/Datatypes.hs
+                       examples/Lang.lhs
+                       examples/Regular.hs
+                       examples/MultiRec.hs
+
+library
+  exposed-modules:
+                       -- Regular part
+                       Generics.Regular.Zipper,
+                       Generics.Regular.Functions.GOrd,
+                       Generics.Regular.Transformations.Explicit,
+                       Generics.Regular.Transformations.RewriteRules,
+                       Generics.Regular.Transformations.ZipperState,
+  
+                       -- MultiRec implementation
+                       Generics.MultiRec.Any,
+                       Generics.MultiRec.Ord,
+                       Generics.MultiRec.Transformations.ZipperState,
+                       Generics.MultiRec.Transformations.RewriteRules,
+                       Generics.MultiRec.Transformations.Explicit,
+
+                       -- Rewriting library for MultiRec
+                       Generics.MultiRec.HZip,
+                       Generics.MultiRec.LR,
+                       Generics.MultiRec.Rewriting,
+                       Generics.MultiRec.Rewriting.Machinery,
+                       Generics.MultiRec.Rewriting.Rules
+
+  -- other-modules:       
+  build-depends:       base >= 4 && < 5, mtl >= 2.1,
+                       regular >= 0.3, rewriting >= 0.2,
+                       multirec >= 0.7.3, zipper >= 0.4.2,
+                       parsec >= 3.1, containers >= 0.1