summaryrefslogtreecommitdiff
path: root/plugins/extraction/table.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/extraction/table.mli
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/extraction/table.mli')
-rw-r--r--plugins/extraction/table.mli41
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