sail
  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
type mut =
  1. | Immutable
  2. | Mutable
type !'a lvar =
  1. | Register of Ast.effect * Ast.effect * 'a
  2. | Enum of 'a
  3. | Local of mut * 'a
  4. | Unbound
val lvar_typ : 'a lvar -> 'a
val no_annot : unit Ast.annot
val gen_loc : Parse_ast.l -> Parse_ast.l
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 : Ast.kind_aux -> Ast.kid -> Ast.kinded_id
val inc_ord : Ast.order
val dec_ord : Ast.order
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
val untyp_pat : 'a Ast.pat -> 'a Ast.pat * Ast.typ option
val uncast_exp : 'a Ast.exp -> 'a Ast.exp * Ast.typ option
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
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 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.effect -> 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
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
val constraint_disj : Ast.n_constraint -> Ast.n_constraint list
module Id : sig ... end
module Kid : sig ... end
module Kind : sig ... end
module KOpt : sig ... end
module Nexp : sig ... end
module BE : 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 BESet : sig ... end
module KidSet : sig ... end
module KBindings : sig ... end
module Bindings : sig ... end
module NCMap : sig ... end
module TypMap : sig ... end
val no_effect : Ast.effect
val mk_effect : Ast.base_effect_aux list -> Ast.effect
val has_effect : Ast.effect -> Ast.base_effect_aux -> bool
val effect_set : Ast.effect -> BESet.t
val equal_effects : Ast.effect -> Ast.effect -> bool
val subseteq_effects : Ast.effect -> Ast.effect -> bool
val union_effects : Ast.effect -> Ast.effect -> Ast.effect
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
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
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
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
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
val kid_loc : Ast.kid -> 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
val string_of_id : Ast.id -> string
val string_of_kid : Ast.kid -> string
val string_of_base_effect_aux : Ast.base_effect_aux -> string
val string_of_kind_aux : Ast.kind_aux -> string
val string_of_kind : Ast.kind -> string
val string_of_base_effect : Ast.base_effect -> string
val string_of_effect : Ast.effect -> 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
val id_of_fundef : 'a Ast.fundef -> 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
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
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 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
val locate : (Ast.l -> Ast.l) -> 'a Ast.exp -> 'a Ast.exp
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
val extern_assoc : string -> (string * string) list -> string option
val find_annot_ast : (Lexing.position * Lexing.position) option -> 'a Ast_defs.ast -> (Ast.l * 'a) option
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