DDC.Core.Exp.Annot.Ctx

Documentation

data Ctx a n

A one-hole context for Exp.

Constructors

CtxTop

The top-level context.

Fields

• ctxEnvX :: !(EnvX n)

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

Check if the context is a top-level let-binding. All bindings in the top-level chain of lets and letrecs are included.

topOfCtx :: Ctx a n -> EnvX n

Get the top level of a context.

takeEnclosingCtx :: Ctx a n -> Maybe (Ctx a n)

Take the enclosing context from a nested one, or Nothing if this is the top-level context.

takeTopNameOfCtx :: Ctx a n -> Maybe n

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

Get the set of value names defined at top-level, including top-level let-bindings and the top level type environment.

encodeCtx :: Ctx a n -> String

Encode a context into a unique string. This is a name for a particlar program context, which is guaranteed to be from names of other contexts. This encoding can be used as a fresh name generator if you can base the names on the context they are created in.