package libsail

  1. Overview
  2. Docs
On This Page
  1. Untyped AST annotations and locations
  2. Variable information
  3. Functions for building and destructuring untyped AST elements
    1. Functions for building untyped AST elements
    2. Unwrap aux constructors
    3. Destruct type annotated patterns and expressions
    4. Utilites for working with kinded_ids
    5. Utility functions for constructing types
    6. Sail built-in types
  4. Simplifcation of numeric expressions and constraints
    1. Functions for building numeric expressions
    2. Functions for building numeric constraints
    3. Functions for building type arguments
  5. Set and Map modules for various AST elements
  6. Functions for working with type quantifiers
  7. Functions to map over annotations in sub-expressions
  8. Printing utilities
  9. Functions for getting identifiers from toplevel definitions
    1. Functions for manipulating identifiers
  10. Misc functions
  11. Manipulating locations
  12. Substitutions
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities and helper functions for operating on Sail ASTs

module Big_int = Nat_big_num

Untyped AST annotations and locations

type uannot

The type of annotations for untyped AST nodes. When expressions are type-checked the untyped annotations are replaced with typed annotations Type_check.tannot.

val empty_uannot : uannot
val add_attribute : Ast.l -> string -> string -> uannot -> uannot

Add an attribute to an annotation. Attributes are attached to expressions in Sail via:

$[attribute argument] expression

The location argument should be a span that corresponds to the attribute itself, and not include the expression.

val remove_attribute : string -> uannot -> uannot
val get_attribute : string -> uannot -> (Ast.l * string) option
val get_attributes : uannot -> (Ast.l * string * string) list
val find_attribute_opt : string -> (Ast.l * string * string) list -> string option
val mk_def_annot : ?doc:string -> ?attrs:(Ast.l * string * string) list -> Ast.l -> Ast.def_annot
val add_def_attribute : Ast.l -> string -> string -> Ast.def_annot -> Ast.def_annot
val get_def_attribute : string -> Ast.def_annot -> (Ast.l * string) option
val def_annot_map_loc : (Ast.l -> Ast.l) -> Ast.def_annot -> Ast.def_annot
val no_annot : Ast.l * uannot

The empty annotation (as a location + uannot pair). Should be used carefully because it can result in unhelpful error messgaes. However a common pattern is generating code with no_annot, then adding location information with the various locate_ functions in this module.

val gen_loc : Parse_ast.l -> Parse_ast.l

gen_loc l takes a location l and generates a location which means 'generated/derived from location l'. This is useful for debugging errors that occur in generated code.

val is_gen_loc : Parse_ast.l -> bool

Variable information

type mut =
  1. | Immutable
  2. | Mutable
type 'a lvar =
  1. | Register of 'a
  2. | Enum of 'a
  3. | Local of mut * 'a
  4. | Unbound of Ast.id

lvar is the type of variables - they can either be registers, local mutable or immutable variables constructors or unbound identifiers.

val is_unbound : 'a lvar -> bool
val lvar_typ : ?loc:Ast.l -> 'a lvar -> 'a

Note: Partial function -- fails for Unbound lvars

val is_order_inc : Ast.order -> bool
val is_order_dec : Ast.order -> bool

Functions for building and destructuring untyped AST elements

Functions for building untyped AST elements

val mk_id : string -> Ast.id
val mk_kid : string -> Ast.kid
val mk_nexp : Ast.nexp_aux -> Ast.nexp
val mk_exp : ?loc:Ast.l -> uannot Ast.exp_aux -> uannot Ast.exp
val mk_pat : ?loc:Ast.l -> uannot Ast.pat_aux -> uannot Ast.pat
val mk_pexp : ?loc:Ast.l -> uannot Ast.pexp_aux -> uannot Ast.pexp
val mk_lit : Ast.lit_aux -> Ast.lit
val mk_lit_exp : ?loc:Ast.l -> Ast.lit_aux -> uannot Ast.exp
val mk_typ_pat : Ast.typ_pat_aux -> Ast.typ_pat
val mk_funcl : ?loc:Ast.l -> Ast.id -> uannot Ast.pat -> uannot Ast.exp -> uannot Ast.funcl
val mk_fundef : uannot Ast.funcl list -> uannot Ast.def
val mk_val_spec : Ast.val_spec_aux -> uannot Ast.def
val mk_typschm : Ast.typquant -> Ast.typ -> Ast.typschm
val mk_typquant : Ast.quant_item list -> Ast.typquant
val mk_qi_id : Ast.kind_aux -> Ast.kid -> Ast.quant_item
val mk_qi_kopt : Ast.kinded_id -> Ast.quant_item
val mk_fexp : Ast.id -> uannot Ast.exp -> uannot Ast.fexp
val mk_kopt : ?loc:Ast.l -> Ast.kind_aux -> Ast.kid -> Ast.kinded_id
val mk_def : ?loc:Ast.l -> 'a Ast.def_aux -> 'a Ast.def
val pat_of_mpat : 'a Ast.mpat -> 'a Ast.pat

