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 ref
val opt_debug_on : string list 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 ref
val indent : int -> string
val debug : context -> string 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_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_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 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 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 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_reset_implicits : PPrint.document -> Ast.typquant -> 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 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 find_exc_typ : 'a Ast.def list -> string
val find_unimplemented : 'a Ast.def list -> Ast_util.IdSet.t
val pp_ast_coq : (PPrint.ToChannel.channel * string list) -> (PPrint.ToChannel.channel * string list) -> Type_check.tannot Ast_defs.ast -> string -> bool -> unit