diff options
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 41 |
1 files changed, 25 insertions, 16 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 14792f8f..1acbe355 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,13 +8,14 @@ open Names open Libnames +open Globnames open Miniml open Declarations -module Refset' : Set.S with type elt = global_reference +module Refset' : CSig.SetS with type elt = global_reference module Refmap' : Map.S with type key = global_reference -val safe_basename_of_global : global_reference -> identifier +val safe_basename_of_global : global_reference -> Id.t (*s Warning and Error messages. *) @@ -29,7 +30,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a -val error_singleton_become_prop : identifier -> 'a +val error_singleton_become_prop : Id.t -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a @@ -37,7 +38,7 @@ val error_MPfile_as_mod : module_path -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -val msg_non_implicit : global_reference -> int -> name -> string +val msg_non_implicit : global_reference -> int -> Name.t -> string val error_non_implicit : string -> 'a val info_file : string -> unit @@ -45,10 +46,9 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : mutual_inductive -> global_reference -> bool -val repr_of_r : global_reference -> module_path * dir_path * label +val repr_of_r : global_reference -> module_path * DirPath.t * Label.t val modpath_of_r : global_reference -> module_path -val label_of_r : global_reference -> label -val current_toplevel : unit -> module_path +val label_of_r : global_reference -> Label.t val base_mp : module_path -> module_path val is_modfile : module_path -> bool val string_of_modfile : module_path -> string @@ -60,8 +60,8 @@ val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t val common_prefix_from_list : module_path -> module_path list -> module_path option -val get_nth_label_mp : int -> module_path -> label -val labels_of_ref : global_reference -> module_path * label list +val get_nth_label_mp : int -> module_path -> Label.t +val labels_of_ref : global_reference -> module_path * Label.t list (*s Some table-related operations *) @@ -85,9 +85,10 @@ val record_fields_of_type : ml_type -> global_reference option list val add_recursors : Environ.env -> mutual_inductive -> unit val is_recursor : global_reference -> bool -val add_projection : int -> constant -> unit +val add_projection : int -> constant -> inductive -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int +val projection_info : global_reference -> inductive * int (* arity *) val add_info_axiom : global_reference -> unit val remove_info_axiom : global_reference -> unit @@ -131,6 +132,14 @@ type opt_flag = 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 Target language. *) type lang = Ocaml | Haskell | Scheme @@ -162,7 +171,7 @@ val implicits_of_global : global_reference -> int list (*s Table for user-given custom ML extractions. *) (* UGLY HACK: registration of a function defined in [extraction.ml] *) -val register_type_scheme_nb_args : (Environ.env -> Term.constr -> int) -> unit +val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t val is_custom : global_reference -> bool val is_inline_custom : global_reference -> bool @@ -176,7 +185,7 @@ val find_custom_match : ml_branch array -> string val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit -val print_extraction_inline : unit -> unit +val print_extraction_inline : unit -> Pp.std_ppcmds val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit @@ -184,14 +193,14 @@ val extract_inductive : reference -> string -> string list -> string option -> unit -type int_or_id = ArgInt of int | ArgId of identifier +type int_or_id = ArgInt of int | ArgId of Id.t val extraction_implicit : reference -> int_or_id list -> unit (*s Table of blacklisted filenames *) -val extraction_blacklist : identifier list -> unit +val extraction_blacklist : Id.t list -> unit val reset_extraction_blacklist : unit -> unit -val print_extraction_blacklist : unit -> unit +val print_extraction_blacklist : unit -> Pp.std_ppcmds |