diff options
Diffstat (limited to 'contrib/extraction/table.mli')
| -rw-r--r-- | contrib/extraction/table.mli | 36 |
1 files changed, 27 insertions, 9 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index c9a4e8da..ca02cb4d 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 10209 2007-10-09 21:49:37Z letouzey $ i*) +(*i $Id: table.mli 10245 2007-10-21 13:41:53Z letouzey $ i*) open Names open Libnames @@ -14,39 +14,49 @@ open Miniml open Declarations val id_of_global : global_reference -> identifier +val pr_long_global : global_reference -> Pp.std_ppcmds + (*s Warning and Error messages. *) +val warning_axioms : unit -> unit val error_axiom_scheme : global_reference -> int -> 'a -val warning_info_ax : global_reference -> unit -val warning_log_ax : global_reference -> unit val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : string -> 'a val error_unknown_module : qualid -> 'a -val error_toplevel : unit -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_MPfile_as_mod : dir_path -> 'a +val error_MPfile_as_mod : module_path -> bool -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -(*s utilities concerning [module_path]. *) +val info_file : string -> unit + +(*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : kernel_name -> global_reference -> bool val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> label - val current_toplevel : unit -> module_path val base_mp : module_path -> module_path -val is_modfile : module_path -> bool +val is_modfile : module_path -> bool +val string_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool val visible_con : constant -> bool +val mp_length : module_path -> int +val prefixes_mp : module_path -> MPset.t +val modfile_of_mp : module_path -> module_path +val common_prefix_from_list : module_path -> module_path list -> module_path +val add_labels_mp : module_path -> label list -> module_path +val get_nth_label_mp : int -> module_path -> label +val get_nth_label : int -> global_reference -> label +val labels_of_ref : global_reference -> module_path * label list (*s Some table-related operations *) @@ -66,6 +76,9 @@ val add_projection : int -> constant -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int +val add_info_axiom : global_reference -> unit +val add_log_axiom : global_reference -> unit + val reset_tables : unit -> unit (*s AutoInline parameter *) @@ -95,9 +108,14 @@ val optims : unit -> opt_flag (*s Target language. *) -type lang = Ocaml | Haskell | Scheme | Toplevel +type lang = Ocaml | Haskell | Scheme val lang : unit -> lang +(*s Extraction mode: modular or monolithic *) + +val set_modular : bool -> unit +val modular : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool |