package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

The type checker API

module Big_int = Nat_big_num
val set_tc_debug : int -> unit

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.

val opt_no_lexp_bounds_check : bool Stdlib.ref

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

val opt_expand_valspec : bool Stdlib.ref

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.

val opt_no_bitfield_expansion : bool Stdlib.ref

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

val opt_strict_var : bool Stdlib.ref

Only allow mutable variables to be declared with var

Environments

type env
module Env : sig ... end

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

val add_existential : Ast.l -> Ast.kinded_id list -> Ast.n_constraint -> Env.t -> Env.t

Environment helper functions

val get_bitfield_ranges : Ast.id -> Env.t -> Ast.index_range Ast_util.Bindings.t

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

val get_bitfield_range : Ast.id -> Ast.id -> Env.t -> Ast.index_range option

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

val orig_kid : Ast.kid -> Ast.kid

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.

val orig_nexp : Ast.nexp -> Ast.nexp
val dvector_typ : Env.t -> Ast.nexp -> Ast.typ -> Ast.typ

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

Type annotations

type tannot

The type of type annotations

val destruct_tannot : tannot -> (Env.t * Ast.typ) option

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.

val mk_tannot : ?uannot:Ast_util.uannot -> Env.t -> Ast.typ -> tannot
val untyped_annot : tannot -> Ast_util.uannot
val map_uannot : (Ast_util.uannot -> Ast_util.uannot) -> tannot -> tannot
val get_instantiations : tannot -> Ast.typ_arg Ast_util.KBindings.t option
val empty_tannot : tannot
val is_empty_tannot : tannot -> bool
val string_of_tannot : tannot -> string
val replace_typ : Ast.typ -> tannot -> tannot
val replace_env : Env.t -> tannot -> tannot

Removing type annotations

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

Checking expressions and patterns

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.

val check_fundef : Env.t -> Ast.def_annot -> Ast_util.uannot Ast.fundef -> tannot Ast.def list * Env.t
val check_val_spec : Env.t -> Ast.def_annot -> Ast_util.uannot Ast.val_spec -> tannot Ast.def list * Env.t
val assert_constraint : Env.t -> bool -> tannot Ast.exp -> Ast.n_constraint option
val check_funcls_complete : Parse_ast.l -> Env.t -> tannot Ast.funcl list -> Ast.typ -> tannot Ast.funcl list * (Ast.def_annot -> Ast.def_annot)

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. Note that this is only exposed so that it can be used during descattering to check completeness of scattered functions, and should not be called otherwise.

val prove : (string * int * int * int) -> Env.t -> Ast.n_constraint -> bool

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.

val solve_unique : Env.t -> Ast.nexp -> Big_int.num option

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

val canonicalize : Env.t -> Ast.typ -> Ast.typ
val subtype_check : Env.t -> Ast.typ -> Ast.typ -> bool
val is_enum_member : Ast.id -> Env.t -> bool
val bind_pat_no_guard : Env.t -> Ast_util.uannot Ast.pat -> Ast.typ -> tannot Ast.pat * Env.t

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.

Destructuring type annotations

Partial functions: The expressions and patterns passed to these functions must be guaranteed to have tannots of the form Some (env, typ) for these to work.

val env_of : tannot Ast.exp -> Env.t
val env_of_annot : (Ast.l * tannot) -> Env.t
val env_of_tannot : tannot -> Env.t
val typ_of : tannot Ast.exp -> Ast.typ
val typ_of_annot : (Ast.l * tannot) -> Ast.typ
val typ_of_tannot : tannot -> Ast.typ
val typ_of_pat : tannot Ast.pat -> Ast.typ
val env_of_pat : tannot Ast.pat -> Env.t
val typ_of_pexp : tannot Ast.pexp -> Ast.typ
val env_of_pexp : tannot Ast.pexp -> Env.t
val typ_of_mpat : tannot Ast.mpat -> Ast.typ
val env_of_mpat : tannot Ast.mpat -> Env.t
val typ_of_mpexp : tannot Ast.mpexp -> Ast.typ
val env_of_mpexp : tannot Ast.mpexp -> Env.t
val effect_of : tannot Ast.exp -> Ast_util.effect
val effect_of_pat : tannot Ast.pat -> Ast_util.effect
val effect_of_annot : tannot -> Ast_util.effect
val add_effect_annot : tannot -> Ast_util.effect -> tannot
val expected_typ_of : (Ast.l * tannot) -> Ast.typ option

Utilities

val destruct_exist_plain : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option

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.

val destruct_exist : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option
val destruct_atom_nexp : Env.t -> Ast.typ -> Ast.nexp option
val destruct_atom_bool : Env.t -> Ast.typ -> Ast.n_constraint option
val destruct_range : Env.t -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp * Ast.nexp) option
val destruct_numeric : ?name:string option -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp) option
val destruct_vector : Env.t -> Ast.typ -> (Ast.nexp * Ast.typ) option
val destruct_bitvector : Env.t -> Ast.typ -> Ast.nexp option
val vector_start_index : Env.t -> Ast.typ -> Ast.nexp
val exist_typ : Parse_ast.l -> (Ast.kid -> Ast.n_constraint) -> (Ast.kid -> Ast.typ) -> Ast.typ

Construct an existential type with a guaranteed fresh identifier.

val subst_unifiers : Ast.typ_arg Ast_util.KBindings.t -> Ast.typ -> Ast.typ

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).

val alpha_equivalent : Env.t -> Ast.typ -> Ast.typ -> bool

Check if two types are alpha equivalent

Throws Invalid_argument if the argument is not a E_app expression

val instantiation_of_without_type : tannot Ast.exp -> Ast.typ_arg Ast_util.KBindings.t

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

val instantiate_simple_equations : Ast.quant_item list -> Ast.typ_arg Ast_util.KBindings.t
val big_int_of_nexp : Ast.nexp -> Big_int.num option

Checking full ASTs

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

val check_defs : Env.t -> Ast_util.uannot Ast.def list -> tannot Ast.def list * Env.t
val check_with_envs : Env.t -> Ast_util.uannot Ast.def list -> (tannot Ast.def list * Env.t) list

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

val initial_env : Env.t

The initial type checking environment

val prove_smt : assumptions:Ast.n_constraint list -> Ast.n_constraint -> bool