module HERMIT.Kure.SumTypes
(
Core(..)
, TyCo(..)
, CoreTC(..)
, coreSyntaxEq
, tyCoSyntaxEq
, coreTCSyntaxEq
, coreAlphaEq
, tyCoAlphaEq
, coreTCAlphaEq
, freeVarsCore
, freeVarsTyCo
, freeVarsCoreTC
, promoteModGutsT
, promoteProgT
, promoteBindT
, promoteDefT
, promoteExprT
, promoteAltT
, promoteTypeT
, promoteCoercionT
, promoteModGutsR
, promoteProgR
, promoteBindR
, promoteDefR
, promoteExprR
, promoteAltR
, promoteTypeR
, promoteCoercionR
, promoteExprBiR
)
where
import Language.KURE.Translate
import Language.KURE.Injection
import Language.KURE.BiTranslate
import HERMIT.Core
import HERMIT.GHC
data Core = GutsCore ModGuts
| ProgCore CoreProg
| BindCore CoreBind
| DefCore CoreDef
| ExprCore CoreExpr
| AltCore CoreAlt
data TyCo = TypeCore Type
| CoercionCore Coercion
data CoreTC = Core Core
| TyCo TyCo
coreAlphaEq :: Core -> Core -> Bool
coreAlphaEq (GutsCore g1) (GutsCore g2) = progAlphaEq (bindsToProg $ mg_binds g1) (bindsToProg $ mg_binds g2)
coreAlphaEq (ProgCore p1) (ProgCore p2) = progAlphaEq p1 p2
coreAlphaEq (BindCore b1) (BindCore b2) = bindAlphaEq b1 b2
coreAlphaEq (DefCore d1) (DefCore d2) = defAlphaEq d1 d2
coreAlphaEq (ExprCore e1) (ExprCore e2) = exprAlphaEq e1 e2
coreAlphaEq (AltCore a1) (AltCore a2) = altAlphaEq a1 a2
coreAlphaEq _ _ = False
tyCoAlphaEq :: TyCo -> TyCo -> Bool
tyCoAlphaEq (TypeCore ty1) (TypeCore ty2) = typeAlphaEq ty1 ty2
tyCoAlphaEq (CoercionCore co1) (CoercionCore co2) = coercionAlphaEq co1 co2
tyCoAlphaEq _ _ = False
coreTCAlphaEq :: CoreTC -> CoreTC -> Bool
coreTCAlphaEq (Core c1) (Core c2) = coreAlphaEq c1 c2
coreTCAlphaEq (TyCo tc1) (TyCo tc2) = tyCoAlphaEq tc1 tc2
coreTCAlphaEq _ _ = False
coreSyntaxEq :: Core -> Core -> Bool
coreSyntaxEq (GutsCore g1) (GutsCore g2) = all2 bindSyntaxEq (mg_binds g1) (mg_binds g2)
coreSyntaxEq (ProgCore p1) (ProgCore p2) = progSyntaxEq p1 p2
coreSyntaxEq (BindCore b1) (BindCore b2) = bindSyntaxEq b1 b2
coreSyntaxEq (DefCore d1) (DefCore d2) = defSyntaxEq d1 d2
coreSyntaxEq (ExprCore e1) (ExprCore e2) = exprSyntaxEq e1 e2
coreSyntaxEq (AltCore a1) (AltCore a2) = altSyntaxEq a1 a2
coreSyntaxEq _ _ = False
tyCoSyntaxEq :: TyCo -> TyCo -> Bool
tyCoSyntaxEq (TypeCore ty1) (TypeCore ty2) = typeSyntaxEq ty1 ty2
tyCoSyntaxEq (CoercionCore co1) (CoercionCore co2) = coercionSyntaxEq co1 co2
tyCoSyntaxEq _ _ = False
coreTCSyntaxEq :: CoreTC -> CoreTC -> Bool
coreTCSyntaxEq (Core c1) (Core c2) = coreSyntaxEq c1 c2
coreTCSyntaxEq (TyCo tc1) (TyCo tc2) = tyCoSyntaxEq tc1 tc2
coreTCSyntaxEq _ _ = False
freeVarsCore :: Core -> VarSet
freeVarsCore = \case
GutsCore g -> freeVarsProg (bindsToProg $ mg_binds g)
ProgCore p -> freeVarsProg p
BindCore b -> freeVarsBind b
DefCore d -> freeVarsDef d
ExprCore e -> freeVarsExpr e
AltCore a -> freeVarsAlt a
freeVarsTyCo :: TyCo -> VarSet
freeVarsTyCo = \case
TypeCore ty -> tyVarsOfType ty
CoercionCore co -> tyCoVarsOfCo co
freeVarsCoreTC :: CoreTC -> VarSet
freeVarsCoreTC = \case
TyCo tyco -> freeVarsTyCo tyco
Core core -> freeVarsCore core
instance Injection ModGuts Core where
inject :: ModGuts -> Core
inject = GutsCore
project :: Core -> Maybe ModGuts
project (GutsCore guts) = Just guts
project _ = Nothing
instance Injection CoreProg Core where
inject :: CoreProg -> Core
inject = ProgCore
project :: Core -> Maybe CoreProg
project (ProgCore bds) = Just bds
project _ = Nothing
instance Injection CoreBind Core where
inject :: CoreBind -> Core
inject = BindCore
project :: Core -> Maybe CoreBind
project (BindCore bnd) = Just bnd
project _ = Nothing
instance Injection CoreDef Core where
inject :: CoreDef -> Core
inject = DefCore
project :: Core -> Maybe CoreDef
project (DefCore def) = Just def
project _ = Nothing
instance Injection CoreAlt Core where
inject :: CoreAlt -> Core
inject = AltCore
project :: Core -> Maybe CoreAlt
project (AltCore expr) = Just expr
project _ = Nothing
instance Injection CoreExpr Core where
inject :: CoreExpr -> Core
inject = ExprCore
project :: Core -> Maybe CoreExpr
project (ExprCore expr) = Just expr
project _ = Nothing
instance Injection Type TyCo where
inject :: Type -> TyCo
inject = TypeCore
project :: TyCo -> Maybe Type
project (TypeCore ty) = Just ty
project _ = Nothing
instance Injection Coercion TyCo where
inject :: Coercion -> TyCo
inject = CoercionCore
project :: TyCo -> Maybe Coercion
project (CoercionCore ty) = Just ty
project _ = Nothing
instance Injection Core CoreTC where
inject :: Core -> CoreTC
inject = Core
project :: CoreTC -> Maybe Core
project (Core core) = Just core
project _ = Nothing
instance Injection TyCo CoreTC where
inject :: TyCo -> CoreTC
inject = TyCo
project :: CoreTC -> Maybe TyCo
project (TyCo tyCo) = Just tyCo
project _ = Nothing
instance Injection ModGuts CoreTC where
inject :: ModGuts -> CoreTC
inject = Core . GutsCore
project :: CoreTC -> Maybe ModGuts
project (Core (GutsCore guts)) = Just guts
project _ = Nothing
instance Injection CoreProg CoreTC where
inject :: CoreProg -> CoreTC
inject = Core . ProgCore
project :: CoreTC -> Maybe CoreProg
project (Core (ProgCore bds)) = Just bds
project _ = Nothing
instance Injection CoreBind CoreTC where
inject :: CoreBind -> CoreTC
inject = Core . BindCore
project :: CoreTC -> Maybe CoreBind
project (Core (BindCore bnd)) = Just bnd
project _ = Nothing
instance Injection CoreDef CoreTC where
inject :: CoreDef -> CoreTC
inject = Core . DefCore
project :: CoreTC -> Maybe CoreDef
project (Core (DefCore def)) = Just def
project _ = Nothing
instance Injection CoreAlt CoreTC where
inject :: CoreAlt -> CoreTC
inject = Core . AltCore
project :: CoreTC -> Maybe CoreAlt
project (Core (AltCore expr)) = Just expr
project _ = Nothing
instance Injection CoreExpr CoreTC where
inject :: CoreExpr -> CoreTC
inject = Core . ExprCore
project :: CoreTC -> Maybe CoreExpr
project (Core (ExprCore expr)) = Just expr
project _ = Nothing
instance Injection Type CoreTC where
inject :: Type -> CoreTC
inject = TyCo . TypeCore
project :: CoreTC -> Maybe Type
project (TyCo (TypeCore ty)) = Just ty
project _ = Nothing
instance Injection Coercion CoreTC where
inject :: Coercion -> CoreTC
inject = TyCo . CoercionCore
project :: CoreTC -> Maybe Coercion
project (TyCo (CoercionCore ty)) = Just ty
project _ = Nothing
promoteModGutsT :: (Monad m, Injection ModGuts g) => Translate c m ModGuts b -> Translate c m g b
promoteModGutsT = promoteWithFailMsgT "This translate can only succeed at the module level."
promoteProgT :: (Monad m, Injection CoreProg g) => Translate c m CoreProg b -> Translate c m g b
promoteProgT = promoteWithFailMsgT "This translate can only succeed at program nodes (the top-level)."
promoteBindT :: (Monad m, Injection CoreBind g) => Translate c m CoreBind b -> Translate c m g b
promoteBindT = promoteWithFailMsgT "This translate can only succeed at binding group nodes."
promoteDefT :: (Monad m, Injection CoreDef g) => Translate c m CoreDef b -> Translate c m g b
promoteDefT = promoteWithFailMsgT "This translate can only succeed at recursive definition nodes."
promoteAltT :: (Monad m, Injection CoreAlt g) => Translate c m CoreAlt b -> Translate c m g b
promoteAltT = promoteWithFailMsgT "This translate can only succeed at case alternative nodes."
promoteExprT :: (Monad m, Injection CoreExpr g) => Translate c m CoreExpr b -> Translate c m g b
promoteExprT = promoteWithFailMsgT "This translate can only succeed at expression nodes."
promoteTypeT :: (Monad m, Injection Type g) => Translate c m Type b -> Translate c m g b
promoteTypeT = promoteWithFailMsgT "This translate can only succeed at type nodes."
promoteCoercionT :: (Monad m, Injection Coercion g) => Translate c m Coercion b -> Translate c m g b
promoteCoercionT = promoteWithFailMsgT "This translate can only succeed at coercion nodes."
promoteModGutsR :: (Monad m, Injection ModGuts g) => Rewrite c m ModGuts -> Rewrite c m g
promoteModGutsR = promoteWithFailMsgR "This rewrite can only succeed at the module level."
promoteProgR :: (Monad m, Injection CoreProg g) => Rewrite c m CoreProg -> Rewrite c m g
promoteProgR = promoteWithFailMsgR "This rewrite can only succeed at program nodes (the top-level)."
promoteBindR :: (Monad m, Injection CoreBind g) => Rewrite c m CoreBind -> Rewrite c m g
promoteBindR = promoteWithFailMsgR "This rewrite can only succeed at binding group nodes."
promoteDefR :: (Monad m, Injection CoreDef g) => Rewrite c m CoreDef -> Rewrite c m g
promoteDefR = promoteWithFailMsgR "This rewrite can only succeed at recursive definition nodes."
promoteAltR :: (Monad m, Injection CoreAlt g) => Rewrite c m CoreAlt -> Rewrite c m g
promoteAltR = promoteWithFailMsgR "This rewrite can only succeed at case alternative nodes."
promoteExprR :: (Monad m, Injection CoreExpr g) => Rewrite c m CoreExpr -> Rewrite c m g
promoteExprR = promoteWithFailMsgR "This rewrite can only succeed at expression nodes."
promoteTypeR :: (Monad m, Injection Type g) => Rewrite c m Type -> Rewrite c m g
promoteTypeR = promoteWithFailMsgR "This rewrite can only succeed at type nodes."
promoteCoercionR :: (Monad m, Injection Coercion g) => Rewrite c m Coercion -> Rewrite c m g
promoteCoercionR = promoteWithFailMsgR "This rewrite can only succeed at coercion nodes."
promoteExprBiR :: (Monad m, Injection CoreExpr g) => BiRewrite c m CoreExpr -> BiRewrite c m g
promoteExprBiR b = bidirectional (promoteExprR $ forwardT b) (promoteExprR $ backwardT b)