set_tc_debug controls the verbosity of the type checker. 0 is silent, 1 prints a tree of the type derivation and 2 is like 1 but with much more debugging information. 3 is the highest level, and is even more verbose still.

opt_no_lexp_bounds_check turns off the bounds checking in vector assignments in l-expressions.

opt_expand_valspec expands typedefs in valspecs during type checking. We prefer not to do it for latex output but it is otherwise a good idea.

Don't expand bitfields (when using old syntax), used for LaTeX output

Only allow mutable variables to be declared with var

The env module defines the internal type checking environment, and contains functions that operate on that state.

Environment helper functions

get_bitfield_ranges id env returns the index ranges of bitfield type id, or raises Not_found if id is not a bitfield type.

get_bitfield_range id field env returns the index_range of field in bitfield type id, or None if the field does not exist.

When the typechecker creates new type variables it gives them fresh names of the form 'fvXXX#name, where XXX is a number (not necessarily three digits), and name is the original name when the type variable was created by renaming an exisiting type variable to avoid shadowing. orig_kid takes such a type variable and strips out the 'fvXXX# part. It returns the type variable unmodified if it is not of this form.

Vector with default order as set in environment by default Order ord

The type of type annotations

Aliases for typed definitions and ASTs for readability

The canonical view of a type annotation is that it is a tuple containing an environment (env), a type (typ), such that check_X env (strip_X X) typ succeeds, where X is typically exp (i.e an expression). Note that it is specifically not guaranteed that calling destruct_tannot followed by mk_tannot returns an identical type annotation.

Strip the type annotations from an expression.

Strip the type annotations from a pattern

Strip the type annotations from a pattern-expression

Strip the type annotations from an l-expression

Check an expression has some type. Returns a fully annotated version of the expression, where each subexpression is annotated with its type and the Environment used while checking it. The can be used to re-start the typechecking process on any sub-expression. so local modifications to the AST can be re-checked.

Use the pattern completeness checker to check completeness of a list of function clauses. This takes care of setting up the environment in the correct way. The type passed is the type of the function (Typ_fn), and the environment should be that attached to either the SD_funcl clause or the FD_function clause.

If the optional global_env option is used, then information about other types will be taken from the global environment - for example this can be used to provide a view of all the enumeration clauses of a scattered enum, whereas the function local environment would contain only those imported before the final clause. Furthermore, all type definitions will be considered as closed.

Attempt to prove a constraint using z3. Returns true if z3 can prove that the constraint is true, returns false if z3 cannot prove the constraint true. Note that this does not guarantee that the constraint is actually false, as the constraint solver is somewhat untrustworthy.

Returns Some c if there is a unique c such that nexp = c

Variant that doesn't introduce new guards for literal patterns, but raises a type error instead. This should always be safe to use on patterns that have previously been type checked.

Extract the argument and return types for a function clause

Returns the type that an expression was checked against, if any. Note that these may be removed if an expression is rewritten.

This function is useful because it can tell us what the bi-directional type-checking was doing.

1. If this returns None, then the type system was inferring a type when creating the annotation.
2. If this returns Some _, then the type system was checking against an expected type.

This can inform us whether certain rewrites need to introduce type annotations to preserve typability.

Safely destructure an existential type. Returns None if the type is not existential. This function will pick a fresh name for the existential to ensure that no name-collisions occur, although we can optionally suggest a name for the case where it would not cause a collision. The "plain" version does not treat numeric types (i.e. range, int, nat) as existentials.

Construct an existential type with a guaranteed fresh identifier.

unify l env goals typ1 typ2 returns set of typ_arg bindings such that substituting those bindings using every type variable in goals will make typ1 and typ2 equal. Will throw a Unification_error if typ1 and typ2 cannot unification (although unification in Sail is not complete). Will throw a type error if any goals appear in in typ2 (occurs check).

Check if two types are alpha equivalent

Throws Invalid_argument if the argument is not a E_app expression

Doesn't use the type of the expression when calculating instantiations. May fail if the arguments aren't sufficient to calculate all unifiers.

Type variable instantiations that inference will extract from constraints

Fully type-check an AST

Some invariants that will hold of a fully checked AST are:

• No internal nodes, such as E_internal_exp, or E_comment nodes.

• E_vector_access nodes and similar will be replaced by function calls E_app to vector access functions. This is different to the old type checker.

• Every expressions type annotation tannot will be Some (typ, env).

• Also every pattern will be annotated with the type it matches.

• Toplevel expressions such as typedefs and some subexpressions such as letbinds may have None as their tannots if it doesn't make sense for them to have type annotations.

check throws type_errors rather than Sail generic errors from Reporting. For a function that uses generic errors, use Type_error.check

The same as check, but exposes the intermediate type-checking environments so we don't have to always re-check the entire AST

The initial type checking environment

The initial type checking environment, with a specific set of available modules.