{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module HERMIT.Kure
    ( -- * KURE

      -- | All the required functionality of KURE is exported here, so other modules do not need to import KURE directly.
      module Language.KURE
    , module Language.KURE.BiTransform
    , module Language.KURE.Lens
    , module Language.KURE.ExtendableContext
    , module Language.KURE.Pathfinder
      -- * Sub-Modules
    , module HERMIT.Kure.Universes
      -- * Synonyms
    , TransformH
    , RewriteH
    , BiRewriteH
    , LensH
    , PathH

      -- * Congruence combinators
      -- ** Modguts
    , modGutsT, modGutsR
      -- ** Program
    , progNilT
    , progConsT, progConsAllR, progConsAnyR, progConsOneR
      -- ** Binding Groups
    , nonRecT, nonRecAllR, nonRecAnyR, nonRecOneR
    , recT, recAllR, recAnyR, recOneR
      -- ** Recursive Definitions
    , defT, defAllR, defAnyR, defOneR
      -- ** Case Alternatives
    , altT, altAllR, altAnyR, altOneR
      -- ** Expressions
    , varT, varR
    , litT, litR
    , appT, appAllR, appAnyR, appOneR
    , lamT, lamAllR, lamAnyR, lamOneR
    , letT, letAllR, letAnyR, letOneR
    , caseT, caseAllR, caseAnyR, caseOneR
    , castT, castAllR, castAnyR, castOneR
    , tickT, tickAllR, tickAnyR, tickOneR
    , typeT, typeR
    , coercionT, coercionR
      -- ** Composite Congruence Combinators
    , defOrNonRecT, defOrNonRecAllR, defOrNonRecAnyR, defOrNonRecOneR
    , recDefT, recDefAllR, recDefAnyR, recDefOneR
    , letNonRecT, letNonRecAllR, letNonRecAnyR, letNonRecOneR
    , letRecT, letRecAllR, letRecAnyR, letRecOneR
    , letRecDefT, letRecDefAllR, letRecDefAnyR, letRecDefOneR
    , consNonRecT, consNonRecAllR, consNonRecAnyR, consNonRecOneR
    , consRecT, consRecAllR, consRecAnyR, consRecOneR
    , consRecDefT, consRecDefAllR, consRecDefAnyR, consRecDefOneR
    , caseAltT, caseAltAllR, caseAltAnyR, caseAltOneR
      -- ** Recursive Composite Congruence Combinators
    , progBindsT, progBindsAllR, progBindsAnyR, progBindsOneR
      -- ** Types
    , tyVarT, tyVarR
    , litTyT, litTyR
    , appTyT, appTyAllR, appTyAnyR, appTyOneR
    , funTyT, funTyAllR, funTyAnyR, funTyOneR
    , forAllTyT, forAllTyAllR, forAllTyAnyR, forAllTyOneR
    , tyConAppT, tyConAppAllR, tyConAppAnyR, tyConAppOneR
      -- ** Coercions
    , reflT, reflR
    , tyConAppCoT, tyConAppCoAllR, tyConAppCoAnyR, tyConAppCoOneR
    , appCoT, appCoAllR, appCoAnyR, appCoOneR
    , forAllCoT, forAllCoAllR, forAllCoAnyR, forAllCoOneR
    , coVarCoT, coVarCoR
    , axiomInstCoT, axiomInstCoAllR, axiomInstCoAnyR, axiomInstCoOneR
    , symCoT, symCoR
    , transCoT, transCoAllR, transCoAnyR, transCoOneR
    , nthCoT, nthCoAllR, nthCoAnyR, nthCoOneR
    , instCoT, instCoAllR, instCoAnyR, instCoOneR
    , lrCoT, lrCoAllR, lrCoAnyR, lrCoOneR
      -- ** Lemmas
    , conjT, conjAllR
    , disjT, disjAllR
    , implT, implAllR
    , equivT, equivAllR
    , quantifiedT, quantifiedR
    , clauseT, clauseR, forallVarsT
      -- * Applicative
      -- | Remove in 7.10
    , (<$>)
    , (<*>)
    ) where

import Language.KURE
import Language.KURE.BiTransform
import Language.KURE.Lens
import Language.KURE.ExtendableContext
import Language.KURE.Pathfinder

import HERMIT.Context
import HERMIT.Core
import HERMIT.GHC
import HERMIT.Kure.Universes
import HERMIT.Lemma
import HERMIT.Monad

import Control.Monad

---------------------------------------------------------------------

type TransformH a b = Transform HermitC HermitM a b
type RewriteH a     = Rewrite   HermitC HermitM a
type BiRewriteH a   = BiRewrite HermitC HermitM a
type LensH a b      = Lens      HermitC HermitM a b
type PathH          = Path Crumb

-- I find it annoying that Applicative is not a superclass of Monad.
-- This causes a warning now, and will need to be CPP'd for 7.10
(<$>) :: Monad m => (a -> b) -> m a -> m b
(<$>) = liftM
{-# INLINE (<$>) #-}

(<*>) :: Monad m => m (a -> b) -> m a -> m b
(<*>) = ap
{-# INLINE (<*>) #-}

---------------------------------------------------------------------

-- | Walking over modules, programs, binding groups, definitions, expressions and case alternatives.
instance (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c) => Walker c Core where

  allR :: forall m. MonadCatch m => Rewrite c m Core -> Rewrite c m Core
  allR r = prefixFailMsg "allR failed: " $
           rewrite $ \ c -> \case
             GutsCore guts  -> inject <$> applyT allRmodguts c guts
             ProgCore p     -> inject <$> applyT allRprog c p
             BindCore bn    -> inject <$> applyT allRbind c bn
             DefCore def    -> inject <$> applyT allRdef c def
             AltCore alt    -> inject <$> applyT allRalt c alt
             ExprCore e     -> inject <$> applyT allRexpr c e
    where
      allRmodguts :: MonadCatch m => Rewrite c m ModGuts
      allRmodguts = modGutsR (extractR r)
      {-# INLINE allRmodguts #-}

      allRprog :: MonadCatch m => Rewrite c m CoreProg
      allRprog = readerT $ \case
                              ProgCons{}  -> progConsAllR (extractR r) (extractR r)
                              _           -> idR
      {-# INLINE allRprog #-}

      allRbind :: MonadCatch m => Rewrite c m CoreBind
      allRbind = readerT $ \case
                              NonRec{}  -> nonRecAllR idR (extractR r) -- we don't descend into the Var
                              Rec _     -> recAllR (const $ extractR r)
      {-# INLINE allRbind #-}

      allRdef :: MonadCatch m => Rewrite c m CoreDef
      allRdef = defAllR idR (extractR r) -- we don't descend into the Id
      {-# INLINE allRdef #-}

      allRalt :: MonadCatch m => Rewrite c m CoreAlt
      allRalt = altAllR idR (const idR) (extractR r) -- we don't descend into the AltCon or Vars
      {-# INLINE allRalt #-}

      allRexpr :: MonadCatch m => Rewrite c m CoreExpr
      allRexpr = readerT $ \case
                              App{}   -> appAllR (extractR r) (extractR r)
                              Lam{}   -> lamAllR idR (extractR r) -- we don't descend into the Var
                              Let{}   -> letAllR (extractR r) (extractR r)
                              Case{}  -> caseAllR (extractR r) idR idR (const $ extractR r) -- we don't descend into the case binder or Type
                              Cast{}  -> castAllR (extractR r) idR -- we don't descend into the Coercion
                              Tick{}  -> tickAllR idR (extractR r) -- we don't descend into the Tickish
                              _       -> idR
      {-# INLINE allRexpr #-}

---------------------------------------------------------------------

-- | Walking over types (only).
instance (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c) => Walker c Type where

  allR :: MonadCatch m => Rewrite c m Type -> Rewrite c m Type
  allR r = prefixFailMsg "allR failed: " $
           readerT $ \case
                        AppTy{}     -> appTyAllR r r
                        FunTy{}     -> funTyAllR r r
                        ForAllTy{}  -> forAllTyAllR idR r
                        TyConApp{}  -> tyConAppAllR idR (const r)
                        _           -> idR

---------------------------------------------------------------------

-- | Walking over coercions (only).
instance (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c) => Walker c Coercion where

  allR :: MonadCatch m => Rewrite c m Coercion -> Rewrite c m Coercion
  allR r = prefixFailMsg "allR failed: " $
           readerT $ \case
                        TyConAppCo{}  -> tyConAppCoAllR idR (const r)
                        AppCo{}       -> appCoAllR r r
                        ForAllCo{}    -> forAllCoAllR idR r
                        SymCo{}       -> symCoR r
                        TransCo{}     -> transCoAllR r r
                        NthCo{}       -> nthCoAllR idR r
                        InstCo{}      -> instCoAllR r idR
                        LRCo{}        -> lrCoAllR idR r
                        AxiomInstCo{} -> axiomInstCoAllR idR idR (const r)
                        _             -> idR

---------------------------------------------------------------------

-- | Walking over types and coercions.
instance (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c) => Walker c TyCo where

  allR :: forall m. MonadCatch m => Rewrite c m TyCo -> Rewrite c m TyCo
  allR r = prefixFailMsg "allR failed: " $
           rewrite $ \ c -> \case
             TypeCore ty     -> inject <$> applyT (allR $ extractR r) c ty -- exploiting the fact that types do not contain coercions
             CoercionCore co -> inject <$> applyT allRcoercion c co
    where
      allRcoercion :: MonadCatch m => Rewrite c m Coercion
      allRcoercion = readerT $ \case
                              Refl{}        -> reflR (extractR r)
                              TyConAppCo{}  -> tyConAppCoAllR idR (const $ extractR r) -- we don't descend into the TyCon
                              AppCo{}       -> appCoAllR (extractR r) (extractR r)
                              ForAllCo{}    -> forAllCoAllR idR (extractR r) -- we don't descend into the TyVar
                              SymCo{}       -> symCoR (extractR r)
                              TransCo{}     -> transCoAllR (extractR r) (extractR r)
                              InstCo{}      -> instCoAllR (extractR r) (extractR r)
                              NthCo{}       -> nthCoAllR idR (extractR r) -- we don't descend into the Int
                              LRCo{}        -> lrCoAllR idR (extractR r)
                              AxiomInstCo{} -> axiomInstCoAllR idR idR (const $ extractR r) -- we don't descend into the axiom or index
                              _             -> idR
      {-# INLINE allRcoercion #-}

---------------------------------------------------------------------

-- | Walking over modules, programs, binding groups, definitions, expressions, case alternatives, lemma quantifiers and lemma clauses.
instance (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadPath c Crumb) => Walker c LCore where

    allR :: forall m. MonadCatch m => Rewrite c m LCore -> Rewrite c m LCore
    allR r = prefixFailMsg "allR failed: " $
                rewrite $ \ c -> \case
                    LQuantified q  -> inject <$> applyT allRquantified c q
                    LClause cl     -> inject <$> applyT allRclause c cl
                    LCore core     -> inject <$> applyT (allR $ extractR r) c core -- exploiting the fact that quantified/clause does not appear within Core
        where
            allRquantified :: MonadCatch m => Rewrite c m Quantified
            allRquantified = quantifiedR idR (extractR r) -- we don't descend into the binders
            {-# INLINE allRquantified #-}

            allRclause :: MonadCatch m => Rewrite c m Clause
            allRclause = readerT $ \case
                                Conj{}  -> conjAllR  (extractR r) (extractR r)
                                Disj{}  -> disjAllR  (extractR r) (extractR r)
                                Impl{}  -> implAllR  (extractR r) (extractR r)
                                Equiv{} -> equivAllR (extractR r) (extractR r)
            {-# INLINE allRclause #-}

---------------------------------------------------------------------

-- | Walking over modules, programs, binding groups, definitions, expressions, case alternatives, types, coercions, lemma quantifiers and lemma clauses.
instance (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadPath c Crumb) => Walker c LCoreTC where

    allR :: forall m. MonadCatch m => Rewrite c m LCoreTC -> Rewrite c m LCoreTC
    allR r = prefixFailMsg "allR failed: " $
                rewrite $ \ c -> \case
                    LTCCore (LQuantified q)  -> inject <$> applyT allRquantified c q
                    LTCCore (LClause cl)     -> inject <$> applyT allRclause c cl
                    LTCCore (LCore core)     -> inject <$> applyT (allR (extractR r :: Rewrite c m CoreTC)) c (Core core) -- convert to CoreTC, and exploit the fact that quantifiers and clauses will not appear in Core/CoreTC
                    LTCTyCo tyCo             -> inject <$> applyT (allR $ extractR r) c tyCo -- exploiting the fact that only types and coercions appear within types and coercions
        where
            allRquantified :: MonadCatch m => Rewrite c m Quantified
            allRquantified = quantifiedR idR (extractR r) -- we don't descend into the binders
            {-# INLINE allRquantified #-}

            allRclause :: MonadCatch m => Rewrite c m Clause
            allRclause = readerT $ \case
                                Conj{}  -> conjAllR (extractR r) (extractR r)
                                Disj{}  -> disjAllR (extractR r) (extractR r)
                                Impl{}  -> implAllR  (extractR r) (extractR r)
                                Equiv{} -> equivAllR (extractR r) (extractR r)
            {-# INLINE allRclause #-}

---------------------------------------------------------------------

-- | Walking over modules, programs, binding groups, definitions, expressions, case alternatives, types and coercions.
instance (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c) => Walker c CoreTC where

  allR :: forall m. MonadCatch m => Rewrite c m CoreTC -> Rewrite c m CoreTC
  allR r = prefixFailMsg "allR failed: " $
           rewrite $ \ c -> \case
             Core (GutsCore guts)  -> inject <$> applyT allRmodguts c guts
             Core (ProgCore p)     -> inject <$> applyT allRprog c p
             Core (BindCore bn)    -> inject <$> applyT allRbind c bn
             Core (DefCore def)    -> inject <$> applyT allRdef c def
             Core (AltCore alt)    -> inject <$> applyT allRalt c alt
             Core (ExprCore e)     -> inject <$> applyT allRexpr c e
             TyCo tyCo             -> inject <$> applyT (allR $ extractR r) c tyCo -- exploiting the fact that only types and coercions appear within types and coercions
    where
      allRmodguts :: MonadCatch m => Rewrite c m ModGuts
      allRmodguts = modGutsR (extractR r)
      {-# INLINE allRmodguts #-}

      allRprog :: MonadCatch m => Rewrite c m CoreProg
      allRprog = readerT $ \case
                              ProgCons{}  -> progConsAllR (extractR r) (extractR r)
                              _           -> idR
      {-# INLINE allRprog #-}

      allRbind :: MonadCatch m => Rewrite c m CoreBind
      allRbind = readerT $ \case
                              NonRec{}  -> nonRecAllR idR (extractR r) -- we don't descend into the Var
                              Rec _     -> recAllR (const $ extractR r)
      {-# INLINE allRbind #-}

      allRdef :: MonadCatch m => Rewrite c m CoreDef
      allRdef = defAllR idR (extractR r) -- we don't descend into the Id
      {-# INLINE allRdef #-}

      allRalt :: MonadCatch m => Rewrite c m CoreAlt
      allRalt = altAllR idR (const idR) (extractR r) -- we don't descend into the AltCon or Vars
      {-# INLINE allRalt #-}

      allRexpr :: MonadCatch m => Rewrite c m CoreExpr
      allRexpr = readerT $ \case
                              App{}      -> appAllR (extractR r) (extractR r)
                              Lam{}      -> lamAllR idR (extractR r) -- we don't descend into the Var
                              Let{}      -> letAllR (extractR r) (extractR r)
                              Case{}     -> caseAllR (extractR r) idR (extractR r) (const $ extractR r) -- we don't descend into the case binder
                              Cast{}     -> castAllR (extractR r) (extractR r)
                              Tick{}     -> tickAllR idR (extractR r) -- we don't descend into the Tickish
                              Type{}     -> typeR (extractR r)
                              Coercion{} -> coercionR (extractR r)
                              _          -> idR
      {-# INLINE allRexpr #-}

---------------------------------------------------------------------

-- Note that we deliberately set the context to empty when descending into a ModGuts.
-- This is to hide the top-level definitions that we include in the context when focusses on ModGuts.
-- This is slightly awkward, but pragmatically useful.

-- | Transform a module.
--   Slightly different to the other congruence combinators: it passes in /all/ of the original to the reconstruction function.
modGutsT :: (ExtendPath c Crumb, HasEmptyContext c, Monad m) => Transform c m CoreProg a -> (ModGuts -> a -> b) -> Transform c m ModGuts b
modGutsT t f = transform $ \ c guts -> f guts <$> applyT t (setEmptyContext c @@ ModGuts_Prog) (bindsToProg $ mg_binds guts)
{-# INLINE modGutsT #-}

-- | Rewrite the 'CoreProg' child of a module.
modGutsR :: (ExtendPath c Crumb, HasEmptyContext c, Monad m) => Rewrite c m CoreProg -> Rewrite c m ModGuts
modGutsR r = modGutsT r (\ guts p -> guts {mg_binds = progToBinds p})
{-# INLINE modGutsR #-}

---------------------------------------------------------------------

-- | Transform an empty list.
progNilT :: Monad m => b -> Transform c m CoreProg b
progNilT b = contextfreeT $ \case
                               ProgNil       -> return b
                               ProgCons _ _  -> fail "not an empty program."
{-# INLINE progNilT #-}

-- | Transform a program of the form: ('CoreBind' @:@ 'CoreProg')
progConsT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m CoreBind a1 -> Transform c m CoreProg a2 -> (a1 -> a2 -> b) -> Transform c m CoreProg b
progConsT t1 t2 f = transform $ \ c -> \case
                                          ProgCons bd p -> f <$> applyT t1 (c @@ ProgCons_Head) bd <*> applyT t2 (addBindingGroup bd c @@ ProgCons_Tail) p
                                          _             -> fail "not a non-empty program."
{-# INLINE progConsT #-}

-- | Rewrite all children of a program of the form: ('CoreBind' @:@ 'CoreProg')
progConsAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg
progConsAllR r1 r2 = progConsT r1 r2 ProgCons
{-# INLINE progConsAllR #-}

-- | Rewrite any children of a program of the form: ('CoreBind' @:@ 'CoreProg')
progConsAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg
progConsAnyR r1 r2 = unwrapAnyR $ progConsAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE progConsAnyR #-}

-- | Rewrite one child of a program of the form: ('CoreBind' @:@ 'CoreProg')
progConsOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg
progConsOneR r1 r2 = unwrapOneR $  progConsAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE progConsOneR #-}

---------------------------------------------------------------------

-- | Transform a binding group of the form: @NonRec@ 'Var' 'CoreExpr'
nonRecT :: (ExtendPath c Crumb, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreBind b
nonRecT t1 t2 f = transform $ \ c -> \case
                                        NonRec v e -> f <$> applyT t1 (c @@ NonRec_Var) v <*> applyT t2 (c @@ NonRec_RHS) e
                                        _          -> fail "not a non-recursive binding group."
{-# INLINE nonRecT #-}

-- | Rewrite all children of a binding group of the form: @NonRec@ 'Var' 'CoreExpr'
nonRecAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind
nonRecAllR r1 r2 = nonRecT r1 r2 NonRec
{-# INLINE nonRecAllR #-}

-- | Rewrite any children of a binding group of the form: @NonRec@ 'Var' 'CoreExpr'
nonRecAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind
nonRecAnyR r1 r2 = unwrapAnyR (nonRecAllR (wrapAnyR r1) (wrapAnyR r2))
{-# INLINE nonRecAnyR #-}

-- | Rewrite one child of a binding group of the form: @NonRec@ 'Var' 'CoreExpr'
nonRecOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind
nonRecOneR r1 r2 = unwrapOneR (nonRecAllR (wrapOneR r1) (wrapOneR r2))
{-# INLINE nonRecOneR #-}


-- | Transform a binding group of the form: @Rec@ ['CoreDef']
recT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Transform c m CoreDef a) -> ([a] -> b) -> Transform c m CoreBind b
recT t f = transform $ \ c -> \case
         Rec bds -> -- The group is recursive, so we add all other bindings in the group to the context (excluding the one under consideration).
                    f <$> sequence [ applyT (t n) (addDefBindingsExcept n bds c @@ Rec_Def n) (Def i e) -- here we convert from (Id,CoreExpr) to CoreDef
                                   | ((i,e),n) <- zip bds [0..]
                                   ]
         _       -> fail "not a recursive binding group."
{-# INLINE recT #-}

-- | Rewrite all children of a binding group of the form: @Rec@ ['CoreDef']
recAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind
recAllR rs = recT rs defsToRecBind
{-# INLINE recAllR #-}

-- | Rewrite any children of a binding group of the form: @Rec@ ['CoreDef']
recAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind
recAnyR rs = unwrapAnyR $ recAllR (wrapAnyR . rs)
{-# INLINE recAnyR #-}

-- | Rewrite one child of a binding group of the form: @Rec@ ['CoreDef']
recOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind
recOneR rs = unwrapOneR $ recAllR (wrapOneR . rs)
{-# INLINE recOneR #-}

---------------------------------------------------------------------

-- | Transform a recursive definition of the form: @Def@ 'Id' 'CoreExpr'
defT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Id a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreDef b
defT t1 t2 f = transform $ \ c (Def i e) -> f <$> applyT t1 (c @@ Def_Id) i <*> applyT t2 (addDefBinding i c @@ Def_RHS) e
{-# INLINE defT #-}

-- | Rewrite all children of a recursive definition of the form: @Def@ 'Id' 'CoreExpr'
defAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef
defAllR r1 r2 = defT r1 r2 Def
{-# INLINE defAllR #-}

-- | Rewrite any children of a recursive definition of the form: @Def@ 'Id' 'CoreExpr'
defAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef
defAnyR r1 r2 = unwrapAnyR (defAllR (wrapAnyR r1) (wrapAnyR r2))
{-# INLINE defAnyR #-}

-- | Rewrite one child of a recursive definition of the form: @Def@ 'Id' 'CoreExpr'
defOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef
defOneR r1 r2 = unwrapOneR (defAllR (wrapOneR r1) (wrapOneR r2))
{-# INLINE defOneR #-}

---------------------------------------------------------------------

-- | Transform a case alternative of the form: ('AltCon', ['Var'], 'CoreExpr')
altT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m AltCon a1 -> (Int -> Transform c m Var a2) -> Transform c m CoreExpr a3 -> (a1 -> [a2] -> a3 -> b) -> Transform c m CoreAlt b
altT t1 ts t2 f = transform $ \ c (con,vs,e) -> f <$> applyT t1 (c @@ Alt_Con) con
                                                  <*> sequence [ applyT (ts n) (c @@ Alt_Var n) v | (v,n) <- zip vs [1..] ]
                                                  <*> applyT t2 (addAltBindings vs c @@ Alt_RHS) e
{-# INLINE altT #-}

-- | Rewrite all children of a case alternative of the form: ('AltCon', 'Id', 'CoreExpr')
altAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt
altAllR r1 rs r2 = altT r1 rs r2 (,,)
{-# INLINE altAllR #-}

-- | Rewrite any children of a case alternative of the form: ('AltCon', 'Id', 'CoreExpr')
altAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt
altAnyR r1 rs r2 = unwrapAnyR (altAllR (wrapAnyR r1) (wrapAnyR . rs) (wrapAnyR r2))
{-# INLINE altAnyR #-}

-- | Rewrite one child of a case alternative of the form: ('AltCon', 'Id', 'CoreExpr')
altOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt
altOneR r1 rs r2 = unwrapOneR (altAllR (wrapOneR r1) (wrapOneR . rs) (wrapOneR r2))
{-# INLINE altOneR #-}

---------------------------------------------------------------------

-- | Transform an expression of the form: @Var@ 'Id'
varT :: (ExtendPath c Crumb, Monad m) => Transform c m Id b -> Transform c m CoreExpr b
varT t = transform $ \ c -> \case
                               Var v -> applyT t (c @@ Var_Id) v
                               _     -> fail "not a variable."
{-# INLINE varT #-}

-- | Rewrite the 'Id' child in an expression of the form: @Var@ 'Id'
varR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr
varR r = varT (Var <$> r)
{-# INLINE varR #-}


-- | Transform an expression of the form: @Lit@ 'Literal'
litT :: (ExtendPath c Crumb, Monad m) => Transform c m Literal b -> Transform c m CoreExpr b
litT t = transform $ \ c -> \case
                               Lit x -> applyT t (c @@ Lit_Lit) x
                               _     -> fail "not a literal."
{-# INLINE litT #-}

-- | Rewrite the 'Literal' child in an expression of the form: @Lit@ 'Literal'
litR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Literal -> Rewrite c m CoreExpr
litR r = litT (Lit <$> r)
{-# INLINE litR #-}


-- | Transform an expression of the form: @App@ 'CoreExpr' 'CoreExpr'
appT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreExpr a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b
appT t1 t2 f = transform $ \ c -> \case
                                     App e1 e2 -> f <$> applyT t1 (c @@ App_Fun) e1 <*> applyT t2 (c @@ App_Arg) e2
                                     _         -> fail "not an application."
{-# INLINE appT #-}

-- | Rewrite all children of an expression of the form: @App@ 'CoreExpr' 'CoreExpr'
appAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
appAllR r1 r2 = appT r1 r2 App
{-# INLINE appAllR #-}

-- | Rewrite any children of an expression of the form: @App@ 'CoreExpr' 'CoreExpr'
appAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
appAnyR r1 r2 = unwrapAnyR $ appAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE appAnyR #-}

-- | Rewrite one child of an expression of the form: @App@ 'CoreExpr' 'CoreExpr'
appOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
appOneR r1 r2 = unwrapOneR $ appAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE appOneR #-}


-- | Transform an expression of the form: @Lam@ 'Var' 'CoreExpr'
lamT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b
lamT t1 t2 f = transform $ \ c -> \case
                                     Lam v e -> f <$> applyT t1 (c @@ Lam_Var) v <*> applyT t2 (addLambdaBinding v c @@ Lam_Body) e
                                     _       -> fail "not a lambda."
{-# INLINE lamT #-}

-- | Rewrite all children of an expression of the form: @Lam@ 'Var' 'CoreExpr'
lamAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
lamAllR r1 r2 = lamT r1 r2 Lam
{-# INLINE lamAllR #-}

-- | Rewrite any children of an expression of the form: @Lam@ 'Var' 'CoreExpr'
lamAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
lamAnyR r1 r2 = unwrapAnyR $ lamAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE lamAnyR #-}

-- | Rewrite one child of an expression of the form: @Lam@ 'Var' 'CoreExpr'
lamOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
lamOneR r1 r2 = unwrapOneR $ lamAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE lamOneR #-}


-- | Transform an expression of the form: @Let@ 'CoreBind' 'CoreExpr'
letT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m CoreBind a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b
letT t1 t2 f = transform $ \ c -> \case
        Let bds e -> -- Note we use the *original* context for the binding group.
                     -- If the bindings are recursive, they will be added to the context by recT.
                     f <$> applyT t1 (c @@ Let_Bind) bds <*> applyT t2 (addBindingGroup bds c @@ Let_Body) e
        _         -> fail "not a let node."
{-# INLINE letT #-}

-- | Rewrite all children of an expression of the form: @Let@ 'CoreBind' 'CoreExpr'
letAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letAllR r1 r2 = letT r1 r2 Let
{-# INLINE letAllR #-}

-- | Rewrite any children of an expression of the form: @Let@ 'CoreBind' 'CoreExpr'
letAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letAnyR r1 r2 = unwrapAnyR $ letAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE letAnyR #-}

-- | Rewrite one child of an expression of the form: @Let@ 'CoreBind' 'CoreExpr'
letOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letOneR r1 r2 = unwrapOneR $ letAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE letOneR #-}


-- | Transform an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt']
caseT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m)
      => Transform c m CoreExpr e
      -> Transform c m Id w
      -> Transform c m Type ty
      -> (Int -> Transform c m CoreAlt alt)
      -> (e -> w -> ty -> [alt] -> b)
      -> Transform c m CoreExpr b
caseT te tw tty talts f = transform $ \ c -> \case
         Case e w ty alts -> f <$> applyT te (c @@ Case_Scrutinee) e
                               <*> applyT tw (c @@ Case_Binder) w
                               <*> applyT tty (c @@ Case_Type) ty
                               <*> sequence [ applyT (talts n) (addCaseBinderBinding (w,e,alt) c @@ Case_Alt n) alt
                                            | (alt,n) <- zip alts [0..]
                                            ]
         _                -> fail "not a case."
{-# INLINE caseT #-}

-- | Rewrite all children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt']
caseAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m)
         => Rewrite c m CoreExpr
         -> Rewrite c m Id
         -> Rewrite c m Type
         -> (Int -> Rewrite c m CoreAlt)
         -> Rewrite c m CoreExpr
caseAllR re rw rty ralts = caseT re rw rty ralts Case
{-# INLINE caseAllR #-}

-- | Rewrite any children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt']
caseAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m)
         => Rewrite c m CoreExpr
         -> Rewrite c m Id
         -> Rewrite c m Type
         -> (Int -> Rewrite c m CoreAlt)
         -> Rewrite c m CoreExpr
caseAnyR re rw rty ralts = unwrapAnyR $ caseAllR (wrapAnyR re) (wrapAnyR rw) (wrapAnyR rty) (wrapAnyR . ralts)
{-# INLINE caseAnyR #-}

-- | Rewrite one child of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' ['CoreAlt']
caseOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m)
         => Rewrite c m CoreExpr
         -> Rewrite c m Id
         -> Rewrite c m Type
         -> (Int -> Rewrite c m CoreAlt)
         -> Rewrite c m CoreExpr
caseOneR re rw rty ralts = unwrapOneR $ caseAllR (wrapOneR re) (wrapOneR rw) (wrapOneR rty) (wrapOneR . ralts)
{-# INLINE caseOneR #-}


-- | Transform an expression of the form: @Cast@ 'CoreExpr' 'Coercion'
castT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreExpr a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b
castT t1 t2 f = transform $ \ c -> \case
                                      Cast e co -> f <$> applyT t1 (c @@ Cast_Expr) e <*> applyT t2 (c @@ Cast_Co) co
                                      _         -> fail "not a cast."
{-# INLINE castT #-}

-- | Rewrite all children of an expression of the form: @Cast@ 'CoreExpr' 'Coercion'
castAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr
castAllR r1 r2 = castT r1 r2 Cast
{-# INLINE castAllR #-}

-- | Rewrite any children of an expression of the form: @Cast@ 'CoreExpr' 'Coercion'
castAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr
castAnyR r1 r2 = unwrapAnyR $ castAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE castAnyR #-}

-- | Rewrite one child of an expression of the form: @Cast@ 'CoreExpr' 'Coercion'
castOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr
castOneR r1 r2 = unwrapOneR $ castAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE castOneR #-}


-- | Transform an expression of the form: @Tick@ 'CoreTickish' 'CoreExpr'
tickT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreTickish a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b
tickT t1 t2 f = transform $ \ c -> \case
                                      Tick tk e -> f <$> applyT t1 (c @@ Tick_Tick) tk <*> applyT t2 (c @@ Tick_Expr) e
                                      _         -> fail "not a tick."
{-# INLINE tickT #-}

-- | Rewrite all children of an expression of the form: @Tick@ 'CoreTickish' 'CoreExpr'
tickAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
tickAllR r1 r2 = tickT r1 r2 Tick
{-# INLINE tickAllR #-}

-- | Rewrite any children of an expression of the form: @Tick@ 'CoreTickish' 'CoreExpr'
tickAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
tickAnyR r1 r2 = unwrapAnyR $ tickAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE tickAnyR #-}

-- | Rewrite any children of an expression of the form: @Tick@ 'CoreTickish' 'CoreExpr'
tickOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
tickOneR r1 r2 = unwrapOneR $ tickAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE tickOneR #-}


-- | Transform an expression of the form: @Type@ 'Type'
typeT :: (ExtendPath c Crumb, Monad m) => Transform c m Type b -> Transform c m CoreExpr b
typeT t = transform $ \ c -> \case
                                Type ty -> applyT t (c @@ Type_Type) ty
                                _       -> fail "not a type."
{-# INLINE typeT #-}

-- | Rewrite the 'Type' child in an expression of the form: @Type@ 'Type'
typeR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m CoreExpr
typeR r = typeT (Type <$> r)
{-# INLINE typeR #-}


-- | Transform an expression of the form: @Coercion@ 'Coercion'
coercionT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion b -> Transform c m CoreExpr b
coercionT t = transform $ \ c -> \case
                                    Coercion co -> applyT t (c @@ Co_Co) co
                                    _           -> fail "not a coercion."
{-# INLINE coercionT #-}

-- | Rewrite the 'Coercion' child in an expression of the form: @Coercion@ 'Coercion'
coercionR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m CoreExpr
coercionR r = coercionT (Coercion <$> r)
{-# INLINE coercionR #-}

---------------------------------------------------------------------

-- Some composite congruence combinators to export.

-- | Transform a definition of the form @NonRec 'Var' 'CoreExpr'@ or @Def 'Id' 'CoreExpr'@
defOrNonRecT :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m g b
defOrNonRecT t1 t2 f = promoteBindT (nonRecT t1 t2 f)
                    <+ promoteDefT  (defT    t1 t2 f)
{-# INLINE defOrNonRecT #-}

-- | Rewrite all children of a definition of the form @NonRec 'Var' 'CoreExpr'@ or @Def 'Id' 'CoreExpr'@
defOrNonRecAllR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g
defOrNonRecAllR r1 r2 = promoteBindR (nonRecAllR r1 r2)
                     <+ promoteDefR  (defAllR    r1 r2)
{-# INLINE defOrNonRecAllR #-}

-- | Rewrite any children of a definition of the form @NonRec 'Var' 'CoreExpr'@ or @Def 'Id' 'CoreExpr'@
defOrNonRecAnyR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g
defOrNonRecAnyR r1 r2 = unwrapAnyR $ defOrNonRecAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE defOrNonRecAnyR #-}

-- | Rewrite one child of a definition of the form @NonRec 'Var' 'CoreExpr'@ or @Def 'Id' 'CoreExpr'@
defOrNonRecOneR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g
defOrNonRecOneR r1 r2 = unwrapAnyR $ defOrNonRecOneR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE defOrNonRecOneR #-}


-- | Transform a binding group of the form: @Rec@ [('Id', 'CoreExpr')]
recDefT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Transform c m Id a1, Transform c m CoreExpr a2)) -> ([(a1,a2)] -> b) -> Transform c m CoreBind b
recDefT ts = recT (\ n -> uncurry defT (ts n) (,))
{-# INLINE recDefT #-}

-- | Rewrite all children of a binding group of the form: @Rec@ [('Id', 'CoreExpr')]
recDefAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind
recDefAllR rs = recAllR (\ n -> uncurry defAllR (rs n))
{-# INLINE recDefAllR #-}

-- | Rewrite any children of a binding group of the form: @Rec@ [('Id', 'CoreExpr')]
recDefAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind
recDefAnyR rs = recAnyR (\ n -> uncurry defAnyR (rs n))
{-# INLINE recDefAnyR #-}

-- | Rewrite one child of a binding group of the form: @Rec@ [('Id', 'CoreExpr')]
recDefOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind
recDefOneR rs = recOneR (\ n -> uncurry defOneR (rs n))
{-# INLINE recDefOneR #-}


-- | Transform a program of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg'
consNonRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> Transform c m CoreProg a3 -> (a1 -> a2 -> a3 -> b) -> Transform c m CoreProg b
consNonRecT t1 t2 t3 f = progConsT (nonRecT t1 t2 (,)) t3 (uncurry f)
{-# INLINE consNonRecT #-}

-- | Rewrite all children of an expression of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg'
consNonRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consNonRecAllR r1 r2 r3 = progConsAllR (nonRecAllR r1 r2) r3
{-# INLINE consNonRecAllR #-}

-- | Rewrite any children of an expression of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg'
consNonRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consNonRecAnyR r1 r2 r3 = progConsAllR (nonRecAnyR r1 r2) r3
{-# INLINE consNonRecAnyR #-}

-- | Rewrite one child of an expression of the form: (@NonRec@ 'Var' 'CoreExpr') @:@ 'CoreProg'
consNonRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consNonRecOneR r1 r2 r3 = progConsAllR (nonRecOneR r1 r2) r3
{-# INLINE consNonRecOneR #-}


-- | Transform an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg'
consRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Transform c m CoreDef a1) -> Transform c m CoreProg a2 -> ([a1] -> a2 -> b) -> Transform c m CoreProg b
consRecT ts t = progConsT (recT ts id) t
{-# INLINE consRecT #-}

-- | Rewrite all children of an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg'
consRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consRecAllR rs r = progConsAllR (recAllR rs) r
{-# INLINE consRecAllR #-}

-- | Rewrite any children of an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg'
consRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consRecAnyR rs r = progConsAnyR (recAnyR rs) r
{-# INLINE consRecAnyR #-}

-- | Rewrite one child of an expression of the form: (@Rec@ ['CoreDef']) @:@ 'CoreProg'
consRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consRecOneR rs r = progConsOneR (recOneR rs) r
{-# INLINE consRecOneR #-}


-- | Transform an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg'
consRecDefT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Transform c m Id a1, Transform c m CoreExpr a2)) -> Transform c m CoreProg a3 -> ([(a1,a2)] -> a3 -> b) -> Transform c m CoreProg b
consRecDefT ts t = consRecT (\ n -> uncurry defT (ts n) (,)) t
{-# INLINE consRecDefT #-}

-- | Rewrite all children of an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg'
consRecDefAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consRecDefAllR rs r = consRecAllR (\ n -> uncurry defAllR (rs n)) r
{-# INLINE consRecDefAllR #-}

-- | Rewrite any children of an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg'
consRecDefAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consRecDefAnyR rs r = consRecAnyR (\ n -> uncurry defAnyR (rs n)) r
{-# INLINE consRecDefAnyR #-}

-- | Rewrite one child of an expression of the form: (@Rec@ [('Id', 'CoreExpr')]) @:@ 'CoreProg'
consRecDefOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg
consRecDefOneR rs r = consRecOneR (\ n -> uncurry defOneR (rs n)) r
{-# INLINE consRecDefOneR #-}


-- | Transform an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr'
letNonRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> Transform c m CoreExpr a3 -> (a1 -> a2 -> a3 -> b) -> Transform c m CoreExpr b
letNonRecT t1 t2 t3 f = letT (nonRecT t1 t2 (,)) t3 (uncurry f)
{-# INLINE letNonRecT #-}

-- | Rewrite all children of an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr'
letNonRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letNonRecAllR r1 r2 r3 = letAllR (nonRecAllR r1 r2) r3
{-# INLINE letNonRecAllR #-}

-- | Rewrite any children of an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr'
letNonRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letNonRecAnyR r1 r2 r3 = letAnyR (nonRecAnyR r1 r2) r3
{-# INLINE letNonRecAnyR #-}

-- | Rewrite one child of an expression of the form: @Let@ (@NonRec@ 'Var' 'CoreExpr') 'CoreExpr'
letNonRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letNonRecOneR r1 r2 r3 = letOneR (nonRecOneR r1 r2) r3
{-# INLINE letNonRecOneR #-}


-- | Transform an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr'
letRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Transform c m CoreDef a1) -> Transform c m CoreExpr a2 -> ([a1] -> a2 -> b) -> Transform c m CoreExpr b
letRecT ts t = letT (recT ts id) t
{-# INLINE letRecT #-}

-- | Rewrite all children of an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr'
letRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letRecAllR rs r = letAllR (recAllR rs) r
{-# INLINE letRecAllR #-}

-- | Rewrite any children of an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr'
letRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letRecAnyR rs r = letAnyR (recAnyR rs) r
{-# INLINE letRecAnyR #-}

-- | Rewrite one child of an expression of the form: @Let@ (@Rec@ ['CoreDef']) 'CoreExpr'
letRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letRecOneR rs r = letOneR (recOneR rs) r
{-# INLINE letRecOneR #-}


-- | Transform an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr'
letRecDefT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Transform c m Id a1, Transform c m CoreExpr a2)) -> Transform c m CoreExpr a3 -> ([(a1,a2)] -> a3 -> b) -> Transform c m CoreExpr b
letRecDefT ts t = letRecT (\ n -> uncurry defT (ts n) (,)) t
{-# INLINE letRecDefT #-}

-- | Rewrite all children of an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr'
letRecDefAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letRecDefAllR rs r = letRecAllR (\ n -> uncurry defAllR (rs n)) r
{-# INLINE letRecDefAllR #-}

-- | Rewrite any children of an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr'
letRecDefAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letRecDefAnyR rs r = letRecAnyR (\ n -> uncurry defAnyR (rs n)) r
{-# INLINE letRecDefAnyR #-}

-- | Rewrite one child of an expression of the form: @Let@ (@Rec@ [('Id', 'CoreExpr')]) 'CoreExpr'
letRecDefOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr
letRecDefOneR rs r = letRecOneR (\ n -> uncurry defOneR (rs n)) r
{-# INLINE letRecDefOneR #-}


-- | Transform an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Var'], 'CoreExpr')]
caseAltT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m)
         => Transform c m CoreExpr sc
         -> Transform c m Id w
         -> Transform c m Type ty
         -> (Int -> (Transform c m AltCon con, (Int -> Transform c m Var v), Transform c m CoreExpr rhs)) -> (sc -> w -> ty -> [(con,[v],rhs)] -> b)
         -> Transform c m CoreExpr b
caseAltT tsc tw tty talts = caseT tsc tw tty (\ n -> let (tcon,tvs,te) = talts n in altT tcon tvs te (,,))
{-# INLINE caseAltT #-}

-- | Rewrite all children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Var'], 'CoreExpr')]
caseAltAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m)
            => Rewrite c m CoreExpr
            -> Rewrite c m Id
            -> Rewrite c m Type
            -> (Int -> (Rewrite c m AltCon, (Int -> Rewrite c m Var), Rewrite c m CoreExpr))
            -> Rewrite c m CoreExpr
caseAltAllR rsc rw rty ralts = caseAllR rsc rw rty (\ n -> let (rcon,rvs,re) = ralts n in altAllR rcon rvs re)
{-# INLINE caseAltAllR #-}

-- | Rewrite any children of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Var'], 'CoreExpr')]
caseAltAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m)
            => Rewrite c m CoreExpr
            -> Rewrite c m Id
            -> Rewrite c m Type
            -> (Int -> (Rewrite c m AltCon, (Int -> Rewrite c m Var), Rewrite c m CoreExpr))
            -> Rewrite c m CoreExpr
caseAltAnyR rsc rw rty ralts = caseAnyR rsc rw rty (\ n -> let (rcon,rvs,re) = ralts n in altAnyR rcon rvs re)
{-# INLINE caseAltAnyR #-}

-- | Rewrite one child of an expression of the form: @Case@ 'CoreExpr' 'Id' 'Type' [('AltCon', ['Var'], 'CoreExpr')]
caseAltOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m)
            => Rewrite c m CoreExpr
            -> Rewrite c m Id
            -> Rewrite c m Type
            -> (Int -> (Rewrite c m AltCon, (Int -> Rewrite c m Var), Rewrite c m CoreExpr))
            -> Rewrite c m CoreExpr
caseAltOneR rsc rw rty ralts = caseOneR rsc rw rty (\ n -> let (rcon,rvs,re) = ralts n in altOneR rcon rvs re)
{-# INLINE caseAltOneR #-}

---------------------------------------------------------------------

-- Recursive composite congruence combinators.

-- | Transform all top-level binding groups in a program.
progBindsT :: forall c m a b. (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Transform c m CoreBind a) -> ([a] -> b) -> Transform c m CoreProg b
progBindsT ts f = f <$> progBindsTaux 0
  where
    progBindsTaux :: Int -> Transform c m CoreProg [a]
    progBindsTaux n = progNilT [] <+ progConsT (ts n) (progBindsTaux (succ n)) (:)
{-# INLINE progBindsT #-}

-- | Rewrite all top-level binding groups in a program.
progBindsAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreBind) -> Rewrite c m CoreProg
progBindsAllR rs = progBindsT rs bindsToProg
{-# INLINE progBindsAllR #-}

-- | Rewrite any top-level binding groups in a program.
progBindsAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreBind) -> Rewrite c m CoreProg
progBindsAnyR rs = unwrapAnyR $ progBindsAllR (wrapAnyR . rs)
{-# INLINE progBindsAnyR #-}

-- | Rewrite any top-level binding groups in a program.
progBindsOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreBind) -> Rewrite c m CoreProg
progBindsOneR rs = unwrapOneR $ progBindsAllR (wrapOneR . rs)
{-# INLINE progBindsOneR #-}

---------------------------------------------------------------------
---------------------------------------------------------------------

-- Types

-- | Transform a type of the form: @TyVarTy@ 'TyVar'
tyVarT :: (ExtendPath c Crumb, Monad m) => Transform c m TyVar b -> Transform c m Type b
tyVarT t = transform $ \ c -> \case
                                 TyVarTy v -> applyT t (c @@ TyVarTy_TyVar) v
                                 _         -> fail "not a type variable."
{-# INLINE tyVarT #-}

-- | Rewrite the 'TyVar' child of a type of the form: @TyVarTy@ 'TyVar'
tyVarR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyVar -> Rewrite c m Type
tyVarR r = tyVarT (TyVarTy <$> r)
{-# INLINE tyVarR #-}


-- | Transform a type of the form: @LitTy@ 'TyLit'
litTyT :: (ExtendPath c Crumb, Monad m) => Transform c m TyLit b -> Transform c m Type b
litTyT t = transform $ \ c -> \case
                                 LitTy x -> applyT t (c @@ LitTy_TyLit) x
                                 _       -> fail "not a type literal."
{-# INLINE litTyT #-}

-- | Rewrite the 'TyLit' child of a type of the form: @LitTy@ 'TyLit'
litTyR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyLit -> Rewrite c m Type
litTyR r = litTyT (LitTy <$> r)
{-# INLINE litTyR #-}


-- | Transform a type of the form: @AppTy@ 'Type' 'Type'
appTyT :: (ExtendPath c Crumb, Monad m) => Transform c m Type a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Type b
appTyT t1 t2 f = transform $ \ c -> \case
                                     AppTy ty1 ty2 -> f <$> applyT t1 (c @@ AppTy_Fun) ty1 <*> applyT t2 (c @@ AppTy_Arg) ty2
                                     _             -> fail "not a type application."
{-# INLINE appTyT #-}

-- | Rewrite all children of a type of the form: @AppTy@ 'Type' 'Type'
appTyAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type
appTyAllR r1 r2 = appTyT r1 r2 AppTy
{-# INLINE appTyAllR #-}

-- | Rewrite any children of a type of the form: @AppTy@ 'Type' 'Type'
appTyAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type
appTyAnyR r1 r2 = unwrapAnyR $ appTyAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE appTyAnyR #-}

-- | Rewrite one child of a type of the form: @AppTy@ 'Type' 'Type'
appTyOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type
appTyOneR r1 r2 = unwrapOneR $ appTyAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE appTyOneR #-}


-- | Transform a type of the form: @FunTy@ 'Type' 'Type'
funTyT :: (ExtendPath c Crumb, Monad m) => Transform c m Type a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Type b
funTyT t1 t2 f = transform $ \ c -> \case
                                     FunTy ty1 ty2 -> f <$> applyT t1 (c @@ FunTy_Dom) ty1 <*> applyT t2 (c @@ FunTy_CoDom) ty2
                                     _             -> fail "not a function type."
{-# INLINE funTyT #-}

-- | Rewrite all children of a type of the form: @FunTy@ 'Type' 'Type'
funTyAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type
funTyAllR r1 r2 = funTyT r1 r2 FunTy
{-# INLINE funTyAllR #-}

-- | Rewrite any children of a type of the form: @FunTy@ 'Type' 'Type'
funTyAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type
funTyAnyR r1 r2 = unwrapAnyR $ funTyAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE funTyAnyR #-}

-- | Rewrite one child of a type of the form: @FunTy@ 'Type' 'Type'
funTyOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type
funTyOneR r1 r2 = unwrapOneR $ funTyAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE funTyOneR #-}


-- | Transform a type of the form: @ForAllTy@ 'Var' 'Type'
forAllTyT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Type b
forAllTyT t1 t2 f = transform $ \ c -> \case
                                          ForAllTy v ty -> f <$> applyT t1 (c @@ ForAllTy_Var) v <*> applyT t2 (addForallBinding v c @@ ForAllTy_Body) ty
                                          _             -> fail "not a forall type."
{-# INLINE forAllTyT #-}

-- | Rewrite all children of a type of the form: @ForAllTy@ 'Var' 'Type'
forAllTyAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type
forAllTyAllR r1 r2 = forAllTyT r1 r2 ForAllTy
{-# INLINE forAllTyAllR #-}

-- | Rewrite any children of a type of the form: @ForAllTy@ 'Var' 'Type'
forAllTyAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type
forAllTyAnyR r1 r2 = unwrapAnyR $ forAllTyAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE forAllTyAnyR #-}

-- | Rewrite one child of a type of the form: @ForAllTy@ 'Var' 'Type'
forAllTyOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type
forAllTyOneR r1 r2 = unwrapOneR $ forAllTyAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE forAllTyOneR #-}


-- | Transform a type of the form: @TyConApp@ 'TyCon' ['KindOrType']
tyConAppT :: (ExtendPath c Crumb, Monad m) => Transform c m TyCon a1 -> (Int -> Transform c m KindOrType a2) -> (a1 -> [a2] -> b) -> Transform c m Type b
tyConAppT t ts f = transform $ \ c -> \case
                                         TyConApp con tys -> f <$> applyT t (c @@ TyConApp_TyCon) con <*> sequence [ applyT (ts n) (c @@ TyConApp_Arg n) ty | (ty,n) <- zip tys [0..] ]
                                         _                -> fail "not a type-constructor application."
{-# INLINE tyConAppT #-}

-- | Rewrite all children of a type of the form: @TyConApp@ 'TyCon' ['KindOrType']
tyConAppAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type
tyConAppAllR r rs = tyConAppT r rs TyConApp
{-# INLINE tyConAppAllR #-}

-- | Rewrite any children of a type of the form: @TyConApp@ 'TyCon' ['KindOrType']
tyConAppAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type
tyConAppAnyR r rs = unwrapAnyR $ tyConAppAllR (wrapAnyR r) (wrapAnyR . rs)
{-# INLINE tyConAppAnyR #-}

-- | Rewrite one child of a type of the form: @TyConApp@ 'TyCon' ['KindOrType']
tyConAppOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type
tyConAppOneR r rs = unwrapOneR $ tyConAppAllR (wrapOneR r) (wrapOneR . rs)
{-# INLINE tyConAppOneR #-}

---------------------------------------------------------------------
---------------------------------------------------------------------

-- Coercions
-- TODO: review and bring all these up-to-date for Coercions w/ Roles in 7.8

-- | Transform a coercion of the form: @Refl@ 'Role' 'Type'
reflT :: (ExtendPath c Crumb, Monad m) => Transform c m Type a1 -> (Role -> a1 -> b) -> Transform c m Coercion b
reflT t f = transform $ \ c -> \case
                                 Refl r ty -> f r <$> applyT t (c @@ Refl_Type) ty
                                 _         -> fail "not a reflexive coercion."

-- | Rewrite the 'Type' child of a coercion of the form: @Refl@ 'Role' 'Type'
reflR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Coercion
reflR r = reflT r Refl
{-# INLINE reflT #-}
{-# INLINE reflR #-}

-- | Transform a coercion of the form: @TyConAppCo@ 'Role' 'TyCon' ['Coercion']
tyConAppCoT :: (ExtendPath c Crumb, Monad m) => Transform c m TyCon a1 -> (Int -> Transform c m Coercion a2) -> (Role -> a1 -> [a2] -> b) -> Transform c m Coercion b
tyConAppCoT t ts f = transform $ \ c -> \case
                                           TyConAppCo r con coes -> f r <$> applyT t (c @@ TyConAppCo_TyCon) con <*> sequence [ applyT (ts n) (c @@ TyConAppCo_Arg n) co | (co,n) <- zip coes [0..] ]
                                           _                     -> fail "not a type-constructor coercion."
{-# INLINE tyConAppCoT #-}

-- | Rewrite all children of a coercion of the form: @TyConAppCo@ 'TyCon' ['Coercion']
tyConAppCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion
tyConAppCoAllR r rs = tyConAppCoT r rs TyConAppCo
{-# INLINE tyConAppCoAllR #-}

-- | Rewrite any children of a coercion of the form: @TyConAppCo@ 'TyCon' ['Coercion']
tyConAppCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion
tyConAppCoAnyR r rs = unwrapAnyR $ tyConAppCoAllR (wrapAnyR r) (wrapAnyR . rs)
{-# INLINE tyConAppCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @TyConAppCo@ 'TyCon' ['Coercion']
tyConAppCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion
tyConAppCoOneR r rs = unwrapOneR $ tyConAppCoAllR (wrapOneR r) (wrapOneR . rs)
{-# INLINE tyConAppCoOneR #-}


-- | Transform a coercion of the form: @AppCo@ 'Coercion' 'Coercion'
appCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b
appCoT t1 t2 f = transform $ \ c -> \case
                                     AppCo co1 co2 -> f <$> applyT t1 (c @@ AppCo_Fun) co1 <*> applyT t2 (c @@ AppCo_Arg) co2
                                     _             -> fail "not a coercion application."
{-# INLINE appCoT #-}

-- | Rewrite all children of a coercion of the form: @AppCo@ 'Coercion' 'Coercion'
appCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion
appCoAllR r1 r2 = appCoT r1 r2 AppCo
{-# INLINE appCoAllR #-}

-- | Rewrite any children of a coercion of the form: @AppCo@ 'Coercion' 'Coercion'
appCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion
appCoAnyR r1 r2 = unwrapAnyR $ appCoAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE appCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @AppCo@ 'Coercion' 'Coercion'
appCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion
appCoOneR r1 r2 = unwrapOneR $ appCoAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE appCoOneR #-}


-- | Transform a coercion of the form: @ForAllCo@ 'TyVar' 'Coercion'
forAllCoT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m TyVar a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b
forAllCoT t1 t2 f = transform $ \ c -> \case
                                          ForAllCo v co -> f <$> applyT t1 (c @@ ForAllCo_TyVar) v <*> applyT t2 (addForallBinding v c @@ ForAllCo_Body) co
                                          _             -> fail "not a forall coercion."
{-# INLINE forAllCoT #-}

-- | Rewrite all children of a coercion of the form: @ForAllCo@ 'TyVar' 'Coercion'
forAllCoAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion
forAllCoAllR r1 r2 = forAllCoT r1 r2 ForAllCo
{-# INLINE forAllCoAllR #-}

-- | Rewrite any children of a coercion of the form: @ForAllCo@ 'TyVar' 'Coercion'
forAllCoAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion
forAllCoAnyR r1 r2 = unwrapAnyR $ forAllCoAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE forAllCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @ForAllCo@ 'TyVar' 'Coercion'
forAllCoOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion
forAllCoOneR r1 r2 = unwrapOneR $ forAllCoAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE forAllCoOneR #-}


-- | Transform a coercion of the form: @CoVarCo@ 'CoVar'
coVarCoT :: (ExtendPath c Crumb, Monad m) => Transform c m CoVar b -> Transform c m Coercion b
coVarCoT t = transform $ \ c -> \case
                                   CoVarCo v -> applyT t (c @@ CoVarCo_CoVar) v
                                   _         -> fail "not a coercion variable."
{-# INLINE coVarCoT #-}

-- | Rewrite the 'CoVar' child of a coercion of the form: @CoVarCo@ 'CoVar'
coVarCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoVar -> Rewrite c m Coercion
coVarCoR r = coVarCoT (CoVarCo <$> r)
{-# INLINE coVarCoR #-}

-- | Transform a coercion of the form: @AxiomInstCo@ ('CoAxiom' 'Branched') 'BranchIndex' ['Coercion']
axiomInstCoT :: (ExtendPath c Crumb, Monad m) => Transform c m (CoAxiom Branched) a1 -> Transform c m BranchIndex a2 -> (Int -> Transform c m Coercion a3) -> (a1 -> a2 -> [a3] -> b) -> Transform c m Coercion b
axiomInstCoT t1 t2 ts f = transform $ \ c -> \case
                                                AxiomInstCo ax idx coes -> f <$> applyT t1 (c @@ AxiomInstCo_Axiom) ax <*> applyT t2 (c @@ AxiomInstCo_Index) idx <*> sequence [ applyT (ts n) (c @@ AxiomInstCo_Arg n) co | (co,n) <- zip coes [0..] ]
                                                _                       -> fail "not a coercion axiom instantiation."
{-# INLINE axiomInstCoT #-}

-- | Rewrite all children of a coercion of the form: @AxiomInstCo@ ('CoAxiom' 'Branched') 'BranchIndex' ['Coercion']
axiomInstCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m (CoAxiom Branched) -> Rewrite c m BranchIndex -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion
axiomInstCoAllR r1 r2 rs = axiomInstCoT r1 r2 rs AxiomInstCo
{-# INLINE axiomInstCoAllR #-}

-- | Rewrite any children of a coercion of the form: @AxiomInstCo@ ('CoAxiom' 'Branched') 'BranchIndex' ['Coercion']
axiomInstCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m (CoAxiom Branched) -> Rewrite c m BranchIndex -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion
axiomInstCoAnyR r1 r2 rs = unwrapAnyR $ axiomInstCoAllR (wrapAnyR r1) (wrapAnyR r2) (wrapAnyR . rs)
{-# INLINE axiomInstCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @AxiomInstCo@ ('CoAxiom' 'Branched') 'BranchIndex' ['Coercion']
axiomInstCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m (CoAxiom Branched) -> Rewrite c m BranchIndex -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion
axiomInstCoOneR r1 r2 rs = unwrapOneR $ axiomInstCoAllR (wrapOneR r1) (wrapOneR r2) (wrapOneR . rs)
{-# INLINE axiomInstCoOneR #-}


-- | Transform a coercion of the form: @SymCo@ 'Coercion'
symCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion b -> Transform c m Coercion b
symCoT t = transform $ \ c -> \case
                                   SymCo co -> applyT t (c @@ SymCo_Co) co
                                   _        -> fail "not a symmetric coercion."
{-# INLINE symCoT #-}

-- | Rewrite the 'Coercion' child of a coercion of the form: @SymCo@ 'Coercion'
symCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion
symCoR r = symCoT (SymCo <$> r)
{-# INLINE symCoR #-}


-- | Transform a coercion of the form: @TransCo@ 'Coercion' 'Coercion'
transCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b
transCoT t1 t2 f = transform $ \ c -> \case
                                          TransCo co1 co2 -> f <$> applyT t1 (c @@ TransCo_Left) co1 <*> applyT t2 (c @@ TransCo_Right) co2
                                          _               -> fail "not a transitive coercion."
{-# INLINE transCoT #-}

-- | Rewrite all children of a coercion of the form: @TransCo@ 'Coercion' 'Coercion'
transCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion
transCoAllR r1 r2 = transCoT r1 r2 TransCo
{-# INLINE transCoAllR #-}

-- | Rewrite any children of a coercion of the form: @TransCo@ 'Coercion' 'Coercion'
transCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion
transCoAnyR r1 r2 = unwrapAnyR $ transCoAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE transCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @TransCo@ 'Coercion' 'Coercion'
transCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion
transCoOneR r1 r2 = unwrapOneR $ transCoAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE transCoOneR #-}


-- | Transform a coercion of the form: @NthCo@ 'Int' 'Coercion'
nthCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Int a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b
nthCoT t1 t2 f = transform $ \ c -> \case
                                          NthCo n co -> f <$> applyT t1 (c @@ NthCo_Int) n <*> applyT t2 (c @@ NthCo_Co) co
                                          _          -> fail "not an Nth coercion."
{-# INLINE nthCoT #-}

-- | Rewrite all children of a coercion of the form: @NthCo@ 'Int' 'Coercion'
nthCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion
nthCoAllR r1 r2 = nthCoT r1 r2 NthCo
{-# INLINE nthCoAllR #-}

-- | Rewrite any children of a coercion of the form: @NthCo@ 'Int' 'Coercion'
nthCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion
nthCoAnyR r1 r2 = unwrapAnyR $ nthCoAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE nthCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @NthCo@ 'Int' 'Coercion'
nthCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion
nthCoOneR r1 r2 = unwrapOneR $ nthCoAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE nthCoOneR #-}


-- | Transform a coercion of the form: @LRCo@ 'LeftOrRight' 'Coercion'
lrCoT :: (ExtendPath c Crumb, Monad m) => Transform c m LeftOrRight a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b
lrCoT t1 t2 f = transform $ \ c -> \case
                                      LRCo lr co -> f <$> applyT t1 (c @@ LRCo_LR) lr <*> applyT t2 (c @@ LRCo_Co) co
                                      _          -> fail "not a left/right coercion."
{-# INLINE lrCoT #-}

-- | Transform all children of a coercion of the form: @LRCo@ 'LeftOrRight' 'Coercion'
lrCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m LeftOrRight -> Rewrite c m Coercion -> Rewrite c m Coercion
lrCoAllR r1 r2 = lrCoT r1 r2 LRCo
{-# INLINE lrCoAllR #-}

-- | Transform any children of a coercion of the form: @LRCo@ 'LeftOrRight' 'Coercion'
lrCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m LeftOrRight -> Rewrite c m Coercion -> Rewrite c m Coercion
lrCoAnyR r1 r2 = unwrapAnyR $ lrCoAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE lrCoAnyR #-}

-- | Transform one child of a coercion of the form: @LRCo@ 'LeftOrRight' 'Coercion'
lrCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m LeftOrRight -> Rewrite c m Coercion -> Rewrite c m Coercion
lrCoOneR r1 r2 = unwrapOneR $ lrCoAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE lrCoOneR #-}


-- | Transform a coercion of the form: @InstCo@ 'Coercion' 'Type'
instCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b
instCoT t1 t2 f = transform $ \ c -> \case
                                          InstCo co ty -> f <$> applyT t1 (c @@ InstCo_Co) co <*> applyT t2 (c @@ InstCo_Type) ty
                                          _            -> fail "not a coercion instantiation."
{-# INLINE instCoT #-}

-- | Rewrite all children of a coercion of the form: @InstCo@ 'Coercion' 'Type'
instCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion
instCoAllR r1 r2 = instCoT r1 r2 InstCo
{-# INLINE instCoAllR #-}

-- | Rewrite any children of a coercion of the form: @InstCo@ 'Coercion' 'Type'
instCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion
instCoAnyR r1 r2 = unwrapAnyR $ instCoAllR (wrapAnyR r1) (wrapAnyR r2)
{-# INLINE instCoAnyR #-}

-- | Rewrite one child of a coercion of the form: @InstCo@ 'Coercion' 'Type'
instCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion
instCoOneR r1 r2 = unwrapOneR $ instCoAllR (wrapOneR r1) (wrapOneR r2)
{-# INLINE instCoOneR #-}

---------------------------------------------------------------------

-- | Transform a clause of the form: @Conj@ 'Quantified' 'Quantified'
conjT :: (ExtendPath c Crumb, Monad m) => Transform c m Quantified a1 -> Transform c m Quantified a2 -> (a1 -> a2 -> b) -> Transform c m Clause b
conjT t1 t2 f = transform $ \ c -> \case
                                     Conj q1 q2 -> f <$> applyT t1 (c @@ Conj_Lhs) q1 <*> applyT t2 (c @@ Conj_Rhs) q2
                                     _          -> fail "not a conjunction."
{-# INLINE conjT #-}

-- | Rewrite all children of a clause of the form: : @Conj@ 'Quantified' 'Quantified'
conjAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Quantified -> Rewrite c m Quantified -> Rewrite c m Clause
conjAllR r1 r2 = conjT r1 r2 Conj
{-# INLINE conjAllR #-}


-- | Transform a clause of the form: @Disj@ 'Quantified' 'Quantified'
disjT :: (ExtendPath c Crumb, Monad m) => Transform c m Quantified a1 -> Transform c m Quantified a2 -> (a1 -> a2 -> b) -> Transform c m Clause b
disjT t1 t2 f = transform $ \ c -> \case
                                     Conj q1 q2 -> f <$> applyT t1 (c @@ Disj_Lhs) q1 <*> applyT t2 (c @@ Disj_Rhs) q2
                                     _          -> fail "not a disjunction."
{-# INLINE disjT #-}

-- | Rewrite all children of a clause of the form: : @Disj@ 'Quantified' 'Quantified'
disjAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Quantified -> Rewrite c m Quantified -> Rewrite c m Clause
disjAllR r1 r2 = disjT r1 r2 Disj
{-# INLINE disjAllR #-}


-- | Transform a clause of the form: @Impl@ 'Quantified' 'Quantified'
implT :: (ExtendPath c Crumb, Monad m) => Transform c m Quantified a1 -> Transform c m Quantified a2 -> (a1 -> a2 -> b) -> Transform c m Clause b
implT t1 t2 f = transform $ \ c -> \case
                                     Impl q1 q2 -> f <$> applyT t1 (c @@ Impl_Lhs) q1 <*> applyT t2 (c @@ Impl_Rhs) q2
                                     _          -> fail "not an implication."
{-# INLINE implT #-}

-- | Rewrite all children of a clause of the form: : @Impl@ 'Quantified' 'Quantified'
implAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Quantified -> Rewrite c m Quantified -> Rewrite c m Clause
implAllR r1 r2 = implT r1 r2 Impl
{-# INLINE implAllR #-}

-- | Transform a clause of the form: @Equiv@ 'CoreExpr' 'CoreExpr'
equivT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreExpr a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m Clause b
equivT t1 t2 f = transform $ \ c -> \case
                                     Equiv e1 e2 -> f <$> applyT t1 (c @@ Eq_Lhs) e1 <*> applyT t2 (c @@ Eq_Rhs) e2
                                     _           -> fail "not an equivalence."
{-# INLINE equivT #-}

-- | Rewrite all children of a clause of the form: : @Equiv@ 'CoreExpr' 'CoreExpr'
equivAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m Clause
equivAllR r1 r2 = equivT r1 r2 Equiv
{-# INLINE equivAllR #-}

---------------------------------------------------------------------

-- | Transform a quantifier of the form: @Quantified@ 'Clause'
quantifiedT :: (ExtendPath c Crumb, AddBindings c, ReadPath c Crumb, Monad m) => Transform c m [CoreBndr] a1 -> Transform c m Clause a2 -> (a1 -> a2 -> b) -> Transform c m Quantified b
quantifiedT t1 t2 f = transform $ \ c (Quantified bs cl) -> let c' = foldl (flip addLambdaBinding) c bs
                                                             in f <$> applyT t1 c bs <*> applyT t2 (c' @@ Forall_Body) cl
{-# INLINE quantifiedT #-}

-- | Rewrite the clause of a quantifier of the form: @Quantified@ 'Clause'
quantifiedR :: (ExtendPath c Crumb, AddBindings c, ReadPath c Crumb, Monad m) => Rewrite c m [CoreBndr] -> Rewrite c m Clause -> Rewrite c m Quantified
quantifiedR r1 r2 = quantifiedT r1 r2 Quantified
{-# INLINE quantifiedR #-}

---------------------------------------------------------------------

instance HasDynFlags m => HasDynFlags (Transform c m a) where
    getDynFlags = constT getDynFlags

---------------------------------------------------------------------

-- | Original clause passed to function so it can decide how to handle connective.
clauseT :: (Monad m, ExtendPath c Crumb) => Transform c m LCore a -> Transform c m LCore b -> (Clause -> a -> b -> d) -> Transform c m Clause d
clauseT t1 t2 f = readerT $ \ cl -> case cl of
                                      Conj{}  -> conjT  (extractT t1) (extractT t2) (f cl)
                                      Disj{}  -> disjT  (extractT t1) (extractT t2) (f cl)
                                      Impl{}  -> implT  (extractT t1) (extractT t2) (f cl)
                                      Equiv{} -> equivT (extractT t1) (extractT t2) (f cl)

clauseR :: (Monad m, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m LCore -> Rewrite c m Clause
clauseR r1 r2 = readerT $ \case
                             Conj{}  -> conjAllR (extractR r1) (extractR r2)
                             Disj{}  -> disjAllR (extractR r1) (extractR r2)
                             Impl{}  -> implAllR (extractR r1) (extractR r2)
                             Equiv{} -> equivAllR (extractR r1) (extractR r2)

-- | Lift a transformation over '[Var]' into a transformation over the universally quantified variables of a 'Quantified'.
forallVarsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m [Var] b -> Transform c m Quantified b
forallVarsT t = quantifiedT t successT const