module HERMIT.Kure
(
module Language.KURE
, module Language.KURE.BiTransform
, module Language.KURE.Lens
, module Language.KURE.ExtendableContext
, module Language.KURE.Pathfinder
, module HERMIT.Kure.Universes
, TransformH
, RewriteH
, BiRewriteH
, LensH
, PathH
, inContextM
, modGutsT, modGutsR
, progNilT
, progConsT, progConsAllR, progConsAnyR, progConsOneR
, nonRecT, nonRecAllR, nonRecAnyR, nonRecOneR
, recT, recAllR, recAnyR, recOneR
, defT, defAllR, defAnyR, defOneR
, altT, altAllR, altAnyR, altOneR
, 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
, 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
, progBindsT, progBindsAllR, progBindsAnyR, progBindsOneR
, tyVarT, tyVarR
, litTyT, litTyR
, appTyT, appTyAllR, appTyAnyR, appTyOneR
, funTyT, funTyAllR, funTyAnyR, funTyOneR
, forAllTyT, forAllTyAllR, forAllTyAnyR, forAllTyOneR
, tyConAppT, tyConAppAllR, tyConAppAnyR, tyConAppOneR
, 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
, conjT, conjAllR
, disjT, disjAllR
, implT, implAllR
, equivT, equivAllR
, forallT, forallR
, (<$>)
, (<*>)
) where
import Control.Monad (ap, liftM)
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 Prelude.Compat hiding ((<$>), (<*>))
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
(<$>) :: Monad m => (a -> b) -> m a -> m b
(<$>) = liftM
(<*>) :: Monad m => m (a -> b) -> m a -> m b
(<*>) = ap
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)
allRprog :: MonadCatch m => Rewrite c m CoreProg
allRprog = readerT $ \case
ProgCons{} -> progConsAllR (extractR r) (extractR r)
_ -> idR
allRbind :: MonadCatch m => Rewrite c m CoreBind
allRbind = readerT $ \case
NonRec{} -> nonRecAllR idR (extractR r)
Rec _ -> recAllR (const $ extractR r)
allRdef :: MonadCatch m => Rewrite c m CoreDef
allRdef = defAllR idR (extractR r)
allRalt :: MonadCatch m => Rewrite c m CoreAlt
allRalt = altAllR idR (const idR) (extractR r)
allRexpr :: MonadCatch m => Rewrite c m CoreExpr
allRexpr = readerT $ \case
App{} -> appAllR (extractR r) (extractR r)
Lam{} -> lamAllR idR (extractR r)
Let{} -> letAllR (extractR r) (extractR r)
Case{} -> caseAllR (extractR r) idR idR (const $ extractR r)
Cast{} -> castAllR (extractR r) idR
Tick{} -> tickAllR idR (extractR r)
_ -> idR
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
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
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
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)
AppCo{} -> appCoAllR (extractR r) (extractR r)
ForAllCo{} -> forAllCoAllR idR (extractR r)
SymCo{} -> symCoR (extractR r)
TransCo{} -> transCoAllR (extractR r) (extractR r)
InstCo{} -> instCoAllR (extractR r) (extractR r)
NthCo{} -> nthCoAllR idR (extractR r)
LRCo{} -> lrCoAllR idR (extractR r)
AxiomInstCo{} -> axiomInstCoAllR idR idR (const $ extractR r)
_ -> idR
instance (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext 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
LClause cl -> inject <$> applyT allRclause c cl
LCore core -> inject <$> applyT (allR $ extractR r) c core
where
allRclause :: MonadCatch m => Rewrite c m Clause
allRclause = readerT $ \case
Forall{} -> forallR idR (extractR r)
Conj{} -> conjAllR (extractR r) (extractR r)
Disj{} -> disjAllR (extractR r) (extractR r)
Impl{} -> implAllR (extractR r) (extractR r)
Equiv{} -> equivAllR (extractR r) (extractR r)
CTrue -> return CTrue
instance (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext 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 (LClause cl) -> inject <$> applyT allRclause c cl
LTCCore (LCore core) -> inject <$> applyT (allR (extractR r :: Rewrite c m CoreTC)) c (Core core)
LTCTyCo tyCo -> inject <$> applyT (allR $ extractR r) c tyCo
where
allRclause :: MonadCatch m => Rewrite c m Clause
allRclause = readerT $ \case
Forall{} -> forallR idR (extractR r)
Conj{} -> conjAllR (extractR r) (extractR r)
Disj{} -> disjAllR (extractR r) (extractR r)
Impl{} -> implAllR (extractR r) (extractR r)
Equiv{} -> equivAllR (extractR r) (extractR r)
CTrue -> return CTrue
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
where
allRmodguts :: MonadCatch m => Rewrite c m ModGuts
allRmodguts = modGutsR (extractR r)
allRprog :: MonadCatch m => Rewrite c m CoreProg
allRprog = readerT $ \case
ProgCons{} -> progConsAllR (extractR r) (extractR r)
_ -> idR
allRbind :: MonadCatch m => Rewrite c m CoreBind
allRbind = readerT $ \case
NonRec{} -> nonRecAllR idR (extractR r)
Rec _ -> recAllR (const $ extractR r)
allRdef :: MonadCatch m => Rewrite c m CoreDef
allRdef = defAllR idR (extractR r)
allRalt :: MonadCatch m => Rewrite c m CoreAlt
allRalt = altAllR idR (const idR) (extractR r)
allRexpr :: MonadCatch m => Rewrite c m CoreExpr
allRexpr = readerT $ \case
App{} -> appAllR (extractR r) (extractR r)
Lam{} -> lamAllR idR (extractR r)
Let{} -> letAllR (extractR r) (extractR r)
Case{} -> caseAllR (extractR r) idR (extractR r) (const $ extractR r)
Cast{} -> castAllR (extractR r) (extractR r)
Tick{} -> tickAllR idR (extractR r)
Type{} -> typeR (extractR r)
Coercion{} -> coercionR (extractR r)
_ -> idR
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)
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})
progNilT :: Monad m => b -> Transform c m CoreProg b
progNilT b = contextfreeT $ \case
ProgNil -> return b
ProgCons _ _ -> fail "not an empty program."
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."
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
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)
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)
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."
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
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))
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))
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 ->
f <$> sequence [ applyT (t n) (addDefBindingsExcept n bds c @@ Rec_Def n) (Def i e)
| ((i,e),n) <- zip bds [0..]
]
_ -> fail "not a recursive binding group."
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
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)
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)
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
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
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))
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))
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
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 (,,)
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))
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))
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."
varR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr
varR r = varT (Var <$> r)
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."
litR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Literal -> Rewrite c m CoreExpr
litR r = litT (Lit <$> r)
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."
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
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)
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)
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."
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
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)
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)
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 ->
f <$> applyT t1 (c @@ Let_Bind) bds <*> applyT t2 (addBindingGroup bds c @@ Let_Body) e
_ -> fail "not a let node."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
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."
typeR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m CoreExpr
typeR r = typeT (Type <$> r)
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."
coercionR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m CoreExpr
coercionR r = coercionT (Coercion <$> r)
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)
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)
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)
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)
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) (,))
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))
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))
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))
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)
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
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
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
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
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
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
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
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
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
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
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
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)
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
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
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
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
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
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
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
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
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
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
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
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 (,,))
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)
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)
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)
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)) (:)
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
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)
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)
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."
tyVarR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyVar -> Rewrite c m Type
tyVarR r = tyVarT (TyVarTy <$> r)
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."
litTyR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyLit -> Rewrite c m Type
litTyR r = litTyT (LitTy <$> r)
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."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
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."
reflR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Coercion
reflR r = reflT r Refl
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."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
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."
coVarCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoVar -> Rewrite c m Coercion
coVarCoR r = coVarCoT (CoVarCo <$> r)
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."
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
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)
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)
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."
symCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion
symCoR r = symCoT (SymCo <$> r)
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."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
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."
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
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)
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)
conjT :: (ExtendPath c Crumb, Monad m) => Transform c m Clause a1 -> Transform c m Clause 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."
conjAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Clause -> Rewrite c m Clause -> Rewrite c m Clause
conjAllR r1 r2 = conjT r1 r2 Conj
disjT :: (ExtendPath c Crumb, Monad m) => Transform c m Clause a1 -> Transform c m Clause 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."
disjAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Clause -> Rewrite c m Clause -> Rewrite c m Clause
disjAllR r1 r2 = disjT r1 r2 Disj
implT :: (ExtendPath c Crumb, LemmaContext c, Monad m)
=> Transform c m Clause a1 -> Transform c m Clause a2 -> (LemmaName -> a1 -> a2 -> b) -> Transform c m Clause b
implT t1 t2 f = transform $ \ c -> \case
Impl nm q1 q2 -> let l = Lemma q1 BuiltIn NotUsed
in f nm <$> applyT t1 (c @@ Impl_Lhs) q1
<*> applyT t2 (addAntecedent nm l c @@ Impl_Rhs) q2
_ -> fail "not an implication."
implAllR :: (ExtendPath c Crumb, LemmaContext c, Monad m)
=> Rewrite c m Clause -> Rewrite c m Clause -> Rewrite c m Clause
implAllR r1 r2 = implT r1 r2 Impl
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."
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
forallT :: (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 Clause b
forallT t1 t2 f = transform $ \ c -> \case
Forall bs cl -> let c' = foldl (flip addLambdaBinding) c bs
in f <$> applyT t1 c bs <*> applyT t2 (c' @@ Forall_Body) cl
_ -> fail "not a quantified clause."
forallR :: (ExtendPath c Crumb, AddBindings c, ReadPath c Crumb, Monad m)
=> Rewrite c m [CoreBndr] -> Rewrite c m Clause -> Rewrite c m Clause
forallR r1 r2 = forallT r1 r2 mkForall
instance HasDynFlags m => HasDynFlags (Transform c m a) where
getDynFlags = constT getDynFlags
inContextM :: c -> Transform c m () a -> m a
inContextM c t = applyT t c ()