Mapping patterns are a subset of patterns, so we can always convert one to the other

Unwrap aux constructors

val unaux_exp : 'a Ast.exp -> 'a Ast.exp_aux
val unaux_pat : 'a Ast.pat -> 'a Ast.pat_aux
val unaux_nexp : Ast.nexp -> Ast.nexp_aux
val unaux_typ : Ast.typ -> Ast.typ_aux
val unaux_kind : Ast.kind -> Ast.kind_aux
val unaux_constraint : Ast.n_constraint -> Ast.n_constraint_aux

Destruct type annotated patterns and expressions

val untyp_pat : 'a Ast.pat -> 'a Ast.pat * Ast.typ option

untyp_pat (P_aux (P_typ (typ, pat)), _) returns Some (pat, typ) or None if the pattern does not match.

val uncast_exp : 'a Ast.exp -> 'a Ast.exp * Ast.typ option

Same as untyp_pat, but for E_typ nodes

Utilites for working with kinded_ids

val kopt_kid : Ast.kinded_id -> Ast.kid
val kopt_kind : Ast.kinded_id -> Ast.kind
val is_int_kopt : Ast.kinded_id -> bool
val is_typ_kopt : Ast.kinded_id -> bool
val is_bool_kopt : Ast.kinded_id -> bool

Utility functions for constructing types

val mk_typ : Ast.typ_aux -> Ast.typ
val mk_typ_arg : Ast.typ_arg_aux -> Ast.typ_arg
val mk_id_typ : Ast.id -> Ast.typ
val is_typ_arg_nexp : Ast.typ_arg -> bool
val is_typ_arg_typ : Ast.typ_arg -> bool
val is_typ_arg_bool : Ast.typ_arg -> bool

Sail built-in types

val unknown_typ : Ast.typ
val int_typ : Ast.typ
val nat_typ : Ast.typ
val atom_typ : Ast.nexp -> Ast.typ
val implicit_typ : Ast.nexp -> Ast.typ
val range_typ : Ast.nexp -> Ast.nexp -> Ast.typ
val bit_typ : Ast.typ
val bool_typ : Ast.typ
val atom_bool_typ : Ast.n_constraint -> Ast.typ
val app_typ : Ast.id -> Ast.typ_arg list -> Ast.typ
val register_typ : Ast.typ -> Ast.typ
val unit_typ : Ast.typ
val string_typ : Ast.typ
val real_typ : Ast.typ
val vector_typ : Ast.nexp -> Ast.typ -> Ast.typ
val bitvector_typ : Ast.nexp -> Ast.typ
val list_typ : Ast.typ -> Ast.typ
val exc_typ : Ast.typ
val tuple_typ : Ast.typ list -> Ast.typ
val function_typ : Ast.typ list -> Ast.typ -> Ast.typ
val is_unit_typ : Ast.typ -> bool
val is_number : Ast.typ -> bool
val is_ref_typ : Ast.typ -> bool
val is_vector_typ : Ast.typ -> bool
val is_bit_typ : Ast.typ -> bool
val is_bitvector_typ : Ast.typ -> bool

Simplifcation of numeric expressions and constraints

These functions simplify nexps and n_constraints using various basic rules. In general they will guarantee to reduce constant numeric expressions like 2 + 5 into 7, although they will not simplify 2^constant, as that often leads to unreadable error messages containing huge numbers.

val nexp_simp : Ast.nexp -> Ast.nexp
val constraint_simp : Ast.n_constraint -> Ast.n_constraint
val constraint_conj : Ast.n_constraint -> Ast.n_constraint list

If a constraint is a conjunction, return a list of all the top-level conjuncts

val constraint_disj : Ast.n_constraint -> Ast.n_constraint list

