{-# LINE 37 "MutualRec.fmt" #-}
  {-#  LANGUAGE GADTs  #-}
  {-#  LANGUAGE KindSignatures  #-}
  {-#  LANGUAGE StandaloneDeriving  #-}
  {-#  LANGUAGE TypeFamilies  #-}
  {-#  LANGUAGE TypeOperators  #-}
  {-#  LANGUAGE FlexibleContexts  #-}
  {-#  LANGUAGE EmptyDataDecls  #-}
  {-#  LANGUAGE ScopedTypeVariables  #-}
  {-#  LANGUAGE MultiParamTypeClasses  #-}
  {-#  LANGUAGE TypeSynonymInstances  #-}
  {-#  LANGUAGE Rank2Types  #-}
  {-#  LANGUAGE FlexibleInstances  #-}
{-# LINE 51 "MutualRec.fmt" #-}
  import Prelude hiding (Functor(..))
  import qualified Prelude
  import Control.Monad hiding (Functor(..))
  import Control.Monad.State hiding (Functor(..))
  --  import Data.Map as M hiding (update, fold)
  import Data.Maybe (fromJust)
  import Control.Arrow ((>>>))
  import Data.Char (toUpper)
{-# LINE 61 "MutualRec.fmt" #-}
  applyRule = undefined
{-# LINE 64 "MutualRec.fmt" #-}
  --  deriving instance Eq Prop
{-# LINE 23 "FixedPoints.lhs" #-}
  data Fix fT  =  In   { out :: (fT (Fix fT)) }
{-# LINE 30 "FixedPoints.lhs" #-}
  outsig=  out :: Fix fT -> fT (Fix fT) {-  .  -}
{-# LINE 50 "FixedPoints.lhs" #-}
  data ExprS  =  ConstS  Int  |  AddS    ExprS  ExprS  |  MulS    ExprS  ExprS
{-# LINE 54 "FixedPoints.lhs" #-}
  data PFExprS2 rT  =  ConstFS  Int  |  AddFS    rT rT  |  MulFS    rT rT
 
  type Expr'S2  =  Fix PFExprS2
{-# LINE 68 "FixedPoints.lhs" #-}
  class DRegular aT where
    dfrom  ::  aT -> Fix (PFS2 aT)
    dto    ::  Fix (PFS2 aT) -> aT
{-# LINE 74 "FixedPoints.lhs" #-}
  instance DRegular ExprS where
    dfrom (ConstS i)  = In (ConstFS i)
    dfrom (AddS e e') = In (AddFS (dfrom e) (dfrom e'))
    dfrom (MulS e e') = In (MulFS (dfrom e) (dfrom e'))
    dto (In (ConstFS i))  = ConstS i
    dto (In (AddFS e e')) = AddS (dto e) (dto e')
    dto (In (MulFS e e')) = MulS (dto e) (dto e')
{-# LINE 87 "FixedPoints.lhs" #-}
  type family PFS2 aT ::  *  ->  * 
{-# LINE 93 "FixedPoints.lhs" #-}
  type instance PFS2 ExprS = PFExprS2
{-# LINE 111 "FixedPoints.lhs" #-}
  class Regular aT where
    fromS  ::  aT -> PFS2 aT aT
    toS    ::  PFS2 aT aT -> aT
{-# LINE 117 "FixedPoints.lhs" #-}
  instance Regular ExprS where
    fromS  =  fromExprS2
    toS    =  toExpr
{-# LINE 125 "FixedPoints.lhs" #-}
  fromExprS2 (ConstS i)  = ConstFS i
  fromExprS2 (AddS e e') = AddFS e e'
  fromExprS2 (MulS e e') = MulFS e e'
  toExpr (ConstFS i)  = ConstS i
  toExpr (AddFS e e') = AddS e e'
  toExpr (MulFS e e') = MulS e e'
{-# LINE 137 "FixedPoints.lhs" #-}
  instance Functor PFExprS2 where
    fmap f (ConstFS i)   =  ConstFS i
    fmap f (AddFS e e')  =  AddFS (f e) (f e')
    fmap f (MulFS e e')  =  MulFS (f e) (f e')
{-# LINE 145 "FixedPoints.lhs" #-}
  foldS ::  (Regular aT, Functor (PFS2 aT)) =>
           (PFS2 aT rT -> rT) -> (aT -> rT)
  foldS f = f . fmap (foldS f) . fromS
 
  unfoldS ::  (Regular aT, Functor (PFS2 aT)) =>
             (rT -> PFS2 aT rT) -> (rT -> aT)
  unfoldS f = toS . fmap (unfoldS f) . f
{-# LINE 163 "FixedPoints.lhs" #-}
  deepFrom :: (Regular aT, Functor (PFS2 aT)) => aT -> Fix (PFS2 aT)
  deepFrom = foldS In
 
  deepTo :: (Regular aT, Functor (PFS2 aT)) => Fix (PFS2 aT) -> aT
  deepTo = unfoldS out
{-# LINE 178 "FixedPoints.lhs" #-}
  composS :: (Regular aT, Functor (PFS2 aT)) => (aT -> aT) -> aT -> aT
  composS f = toS . fmap f . fromS
{-# LINE 198 "FixedPoints.lhs" #-}
  data KS aT         rT  =  K_ aT
  data IdS           rT  =  Id_ rT
  data (fT `TimesS` gT)  rT  =  fT rT `TimesS` gT rT
  data (fT `PlusS` gT)  rT  =  LS (fT rT) | RS (gT rT)
 
  infixr 7 `TimesS`
  infixr 6 `PlusS`
{-# LINE 215 "FixedPoints.lhs" #-}
  type PFExpr  =  KS Int  `PlusS`  (IdS `TimesS` IdS  )  `PlusS`  (IdS `TimesS` IdS  ) 
 
  type Expr'S   =  Fix PFExpr
{-# LINE 221 "FixedPoints.lhs" #-}
  type family PFS aT ::  *  ->  * 
  type instance PFS ExprS = PFExpr
{-# LINE 232 "FixedPoints.lhs" #-}
  class Functor fT where
    fmap :: (aT -> bT) -> fT aT -> fT bT
  
  instance Functor IdS where
    fmap f (Id_ x) = Id_ (f x)
  
  instance Functor (KS aT) where
    fmap _ (K_ x) = K_ x
 
  instance (Functor fT, Functor gT) => Functor (fT `PlusS` gT) where
    fmap f (LS x)  = LS (fmap f x)
    fmap f (RS y)  = RS (fmap f y)
  
  instance (Functor fT, Functor gT) => Functor (fT `TimesS` gT) where
    fmap f (x `TimesS` y) = fmap f x `TimesS` fmap f y
{-# LINE 271 "FixedPoints.lhs" #-}
  dfromExpr' :: ExprS -> PFS ExprS ExprS
  dfromExpr' (ConstS i)   =  LS     (K_ i)
  dfromExpr' (AddS e e')  =  RS (LS  (Id_ e `TimesS` Id_ e'))
  dfromExpr' (MulS e e')  =  RS (RS  (Id_ e `TimesS` Id_ e'))
{-# LINE 15 "MultiTypes.lhs" #-}
  data ExprM   =  ConstM  Int
              |  AddM    ExprM  ExprM
              |  MulM    ExprM  ExprM
              |  EVarM   Var
              |  LetM    DeclM  ExprM
 
  data DeclM   =  Var := ExprM
              |  Seq    DeclM  DeclM
 
  type Var    =  String
{-# LINE 28 "MultiTypes.lhs" #-}
  deriving instance Show ExprM
  deriving instance Show DeclM
  deriving instance Eq ExprM
  deriving instance Eq DeclM
{-# LINE 56 "MultiTypes.lhs" #-}
  data Fix_2 fT gT = In_2 (fT (Fix_2 fT gT) (Fix_2 gT fT))
{-# LINE 167 "MultiTypes.lhs" #-}
  data HFix (fT :: ( *   ->  * ) -> ( *   ->  * )) (ixT ::  *  ) =
    HIn (fT (HFix fT) ixT)
{-# LINE 182 "MultiTypes.lhs" #-}
  data ASTM ::  *   ->  *  where
    Expr_  ::  ASTM ExprM
    Decl_  ::  ASTM DeclM
    Var_   ::  ASTM Var
{-# LINE 195 "MultiTypes.lhs" #-}
  class HFunctor  (phi ::  *   ->  * )
                  (fT :: ( *   ->  * ) -> ( *   ->  * )) where
    hmap :: (forall (ixT ::  *  ). phi ixT -> rT ixT -> rT' ixT) -> (fT rT ixT -> fT rT' ixT)
{-# LINE 212 "MultiTypes.lhs" #-}
  class El (phi ::  *   ->  * ) (ixT ::  *  ) where
    proof :: phi ixT
{-# LINE 220 "MultiTypes.lhs" #-}
  instance El ASTM ExprM  where proof = Expr_
  instance El ASTM DeclM  where proof = Decl_
  instance El ASTM Var   where proof = Var_
{-# LINE 245 "MultiTypes.lhs" #-}
  data PFASTManual :: ( *   ->  * ) -> ( *   ->  * ) where
 
    ConstF     ::  Int                 ->  PFASTManual rT ExprM
    AddF       ::  rT ExprM -> rT ExprM  ->  PFASTManual rT ExprM
    MulF       ::  rT ExprM -> rT ExprM  ->  PFASTManual rT ExprM
    EVarF      ::  rT Var              ->  PFASTManual rT ExprM
    LetF       ::  rT DeclM -> rT ExprM  ->  PFASTManual rT ExprM
 
    BindF      ::  rT Var -> rT ExprM   ->  PFASTManual rT DeclM
    SeqF       ::  rT DeclM -> rT DeclM  ->  PFASTManual rT DeclM
 
    VF         ::  String              ->  PFASTManual rT Var
{-# LINE 267 "MultiTypes.lhs" #-}
  type Expr'  =  HFix PFASTManual ExprM
  type Decl'  =  HFix PFASTManual DeclM
  type Var'   =  HFix PFASTManual Var
{-# LINE 276 "MultiTypes.lhs" #-}
  class FamilyManual phi where
    fromManual   ::  phi ixT -> ixT -> PFManual phi I ixT
    toManual     ::  phi ixT -> PFManual phi I ixT -> ixT
 
  type family PFManual (phi ::  *   ->  * ) :: ( *   ->  * ) -> ( *   ->  * )
{-# LINE 298 "MultiTypes.lhs" #-}
  data I (ixT ::  *  ) = I_ { unI :: ixT }
{-# LINE 310 "MultiTypes.lhs" #-}
  type instance PFManual ASTM = PFASTManual
 
  instance FamilyManual ASTM where
    fromManual  =  fromASTManual
    toManual    =  toASTManual
{-# LINE 320 "MultiTypes.lhs" #-}
  fromASTManual :: ASTM ixT -> ixT -> PFManual ASTM I ixT
  fromASTManual Expr_ (ConstM i)  = ConstF i
  fromASTManual Expr_ (AddM e e') = AddF (I_ e) (I_ e')
  fromASTManual Expr_ (MulM e e') = MulF (I_ e) (I_ e')
  fromASTManual Expr_ (EVarM x)   = EVarF (I_ x)
  fromASTManual Expr_ (LetM d e)  = LetF (I_ d) (I_ e)
  fromASTManual Decl_ (x := e)   = BindF (I_ x) (I_ e)
  fromASTManual Decl_ (Seq d d') = SeqF (I_ d) (I_ d')
  fromASTManual Var_  x          = VF x
 
  toASTManual :: ASTM ixT -> PFManual ASTM I ixT -> ixT
  toASTManual Expr_ (ConstF i)  = ConstM i
  toASTManual Expr_ (AddF (I_ e) (I_ e')) = AddM e e'
  toASTManual Expr_ (MulF (I_ e) (I_ e')) = MulM e e'
  toASTManual Expr_ (EVarF (I_ x))        = EVarM x
  toASTManual Expr_ (LetF (I_ d) (I_ e))  = LetM d e
  toASTManual Decl_ (BindF (I_ x) (I_ e)) = x := e
  toASTManual Decl_ (SeqF (I_ d) (I_ d')) = Seq d d'
  toASTManual Var_  (VF x)                = x
{-# LINE 365 "MultiTypes.lhs" #-}
  infixr 5  `PlusM`
  infixr 7  `TimesM`
{-# LINE 370 "MultiTypes.lhs" #-}
  data KM aT         (rT ::  *   ->  * ) (ixT ::  *  )   =  K_M aT
  data (fT `PlusM` gT)  (rT ::  *   ->  * ) (ixT ::  *  )   =  LM (fT rT ixT) | RM (gT rT ixT)
  data (fT `TimesM` gT)  (rT ::  *   ->  * ) (ixT ::  *  )   =  fT rT ixT `TimesM` gT rT ixT
{-# LINE 379 "MultiTypes.lhs" #-}
  data IdM (ixrT ::  *  ) (rT ::  *   ->  * ) (ixT ::  *  )   =  Id_M (rT ixrT)
{-# LINE 393 "MultiTypes.lhs" #-}
  infix  6 `TagM`
 
  data (fT `TagM` (ixtT ::  *  )) (rT ::  *   ->  * ) (ixT ::  *  ) where
    TagM :: fT rT ixT -> (fT `TagM` ixT) rT ixT
{-# LINE 405 "MultiTypes.lhs" #-}
  type PFAST  =  KM Int                  `TagM`  ExprM  `PlusM`  --  |Const|
                 (IdM ExprM `TimesM` IdM ExprM)  `TagM`  ExprM  `PlusM`  --  |Add|
                 (IdM ExprM `TimesM` IdM ExprM)  `TagM`  ExprM  `PlusM`  --  |Mul|
                 IdM Var                 `TagM`  ExprM  `PlusM`  --  |EVar|
                 (IdM DeclM `TimesM` IdM ExprM)  `TagM`  ExprM  `PlusM`  --  |Let|
                 (IdM Var `TimesM` IdM ExprM)   `TagM`  DeclM  `PlusM`  --  |:=|
                 (IdM DeclM `TimesM` IdM DeclM)  `TagM`  DeclM  `PlusM`  --  |Seq|
                 KM String               `TagM`  Var        --  |V|
{-# LINE 420 "MultiTypes.lhs" #-}
  class Family phi where
    fromM   ::  forall (ixT ::  *  ) . phi ixT -> ixT -> PF phi I ixT
    toM     ::  forall (ixT ::  *  ) . phi ixT -> PF phi I ixT -> ixT
 
  type family PF (phi ::  *   ->  * ) :: ( *   ->  * ) -> ( *   ->  * )
 
  type instance PF ASTM = PFAST
  
  instance Family ASTM where
    fromM = fromAST
    toM   = toAST
{-# LINE 438 "MultiTypes.lhs" #-}
  fromAST :: ASTM ixT -> ixT -> PFAST I ixT
  fromAST Expr_  (ConstM i)     =
    LM                     (TagM (K_M i))
  fromAST Expr_  (AddM  e e')   =
    RM (LM                  (TagM (ci e `TimesM` ci e')))
  fromAST Expr_  (MulM  e e')   =
    RM (RM (LM               (TagM (ci e `TimesM` ci e'))))
  fromAST Expr_  (EVarM x)      =
    RM (RM (RM (LM            (TagM (ci x)))))
  fromAST Expr_  (LetM d e)     =
    RM (RM (RM (RM (LM         (TagM (ci d `TimesM` ci e))))))
  fromAST Decl_  (x := e)      =
    RM (RM (RM (RM (RM (LM      (TagM (ci x `TimesM` ci e)))))))
  fromAST Decl_  (Seq d d')    =
    RM (RM (RM (RM (RM (RM (LM   (TagM (ci d `TimesM` ci d'))))))))
  fromAST Var_   x             =
    RM (RM (RM (RM (RM (RM (RM   (TagM (K_M x))))))))
 
  ci x = Id_M (I_ x)
{-# LINE 460 "MultiTypes.lhs" #-}
  toAST :: ASTM ixT -> PFAST I ixT -> ixT
  toAST Expr_  (LM                     (TagM (K_M i))           )   =   (ConstM i)
  toAST Expr_  (RM (LM                  (TagM (e `TimesM` e')))     )   =   (AddM  (di e) (di e'))
  toAST Expr_  (RM (RM (LM               (TagM (e `TimesM` e'))))    )   =   (MulM  (di e) (di e'))
  toAST Expr_  (RM (RM (RM (LM            (TagM (x)))))           )   =   (EVarM (di x))
  toAST Expr_  (RM (RM (RM (RM (LM         (TagM (d `TimesM` e))))))   )   =   (LetM (di d) (di e))
  toAST Decl_  (RM (RM (RM (RM (RM (LM      (TagM (x `TimesM` e)))))))  )   =   ((di x) := (di e))
  toAST Decl_  (RM (RM (RM (RM (RM (RM (LM   (TagM (d `TimesM` d')))))))))   =   (Seq (di d) (di d'))
  toAST Var_   (RM (RM (RM (RM (RM (RM (RM   (TagM (K_M x))))))))     )   =   x
 
  di (Id_M (I_ x)) = x
{-# LINE 479 "MultiTypes.lhs" #-}
  instance El phi ixtT => HFunctor phi (IdM ixtT) where
    hmap f (Id_M x) = Id_M (f proof x)
 
  instance HFunctor phi (KM aT) where
    hmap f (K_M x) = K_M x
 
  instance  (HFunctor phi fT, HFunctor phi gT) =>
            HFunctor phi (fT `PlusM` gT) where
    hmap f (LM x)  =  LM (hmap f x)
    hmap f (RM y)  =  RM (hmap f y)
 
  instance  (HFunctor phi fT, HFunctor phi gT) =>
            HFunctor phi (fT `TimesM` gT) where
    hmap f (x `TimesM` y) = hmap f x `TimesM` hmap f y
 
  instance HFunctor phi fT => HFunctor phi (fT `TagM` ixT) where
    hmap f (TagM x) = TagM (hmap f x)
{-# LINE 11 "RecursionSchemes.lhs" #-}
  compos ::  (Family phi, HFunctor phi (PF phi)) =>
             (forall ixT. phi ixT -> ixT -> ixT) -> phi ixT -> ixT -> ixT
  compos f p = toM p . hmap (\ p -> I_ . f p . unI) . fromM p
{-# LINE 2 "Example.lhs" #-}
  example = LetM  ("x" := MulM (ConstM 6) (ConstM 9))
                 (AddM (EVarM "x") (EVarM "y"))
{-# LINE 34 "RecursionSchemes.lhs" #-}
  renameVar :: ExprM -> ExprM
  renameVar = renameVar' Expr_
    where
      renameVar' :: ASTM aT -> aT -> aT
      renameVar' Var_  x = x ++ "_"
      renameVar' p     x = compos renameVar' p x
{-# LINE 43 "RecursionSchemes.lhs" #-}
  test_renameVar =LetM  ("x_" := MulM (ConstM 6) (ConstM 9))
                        (AddM (EVarM "x_") (EVarM "y_"))== renameVar example
{-# LINE 51 "RecursionSchemes.lhs" #-}
  type Algebra phi rT = forall ixT. phi ixT -> PF phi rT ixT -> rT ixT
 
  fold ::  (Family phi, HFunctor phi (PF phi)) =>
           Algebra phi rT -> phi ixT -> ixT -> rT ixT
  fold f p = f p . hmap (\ p (I_ x) -> fold f p x) . fromM p
{-# LINE 77 "RecursionSchemes.lhs" #-}
  type family Alg  (fT :: ( *   ->  * ) ->  *   ->  * )
                   (rT ::  *   ->  * ) (ixT ::  * ) ::  * 
 
  type instance Alg (KM aT)            rT ixT  =  aT -> rT ixT
  type instance Alg (IdM ixtT)         rT ixT  =  rT ixtT -> rT ixT
  type instance Alg (fT `PlusM` gT)       rT ixT  =  (Alg fT rT ixT, Alg gT rT ixT)
  type instance Alg (KM aT `TimesM` gT)     rT ixT  =  aT -> Alg gT rT ixT
  type instance Alg (IdM ixtT `TimesM` gT)  rT ixT  =  rT ixtT -> Alg gT rT ixT
  type instance Alg (fT `TagM` ixtT)     rT ixT  =  Alg fT rT ixtT
{-# LINE 100 "RecursionSchemes.lhs" #-}
  class Apply (fT :: ( *   ->  * ) ->  *   ->  * ) where
    apply  :: Alg fT rT ixT -> fT rT ixT -> rT ixT
 
  instance Apply (KM a) where
    apply  f (K_M x) = f x
 
  instance Apply (IdM xi) where
    apply  f (Id_M x) = f x
 
  instance (Apply f, Apply g) => Apply (f `PlusM` g) where
    apply  (f,g) (LM x) = apply f x
    apply  (f,g) (RM x) = apply g x
 
  instance Apply g => Apply (KM a `TimesM` g) where
    apply f (K_M x `TimesM` y) = apply (f x) y 
 
  instance Apply g => Apply (IdM xi `TimesM` g) where
    apply f (Id_M x `TimesM` y) = apply (f x) y
 
  instance Apply f => Apply (f `TagM` xi) where
    apply f (TagM x) = apply f x
{-# LINE 125 "RecursionSchemes.lhs" #-}
  infixr 1 &
  (&) = (,)
{-# LINE 145 "RecursionSchemes.lhs" #-}
  data family Value aT ::  * 
  data instance Value ExprM  =  EV  (Env -> Int)
  data instance Value DeclM  =  DV  (Env -> Env)
  data instance Value Var   =  VV  Var
 
  type Env = [(Var, Int)]
{-# LINE 164 "RecursionSchemes.lhs" #-}
  evalAlg :: Algebra ASTM Value
  evalAlg = const (apply
    (  (\ x              ->  EV (const x))              --  |Const|
    &  (\ (EV x) (EV y)  ->  EV (\ m -> x m + y m))     --  |Add|
    &  (\ (EV x) (EV y)  ->  EV (\ m -> x m  *  y m))     --  |Mul|
    &  (\ (VV x)         ->  EV (fromJust . lookup x))  --  |EVar|
    &  (\ (DV e) (EV x)  ->  EV (\ m -> x (e m)))       --  |Let|
    &  (\ (VV x) (EV v)  ->  DV (\ m -> (x, v m) : m))  --  |:=|
    &  (\ (DV f) (DV g)  ->  DV (g . f))                --  |Seq|
    &  (\ x              ->  VV x)))                    --  |V|
{-# LINE 179 "RecursionSchemes.lhs" #-}
  eval :: ExprM -> Env -> Int
  eval x = let (EV f) = fold evalAlg Expr_ x in f
{-# LINE 186 "RecursionSchemes.lhs" #-}
  evalexample=  eval example [("y", -12)]
{-# LINE 190 "RecursionSchemes.lhs" #-}
  test_evalexample =42==evalexample {- . -}
{-# LINE 47 "Zipper.lhs" #-}
  data LocAST ::  *   ->  *  where
    LocAST :: ASTM ixT -> ixT -> CtxsAST aT ixT -> LocAST aT
{-# LINE 54 "Zipper.lhs" #-}
  data CtxsAST ::  *   ->  *   ->  *  where
    NilAST    ::  CtxsAST aT aT
    ConsAST   ::  CtxAST ixT bT -> CtxsAST aT ixT -> CtxsAST aT bT 
{-# LINE 75 "Zipper.lhs" #-}
  data CtxAST ::  *   ->  *   ->  *  where
    
    AddC1      ::  ExprM  ->  CtxAST ExprM  ExprM
    AddC2      ::  ExprM  ->  CtxAST ExprM  ExprM
    MulC1      ::  ExprM  ->  CtxAST ExprM  ExprM
    MulC2      ::  ExprM  ->  CtxAST ExprM  ExprM
    EVarC      ::            CtxAST ExprM  Var
    LetC1      ::  ExprM  ->  CtxAST ExprM  DeclM
    LetC2      ::  DeclM  ->  CtxAST ExprM  ExprM
 
    BindC1     ::  ExprM  ->  CtxAST DeclM  Var
    BindC2     ::  Var   ->  CtxAST DeclM  ExprM
    SeqC1      ::  DeclM  ->  CtxAST DeclM  DeclM
    SeqC2      ::  DeclM  ->  CtxAST DeclM  DeclM
{-# LINE 100 "Zipper.lhs" #-}
  con1=   LetM    ::      DeclM  ->     ExprM  ->           ExprM
{-# LINE 114 "Zipper.lhs" #-}
  con2=   LetF   ::  rT  DeclM  -> rT  ExprM  -> PFASTManual rT  ExprM
{-# LINE 122 "Zipper.lhs" #-}
  con3=   LetC1  ::  ExprM -> CtxAST ExprM DeclM
{-# LINE 127 "Zipper.lhs" #-}
  con4=   LetC2  ::  DeclM -> CtxAST ExprM ExprM
{-# LINE 142 "Zipper.lhs" #-}
  downAST :: LocAST ixT -> Maybe (LocAST ixT)
 
  downAST (LocAST Expr_  (AddM  e e')   cs)  =
     Just (LocAST Expr_  e   (ConsAST (AddC1 e')  cs))
  downAST (LocAST Expr_  (MulM  e e')   cs)  =
     Just (LocAST Expr_  e   (ConsAST (MulC1 e')  cs))
  downAST (LocAST Expr_  (EVarM x)      cs)  =
     Just (LocAST Var_   x   (ConsAST EVarC       cs))
  downAST (LocAST Expr_  (LetM d e)     cs)  =
     Just (LocAST Decl_  d   (ConsAST (LetC1 e)   cs))
 
  downAST (LocAST Decl_  (x := e)      cs)  =
     Just (LocAST Var_   x   (ConsAST (BindC1 e)  cs))
  downAST (LocAST Decl_  (Seq d d')    cs)  =
     Just (LocAST Decl_  d   (ConsAST (SeqC1 d')  cs))
 
  downAST _                               =  Nothing
{-# LINE 164 "Zipper.lhs" #-}
  rightAST :: LocAST ixT -> Maybe (LocAST ixT)
 
  rightAST (LocAST _ e   (ConsAST (AddC1  e')   cs))     =
    Just (LocAST Expr_  e'  (ConsAST (AddC2 e)    cs))
  rightAST (LocAST _ e   (ConsAST (MulC1  e')   cs))     =
    Just (LocAST Expr_  e'  (ConsAST (MulC2 e)    cs))
  rightAST (LocAST _ d   (ConsAST (LetC1 e)     cs))     =
    Just (LocAST Expr_  e   (ConsAST (LetC2 d)    cs))
 
  rightAST (LocAST _ x   (ConsAST (BindC1 e)    cs))     =
    Just (LocAST Expr_  e   (ConsAST (BindC2 x)   cs))
  rightAST (LocAST _ d   (ConsAST (SeqC1 d')    cs))     =
    Just (LocAST Decl_  d'  (ConsAST (SeqC2 d)    cs))
 
  rightAST _                                        =  Nothing
{-# LINE 189 "Zipper.lhs" #-}
  upAST :: LocAST ixT -> Maybe (LocAST ixT)
  upAST    (LocAST _ e   (ConsAST (AddC1  e')  cs))     =  Just (LocAST Expr_  (AddM  e e')    cs)
  upAST    (LocAST _ e'  (ConsAST (AddC2  e)   cs))     =  Just (LocAST Expr_  (AddM  e e')    cs)
  upAST    (LocAST _ e   (ConsAST (MulC1  e')  cs))     =  Just (LocAST Expr_  (MulM  e e')    cs)
  upAST    (LocAST _ e'  (ConsAST (MulC2  e)   cs))     =  Just (LocAST Expr_  (MulM  e e')    cs)
  upAST    (LocAST _ x   (ConsAST EVarC        cs))     =  Just (LocAST Expr_  (EVarM x)       cs)
  upAST    (LocAST _ d   (ConsAST (LetC1 e)    cs))     =  Just (LocAST Expr_  (LetM d e)      cs)
  upAST    (LocAST _ e   (ConsAST (LetC2 d)    cs))     =  Just (LocAST Expr_  (LetM d e)      cs)
 
  upAST    (LocAST _ x   (ConsAST (BindC1 e)   cs))     =  Just (LocAST Decl_  (x := e)       cs)
  upAST    (LocAST _ e   (ConsAST (BindC2 x)   cs))     =  Just (LocAST Decl_  (x := e)       cs)
  upAST    (LocAST _ d   (ConsAST (SeqC1 d')   cs))     =  Just (LocAST Decl_  (Seq d d')     cs)
  upAST    (LocAST _ d'  (ConsAST (SeqC2 d)    cs))     =  Just (LocAST Decl_  (Seq d d')     cs)
 
  upAST    _                                       =  Nothing
{-# LINE 215 "Zipper.lhs" #-}
  enterAST :: ASTM ixT -> ixT -> LocAST ixT
  enterAST p e = LocAST p e NilAST
{-# LINE 221 "Zipper.lhs" #-}
  leaveAST :: LocAST ExprM -> ExprM
  leaveAST (LocAST _ e NilAST)        =  e
  leaveAST loc                   =  leaveAST (fromJust (upAST loc))
{-# LINE 229 "Zipper.lhs" #-}
  updateAST ::  (forall ixT . ASTM ixT -> ixT -> ixT) -> 
             LocAST ExprM -> LocAST ExprM
  updateAST f (LocAST p x cs) = LocAST p (f p x) cs
{-# LINE 243 "Zipper.lhs" #-}
  typebcomp=  (>>>) :: (aT -> bT) -> (bT -> cT) -> (aT -> cT)
{-# LINE 249 "Zipper.lhs" #-}
  typemcomp :: Monad mT => (aT -> mT bT) -> (bT -> mT cT) -> (aT -> mT cT)
{-# LINE 253 "Zipper.lhs" #-}
  typemcomp=  (>=>) :: Monad mT => (aT -> mT bT) -> (bT -> mT cT) -> (aT -> mT cT) {- . -}
{-# LINE 259 "Zipper.lhs" #-}
  demoupdate=   enterAST Expr_ >>> downAST >=> downAST >=> rightAST >=> updateAST solve >>> 
                      leaveAST >>> return $ example
{-# LINE 267 "Zipper.lhs" #-}
  solve :: ASTM ixT -> ixT -> ixT
  solve Expr_  _  =  ConstM 42
  solve _      x  =  x
{-# LINE 274 "Zipper.lhs" #-}
  test_demoupdate =Just (LetM ("x" := ConstM 42) (AddM (EVarM "x") (EVarM "y")))==demoupdate 
{-# LINE 291 "Zipper.lhs" #-}
  data Loc :: ( *   ->  * ) ->  *   ->  *  where
    Loc_ ::  (Family phi, Zipper phi (PF phi)) =>
             phi ixT -> ixT -> Ctxs phi aT ixT -> Loc phi aT
 
  data Ctxs :: ( *   ->  * ) ->  *   ->  *   ->  *  where
    Nil   ::  Ctxs phi aT aT
    Cons  ::  phi ixT -> Ctx (PF phi) ixT bT -> Ctxs phi aT ixT -> Ctxs phi aT bT
{-# LINE 315 "Zipper.lhs" #-}
  data family Ctx fT ::  *   ->  *   ->  * 
{-# LINE 324 "Zipper.lhs" #-}
  data instance Ctx (KM aT)       ixT bT  =  CK Void
  data instance Ctx (fT `PlusM` gT)  ixT bT  =  CL  (Ctx fT  ixT bT)
                                         |  CR  (Ctx gT  ixT bT)
  data instance Ctx (fT `TimesM` gT)  ixT bT  =  C1  (Ctx fT  ixT bT) (gT I ixT)
                                         |  C2  (fT I ixT) (Ctx gT ixT bT)
{-# LINE 333 "Zipper.lhs" #-}
  data Void
{-# LINE 355 "Zipper.lhs" #-}
  data (:=:) ::  *  ->  *  ->  *  where
    Refl :: aT :=: aT
{-# LINE 359 "Zipper.lhs" #-}
  data instance Ctx (IdM xiT)      ixT bT  =  CId   (bT :=: xiT)
  data instance Ctx (fT `TagM` xiT)  ixT bT  =  CTag  (ixT :=: xiT)
                                                   (Ctx fT ixT bT)
{-# LINE 6 "ZipperClass.lhs" #-}
  class Zipper phi fT where
    
{-# LINE 2 "ZipperFirst.lhs" #-}
    first  ::  (forall bT. phi bT -> bT -> Ctx fT ixT bT -> aT) ->
               fT I ixT -> Maybe aT
{-# LINE 2 "ZipperFill.lhs" #-}
    fill   ::  phi bT -> bT -> Ctx fT ixT bT -> fT I ixT
{-# LINE 2 "ZipperNext.lhs" #-}
    next  ::  (forall bT. phi bT -> bT -> Ctx fT ixT bT -> aT) ->
              (phi bT -> bT -> Ctx fT ixT bT -> Maybe aT)
{-# LINE 409 "Zipper.lhs" #-}
  down :: Loc phi ixT -> Maybe (Loc phi ixT)
  down (Loc_ p x cs) =
    first (\ p' z c -> Loc_ p' z (Cons p c cs)) (fromM p x)
{-# LINE 6 "ZipperInstanceK.lhs" #-}
  instance Zipper phi (KM aT) where
    
{-# LINE 2 "ZipperFirstK.lhs" #-}
    first f (K_M a)       = Nothing
{-# LINE 2 "ZipperFillK.lhs" #-}
    fill p x (CK void) = impossible void
{-# LINE 2 "ZipperNextK.lhs" #-}
    next f p x (CK void) = impossible void
{-# LINE 6 "ZipperInstanceSum.lhs" #-}
  instance (Zipper phi fT, Zipper phi gT) => Zipper phi (fT `PlusM` gT) where
    
{-# LINE 2 "ZipperFirstSum.lhs" #-}
    first f (LM x)              = first (\ p z c -> f p z (CL c))  x
    first f (RM y)              = first (\ p z c -> f p z (CR c))  y
{-# LINE 2 "ZipperFillSum.lhs" #-}
    fill p x (CL  c)  =  LM  (fill p x c)
    fill p x (CR  c)  =  RM  (fill p x c)
{-# LINE 2 "ZipperNextSum.lhs" #-}
    next f p x  (CL c)            =  next (\ p z c -> f p z (CL c)) p x  c
    next f p y  (CR c)            =  next (\ p z c -> f p z (CR c)) p y  c
{-# LINE 6 "ZipperInstanceProd.lhs" #-}
  instance (Zipper phi fT, Zipper phi gT) => Zipper phi (fT `TimesM` gT) where
    
{-# LINE 5 "ZipperFirstProd.lhs" #-}
    first f (x `TimesM` y) =  first (\ p z c -> f p z (C1  c  y))  x
                 `mplus`  first (\ p z c -> f p z (C2  x  c))  y
{-# LINE 2 "ZipperFillProd.lhs" #-}
    fill p x  (C1  c  y)  =  fill p x c `TimesM` y
    fill p y  (C2  x  c)  =  x `TimesM` fill p y c
{-# LINE 5 "ZipperNextProd.lhs" #-}
    next f p x  (C1 c y)         =  
               next   (\ p' z c' -> f p' z (C1  c'            y   ))   p  x  c
       `mplus`  first  (\ p' z c' -> f p' z (C2  (fill p x c)  c'  ))      y
    next f p y  (C2 x c)         =  
                next   (\ p' z c' -> f p' z (C2  x             c'  ))   p  y  c
{-# LINE 6 "ZipperInstanceId.lhs" #-}
  instance El phi xiT => Zipper phi (IdM xiT) where
    
{-# LINE 7 "ZipperFirstId.lhs" #-}
    first f (Id_M (I_ x))  =  return (f proof x (CId Refl))
{-# LINE 9 "ZipperFillId.lhs" #-}
    fill p x  (CId refl)  =  castId refl (\ x ->  Id_M (I_ x)) x
{-# LINE 2 "ZipperNextId.lhs" #-}
    next f p x (CId refl)  =  Nothing
{-# LINE 6 "ZipperInstanceTag.lhs" #-}
  instance Zipper phi fT => Zipper phi (fT `TagM` xiT) where
    
{-# LINE 2 "ZipperFirstTag.lhs" #-}
    first f (TagM x)        = first (\ p z c -> f p z (CTag Refl c)) x
{-# LINE 9 "ZipperFillTag.lhs" #-}
    fill p x  (CTag refl c)  =  castTag refl  TagM (fill p x c) 
{-# LINE 2 "ZipperNextTag.lhs" #-}
    next f p x (CTag refl c)  =  next (\ p z c' -> f p z (CTag refl c')) p x c
{-# LINE 503 "Zipper.lhs" #-}
  up :: Loc phi ixT -> Maybe (Loc phi ixT)
  up (Loc_ p x Nil)             =  Nothing
  up (Loc_ p x (Cons p' c cs))  =  Just (Loc_ p' (toM p' (fill p x c)) cs)
{-# LINE 526 "Zipper.lhs" #-}
  impossible :: Void -> aT
  impossible void = error "impossible"
{-# LINE 542 "Zipper.lhs" #-}
  castId  :: (bT :=: xiT)
          -> (xiT -> IdM xiT I ixT)
          -> (bT  -> IdM xiT I ixT)
  castId  Refl f = f
{-# LINE 550 "Zipper.lhs" #-}
  castTag  :: (ixT :=: xiT)
           -> (fT I ixT -> (f `TagM` ixT) I ixT)
           -> (fT I ixT -> (f `TagM` xiT) I ixT)
  castTag  Refl f = f
{-# LINE 573 "Zipper.lhs" #-}
  right :: Loc phi ixT -> Maybe (Loc phi ixT)
  right (Loc_ p x Nil)             =  Nothing
  right (Loc_ p x (Cons p' c cs))  = 
    next (\ p z c' -> Loc_ p z (Cons p' c' cs)) p x c
{-# LINE 609 "Zipper.lhs" #-}
  enter :: (Family phi, Zipper phi (PF phi)) => phi ixT -> ixT -> Loc phi ixT
  enter p x = Loc_ p x Nil 
 
  leave :: Loc phi ixT -> ixT
  leave (Loc_ p x Nil)        =  x
  leave loc                   =  leave (fromJust (up loc))
 
  update ::  (forall ixT . phi ixT -> ixT -> ixT) -> Loc phi ixT -> Loc phi ixT
  update f (Loc_ p x cs) = Loc_ p (f p x) cs
{-# LINE 623 "Zipper.lhs" #-}
  demoupdateg=   enter Expr_ >>> down >=> down >=> right >=> update solve>>> 
                       leave >>> return $ example
{-# LINE 632 "Zipper.lhs" #-}
  test_demoupdateg =Just (LetM ("x" := ConstM 42) (AddM (EVarM "x") (EVarM "y")))==demoupdateg 
{-# LINE 43 "GenericRewriting.lhs" #-}
  data ExprSch  =  MVar_    String       |  ConstSch   Int
              |  AddSch     ExprSch ExprSch  |  MulSch     ExprSch ExprSch
 
  matchS :: ExprSch -> ExprS -> Maybe [(String, ExprS)]
{-# LINE 50 "GenericRewriting.lhs" #-}
  matchS _ _ = Just [("x", ConstS 6), ("y", ConstS 9)]
{-# LINE 53 "GenericRewriting.lhs" #-}
  deriving instance Eq ExprS
  deriving instance Show ExprS
{-# LINE 59 "GenericRewriting.lhs" #-}
  matchexample=   matchS  (MulSch (MVar_ "x") (MVar_ "y"))
                                (MulS (ConstS 6) (ConstS 9))
{-# LINE 66 "GenericRewriting.lhs" #-}
  test_matchexample =Just [("x",ConstS 6),("y",ConstS 9)]==matchexample {-  .  -}
{-# LINE 77 "GenericRewriting.lhs" #-}
  type SchemeOfS aT = Fix (KS String `PlusS` PFS aT)
{-# LINE 83 "GenericRewriting.lhs" #-}
  schemeexample :: SchemeOfS ExprS
{-# LINE 87 "GenericRewriting.lhs" #-}
  schemeexample=  In (RS (RS (RS (Id_ (In (LS (K_ "x")))`TimesS`Id_ (In (LS (K_ "y")))))))
{-# LINE 108 "GenericRewriting.lhs" #-}
  type SchemeOf phi  = HFix (KM String `PlusM` PF phi)
{-# LINE 121 "GenericRewriting.lhs" #-}
  data DynIx phi  =  forall ixT . DynIx (phi ixT) ixT
  type Subst phi  =  [(String,DynIx phi)]
{-# LINE 135 "GenericRewriting.lhs" #-}
  from'' x = fromM x
{-# LINE 151 "GenericRewriting.lhs" #-}
  type MatchM sT aT = StateT (Subst sT) Maybe aT
 
  matchM ::  (Family phi, HZip phi (PF phi)) => phi ixT ->
             SchemeOf phi ixT -> I ixT -> MatchM phi ()
  matchM p (HIn (LM (K_M mvar))) (I_ e)
     =  do  subst <- get
            case Prelude.lookup mvar subst of
              Nothing     -> put ((mvar,DynIx p e) : subst)
              Just _      -> fail ("repeated use: " ++ mvar)
  matchM p (HIn (RM r)) (I_ e) 
     =  combine matchM r (from'' p e)
{-# LINE 182 "GenericRewriting.lhs" #-}
  matchexpr1=  MulM (ConstM 6) (ConstM 9)
{-# LINE 190 "GenericRewriting.lhs" #-}
  matchexpr2=  MulSch (MVar_ "x") (MVar_ "y") {-  .  -}
{-# LINE 202 "GenericRewriting.lhs" #-}
  matchMulti  ::  (Family phi, HZip phi (PF phi)) => phi ixT ->
             SchemeOf phi ixT -> ixT -> Maybe (Subst phi)
  matchMulti p scheme tm = execStateT (matchM p scheme (I_ tm)) []
{-# LINE 222 "GenericRewriting.lhs" #-}
  class HZip phi fT where
    hzipM  ::  Monad mT =>
               (forall ixT. phi ixT -> rT ixT -> rT' ixT -> mT (rT'' ixT)) ->
               fT rT ixT -> fT rT' ixT -> mT (fT rT'' ixT)
{-# LINE 237 "GenericRewriting.lhs" #-}
  data K' aT bT = K'_ { unK' :: aT }
 
  combine  ::  (Monad mT, HZip phi fT) =>
               (forall ixT. phi ixT -> rT ixT -> rT' ixT -> mT ()) ->
               fT rT ixT -> fT rT' ixT -> mT ()
  combine f x y = do  hzipM wrapf x y
                      return ()
    where wrapf p x y = do  f p x y
                            return (K'_ ())
{-# LINE 252 "GenericRewriting.lhs" #-}
  instance El phi ixrT => HZip phi (IdM ixrT) where
    hzipM f (Id_M x) (Id_M y) = liftM Id_M (f proof x y)
  
  instance (HZip phi aT,HZip phi bT) => HZip phi (aT `TimesM` bT) where
    hzipM f (x1 `TimesM` x2) (y1 `TimesM` y2)
      = liftM2 (TimesM) (hzipM f x1 y1) (hzipM f x2 y2)
  
  instance (HZip phi aT,HZip phi bT) => HZip phi (aT `PlusM` bT) where
    hzipM f  (LM x)  (LM y)  =  liftM LM (hzipM f x y)
    hzipM f  (RM x)  (RM y)  =  liftM RM (hzipM f x y)
    hzipM f  _      _      =  fail "zip failed in :+:"
{-# LINE 265 "GenericRewriting.lhs" #-}
  instance HZip phi fT => HZip phi (fT `TagM` ixT) where
    hzipM f (TagM x) (TagM y) = liftM TagM (hzipM f x y)
  
  instance Eq aT => HZip phi (KM aT) where
    hzipM f (K_M x) (K_M y)   |  x == y     =  return (K_M x)
                            |  otherwise  =  fail "zip failed in K"