module HERMIT.Kure.Universes
(
Core(..)
, TyCo(..)
, LCore(..)
, LCoreTC(..)
, CoreTC(..)
, coreSyntaxEq
, tyCoSyntaxEq
, coreTCSyntaxEq
, lcoreSyntaxEq
, lcoreTCSyntaxEq
, coreAlphaEq
, tyCoAlphaEq
, coreTCAlphaEq
, freeVarsCore
, freeVarsTyCo
, freeVarsCoreTC
, promoteModGutsT
, promoteProgT
, promoteBindT
, promoteDefT
, promoteExprT
, promoteAltT
, promoteTypeT
, promoteCoercionT
, promoteQuantifiedT
, promoteClauseT
, promoteCoreT
, promoteLCoreT
, promoteCoreTCT
, promoteModGutsR
, promoteProgR
, promoteBindR
, promoteDefR
, promoteExprR
, promoteAltR
, promoteTypeR
, promoteCoercionR
, promoteQuantifiedR
, promoteClauseR
, promoteCoreR
, promoteLCoreR
, promoteCoreTCR
, promoteExprBiR
) where
import Language.KURE.Transform
import Language.KURE.Injection
import Language.KURE.BiTransform
import HERMIT.Core
import HERMIT.GHC
import HERMIT.Lemma
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
data LCore = LQuantified Quantified
| LClause Clause
| LCore Core
data LCoreTC = LTCCore LCore
| LTCTyCo 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
lcoreSyntaxEq :: LCore -> LCore -> Bool
lcoreSyntaxEq (LCore c1) (LCore c2) = coreSyntaxEq c1 c2
lcoreSyntaxEq (LClause cl1) (LClause cl2) = clauseSyntaxEq cl1 cl2
lcoreSyntaxEq (LQuantified q1) (LQuantified q2) = quantifiedSyntaxEq q1 q2
lcoreSyntaxEq _ _ = False
lcoreTCSyntaxEq :: LCoreTC -> LCoreTC -> Bool
lcoreTCSyntaxEq (LTCCore lc1) (LTCCore lc2) = lcoreSyntaxEq lc1 lc2
lcoreTCSyntaxEq (LTCTyCo tc1) (LTCTyCo tc2) = tyCoSyntaxEq tc1 tc2
lcoreTCSyntaxEq _ _ = 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 LCore where
inject :: Core -> LCore
inject = LCore
project :: LCore -> Maybe Core
project (LCore c) = Just c
project _ = Nothing
instance Injection Clause LCore where
inject :: Clause -> LCore
inject = LClause
project :: LCore -> Maybe Clause
project (LClause cl) = Just cl
project _ = Nothing
instance Injection Quantified LCore where
inject :: Quantified -> LCore
inject = LQuantified
project :: LCore -> Maybe Quantified
project (LQuantified q) = Just q
project _ = Nothing
instance Injection LCore LCoreTC where
inject :: LCore -> LCoreTC
inject = LTCCore
project :: LCoreTC -> Maybe LCore
project (LTCCore core) = Just core
project _ = Nothing
instance Injection TyCo LCoreTC where
inject :: TyCo -> LCoreTC
inject = LTCTyCo
project :: LCoreTC -> Maybe TyCo
project (LTCTyCo tyCo) = Just tyCo
project _ = Nothing
instance Injection ModGuts LCore where
inject :: ModGuts -> LCore
inject = LCore . inject
project :: LCore -> Maybe ModGuts
project (LCore c) = project c
project _ = Nothing
instance Injection CoreProg LCore where
inject :: CoreProg -> LCore
inject = LCore . inject
project :: LCore -> Maybe CoreProg
project (LCore c) = project c
project _ = Nothing
instance Injection CoreExpr LCore where
inject :: CoreExpr -> LCore
inject = LCore . inject
project :: LCore -> Maybe CoreExpr
project (LCore c) = project c
project _ = Nothing
instance Injection CoreBind LCore where
inject :: CoreBind -> LCore
inject = LCore . inject
project :: LCore -> Maybe CoreBind
project (LCore c) = project c
project _ = Nothing
instance Injection CoreDef LCore where
inject :: CoreDef -> LCore
inject = LCore . inject
project :: LCore -> Maybe CoreDef
project (LCore c) = project c
project _ = Nothing
instance Injection CoreAlt LCore where
inject :: CoreAlt -> LCore
inject = LCore . inject
project :: LCore -> Maybe CoreAlt
project (LCore c) = project c
project _ = Nothing
instance Injection Quantified LCoreTC where
inject :: Quantified -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe Quantified
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection Clause LCoreTC where
inject :: Clause -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe Clause
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection Core LCoreTC where
inject :: Core -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe Core
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection ModGuts LCoreTC where
inject :: ModGuts -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe ModGuts
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection CoreProg LCoreTC where
inject :: CoreProg -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe CoreProg
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection CoreExpr LCoreTC where
inject :: CoreExpr -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe CoreExpr
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection CoreBind LCoreTC where
inject :: CoreBind -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe CoreBind
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection CoreDef LCoreTC where
inject :: CoreDef -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe CoreDef
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection CoreAlt LCoreTC where
inject :: CoreAlt -> LCoreTC
inject = LTCCore . inject
project :: LCoreTC -> Maybe CoreAlt
project (LTCCore lc) = project lc
project _ = Nothing
instance Injection Type LCoreTC where
inject :: Type -> LCoreTC
inject = LTCTyCo . inject
project :: LCoreTC -> Maybe Type
project (LTCTyCo tc) = project tc
project _ = Nothing
instance Injection Coercion LCoreTC where
inject :: Coercion -> LCoreTC
inject = LTCTyCo . inject
project :: LCoreTC -> Maybe Coercion
project (LTCTyCo tc) = project tc
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
instance Injection CoreTC LCoreTC where
inject :: CoreTC -> LCoreTC
inject (Core c) = LTCCore (LCore c)
inject (TyCo tc) = LTCTyCo tc
project :: LCoreTC -> Maybe CoreTC
project (LTCCore c) = Core `fmap` project c
project (LTCTyCo tc) = Just (TyCo tc)
promoteModGutsT :: (Monad m, Injection ModGuts g) => Transform c m ModGuts b -> Transform c m g b
promoteModGutsT = promoteWithFailMsgT "This translate can only succeed at the module level."
promoteProgT :: (Monad m, Injection CoreProg g) => Transform c m CoreProg b -> Transform c m g b
promoteProgT = promoteWithFailMsgT "This translate can only succeed at program nodes (the top-level)."
promoteBindT :: (Monad m, Injection CoreBind g) => Transform c m CoreBind b -> Transform c m g b
promoteBindT = promoteWithFailMsgT "This translate can only succeed at binding group nodes."
promoteDefT :: (Monad m, Injection CoreDef g) => Transform c m CoreDef b -> Transform c m g b
promoteDefT = promoteWithFailMsgT "This translate can only succeed at recursive definition nodes."
promoteAltT :: (Monad m, Injection CoreAlt g) => Transform c m CoreAlt b -> Transform c m g b
promoteAltT = promoteWithFailMsgT "This translate can only succeed at case alternative nodes."
promoteExprT :: (Monad m, Injection CoreExpr g) => Transform c m CoreExpr b -> Transform c m g b
promoteExprT = promoteWithFailMsgT "This translate can only succeed at expression nodes."
promoteTypeT :: (Monad m, Injection Type g) => Transform c m Type b -> Transform c m g b
promoteTypeT = promoteWithFailMsgT "This translate can only succeed at type nodes."
promoteCoercionT :: (Monad m, Injection Coercion g) => Transform c m Coercion b -> Transform c m g b
promoteCoercionT = promoteWithFailMsgT "This translate can only succeed at coercion nodes."
promoteQuantifiedT :: (Monad m, Injection Quantified g) => Transform c m Quantified b -> Transform c m g b
promoteQuantifiedT = promoteWithFailMsgT "This translate can only succeed at quantified nodes."
promoteClauseT :: (Monad m, Injection Clause g) => Transform c m Clause b -> Transform c m g b
promoteClauseT = promoteWithFailMsgT "This translate can only succeed at clause nodes."
promoteCoreT :: (Monad m, Injection Core g) => Transform c m Core b -> Transform c m g b
promoteCoreT = promoteWithFailMsgT "This translate can only succeed at core nodes."
promoteLCoreT :: (Monad m, Injection LCore g) => Transform c m LCore b -> Transform c m g b
promoteLCoreT = promoteWithFailMsgT "This translate can only succeed at lemma or core nodes."
promoteCoreTCT :: (Monad m, Injection CoreTC g) => Transform c m CoreTC b -> Transform c m g b
promoteCoreTCT = promoteWithFailMsgT "This translate can only succeed at core 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."
promoteQuantifiedR :: (Monad m, Injection Quantified g) => Rewrite c m Quantified -> Rewrite c m g
promoteQuantifiedR = promoteWithFailMsgR "This rewrite can only succeed at quantified nodes."
promoteClauseR :: (Monad m, Injection Clause g) => Rewrite c m Clause -> Rewrite c m g
promoteClauseR = promoteWithFailMsgR "This rewrite can only succeed at quantified nodes."
promoteCoreR :: (Monad m, Injection Core g) => Rewrite c m Core -> Rewrite c m g
promoteCoreR = promoteWithFailMsgR "This rewrite can only succeed at core nodes."
promoteLCoreR :: (Monad m, Injection LCore g) => Rewrite c m LCore -> Rewrite c m g
promoteLCoreR = promoteWithFailMsgR "This rewrite can only succeed at lemma or core nodes."
promoteCoreTCR :: (Monad m, Injection CoreTC g) => Rewrite c m CoreTC -> Rewrite c m g
promoteCoreTCR = promoteWithFailMsgR "This rewrite can only succeed at core nodes."
promoteExprBiR :: (Monad m, Injection CoreExpr g) => BiRewrite c m CoreExpr -> BiRewrite c m g
promoteExprBiR = promoteWithFailMsgBiR "This rewrite can only succeed at expression nodes."