Documentation

A type environment maps a variable's name to its type.

Returns True when x is a subtype of y.

Returns True when x is a supertype of y (i.e, when y is a subtype of x).

Returns a type that is a supertype of both x and y; the type it returns is the "least upper bound" (⊔) of x and y. Because Moses has pairs and functions, the type returned may not be equal to either of the supplied types. In the worst case, everything falls under the supertype ANY.

Returns a type that is a subtype of both x and y; the type it returns is the "greatest lower bound" (⊓) of x and y. Because Moses has pairs and functions, the type returned may not be equal to either of the supplied types. In the worst case, everything is above the subtype NONE.

TODO: You can remove this definition when you've implemented commonSupertype and commonSubtype.

You can manually use checkTypeof to enter expressions and check their types, e.g, checkTypeof "42" checkTypeof "1+1"

A handy function for producing an error message.

Given a typing environment and an expression, typechecks the expression AND makes sure that the resulting type is BoolTy (or else fails).

Given a typing environment and an expression, typechecks the expression AND makes sure that the resulting type is StringTy (or else fails).

Given a typing environment and an expression, typechecks the expression AND makes sure that the resulting type is either IntTy or RealTy (or else fails).

Given a typing environment and an expression, typechecks the expression AND makes sure that the resulting type is some kind of list: ListTy elemTy (or else fails).

Given a typing environment and an expression, typechecks the expression AND makes sure that the resulting type is some kind of function: FunTy argTy resTy (or else fails).

Given a size n, a typing environment, and an expression, typechecks the expression AND makes sure that the resulting type is some kind of tuple of size n: TupleTy tyList where tyList has size n (or else fails).

Given an expected type ty, a typing environment, and an expression, typechecks the expression AND makes sure that the resulting type is exactly ty (or else fails).

A general version of bounded type checking, used by other helper functions to provide constraints on the type of an expression.

The call

typeofExprBounded lowerTy upperTy tenv expr

Given a typing environment and an expression, checks that the expression is well typed. This is the main typechecking function.

Determine how to display a value of a given type.