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
, 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
, quantifiedT, quantifiedR
, clauseT, clauseR, forallVarsT
, (<$>)
, (<*>)
) 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
(<$>) :: 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, 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
where
allRquantified :: MonadCatch m => Rewrite c m Quantified
allRquantified = quantifiedR idR (extractR r)
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)
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)
LTCTyCo tyCo -> inject <$> applyT (allR $ extractR r) c tyCo
where
allRquantified :: MonadCatch m => Rewrite c m Quantified
allRquantified = quantifiedR idR (extractR r)
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)
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 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."
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
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."
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
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."
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
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
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
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
instance HasDynFlags m => HasDynFlags (Transform c m a) where
getDynFlags = constT getDynFlags
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)
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