package libsail

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

Module Libsail.Type_checkSource

The type checker API

module Big_int = Nat_big_num
Sourceval opt_tc_debug : int 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.

Sourceval opt_no_lexp_bounds_check : bool ref

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

Sourceval opt_expand_valspec : bool 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.

Sourceval opt_smt_linearize : bool ref

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

Sourceval opt_smt_div : bool ref

Allow use of div and mod when rewriting nexps

Sourceval opt_no_bitfield_expansion : bool ref

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

Sourceval opt_check_completeness : bool ref

Check pattern-match completeness when type-checking

Type errors

Sourcetype constraint_reason = (Ast.l * string) option
Sourcetype 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
Sourcetype env
Sourceexception Type_error of env * Ast.l * type_error
Sourceval typ_debug : ?level:int -> string Lazy.t -> unit
Sourceval typ_print : string Lazy.t -> unit

Environments

Sourcemodule Env : sig ... end

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

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

Environment helper functions

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

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

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

Type annotations

Sourcetype tannot

The type of type annotations

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

Sourceval mk_tannot : Env.t -> Ast.typ -> tannot
Sourceval get_instantiations : tannot -> Ast.typ_arg Ast_util.KBindings.t option
Sourceval empty_tannot : tannot
Sourceval is_empty_tannot : tannot -> bool
Sourceval string_of_tannot : tannot -> string
Sourceval replace_typ : Ast.typ -> tannot -> tannot
Sourceval replace_env : Env.t -> tannot -> tannot

Removing type annotations

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

Strip the type annotations from an expression.

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

Strip the type annotations from a pattern

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

Strip the type annotations from a pattern-expression

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

Strip the type annotations from an l-expression

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

Strip location information from types for comparison purposes

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

Checking expressions and patterns

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

Sourceval infer_exp : Env.t -> unit Ast.exp -> tannot Ast.exp
Sourceval infer_pat : Env.t -> unit Ast.pat -> tannot Ast.pat * Env.t * unit Ast.exp list
Sourceval infer_lexp : Env.t -> unit Ast.lexp -> tannot Ast.lexp
Sourceval check_case : Env.t -> Ast.typ -> unit Ast.pexp -> Ast.typ -> tannot Ast.pexp
Sourceval check_funcl : Env.t -> 'a Ast.funcl -> Ast.typ -> tannot Ast.funcl
Sourceval check_fundef : Env.t -> 'a Ast.fundef -> tannot Ast.def list * Env.t
Sourceval check_val_spec : Env.t -> 'a Ast.val_spec -> tannot Ast.def list * Env.t
Sourceval assert_constraint : Env.t -> bool -> tannot Ast.exp -> Ast.n_constraint option
Sourceval 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.

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

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

Sourceval canonicalize : Env.t -> Ast.typ -> Ast.typ
Sourceval subtype_check : Env.t -> Ast.typ -> Ast.typ -> bool
Sourceval is_enum_member : Ast.id -> Env.t -> bool
Sourceval bind_pat : Env.t -> unit Ast.pat -> Ast.typ -> tannot Ast.pat * Env.t * unit Ast.exp list
Sourceval 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.

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

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

Utilities

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

Sourceval destruct_exist : ?name:string option -> Ast.typ -> (Ast.kinded_id list * Ast.n_constraint * Ast.typ) option
Sourceval destruct_atom_nexp : Env.t -> Ast.typ -> Ast.nexp option
Sourceval destruct_atom_bool : Env.t -> Ast.typ -> Ast.n_constraint option
Sourceval destruct_range : Env.t -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp * Ast.nexp) option
Sourceval destruct_numeric : ?name:string option -> Ast.typ -> (Ast.kid list * Ast.n_constraint * Ast.nexp) option
Sourceval destruct_vector : Env.t -> Ast.typ -> (Ast.nexp * Ast.order * Ast.typ) option
Sourceval destruct_bitvector : Env.t -> Ast.typ -> (Ast.nexp * Ast.order) option

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

Sourceval 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

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

Sourceval instantiate_simple_equations : Ast.quant_item list -> Ast.typ_arg Ast_util.KBindings.t
Sourceval 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

Sourceval check_defs : Env.t -> 'a Ast.def list -> tannot Ast.def list * Env.t
Sourceval 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

Sourceval initial_env : Env.t

The initial type checking environment

Sourceval prove_smt : Env.t -> Ast.n_constraint -> bool