package libsail

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Type errors
Environments
Type annotations
Removing type annotations
Checking expressions and patterns
Destructuring type annotations
Utilities
Checking full ASTs

package libsail

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
  - Chunk_ast
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Format_sail
    
    CONFIG
    
    Make
    
    Config
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    Config
    
    IdGraph
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Mappings
  - Monad_params
  - Monomorphise
  - Nl_flow
  - Outcome_rewrites
  - Parse_ast
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
  - Profile
  - Property
    
    Event
  - Reporting
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
    
    PC
    
    PC_config
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_error
  - Util
    
    Duplicate
    
    S
    
    IntIntSet
    
    IntSet
  - Value
    
    StringMap
  - Value2

Legend:
Library
Module
Module type
Parameter
Class
Class type

The type checker API

module Big_int = Nat_big_num

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

val opt_no_lexp_bounds_check : bool ref

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

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

val opt_smt_linearize : bool ref

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

val opt_no_bitfield_expansion : bool ref

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

Type errors

type constraint_reason = (Ast.l * string) option

type type_error =

| Err_no_casts of Ast_util.uannot Ast.exp * Ast.typ * Ast.typ * type_error * type_error list
| Err_no_overloading of Ast.id * (Ast.id * type_error) list
| Err_unresolved_quants of Ast.id * Ast.quant_item list * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * Ast.n_constraint list
| Err_failed_constraint of Ast.n_constraint * (Ast_util.mut * Ast.typ) Ast_util.Bindings.t * Ast.n_constraint list
| Err_subtype of Ast.typ * Ast.typ * Ast.n_constraint option * (constraint_reason * Ast.n_constraint) list * Ast.l Ast_util.KBindings.t
| Err_no_num_ident of Ast.id
| Err_other of string
| 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 Lazy.t -> unit

val typ_print : string 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 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

val strip_exp : tannot Ast.exp -> Ast_util.uannot Ast.exp

Strip the type annotations from an expression.

val strip_pat : tannot Ast.pat -> Ast_util.uannot Ast.pat

Strip the type annotations from a pattern

val strip_mpat : tannot Ast.mpat -> Ast_util.uannot Ast.mpat

val strip_pexp : tannot Ast.pexp -> Ast_util.uannot Ast.pexp

Strip the type annotations from a pattern-expression

val strip_lexp : tannot Ast.lexp -> Ast_util.uannot Ast.lexp

Strip the type annotations from an l-expression

val strip_mpexp : tannot Ast.mpexp -> Ast_util.uannot Ast.mpexp

val strip_mapcl : tannot Ast.mapcl -> Ast_util.uannot Ast.mapcl

val strip_letbind : tannot Ast.letbind -> Ast_util.uannot Ast.letbind

val strip_val_spec : tannot Ast.val_spec -> Ast_util.uannot Ast.val_spec

val strip_funcl : tannot Ast.funcl -> Ast_util.uannot Ast.funcl

val strip_register : tannot Ast.dec_spec -> Ast_util.uannot Ast.dec_spec

val strip_typedef : tannot Ast.type_def -> Ast_util.uannot Ast.type_def

val strip_def : tannot Ast.def -> Ast_util.uannot Ast.def

val strip_ast : tannot Ast_defs.ast -> Ast_util.uannot Ast_defs.ast

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 -> Ast_util.uannot 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 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 infer_exp : Env.t -> Ast_util.uannot Ast.exp -> tannot Ast.exp

val infer_pat : 
  Env.t ->
  Ast_util.uannot Ast.pat ->
  tannot Ast.pat * Env.t * Ast_util.uannot Ast.exp list

val infer_lexp : Env.t -> Ast_util.uannot Ast.lexp -> tannot Ast.lexp

val check_case : 
  Env.t ->
  Ast.typ ->
  Ast_util.uannot Ast.pexp ->
  Ast.typ ->
  tannot Ast.pexp

val check_funcl : 
  Env.t ->
  Ast_util.uannot Ast.funcl ->
  Ast.typ ->
  tannot Ast.funcl

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 : 
  Env.t ->
  Ast_util.uannot Ast.pat ->
  Ast.typ ->
  tannot Ast.pat * Env.t * Ast_util.uannot Ast.exp list

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.

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

val tc_assume : Ast.n_constraint -> tannot Ast.exp -> tannot Ast.exp

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

val unify : 
  Ast.l ->
  Env.t ->
  Ast_util.KidSet.t ->
  Ast.typ ->
  Ast.typ ->
  Ast.typ_arg Ast_util.KBindings.t

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

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

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 ->
  Ast_util.uannot 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 ->
  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 : Env.t -> Ast.n_constraint -> bool