Same as constraint_conj but for disjunctions

type effect
val no_effect : effect
val monadic_effect : effect
val effectful : effect -> bool
val equal_effects : effect -> effect -> bool
val subseteq_effects : effect -> effect -> bool
val union_effects : effect -> effect -> effect

Functions for building numeric expressions

val nconstant : Big_int.num -> Ast.nexp
val nint : int -> Ast.nexp
val nminus : Ast.nexp -> Ast.nexp -> Ast.nexp
val nsum : Ast.nexp -> Ast.nexp -> Ast.nexp
val ntimes : Ast.nexp -> Ast.nexp -> Ast.nexp
val npow2 : Ast.nexp -> Ast.nexp
val nvar : Ast.kid -> Ast.nexp
val napp : Ast.id -> Ast.nexp list -> Ast.nexp
val nid : Ast.id -> Ast.nexp

Functions for building numeric constraints

val nc_lteq : Ast.nexp -> Ast.nexp -> Ast.n_constraint
val nc_gteq : Ast.nexp -> Ast.nexp -> Ast.n_constraint
val nc_true : Ast.n_constraint
val nc_false : Ast.n_constraint
val nc_set : Ast.kid -> Big_int.num list -> Ast.n_constraint
val nc_int_set : Ast.kid -> int list -> Ast.n_constraint
val nc_var : Ast.kid -> Ast.n_constraint

Functions for building type arguments

val arg_nexp : ?loc:Ast.l -> Ast.nexp -> Ast.typ_arg
val arg_typ : ?loc:Ast.l -> Ast.typ -> Ast.typ_arg
val arg_bool : ?loc:Ast.l -> Ast.n_constraint -> Ast.typ_arg
val arg_kopt : Ast.kinded_id -> Ast.typ_arg

Set and Map modules for various AST elements

module Id : sig ... end
module Kid : sig ... end
module Kind : sig ... end
module KOpt : sig ... end
module Nexp : sig ... end
module NC : sig ... end
module Typ : sig ... end
module IdSet : sig ... end
module NexpSet : sig ... end
module NexpMap : sig ... end
module KOptSet : sig ... end
module KOptMap : sig ... end
module KidSet : sig ... end
module KBindings : sig ... end
module Bindings : sig ... end
module NCMap : sig ... end
module TypMap : sig ... end

Functions for working with type quantifiers

val quant_items : Ast.typquant -> Ast.quant_item list
val quant_kopts : Ast.typquant -> Ast.kinded_id list
val quant_split : Ast.typquant -> Ast.kinded_id list * Ast.n_constraint list
val quant_map_items : (Ast.quant_item -> Ast.quant_item) -> Ast.typquant -> Ast.typquant
val is_quant_kopt : Ast.quant_item -> bool
val is_quant_constraint : Ast.quant_item -> bool

Functions to map over annotations in sub-expressions

val map_exp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.exp -> 'b Ast.exp
val map_pat_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.pat -> 'b Ast.pat
val map_pexp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.pexp -> 'b Ast.pexp
val map_lexp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.lexp -> 'b Ast.lexp
val map_letbind_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.letbind -> 'b Ast.letbind
val map_mpat_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mpat -> 'b Ast.mpat
val map_mpexp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mpexp -> 'b Ast.mpexp
val map_mapcl_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mapcl -> 'b Ast.mapcl
val map_typedef_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.type_def -> 'b Ast.type_def
val map_fundef_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.fundef -> 'b Ast.fundef
val map_funcl_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.funcl -> 'b Ast.funcl
val map_mapdef_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mapdef -> 'b Ast.mapdef
val map_valspec_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.val_spec -> 'b Ast.val_spec
val map_register_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.dec_spec -> 'b Ast.dec_spec
val map_scattered_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.scattered_def -> 'b Ast.scattered_def
val map_def_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.def -> 'b Ast.def
val map_ast_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast_defs.ast -> 'b Ast_defs.ast
val id_loc : Ast.id -> Parse_ast.l

Extract locations from terms

val kid_loc : Ast.kid -> Parse_ast.l
val kopt_loc : Ast.kinded_id -> Parse_ast.l
val typ_loc : Ast.typ -> Parse_ast.l
val pat_loc : 'a Ast.pat -> Parse_ast.l
val mpat_loc : 'a Ast.mpat -> Parse_ast.l
val exp_loc : 'a Ast.exp -> Parse_ast.l
val nexp_loc : Ast.nexp -> Parse_ast.l
val def_loc : 'a Ast.def -> Parse_ast.l

