package libsail

  1. Overview
  2. Docs
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
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 Unknown lvars

val no_annot : unit Ast.annot

The empty annotation. 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

Functions for building (untyped) AST elements

val mk_id : string -> Ast.id
val mk_kid : string -> Ast.kid
val mk_ord : Ast.order_aux -> Ast.order
val mk_nexp : Ast.nexp_aux -> Ast.nexp
val mk_exp : ?loc:Ast.l -> unit Ast.exp_aux -> unit Ast.exp
val mk_pat : unit Ast.pat_aux -> unit Ast.pat
val mk_mpat : unit Ast.mpat_aux -> unit Ast.mpat
val mk_pexp : ?loc:Ast.l -> unit Ast.pexp_aux -> unit Ast.pexp
val mk_mpexp : unit Ast.mpexp_aux -> unit Ast.mpexp
val mk_lexp : unit Ast.lexp_aux -> unit Ast.lexp
val mk_lit : Ast.lit_aux -> Ast.lit
val mk_lit_exp : Ast.lit_aux -> unit Ast.exp
val mk_typ_pat : Ast.typ_pat_aux -> Ast.typ_pat
val mk_funcl : Ast.id -> unit Ast.pat -> unit Ast.exp -> unit Ast.funcl
val mk_fundef : unit Ast.funcl list -> unit Ast.def
val mk_val_spec : Ast.val_spec_aux -> unit 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 -> unit Ast.exp -> unit Ast.fexp
val mk_letbind : unit Ast.pat -> unit Ast.exp -> unit Ast.letbind
val mk_kopt : ?loc:Ast.l -> Ast.kind_aux -> Ast.kid -> Ast.kinded_id
val inc_ord : Ast.order
val dec_ord : Ast.order

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_order : Ast.order -> Ast.order_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_cast 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_order_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_order : Ast.typ_arg -> bool
val is_typ_arg_bool : Ast.typ_arg -> bool

Sail builtin 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.order -> Ast.typ -> Ast.typ
val bitvector_typ : Ast.nexp -> Ast.order -> 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

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
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_order : ?loc:Ast.l -> Ast.order -> 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

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_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 exp_loc : 'a Ast.exp -> 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_order : Ast.order -> 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 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.order * Ast.typ
val vector_start_index : Ast.typ -> Ast.nexp
val is_order_inc : Ast.order -> bool
val kopts_of_order : Ast.order -> KOptSet.t
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_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 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 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 order_subst : Ast.kid -> Ast.typ_arg -> Ast.order -> Ast.order
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
val attach_comments : Lexer.comment list -> 'a Ast.def list -> 'a Ast.def list

Attach comments produced by the lexer into their nearest nodes in the abstract syntax tree