Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Libnamesopen Minimlopen Declarations
module Refset' : CSig.USetS with type elt = globalmodule Refmap' : CSig.UMapS with type key = global
type t
val safe_basename_of_global : t -> global -> Id.t
val make_table : unit -> t
(*s Warning and Error messages. *)
val warning_axioms : t -> unitval warning_opaques : t -> bool -> unitval warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * GlobRef.t -> unitval warning_id : string -> unit(*s Target language. *)
type lang = | Ocaml | Haskell | Scheme | JSON | External of string (** provided by a plugin *)
val lang : unit -> langval lang_name : lang -> string
val error_axiom_scheme : ?loc:Loc.t -> global -> int -> 'aval error_constant : ?loc:Loc.t -> global -> 'aval error_inductive : ?loc:Loc.t -> global -> 'aval error_nb_cons : unit -> 'aval error_module_clash : ModPath.t -> ModPath.t -> 'aval error_no_module_expr : ModPath.t -> 'aval error_singleton_become_prop : inductive -> 'aval error_unknown_module : ?loc:Loc.t -> qualid -> 'aval error_not_modular : lang -> 'aval error_not_visible : global -> 'aval error_MPfile_as_mod : ModPath.t -> bool -> 'aval check_inside_section : unit -> unitval check_loaded_modfile : ModPath.t -> unitval msg_of_implicit : kill_reason -> stringval err_or_warn_remaining_implicit : kill_reason -> unit
val info_file : string -> unit
(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
val occur_kn_in_ref : MutInd.t -> global -> boolval repr_of_r : global -> KerName.tval modpath_of_r : global -> ModPath.tval label_of_r : global -> Id.tval base_mp : ModPath.t -> ModPath.tval is_modfile : ModPath.t -> boolval string_of_modfile : t -> DirPath.t -> stringval file_of_modfile : t -> DirPath.t -> stringval is_toplevel : ModPath.t -> boolval at_toplevel : ModPath.t -> boolval mp_length : ModPath.t -> intval prefixes_mp : ModPath.t -> ModPath.Set.tval common_prefix_from_list : ModPath.t -> ModPath.t list -> ModPath.t optionval get_nth_label_mp : int -> ModPath.t -> Id.tval labels_of_ref : global -> ModPath.t * Id.t list
(*s Some table-related operations *)
(* For avoiding repeated extraction of the same constant or inductive, we use cache functions below. Indexing by constant name isn't enough, due to modules we could have a same constant name but different content. So we check that the [constant_body] hasn't changed from recording time to retrieving time. Same for inductive : we store [mutual_inductive_body] as checksum. In both case, we should ideally also check the env *)
val add_typedef : t -> Constant.t -> InfvInst.t -> constant_body -> ml_type -> unitval lookup_typedef : t -> Constant.t -> InfvInst.t -> constant_body -> ml_type option
val add_cst_type : t -> Constant.t -> InfvInst.t -> constant_body -> ml_schema -> unitval lookup_cst_type : t -> Constant.t -> InfvInst.t -> constant_body -> ml_schema option
val add_ind : t -> MutInd.t -> InfvInst.t -> mutual_inductive_body -> ml_ind -> unitval lookup_ind : t -> MutInd.t -> InfvInst.t -> mutual_inductive_body -> ml_ind option
val add_inductive_kind : t -> MutInd.t -> InfvInst.t -> inductive_kind -> unitval is_coinductive : t -> global -> boolval is_coinductive_type : t -> ml_type -> bool(* What are the fields of a record (empty for a non-record) *)val get_record_fields : t -> global -> global option listval record_fields_of_type : t -> ml_type -> global option list
val add_recursors : t -> Environ.env -> MutInd.t -> unitval is_recursor : t -> global -> bool
val add_projection : t -> int -> Constant.t -> inductive -> unitval is_projection : t -> global -> bool
val add_info_axiom : t -> GlobRef.t -> unitval remove_info_axiom : t -> GlobRef.t -> unitval add_log_axiom : t -> GlobRef.t-> unitval add_symbol : t -> GlobRef.t -> unitval add_symbol_rule : t -> GlobRef.t -> Id.t -> unit
val add_opaque : t -> GlobRef.t -> unitval remove_opaque : t -> GlobRef.t -> unit
(*s Output Directory parameter *)
val output_directory : unit -> string
(*s AccessOpaque parameter *)
val access_opaque : unit -> bool
(*s AutoInline parameter *)
val auto_inline : unit -> bool
(*s TypeExpand parameter *)
val type_expand : unit -> bool
(*s KeepSingleton parameter *)
val keep_singleton : unit -> bool
(*s Prefix parameter *)
val prefix : unit -> string
(*s Optimize parameter *)
type opt_flag = { opt_kill_dum : bool; (* 1 *) opt_fix_fun : bool; (* 2 *) opt_case_iot : bool; (* 4 *) opt_case_idr : bool; (* 8 *) opt_case_idg : bool; (* 16 *) opt_case_cst : bool; (* 32 *) opt_case_fun : bool; (* 64 *) opt_case_app : bool; (* 128 *) opt_let_app : bool; (* 256 *) opt_lin_let : bool; (* 512 *) opt_lin_beta : bool } (* 1024 *)
val optims : unit -> opt_flag
(*s Controls whether dummy lambda are removed *)
val conservative_types : unit -> bool
(*s A comment to print at the beginning of the files *)
val file_comment : unit -> string
(*s Table for custom inlining *)
val to_inline : global -> boolval to_keep : global -> bool
(*s Table for implicits arguments *)
val implicits_of_global : global -> Int.Set.t
(*s Table for user-given custom ML extractions. *)
(* UGLY HACK: registration of a function defined in [extraction.ml] *)val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
val is_custom : global -> boolval is_inline_custom : global -> boolval is_foreign_custom : global -> boolval find_callback : global -> string optionval find_custom : global -> stringval find_type_custom : global -> string list * string
val is_custom_match : ml_branch array -> boolval find_custom_match : ml_branch array -> string
(*s Extraction commands. *)
val extraction_language : lang -> unitval extraction_inline : bool -> qualid list -> unitval print_extraction_inline : unit -> Pp.tval print_extraction_foreign : unit -> Pp.tval print_extraction_callback : unit -> Pp.tval reset_extraction_inline : unit -> unitval reset_extraction_foreign : unit -> unitval reset_extraction_callback : unit -> unitval extract_callback : string option -> qualid -> unitval extract_constant_inline : bool -> qualid -> string list -> string -> unitval extract_constant_foreign : qualid -> string -> unitval extract_inductive : qualid -> string -> string list -> string option -> unit
type int_or_id = ArgInt of int | ArgId of Id.tval extraction_implicit : qualid -> int_or_id list -> unit
(*s Table of blacklisted filenames *)
val extraction_blacklist : string list -> unitval reset_extraction_blacklist : unit -> unitval print_extraction_blacklist : unit -> Pp.t