Safe Haskell | Safe |
---|---|
Language | Haskell98 |
- data Ctx a n
- = CtxTop {
- ctxDataDefs :: !(DataDefs n)
- ctxKindEnv :: !(KindEnv n)
- ctxTypeEnv :: !(TypeEnv n)
- | CtxLAM !(Ctx a n) !a !(Bind n)
- | CtxLam !(Ctx a n) !a !(Bind n)
- | CtxAppLeft !(Ctx a n) !a !(Exp a n)
- | CtxAppRight !(Ctx a n) !a !(Exp a n)
- | CtxLetBody !(Ctx a n) !a !(Lets a n)
- | CtxLetLLet !(Ctx a n) !a !(Bind n) !(Exp a n)
- | CtxLetLRec !(Ctx a n) !a ![(Bind n, Exp a n)] !(Bind n) ![(Bind n, Exp a n)] !(Exp a n)
- | CtxCaseScrut !(Ctx a n) !a ![Alt a n]
- | CtxCaseAlt !(Ctx a n) !a !(Exp a n) ![Alt a n] !(Pat n) ![Alt a n]
- | CtxCastBody !(Ctx a n) !a !(Cast a n)
- = CtxTop {
- isTopLetCtx :: Ctx a n -> Bool
- topOfCtx :: Ctx a n -> (DataDefs n, KindEnv n, TypeEnv n)
- takeEnclosingCtx :: Ctx a n -> Maybe (Ctx a n)
- takeTopNameOfCtx :: Ctx a n -> Maybe n
- takeTopLetEnvNamesOfCtx :: Ord n => Ctx a n -> Set n
- encodeCtx :: Ctx a n -> String
Documentation
A one-hole context for Exp
.
CtxTop | The top-level context. |
| |
CtxLAM !(Ctx a n) !a !(Bind n) | Body of a type abstraction. |
CtxLam !(Ctx a n) !a !(Bind n) | Body of a value or witness abstraction. |
CtxAppLeft !(Ctx a n) !a !(Exp a n) | Left of an application. |
CtxAppRight !(Ctx a n) !a !(Exp a n) | Right of an application. |
CtxLetBody !(Ctx a n) !a !(Lets a n) | Body of a let-expression. |
CtxLetLLet !(Ctx a n) !a !(Bind n) !(Exp a n) | In a non-recursive let-binding. We store the binder and body of the let expression. |
CtxLetLRec !(Ctx a n) !a ![(Bind n, Exp a n)] !(Bind n) ![(Bind n, Exp a n)] !(Exp a n) | In a recursive binding. |
CtxCaseScrut !(Ctx a n) !a ![Alt a n] | Scrutinee of a case expression. |
CtxCaseAlt !(Ctx a n) !a !(Exp a n) ![Alt a n] !(Pat n) ![Alt a n] | In a case alternative. |
CtxCastBody !(Ctx a n) !a !(Cast a n) | Body of a type cast |
isTopLetCtx :: Ctx a n -> Bool Source
Check if the context is a top-level let-binding. All bindings in the top-level chain of lets and letrecs are included.
takeEnclosingCtx :: Ctx a n -> Maybe (Ctx a n) Source
Take the enclosing context from a nested one,
or Nothing
if this is the top-level context.
takeTopNameOfCtx :: Ctx a n -> Maybe n Source
Take the name of the outer-most enclosing let-binding of this context, if there is one.
takeTopLetEnvNamesOfCtx :: Ord n => Ctx a n -> Set n Source
Get the set of value names defined at top-level, including top-level let-bindings and the top level type environment.