Documentation

Check an expression. Given the data definitions, an general type environment, a function map, a constraint set, a region set, an (input) location state map, and the expression, this function will either throw an error, or return a pair of expression type and new location state map.

Main entry point, checks a whole program (functions and main body).

These are the kinds of errors that the type checker may throw. There are a few named errors that I thought would be common, like variables not being found, locations being used incorrectly, etc. For other errors, there's a GenericTC form that takes some expression and string (containing an error message).

A region set is (as you would expect) a set of regions. They are the regions that are currently live while checking a particular expression.

A map from locations to their type state. This tracks the current state of a location at a certain point in a program. The type checker threads this through by taking an input map that represents the location states before checking a particular expression, and returns an output map that represents the location states after checking that particular expression. All we need to know in this map is whether each location is an input or output location, and whether we've taken an offset of the location in a letloc form.

A set of constraints (which are re-used location expressions) which encode relationships between locations. These are used by the type checker to verify that locations are used correctly.

The following are valid constraints: * StartOfC LocVar Region * AfterConstantC Int LocVar LocVar * AfterVariableC Var LocVar LocVar * InRegionC LocVar Region * FromEndC

While the first four can appear in syntax before RouteEnds, the fifth (fromEnd) should only be introduced by the RouteEnds pass.

Constraints on locations. Used during typechecking. Roughly analogous to LocExp.

A location has been aliased if we have taken an offset of it while introducing a new location. These show up in the LocationTypeState below.

The type checking monad. Just for throwing errors, but could in the future be parameterized by whatever other logging, etc, monad we want the compiler to use.