Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data CoreProg
- data CoreDef = Def Id CoreExpr
- type CoreTickish = Tickish Id
- progSyntaxEq :: CoreProg -> CoreProg -> Bool
- bindSyntaxEq :: CoreBind -> CoreBind -> Bool
- defSyntaxEq :: CoreDef -> CoreDef -> Bool
- exprSyntaxEq :: CoreExpr -> CoreExpr -> Bool
- altSyntaxEq :: CoreAlt -> CoreAlt -> Bool
- typeSyntaxEq :: Type -> Type -> Bool
- coercionSyntaxEq :: Coercion -> Coercion -> Bool
- progAlphaEq :: CoreProg -> CoreProg -> Bool
- bindAlphaEq :: CoreBind -> CoreBind -> Bool
- defAlphaEq :: CoreDef -> CoreDef -> Bool
- exprAlphaEq :: CoreExpr -> CoreExpr -> Bool
- altAlphaEq :: CoreAlt -> CoreAlt -> Bool
- typeAlphaEq :: Type -> Type -> Bool
- coercionAlphaEq :: Coercion -> Coercion -> Bool
- defsToRecBind :: [CoreDef] -> CoreBind
- defToIdExpr :: CoreDef -> (Id, CoreExpr)
- progToBinds :: CoreProg -> [CoreBind]
- bindsToProg :: [CoreBind] -> CoreProg
- bindToVarExprs :: CoreBind -> [(Var, CoreExpr)]
- progIds :: CoreProg -> [Id]
- bindVars :: CoreBind -> [Var]
- defId :: CoreDef -> Id
- altVars :: CoreAlt -> [Var]
- freeVarsProg :: CoreProg -> VarSet
- freeVarsBind :: CoreBind -> VarSet
- freeVarsDef :: CoreDef -> VarSet
- freeVarsExpr :: CoreExpr -> VarSet
- freeVarsAlt :: CoreAlt -> VarSet
- freeVarsVar :: Var -> VarSet
- localFreeVarsAlt :: CoreAlt -> VarSet
- freeVarsType :: Type -> TyVarSet
- freeVarsCoercion :: Coercion -> VarSet
- localFreeVarsExpr :: CoreExpr -> VarSet
- freeIdsExpr :: CoreExpr -> IdSet
- localFreeIdsExpr :: CoreExpr -> VarSet
- isCoArg :: CoreExpr -> Bool
- exprKindOrType :: CoreExpr -> KindOrType
- exprTypeM :: Monad m => CoreExpr -> m Type
- endoFunTypeM :: MonadCatch m => Type -> m ([TyVar], Type)
- splitTyConAppM :: Monad m => Type -> m (TyCon, [Type])
- splitFunTypeM :: MonadCatch m => Type -> m ([TyVar], Type, Type)
- endoFunExprTypeM :: MonadCatch m => CoreExpr -> m ([TyVar], Type)
- funExprArgResTypesM :: MonadCatch m => CoreExpr -> m ([TyVar], Type, Type)
- funExprsWithInverseTypes :: MonadCatch m => CoreExpr -> CoreExpr -> m (Type, Type)
- appCount :: CoreExpr -> Int
- mapAlts :: (CoreExpr -> CoreExpr) -> [CoreAlt] -> [CoreAlt]
- substCoreAlt :: Var -> CoreExpr -> CoreAlt -> CoreAlt
- substCoreExpr :: Var -> CoreExpr -> CoreExpr -> CoreExpr
- betaReduceAll :: CoreExpr -> [CoreExpr] -> (CoreExpr, [CoreExpr])
- mkDataConApp :: [Type] -> DataCon -> [Var] -> CoreExpr
- data Crumb
- = ModGuts_Prog
- | ProgCons_Head
- | ProgCons_Tail
- | NonRec_RHS
- | NonRec_Var
- | Rec_Def Int
- | Def_Id
- | Def_RHS
- | Var_Id
- | Lit_Lit
- | App_Fun
- | App_Arg
- | Lam_Var
- | Lam_Body
- | Let_Bind
- | Let_Body
- | Case_Scrutinee
- | Case_Binder
- | Case_Type
- | Case_Alt Int
- | Cast_Expr
- | Cast_Co
- | Tick_Tick
- | Tick_Expr
- | Type_Type
- | Co_Co
- | Alt_Con
- | Alt_Var Int
- | Alt_RHS
- | TyVarTy_TyVar
- | LitTy_TyLit
- | AppTy_Fun
- | AppTy_Arg
- | TyConApp_TyCon
- | TyConApp_Arg Int
- | FunTy_Dom
- | FunTy_CoDom
- | ForAllTy_Var
- | ForAllTy_Body
- | Refl_Type
- | TyConAppCo_TyCon
- | TyConAppCo_Arg Int
- | AppCo_Fun
- | AppCo_Arg
- | ForAllCo_TyVar
- | ForAllCo_Body
- | CoVarCo_CoVar
- | AxiomInstCo_Axiom
- | AxiomInstCo_Index
- | AxiomInstCo_Arg Int
- | UnsafeCo_Left
- | UnsafeCo_Right
- | SymCo_Co
- | TransCo_Left
- | TransCo_Right
- | NthCo_Int
- | NthCo_Co
- | InstCo_Co
- | InstCo_Type
- | LRCo_LR
- | LRCo_Co
- | Forall_Body
- | Conj_Lhs
- | Conj_Rhs
- | Disj_Lhs
- | Disj_Rhs
- | Impl_Lhs
- | Impl_Rhs
- | Eq_Lhs
- | Eq_Rhs
- showCrumbs :: [Crumb] -> String
- leftSibling :: Crumb -> Maybe Crumb
- rightSibling :: Crumb -> Maybe Crumb
Generic Data Type
A program is a telescope of nested binding groups.
That is, each binding scopes over the remainder of the program.
In GHC Core, programs are encoded as [CoreBind
].
This data type is isomorphic.
type CoreTickish = Tickish Id Source
Equality
We define both syntactic equality and alpha equality.
Syntactic Equality
progSyntaxEq :: CoreProg -> CoreProg -> Bool Source
Syntactic Equality of programs.
bindSyntaxEq :: CoreBind -> CoreBind -> Bool Source
Syntactic Equality of binding groups.
defSyntaxEq :: CoreDef -> CoreDef -> Bool Source
Syntactic Equality of recursive definitions.
exprSyntaxEq :: CoreExpr -> CoreExpr -> Bool Source
Syntactic Equality of expressions.
altSyntaxEq :: CoreAlt -> CoreAlt -> Bool Source
Syntactic Equality of case alternatives.
Alpha Equality
progAlphaEq :: CoreProg -> CoreProg -> Bool Source
Alpha equality of programs.
bindAlphaEq :: CoreBind -> CoreBind -> Bool Source
Alpha equality of binding groups.
defAlphaEq :: CoreDef -> CoreDef -> Bool Source
Alpha equality of recursive definitions.
exprAlphaEq :: CoreExpr -> CoreExpr -> Bool Source
Alpha equality of expressions.
altAlphaEq :: CoreAlt -> CoreAlt -> Bool Source
Alpha equality of case alternatives.
typeAlphaEq :: Type -> Type -> Bool Source
Alpha equality of types.
coercionAlphaEq :: Coercion -> Coercion -> Bool Source
Alpha equality of coercions.
Conversions to/from Core
defsToRecBind :: [CoreDef] -> CoreBind Source
Convert a list of recursive definitions into an (isomorphic) recursive binding group.
defToIdExpr :: CoreDef -> (Id, CoreExpr) Source
Convert a definition to an identifier/expression pair.
progToBinds :: CoreProg -> [CoreBind] Source
Get the list of bindings in a program.
bindsToProg :: [CoreBind] -> CoreProg Source
Build a program from a list of bindings. Note that bindings earlier in the list are considered scope over bindings later in the list.
bindToVarExprs :: CoreBind -> [(Var, CoreExpr)] Source
Extract the list of variable/expression pairs from a binding group.
Collecting variable bindings
Collecting free variables
The GHC Function exprFreeVars defined in CoreFVs only returns *locally-defined* free variables. In HERMIT, this is typically not what we want, so we define our own functions. We reuse some of the functionality in CoreFVs, but alas much of it is not exposed, so we have to reimplement some of it. We do not use GHC's exprSomeFreeVars because it does not return the full set of free vars for a Var. It only returns the Var itself, rather than extendVarSet (freeVarsVar v) v like it should.
freeVarsProg :: CoreProg -> VarSet Source
Find all free variables in a program.
freeVarsBind :: CoreBind -> VarSet Source
Find all free identifiers in a binding group, which excludes any variables bound in the group.
freeVarsDef :: CoreDef -> VarSet Source
Find all free variables in a recursive definition, which excludes the bound variable.
freeVarsExpr :: CoreExpr -> VarSet Source
Find all free variables in an expression.
freeVarsAlt :: CoreAlt -> VarSet Source
Find all free variables in a case alternative, which excludes any variables bound in the alternative.
freeVarsVar :: Var -> VarSet Source
Find all free variables on a binder. Equivalent to idFreeVars, but safe to call on type bindings.
localFreeVarsAlt :: CoreAlt -> VarSet Source
Find all free local variables in a case alternative, which excludes any variables bound in the alternative.
freeVarsType :: Type -> TyVarSet Source
Find all free variables in a type.
freeVarsCoercion :: Coercion -> VarSet Source
Find all free variables in a coercion.
localFreeVarsExpr :: CoreExpr -> VarSet Source
Find all locally defined free variables in an expression.
freeIdsExpr :: CoreExpr -> IdSet Source
Find all free identifiers in an expression.
localFreeIdsExpr :: CoreExpr -> VarSet Source
Find all locally defined free identifiers in an expression.
Utilities
isCoArg :: CoreExpr -> Bool Source
Returns True
iff the expression is a Coercion
expression at its top level.
endoFunTypeM :: MonadCatch m => Type -> m ([TyVar], Type) Source
Return the domain/codomain type of an endofunction type.
splitTyConAppM :: Monad m => Type -> m (TyCon, [Type]) Source
As splitTyConApp
, catching failure in a monad.
splitFunTypeM :: MonadCatch m => Type -> m ([TyVar], Type, Type) Source
Get the quantified variables, domain, and codomain of a function type.
endoFunExprTypeM :: MonadCatch m => CoreExpr -> m ([TyVar], Type) Source
Return the domain/codomain type of an endofunction expression.
funExprArgResTypesM :: MonadCatch m => CoreExpr -> m ([TyVar], Type, Type) Source
Return the domain and codomain types of a function expression.
funExprsWithInverseTypes :: MonadCatch m => CoreExpr -> CoreExpr -> m (Type, Type) Source
Check two expressions have types a -> b
and b -> a
, returning (a,b)
.
mapAlts :: (CoreExpr -> CoreExpr) -> [CoreAlt] -> [CoreAlt] Source
Map a function over the RHS of each case alternative.
substCoreAlt :: Var -> CoreExpr -> CoreAlt -> CoreAlt Source
Substitute all occurrences of a variable with an expression, in a case alternative.
substCoreExpr :: Var -> CoreExpr -> CoreExpr -> CoreExpr Source
Substitute all occurrences of a variable with an expression, in an expression.
betaReduceAll :: CoreExpr -> [CoreExpr] -> (CoreExpr, [CoreExpr]) Source
Beta-reduce as many lambda-binders as possible.
mkDataConApp :: [Type] -> DataCon -> [Var] -> CoreExpr Source
Build a constructor application. Accepts a list of types to which the type constructor is instantiated. Ex.
data T a b = C a b Int
Pseudocode:
mkDataConApp [a',b'] C [x,y,z] ==> C a' b' (x::a') (y::b') (z::Int) :: T a' b'
Crumbs
Crumbs record a path through the tree, using descriptive constructor names.
Eq Crumb | |
Read Crumb | |
Show Crumb | |
Extern Crumb | |
Extern LocalPathH | |
ExtendPath HermitC Crumb | Extend the |
ExtendPath PrettyC Crumb | |
ReadPath HermitC Crumb | Retrieve the |
ReadPath PrettyC Crumb | |
HasEmptyContext c => HasEmptyContext (ExtendContext c (LocalPath Crumb)) | |
Extern (TransformH LCoreTC LocalPathH) | |
Extern (TransformH LCore LocalPathH) | |
ReadPath c Crumb => ReadPath (ExtendContext c e) Crumb | |
type Box Crumb = CrumbBox | |
type Box LocalPathH = PathBox | |
type Box (TransformH LCoreTC LocalPathH) = TransformLCoreTCPathBox | |
type Box (TransformH LCore LocalPathH) = TransformLCorePathBox |
showCrumbs :: [Crumb] -> String Source
leftSibling :: Crumb -> Maybe Crumb Source