sail
  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
val opt_sequential : bool ref
val opt_mwords : bool ref
type context = {
  1. early_ret : bool;
  2. bound_nexps : Ast_util.NexpSet.t;
  3. top_env : Type_check.Env.t;
}
val empty_ctxt : context
val print_to_from_interp_value : bool ref
val langlebar : PPrint.document
val ranglebar : PPrint.document
val anglebars : PPrint.document -> PPrint.document
val doc_var : Ast.kid -> PPrint.document
val is_number_char : char -> bool
val fix_id : bool -> string -> string
val doc_id_lem : Ast.id -> PPrint.document
val doc_id_lem_type : Ast.id -> PPrint.document
val doc_id_lem_ctor : Ast.id -> PPrint.document
val deinfix : Ast.id -> Ast.id
val doc_var_lem : Ast.kid -> PPrint.document
val doc_docstring_lem : (Parse_ast.l * 'a) -> PPrint.document
val simple_annot : Parse_ast.l -> 'a -> Parse_ast.l * (Type_check.Env.t * 'a * Ast.effect) option
val effectful_set : 'a list -> bool
val effectful : Ast.effect -> bool
val is_regtyp : Ast.typ -> 'a -> bool
val doc_nexp_lem : Ast.nexp -> PPrint.document
val orig_nexp : Ast.nexp -> Ast.nexp
val lem_nexps_of_typ : Ast.typ -> Ast_util.NexpSet.t
val lem_nexps_of_typ_arg : Ast.typ_arg -> Ast_util.NexpSet.t
val lem_tyvars_of_typ : Ast.typ -> Ast_util.KidSet.t
val doc_typ_lem : Type_check.Env.t -> Ast.typ -> PPrint.document
val doc_atomic_typ_lem : bool -> Ast.typ -> PPrint.document
val contains_t_pp_var : 'a -> Ast.typ -> bool
val replace_typ_size : context -> Type_check.Env.t -> Ast.typ -> Ast.typ option
val replace_typ_arg_size : context -> Type_check.Env.t -> Ast.typ_arg -> Ast.typ_arg option
val make_printable_type : context -> Type_check.Env.t -> Ast.typ -> Ast.typ option
val doc_tannot_lem : context -> Type_check.Env.t -> bool -> Ast.typ -> PPrint.document
val doc_lit_lem : Ast.lit -> PPrint.document
val kid_nexps_of_typquant : Ast.typquant -> Ast.nexp list
val doc_typquant_items_lem : Ast.nexp list -> PPrint.document
val typeclass_nexps : Ast.typ -> Ast_util.NexpSet.t
val doc_typclasses_lem : Ast.typ -> PPrint.document * Ast_util.NexpSet.t
val doc_typschm_lem : Type_check.Env.t -> bool -> Ast.typschm -> PPrint.document
val is_ctor : Type_check.Env.t -> Ast.id -> bool
val doc_pat_lem : context -> bool -> Type_check.tannot Ast.pat -> PPrint.document
val typ_needs_printed : Ast.typ -> bool
val typ_needs_printed_arg : Ast.typ_arg -> bool
val contains_early_return : 'a Ast.exp -> bool
type is_bitvector_cast =
  1. | BVC_yes
  2. | BVC_allowed
  3. | BVC_not
val is_bitvector_cast_out : 'a Ast.exp -> bool
val find_e_ids : 'a Ast.exp -> Ast_util.IdSet.t
val typ_id_of : Ast.typ -> Ast.id
val prefix_recordtype : bool
val report : Parse_ast.l -> (string * int * int * int) -> string -> exn
val doc_exp_lem : context -> bool -> Type_check.tannot Ast.exp -> PPrint.document
val doc_type_union_lem : Type_check.Env.t -> Ast.type_union -> PPrint.document
val doc_typquant_sorts : PPrint.document -> Ast.typquant -> PPrint.document
val doc_sia_id : Ast.id -> PPrint.document
val doc_typdef_lem : Type_check.Env.t -> 'a Ast.type_def -> PPrint.document
val args_of_typs : Ast.l -> Type_check.Env.t -> Ast.typ list -> Type_check.tannot Ast.pat list * Type_check.tannot Ast.exp list
val doc_tannot_opt_lem : Type_check.Env.t -> Ast.tannot_opt -> PPrint.document
val doc_fun_body_lem : context -> Type_check.tannot Ast.exp -> PPrint.document
val get_id : 'a Ast.funcl list -> Ast.id
module StringSet : sig ... end
val doc_spec_lem : Type_check.Env.t -> 'a Ast.val_spec -> PPrint.document
val is_field_accessor : (string * ('a * 'b * ('c * Ast.id) list)) list -> 'd Ast.fundef -> bool
val int_of_field_index : string -> Ast.id -> Ast.nexp -> Ast_util.Big_int.num
val doc_regtype_fields : (string * (Ast.nexp * Ast.nexp * (Ast.index_range * Ast.id) list)) -> PPrint.document
val find_exc_typ : 'a Ast.def list -> string
val pp_ast_lem : (PPrint.ToChannel.channel * string list) -> (PPrint.ToChannel.channel * string list) -> Type_check.Env.t -> Type_check.tannot Ast_defs.ast -> string -> unit