ddc-core- Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe




data Ctx a n Source #

A one-hole context for Exp.



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.

topOfCtx :: Ctx a n -> EnvX n Source #

Get the top level of a context.

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.

encodeCtx :: Ctx a n -> String Source #

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.