package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
val opt_sequential : bool Stdlib.ref
val opt_mwords : bool Stdlib.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 Stdlib.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 simple_num : Parse_ast.l -> Nat_big_num.num -> (Type_check.Env.t * Ast.typ * Ast.effect) option Ast.exp
val effectful_set : 'a list -> bool
val effectful : Ast.effect -> bool
val is_regtyp : Ast.typ -> 'a -> bool
val lemnum : (Pretty_print_common.Big_int.num -> string) -> Pretty_print_common.Big_int.num -> string
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 min_int32 : Pretty_print_common.Big_int.num
val max_int32 : Pretty_print_common.Big_int.num
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_let_lem : context -> Type_check.tannot Ast.letbind -> 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 doc_funcl_lem : Type_check.Env.t -> Type_check.tannot Ast.funcl -> PPrint.document
val get_id : 'a Ast.funcl list -> Ast.id
module StringSet : sig ... end
val doc_fundef_rhs_lem : Type_check.Env.t -> Type_check.tannot Ast.fundef -> PPrint.document
val doc_mutrec_lem : Type_check.Env.t -> Type_check.tannot Ast.fundef list -> PPrint.document
val doc_fundef_lem : Type_check.Env.t -> Type_check.tannot Ast.fundef -> PPrint.document
val doc_dec_lem : Type_check.tannot Ast.dec_spec -> PPrint.document
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 doc_def_lem : Type_check.Env.t -> Type_check.tannot Ast.def -> 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct