package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module StringSet : sig ... end
val list_contains : ('a -> 'b -> int) -> 'b list -> 'a list -> 'b list option
val opt_undef_axioms : bool Stdlib.ref
val opt_debug_on : string list Stdlib.ref
type context = {
  1. early_ret : bool;
  2. kid_renames : Ast.kid Ast_util.KBindings.t;
  3. kid_id_renames : Ast.id option Ast_util.KBindings.t;
  4. kid_id_renames_rev : Ast.kid Ast_util.Bindings.t;
  5. bound_nvars : Ast_util.KidSet.t;
  6. build_at_return : string option;
  7. recursive_fns : (int * int) Ast_util.Bindings.t;
  8. debug : bool;
}
val empty_ctxt : context
val add_single_kid_id_rename : context -> Ast_util.Bindings.key -> Ast_util.KBindings.key -> context
val debug_depth : int Stdlib.ref
val indent : int -> string
val debug : context -> string Stdlib.Lazy.t -> unit
val langlebar : PPrint.document
val ranglebar : PPrint.document
val anglebars : PPrint.document -> PPrint.document
val enclose_record : PPrint.document -> PPrint.document
val enclose_record_update : PPrint.document -> PPrint.document
val bigarrow : PPrint.document
val separate_opt : PPrint.document -> ('a -> PPrint.document option) -> 'a list -> PPrint.document
val is_number_char : char -> bool
val is_enum : Type_check.Env.t -> Ast.id -> bool
val fix_id : bool -> string -> string
val string_id : Ast.id -> Ast.x
val doc_id : Ast.id -> PPrint.document
val doc_id_type : Ast.id -> PPrint.document
val doc_id_ctor : Ast.id -> PPrint.document
val doc_var : context -> Ast_util.KBindings.key -> PPrint.document
val doc_docstring : (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 : context -> ?skip_vars:Ast_util.KidSet.t -> Ast.nexp -> PPrint.document
val orig_nexp : Ast.nexp -> Ast.nexp
val orig_typ_arg : Ast.typ_arg -> Ast.typ_arg
val coq_nvars_of_typ : Ast.typ -> Ast_util.KidSet.t
val coq_nvars_of_typ_arg : Ast.typ_arg -> Ast_util.KidSet.t
val maybe_expand_range_type : Ast.typ -> Ast.typ option
val expand_range_type : Ast.typ -> Ast.typ
val doc_nc_fn : Ast.id -> PPrint.document
val merge_kid_count : int Ast_util.KBindings.t -> int Ast_util.KBindings.t -> int Ast_util.KBindings.t
val count_nexp_vars : Ast.nexp -> int Ast_util.KBindings.t
val count_nc_vars : Ast.n_constraint -> int Ast_util.KBindings.t
type atom_bool_prop =
  1. | Bool_boring
  2. | Bool_complex of Ast.kinded_id list * Ast.n_constraint * Ast.n_constraint
val simplify_atom_bool : 'a -> Ast.kinded_id list -> Ast.n_constraint -> Ast.n_constraint -> atom_bool_prop
type ex_kind =
  1. | ExNone
  2. | ExGeneral
val string_of_ex_kind : ex_kind -> string
val classify_ex_type : context -> 'a -> ?binding:Ast.id -> ?rawbools:bool -> Ast.typ -> ex_kind * Ast.kinded_id list * Ast.typ
val flatten_nc : Ast.n_constraint -> Ast.n_constraint list
val doc_typ_fns : context -> Type_check.Env.t -> (Ast.typ -> PPrint.document) * (bool -> Ast.typ -> PPrint.document) * (?prop_vars:bool -> Ast.typ_arg -> PPrint.document)
val doc_typ : context -> Type_check.Env.t -> Ast.typ -> PPrint.document
val doc_atomic_typ : context -> Type_check.Env.t -> bool -> Ast.typ -> PPrint.document
val doc_typ_arg : context -> Type_check.Env.t -> ?prop_vars:bool -> Ast.typ_arg -> PPrint.document
val doc_arithfact : context -> Type_check.Env.t -> ?exists:Ast.kid list -> ?extra:PPrint.document -> Ast.n_constraint -> PPrint.document
val doc_nc_exp : context -> Type_check.Env.t -> Ast.n_constraint -> PPrint.document
val contains_t_pp_var : context -> Ast.typ -> bool
val doc_tannot : context -> Type_check.Env.t -> bool -> Ast.typ -> PPrint.document
val coq_escape_string : string -> string
val doc_lit : Ast.lit -> PPrint.document
val doc_quant_item_id : ?prop_vars:bool -> context -> (PPrint.document -> 'a) -> Ast.quant_item -> 'a option
val quant_item_id_name : context -> Ast.quant_item -> PPrint.document option
val doc_quant_item_constr : ?prop_vars:bool -> context -> Type_check.Env.t -> 'a -> Ast.quant_item -> PPrint.document option
val quant_item_constr_name : 'a -> Ast.quant_item -> PPrint.document option
val doc_typquant_items : ?prop_vars:bool -> context -> Type_check.Env.t -> (PPrint.document -> PPrint.document) -> Ast.typquant -> PPrint.document
val doc_typquant_items_separate : context -> Type_check.Env.t -> (PPrint.document -> 'a) -> Ast.typquant -> 'a list * PPrint.document list
val typquant_names_separate : context -> Ast.typquant -> PPrint.document list * PPrint.document list
val doc_typquant : context -> Type_check.Env.t -> Ast.typquant -> PPrint.document -> PPrint.document
val typeclass_nexps : Ast.typ -> Ast_util.NexpSet.t
val doc_typschm : context -> Type_check.Env.t -> bool -> Ast.typschm -> PPrint.document
val is_ctor : Type_check.Env.t -> Ast.id -> bool
val is_auto_decomposed_exist : context -> Type_check.Env.t -> ?rawbools:bool -> Ast.typ -> (Ast.kinded_id list * Ast.typ) option
val filter_dep_tuple : Ast.kinded_id list -> ('a * Ast.typ) list -> ('a * Ast.typ) option list * ('a * Ast.typ) list
val filter_dep_pattern_tuple : Ast.kinded_id list -> 'a Ast.pat -> Ast.typ -> PPrint.document option * 'a Ast.pat * Ast.typ
val doc_pat : context -> bool -> bool -> (Type_check.tannot Ast.pat * Ast.typ) -> PPrint.document
val contains_early_return : 'a Ast.exp -> bool
val find_e_ids : 'a Ast.exp -> Ast_util.IdSet.t
val typ_id_of : Ast.typ -> Ast.id
val nexp_const_eval : Ast.nexp -> Ast.nexp
val similar_nexps : context -> Type_check.Env.t -> Ast.nexp -> Ast.nexp -> bool
val constraint_fns : string list
val condition_produces_constraint : context -> Type_check.tannot Ast.exp -> bool
val no_proof_fns : string list
val is_no_proof_fn : Type_check.Env.t -> Ast.id -> bool
val replace_atom_return_type : Ast.typ -> string option * Ast.typ
val is_range_from_atom : Type_check.Env.t -> Ast.typ -> Ast.typ -> bool
val general_typ_of_annot : (Ast.l * Type_check.tannot) -> Ast.typ
val general_typ_of : Type_check.tannot Ast.exp -> Ast.typ
val is_prefix : string -> string -> bool
val merge_new_tyvars : context -> Type_check.Env.t -> 'a Ast.pat -> Type_check.Env.t -> context
val maybe_parens_comma_list : (bool -> 'a -> PPrint.document) -> 'a list -> PPrint.document
val prefix_recordtype : bool
val report : Parse_ast.l -> (string * int * int * int) -> string -> exn
val doc_exp : context -> bool -> Type_check.tannot Ast.exp -> PPrint.document
val doc_let : context -> Type_check.tannot Ast.letbind -> PPrint.document
val list_init : int -> (int -> 'a) -> 'a list
val types_used_with_generic_eq : Type_check.tannot Ast.def list -> Ast_util.IdSet.t
val doc_type_union : context -> PPrint.document -> Ast.type_union -> PPrint.document
val doc_reset_implicits : PPrint.document -> Ast.typquant -> PPrint.document
val doc_typdef : Ast_util.IdSet.t -> 'a Ast.type_def -> PPrint.document
val doc_fun_body : context -> Type_check.tannot Ast.exp -> PPrint.document
val demote_as_pattern : int -> ('a Ast.pat * 'b) -> ('a Ast.pat * 'b) * ('a Ast.exp -> 'a Ast.exp)
val pat_is_plain_binder : Type_check.Env.t -> 'a Ast.pat -> Ast.id option option
val demote_all_patterns : Type_check.Env.t -> int -> ('a Ast.pat * Ast.typ) -> ('a Ast.pat * Ast.typ) * ('a Ast.exp -> 'a Ast.exp)
val atom_constraint : context -> (Type_check.tannot Ast.pat * Ast.typ) -> PPrint.document option
val all_ids : 'a Ast.pexp -> Ast_util.IdSet.t
val tyvars_of_typquant : Ast.typquant -> Ast_util.KidSet.t
val merge_var_patterns : Ast.id option Ast_util.KBindings.t -> ('a Ast.pat * 'b) list -> Ast.id option Ast_util.KBindings.t * ('a Ast.pat * 'b) list
type mutrec_pos =
  1. | NotMutrec
  2. | FirstFn
  3. | LaterFn
val doc_funcl_init : mutrec_pos -> 'a Ast.rec_opt -> ?rec_set:'b -> Type_check.tannot Ast.funcl -> (PPrint.document * PPrint.document) * context * (Type_check.tannot Ast.exp * Ast.effect * string option * PPrint.document list)
val doc_funcl_body : context -> (Type_check.tannot Ast.exp * Ast.effect * string option * PPrint.document list) -> PPrint.document
val get_id : 'a Ast.funcl list -> Ast.id
val doc_fundef_rhs : ?mutrec:mutrec_pos -> 'a -> Type_check.tannot Ast.fundef -> (PPrint.document * PPrint.document) * context * (Type_check.tannot Ast.exp * Ast.effect * string option * PPrint.document list)
val doc_mutrec : 'a -> Type_check.tannot Ast.fundef list -> PPrint.document
val doc_funcl : mutrec_pos -> 'a Ast.rec_opt -> Type_check.tannot Ast.funcl -> PPrint.document * PPrint.document * PPrint.document
val doc_fundef : Type_check.tannot Ast.fundef -> PPrint.document
val doc_dec : Type_check.tannot Ast.dec_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_axiom_typschm : Type_check.Env.t -> Ast.l -> (Ast.typquant * Ast.typ) -> PPrint.document
val doc_val_spec : Ast_util.IdSet.t -> Type_check.tannot Ast.val_spec -> PPrint.document
val doc_val : 'a Ast.pat -> Type_check.tannot Ast.exp -> PPrint.document
val doc_def : Ast_util.IdSet.t -> Ast_util.IdSet.t -> Type_check.tannot Ast.def -> PPrint.document
val find_exc_typ : 'a Ast.def list -> string
val find_unimplemented : 'a Ast.def list -> Ast_util.IdSet.t
val pp_defs_coq : (PPrint.ToChannel.channel * string list) -> (PPrint.ToChannel.channel * string list) -> Type_check.tannot Ast.defs -> string -> bool -> 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