DDC.Core.Eval.Check

Check for conflicting store capabilities in the initial program.

Documentation

checkCapsModule :: Module a Name -> Maybe (Error a)

Check for conflicting store capabilities in a module.

checkCapsX :: Exp a Name -> Maybe (Error a)

Check for conflicting store capabilities in an expression.

data Error a

Things that can go wrong with the capabilities in a program.

Constructors

ErrorConflict

Conflicting capabilities in program.

Fields

errorRegions :: Rgn

errorCap1 :: Cap

errorCap2 :: Cap

ErrorPartial

A partially applied capability constructor. In the formal semantics, capabilities are atomic, so this isn't a problem. However, as we're representing them with general witness appliction we need to ensure the constructors aren't partially applied.

Fields

errorWitness :: Witness () Name

ErrorNonHandle

A capability constructor applied to a non-region handle. As with ErrorPartial we only need to check for this because we're using general witness application to represent capabilities, instead of having an atomic form.

Fields

errorWitness :: Witness () Name

Instances

Pretty (Error a)