package libsail
Module LibsailSource
Module for breaking AST into syntactic chunks and interleaving comments.
const_prop target ast ref_vars substs assigns exp performs constant propagation on exp where substs is a pair of substitutions on immutable variables and type variables, assigns is a substitution on mutable variables, and ref_vars is the set of variable which may have had a reference taken (and hence we cannot reliably track).
This module implements the interface with the Z3 (or other) SMT solver
In Sail, we need to distinguish between pure and impure (side-effecting) functions. This is because there are few places, such as top-level let-bindings and loop termination measures where side effects must clearly be forbidden. This module implements inference for which functions are pure and which are effectful, and checking the above purity restrictions.
Initial desugaring pass over AST after parsing
Compile Sail ASTs to Jib intermediate representation
Utilities and helper functions for operating on Jib instructions and definitions
Definition of Sail project files, and functions for working with them.
This file implements utilities for dealing with $property and $counterexample pragmas.
Rewrites for removing polymorphism from specifications
The type checker API
Type error utilities