Printing utilities

Note: For debugging and error messages only - not guaranteed to produce parseable Sail, or even print all language constructs!

val string_of_id : Ast.id -> string
val string_of_kid : Ast.kid -> string
val string_of_kind_aux : Ast.kind_aux -> string
val string_of_kind : Ast.kind -> string
val string_of_nexp : Ast.nexp -> string
val string_of_typ : Ast.typ -> string
val string_of_typ_arg : Ast.typ_arg -> string
val string_of_typ_pat : Ast.typ_pat -> string
val string_of_n_constraint : Ast.n_constraint -> string
val string_of_kinded_id : Ast.kinded_id -> string
val string_of_quant_item : Ast.quant_item -> string
val string_of_typquant : Ast.typquant -> string
val string_of_typschm : Ast.typschm -> string
val string_of_lit : Ast.lit -> string
val string_of_exp : 'a Ast.exp -> string
val string_of_pexp : 'a Ast.pexp -> string
val string_of_lexp : 'a Ast.lexp -> string
val string_of_pat : 'a Ast.pat -> string
val string_of_mpat : 'a Ast.mpat -> string
val string_of_letbind : 'a Ast.letbind -> string
val string_of_index_range : Ast.index_range -> string

Functions for getting identifiers from toplevel definitions

val id_of_fundef : 'a Ast.fundef -> Ast.id
val id_of_mapdef : 'a Ast.mapdef -> Ast.id
val id_of_type_def : 'a Ast.type_def -> Ast.id
val id_of_val_spec : 'a Ast.val_spec -> Ast.id
val id_of_dec_spec : 'a Ast.dec_spec -> Ast.id

Functions for manipulating identifiers

val deinfix : Ast.id -> Ast.id
val id_of_kid : Ast.kid -> Ast.id
val kid_of_id : Ast.id -> Ast.kid
val prepend_id : string -> Ast.id -> Ast.id
val append_id : Ast.id -> string -> Ast.id
val prepend_kid : string -> Ast.kid -> Ast.kid

Misc functions

val nexp_frees : Ast.nexp -> KidSet.t
val nexp_identical : Ast.nexp -> Ast.nexp -> bool
val is_nexp_constant : Ast.nexp -> bool
val int_of_nexp_opt : Ast.nexp -> Big_int.num option
val lexp_to_exp : 'a Ast.lexp -> 'a Ast.exp
val typ_app_args_of : Ast.typ -> string * Ast.typ_arg_aux list * Ast.l
val vector_typ_args_of : Ast.typ -> Ast.nexp * Ast.typ
val kopts_of_nexp : Ast.nexp -> KOptSet.t
val kopts_of_typ : Ast.typ -> KOptSet.t
val kopts_of_typ_arg : Ast.typ_arg -> KOptSet.t
val kopts_of_constraint : Ast.n_constraint -> KOptSet.t
val kopts_of_quant_item : Ast.quant_item -> KOptSet.t
val tyvars_of_nexp : Ast.nexp -> KidSet.t
val tyvars_of_typ : Ast.typ -> KidSet.t
val tyvars_of_typ_arg : Ast.typ_arg -> KidSet.t
val tyvars_of_constraint : Ast.n_constraint -> KidSet.t
val tyvars_of_quant_item : Ast.quant_item -> KidSet.t
val is_kid_generated : Ast.kid -> bool
val undefined_of_typ : bool -> Ast.l -> (Ast.typ -> 'annot) -> Ast.typ -> 'annot Ast.exp
val pattern_vector_subranges : 'a Ast.pat -> (Big_int.num * Big_int.num) list Bindings.t
val destruct_pexp : 'a Ast.pexp -> 'a Ast.pat * 'a Ast.exp option * 'a Ast.exp * (Ast.l * 'a)
val construct_pexp : ('a Ast.pat * 'a Ast.exp option * 'a Ast.exp * (Ast.l * 'a)) -> 'a Ast.pexp
val destruct_mpexp : 'a Ast.mpexp -> 'a Ast.mpat * 'a Ast.exp option * (Ast.l * 'a)
val construct_mpexp : ('a Ast.mpat * 'a Ast.exp option * (Ast.l * 'a)) -> 'a Ast.mpexp
val is_valspec : Ast.id -> 'a Ast.def -> bool
val is_fundef : Ast.id -> 'a Ast.def -> bool
val rename_valspec : Ast.id -> 'a Ast.val_spec -> 'a Ast.val_spec
val rename_fundef : Ast.id -> 'a Ast.fundef -> 'a Ast.fundef
val split_defs : ('a Ast.def -> bool) -> 'a Ast.def list -> ('a Ast.def list * 'a Ast.def * 'a Ast.def list) option
val append_ast : 'a Ast_defs.ast -> 'a Ast_defs.ast -> 'a Ast_defs.ast
val append_ast_defs : 'a Ast_defs.ast -> 'a Ast.def list -> 'a Ast_defs.ast
val concat_ast : 'a Ast_defs.ast list -> 'a Ast_defs.ast
val type_union_id : Ast.type_union -> Ast.id
val ids_of_def : 'a Ast.def -> IdSet.t
val ids_of_defs : 'a Ast.def list -> IdSet.t
val ids_of_ast : 'a Ast_defs.ast -> IdSet.t
val val_spec_ids : 'a Ast.def list -> IdSet.t
val record_ids : 'a Ast.def list -> IdSet.t
val get_scattered_union_clauses : Ast.id -> 'a Ast.def list -> Ast.type_union list
val get_scattered_enum_clauses : Ast.id -> 'a Ast.def list -> Ast.id list
val pat_ids : 'a Ast.pat -> IdSet.t
val subst : Ast.id -> 'a Ast.exp -> 'a Ast.exp -> 'a Ast.exp
val hex_to_bin : string -> string
val vector_string_to_bit_list : Ast.lit -> Ast.lit list

Manipulating locations

val locate : (Ast.l -> Ast.l) -> 'a Ast.exp -> 'a Ast.exp

locate takes an expression and recursively sets the location in every subexpression using a function that takes the orginal location as an argument. Expressions build using mk_exp and similar do not have locations, so they can then be annotated as e.g. locate (gen_loc l) (mk_exp ...) where l is the location from which the code is being generated.

val locate_pat : (Ast.l -> Ast.l) -> 'a Ast.pat -> 'a Ast.pat
val locate_lexp : (Ast.l -> Ast.l) -> 'a Ast.lexp -> 'a Ast.lexp
val locate_typ : (Ast.l -> Ast.l) -> Ast.typ -> Ast.typ
val unique : Ast.l -> Ast.l

Make a unique location by giving it a Parse_ast.Unique wrapper with a generated number.

val extern_assoc : string -> Ast.extern option -> string option
val find_annot_ast : (Stdlib.Lexing.position * Stdlib.Lexing.position) option -> 'a Ast_defs.ast -> (Ast.l * 'a) option

Try to find the annotation closest to the provided (simplified) location. Note that this function makes no guarantees about finding the closest annotation or even finding an annotation at all. This is used by the Emacs mode to provide type-at-cursor functionality and we don't mind if it's a bit fuzzy in that context.

Substitutions

The function X_subst substitutes a type argument into something of type X. The type of the type argument determines which kind of type variables will be replaced

val nexp_subst : Ast.kid -> Ast.typ_arg -> Ast.nexp -> Ast.nexp
val constraint_subst : Ast.kid -> Ast.typ_arg -> Ast.n_constraint -> Ast.n_constraint
val typ_subst : Ast.kid -> Ast.typ_arg -> Ast.typ -> Ast.typ
val typ_arg_subst : Ast.kid -> Ast.typ_arg -> Ast.typ_arg -> Ast.typ_arg
val subst_kid : (Ast.kid -> Ast.typ_arg -> 'a -> 'a) -> Ast.kid -> Ast.kid -> 'a -> 'a
val subst_kids_nexp : Ast.nexp KBindings.t -> Ast.nexp -> Ast.nexp
val subst_kids_typ : Ast.nexp KBindings.t -> Ast.typ -> Ast.typ
val subst_kids_typ_arg : Ast.nexp KBindings.t -> Ast.typ_arg -> Ast.typ_arg
val quant_item_subst_kid : Ast.kid -> Ast.kid -> Ast.quant_item -> Ast.quant_item
val typquant_subst_kid : Ast.kid -> Ast.kid -> Ast.typquant -> Ast.typquant
val simple_string_of_loc : Parse_ast.l -> string