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 opt_tc_debug : int Stdlib.ref

opt_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 of 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_smt_linearize : bool Stdlib.ref

Linearize cases involving power where we would otherwise require the SMT solver to use non-linear arithmetic.

val opt_smt_div : bool Stdlib.ref

Allow use of div and mod when rewriting nexps

val opt_no_bitfield_expansion : bool Stdlib.ref

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

val opt_check_completeness : bool Stdlib.ref

Check pattern-match completeness when type-checking

Type errors

type constraint_reason = (Ast.l * string) option
type type_error =
  1. | Err_no_casts of unit Ast.exp * Ast.typ * Ast.typ * type_error * type_error list
  2. | Err_no_overloading of Ast.id * (Ast.id * type_error) list
  3. | Err_unresolved_quants of Ast.id * Ast.quant_item list * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * Ast.n_constraint list
  4. | Err_failed_constraint of Ast.n_constraint * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * Ast.n_constraint list
  5. | Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint option * (constraint_reason * Ast.n_constraint) list * Ast.l Ast_util.KBindings.t
  6. | Err_no_num_ident of Ast.id
  7. | Err_other of string
  8. | Err_inner of type_error * Ast.l * string * string option * type_error
type env
exception Type_error of env * Ast.l * type_error
val typ_debug : ?level:int -> string Stdlib.Lazy.t -> unit
val typ_print : string Stdlib.Lazy.t -> unit

Environments

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 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 : Env.t -> Ast.typ -> 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

val strip_exp : 'a Ast.exp -> unit Ast.exp

Strip the type annotations from an expression.

val strip_pat : 'a Ast.pat -> unit Ast.pat

Strip the type annotations from a pattern

val strip_pexp : 'a Ast.pexp -> unit Ast.pexp

Strip the type annotations from a pattern-expression

val strip_lexp : 'a Ast.lexp -> unit Ast.lexp

Strip the type annotations from an l-expression

val strip_mpexp : 'a Ast.mpexp -> unit Ast.mpexp
val strip_mapcl : 'a Ast.mapcl -> unit Ast.mapcl
val strip_typ : Ast.typ -> Ast.typ

Strip location information from types for comparison purposes

val strip_typq : Ast.typquant -> Ast.typquant
val strip_id : Ast.id -> Ast.id
val strip_kid : Ast.kid -> Ast.kid
val strip_nexp_aux : Ast.nexp_aux -> Ast.nexp_aux
val strip_nexp : Ast.nexp -> Ast.nexp
val strip_n_constraint_aux : Ast.n_constraint_aux -> Ast.n_constraint_aux
val strip_n_constraint : Ast.n_constraint -> Ast.n_constraint
val strip_typ_aux : Ast.typ_aux -> Ast.typ_aux

Checking expressions and patterns

val check_exp : Env.t -> unit Ast.exp -> Ast.typ -> tannot Ast.exp

Check an expression has some type. Returns a fully annotated version of the expression, where each subexpression is annotated with it's 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 infer_exp : Env.t -> unit Ast.exp -> tannot Ast.exp
val infer_pat : Env.t -> unit Ast.pat -> tannot Ast.pat * Env.t * unit Ast.exp list
val infer_lexp : Env.t -> unit Ast.lexp -> tannot Ast.lexp
val check_case : Env.t -> Ast.typ -> unit Ast.pexp -> Ast.typ -> tannot Ast.pexp
val check_funcl : Env.t -> 'a Ast.funcl -> Ast.typ -> tannot Ast.funcl
val check_fundef : Env.t -> 'a Ast.fundef -> tannot Ast.def list * Env.t
val check_val_spec : Env.t -> 'a Ast.val_spec -> tannot Ast.def list * Env.t
val assert_constraint : Env.t -> bool -> tannot Ast.exp -> Ast.n_constraint option
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 : Env.t -> unit Ast.pat -> Ast.typ -> tannot Ast.pat * Env.t * unit Ast.exp list
val bind_pat_no_guard : Env.t -> unit 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.

val typ_error : Env.t -> Ast.l -> string -> 'a

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.order * Ast.typ) option
val destruct_bitvector : Env.t -> Ast.typ -> (Ast.nexp * Ast.order) option
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

val check : Env.t -> 'a Ast_defs.ast -> tannot Ast_defs.ast * Env.t

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 -> 'a Ast.def list -> tannot Ast.def list * Env.t
val check_with_envs : Env.t -> 'a 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 : Env.t -> Ast.n_constraint -> bool