DDC.Core.Check.CheckExp

Type checker for the Disciple Core language.

Documentation

checkExp

Arguments

:: (Ord n, Pretty n)

=> DataDefs n

Data type definitions.

-> Env n

Kind environment.

-> Env n

Type environment.

-> Exp a n

Expression to check.

-> Either (Error a n) (Exp a n, Type n, Effect n, Closure n)

Type check an expression.

If it's good, you get a new version with types attached to all the bound variables, as well its the type, effect and closure.

If it's bad, you get a description of the error.

The returned expression has types attached to all variable occurrences, so you can call typeOfExp on any open subterm.

typeOfExp :: (Ord n, Pretty n) => DataDefs n -> Exp a n -> Either (Error a n) (Type n)

Like checkExp, but check in an empty environment, and only return the value type of an expression.

As this function is not given an environment, the types of free variables must be attached directly to the bound occurrences. This attachment is performed by checkExp above.

type CheckM a n = CheckM (Error a n)

Type checker monad. Used to manage type errors.

checkExpM

Arguments

:: (Ord n, Pretty n)

=> DataDefs n

Data type definitions.

-> Env n

Kind environment.

-> Env n

Type environment.

-> Exp a n

Expression to check.

-> CheckM a n (Exp a n, Type n, TypeSum n, Set (TaggedClosure n))

Like checkExp but using the CheckM monad to handle errors.

data TaggedClosure n

A closure-term tagged with the bound variable that the term is due to.

Constructors

GBoundVal (Bound n) (TypeSum n)

Term due to a free value variable.

GBoundRgnVar (Bound n)

Term due to a free region variable.

GBoundRgnCon (Bound n)

Term due to a region handle.

Instances

LowerT TaggedClosure

Eq n => Eq (TaggedClosure n)

Ord n => Ord (TaggedClosure n)

Show n => Show (TaggedClosure n)

(Eq n, Pretty n) => Pretty (TaggedClosure n)