sig
val bool_ty : Types.t
val nat_ty : Types.t
val lookup_env_opt :
Typed_ast.env -> Name.t list -> Typed_ast.local_env option
val lookup_env : Typed_ast.env -> Name.t list -> Typed_ast.local_env
val env_apply :
Typed_ast.env ->
Ast.component option ->
Name.t -> (Typed_ast.name_kind * Path.t * Ast.l) option
val lookup_mod_descr_opt :
Typed_ast.env -> Name.t list -> Name.t -> Typed_ast.mod_descr option
val lookup_mod_descr :
Typed_ast.env -> Name.t list -> Name.t -> Typed_ast.mod_descr
val names_get_const :
Typed_ast.env ->
Name.t list -> Name.t -> Types.const_descr_ref * Typed_ast.const_descr
val strings_get_const :
Typed_ast.env ->
string list -> string -> Types.const_descr_ref * Typed_ast.const_descr
val get_const :
Typed_ast.env -> string -> Types.const_descr_ref * Typed_ast.const_descr
val const_exists : Typed_ast.env -> string -> bool
val const_descr_to_kind :
Types.const_descr_ref * Typed_ast.const_descr -> Typed_ast.name_kind
val strings_get_const_id :
Typed_ast.env ->
Ast.l ->
string list ->
string ->
Types.t list -> Types.const_descr_ref Types.id * Typed_ast.const_descr
val get_const_id :
Typed_ast.env ->
Ast.l ->
string ->
Types.t list -> Types.const_descr_ref Types.id * Typed_ast.const_descr
val strings_mk_const_exp :
Typed_ast.env ->
Ast.l -> string list -> string -> Types.t list -> Typed_ast.exp
val mk_const_exp :
Typed_ast.env -> Ast.l -> string -> Types.t list -> Typed_ast.exp
val dest_field_types :
Ast.l ->
Typed_ast.env ->
Types.const_descr_ref -> Types.t * Path.t * Typed_ast.const_descr
val get_field_type_descr :
Ast.l -> Typed_ast.env -> Types.const_descr_ref -> Types.type_descr
val get_field_all_fields :
Ast.l ->
Typed_ast.env -> Types.const_descr_ref -> Types.const_descr_ref list
val lookup_class_descr :
Ast.l -> Typed_ast.env -> Path.t -> Types.class_descr
val lookup_field_for_class_method :
Ast.l ->
Types.class_descr -> Types.const_descr_ref -> Types.const_descr_ref
val lookup_inst_method_for_class_method :
Ast.l -> Types.instance -> Types.const_descr_ref -> Types.const_descr_ref
val class_descr_get_dict_type : Types.class_descr -> Types.t -> Types.t
val class_all_methods_inlined_for_target :
Ast.l -> Typed_ast.env -> Target.target -> Path.t -> bool
val update_const_descr :
Ast.l ->
(Typed_ast.const_descr -> Typed_ast.const_descr) ->
Types.const_descr_ref -> Typed_ast.env -> Typed_ast.env
val c_env_store :
Typed_ast.c_env ->
Typed_ast.const_descr -> Typed_ast.c_env * Types.const_descr_ref
val c_env_save :
Typed_ast.c_env ->
Types.const_descr_ref option ->
Typed_ast.const_descr -> Typed_ast.c_env * Types.const_descr_ref
val const_target_rep_to_loc : Typed_ast.const_target_rep -> Ast.l
val const_target_rep_allow_override : Typed_ast.const_target_rep -> bool
val type_target_rep_to_loc : Types.type_target_rep -> Ast.l
val type_target_rep_allow_override : Types.type_target_rep -> bool
val constant_descr_to_name :
Target.target -> Typed_ast.const_descr -> bool * Name.t * Name.t option
val const_descr_ref_to_ascii_name :
Typed_ast.c_env -> Types.const_descr_ref -> Name.t
val type_descr_to_name :
Target.target -> Path.t -> Types.type_descr -> Name.t
val constant_descr_rename :
Target.non_ident_target ->
Name.t ->
Ast.l ->
Typed_ast.const_descr -> Typed_ast.const_descr * (Ast.l * Name.t) option
val mod_target_rep_rename :
Target.non_ident_target ->
string ->
Name.t ->
Ast.l ->
Typed_ast.mod_target_rep Target.Targetmap.t ->
Typed_ast.mod_target_rep Target.Targetmap.t
val type_descr_rename :
Target.non_ident_target ->
Name.t ->
Ast.l -> Types.type_descr -> Types.type_descr * (Ast.l * Name.t) option
val type_defs_rename_type :
Ast.l ->
Types.type_defs ->
Path.t -> Target.non_ident_target -> Name.t -> Types.type_defs
val const_descr_has_target_rep :
Target.target -> Typed_ast.const_descr -> bool
val mk_name_lskips_annot :
Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.name_lskips_annot
val dest_var_exp : Typed_ast.exp -> Name.t option
val is_var_exp : Typed_ast.exp -> bool
val dest_tup_exp : int option -> Typed_ast.exp -> Typed_ast.exp list option
val is_tup_exp : int option -> Typed_ast.exp -> bool
val is_var_tup_exp : Typed_ast.exp -> bool
val mk_tf_exp : bool -> Typed_ast.exp
val dest_tf_exp : Typed_ast.exp -> bool option
val is_tf_exp : bool -> Typed_ast.exp -> bool
val dest_const_exp : Typed_ast.exp -> Types.const_descr_ref Types.id option
val is_const_exp : Typed_ast.exp -> bool
val dest_num_exp : Typed_ast.exp -> int option
val is_num_exp : Typed_ast.exp -> bool
val mk_num_exp : Types.t -> int -> Typed_ast.exp
val is_empty_backend_exp : Typed_ast.exp -> bool
val mk_eq_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_and_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_and_exps : Typed_ast.env -> Typed_ast.exp list -> Typed_ast.exp
val mk_le_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_sub_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_from_list_exp : Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp
val mk_cross_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_set_sigma_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_set_filter_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_set_image_exp :
Typed_ast.env -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_fun_exp : Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.exp
val mk_opt_fun_exp : Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.exp
val mk_app_exp :
Ast.l ->
Types.type_defs -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_list_app_exp :
Ast.l ->
Types.type_defs -> Typed_ast.exp -> Typed_ast.exp list -> Typed_ast.exp
val mk_eta_expansion_exp :
Types.type_defs -> Name.t list -> Typed_ast.exp -> Typed_ast.exp
val mk_paren_exp : Typed_ast.exp -> Typed_ast.exp
val mk_opt_paren_exp : Typed_ast.exp -> Typed_ast.exp
val may_need_paren : Typed_ast.exp -> bool
val mk_case_exp :
bool ->
Ast.l ->
Typed_ast.exp ->
(Typed_ast.pat * Typed_ast.exp) list -> Types.t -> Typed_ast.exp
val mk_let_exp :
Ast.l -> Name.t * Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_if_exp :
Ast.l -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp -> Typed_ast.exp
val mk_undefined_exp : Ast.l -> string -> Types.t -> Typed_ast.exp
val mk_dummy_exp : Types.t -> Typed_ast.exp
val dest_app_exp : Typed_ast.exp -> (Typed_ast.exp * Typed_ast.exp) option
val strip_app_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list
val dest_infix_exp :
Typed_ast.exp -> (Typed_ast.exp * Typed_ast.exp * Typed_ast.exp) option
val is_infix_exp : Typed_ast.exp -> bool
val strip_infix_exp : Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list
val strip_app_infix_exp :
Typed_ast.exp -> Typed_ast.exp * Typed_ast.exp list * bool
val is_type_def_abbrev : Typed_ast.def -> bool
val is_type_def_record : Typed_ast.def -> bool
type used_entities = {
used_consts : Types.const_descr_ref list;
used_consts_set : Types.Cdset.t;
used_types : Path.t list;
used_types_set : Types.Pset.t;
used_modules : Path.t list;
used_modules_set : Types.Pset.t;
used_tnvars : Types.TNset.t;
}
val empty_used_entities : Typed_ast_syntax.used_entities
val add_exp_entities :
Typed_ast_syntax.used_entities ->
Typed_ast.exp -> Typed_ast_syntax.used_entities
val add_def_aux_entities :
Target.target ->
bool ->
Typed_ast_syntax.used_entities ->
Typed_ast.def_aux -> Typed_ast_syntax.used_entities
val add_def_entities :
Target.target ->
bool ->
Typed_ast_syntax.used_entities ->
Typed_ast.def -> Typed_ast_syntax.used_entities
val get_checked_modules_entities :
Target.target ->
bool -> Typed_ast.checked_module list -> Typed_ast_syntax.used_entities
val remove_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
val drop_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
val space_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
val space_com_init_ws : Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips
val strip_paren_typ_exp : Typed_ast.exp -> Typed_ast.exp
val is_recursive_def : Typed_ast.def_aux -> bool * bool
val try_termination_proof :
Target.target ->
Typed_ast.c_env -> Typed_ast.def_aux -> bool * bool * bool
val is_pp_loc : Ast.l -> bool
val is_pp_exp : Typed_ast.exp -> bool
val is_pp_def : Typed_ast.def -> bool
val val_def_get_name : Typed_ast.val_def -> Name.t option
val val_def_get_class_constraints_no_target_rep :
Typed_ast.env ->
Target.target -> Typed_ast.val_def -> (Path.t * Types.tnvar) list
val val_def_get_class_constraints :
Typed_ast.env -> Typed_ast.val_def -> (Path.t * Types.tnvar) list
val val_def_get_free_tnvars :
Typed_ast.env -> Typed_ast.val_def -> Types.TNset.t
val env_tag_to_string : Typed_ast.env_tag -> string
val constr_family_to_id :
Ast.l ->
Typed_ast.env ->
Types.t ->
Types.constr_family_descr ->
(Types.const_descr_ref Types.id list *
(Types.t -> Types.const_descr_ref Types.id) option)
option
val check_constr_family :
Ast.l -> Typed_ast.env -> Types.t -> Types.constr_family_descr -> unit
val check_for_inline_cycles : Target.target -> Typed_ast.c_env -> unit
end