From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- library/libnames.mli | 116 +++++++++++++++++++++++++++++++++------------------ 1 file changed, 76 insertions(+), 40 deletions(-) (limited to 'library/libnames.mli') diff --git a/library/libnames.mli b/library/libnames.mli index cc664a08..9ee7d0ab 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Pp @@ -24,6 +24,18 @@ type global_reference = | ConstructRef of constructor val isVarRef : global_reference -> bool +val isConstRef : global_reference -> bool +val isIndRef : global_reference -> bool +val isConstructRef : global_reference -> bool + +val eq_gr : global_reference -> global_reference -> bool +val canonical_gr : global_reference -> global_reference + +val destVarRef : global_reference -> variable +val destConstRef : global_reference -> constant +val destIndRef : global_reference -> inductive +val destConstructRef : global_reference -> constructor + val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr @@ -39,97 +51,112 @@ val global_of_constr : constr -> global_reference val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference -module Refset : Set.S with type elt = global_reference +module RefOrdered : sig + type t = global_reference + val compare : global_reference -> global_reference -> int +end + + +module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference +(*s Extended global references *) + +type syndef_name = kernel_name + +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name + (*s Dirpaths *) val pr_dirpath : dir_path -> Pp.std_ppcmds val dirpath_of_string : string -> dir_path +val string_of_dirpath : dir_path -> string -(* Give the immediate prefix of a [dir_path] *) -val dirpath_prefix : dir_path -> dir_path +(* Pop the suffix of a [dir_path] *) +val pop_dirpath : dir_path -> dir_path + +(* Pop the suffix n times *) +val pop_dirpath_n : int -> dir_path -> dir_path (* Give the immediate prefix and basename of a [dir_path] *) val split_dirpath : dir_path -> dir_path * identifier -val extend_dirpath : dir_path -> module_ident -> dir_path +val add_dirpath_suffix : dir_path -> module_ident -> dir_path val add_dirpath_prefix : module_ident -> dir_path -> dir_path val chop_dirpath : int -> dir_path -> dir_path * dir_path +val append_dirpath : dir_path -> dir_path -> dir_path + val drop_dirpath_prefix : dir_path -> dir_path -> dir_path -val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool -val append_dirpath : dir_path -> dir_path -> dir_path module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path -(*s Section paths are {\em absolute} names *) -type section_path +(*s Full paths are {\em absolute} paths of declarations *) +type full_path -(* Constructors of [section_path] *) -val make_path : dir_path -> identifier -> section_path +(* Constructors of [full_path] *) +val make_path : dir_path -> identifier -> full_path -(* Destructors of [section_path] *) -val repr_path : section_path -> dir_path * identifier -val dirpath : section_path -> dir_path -val basename : section_path -> identifier +(* Destructors of [full_path] *) +val repr_path : full_path -> dir_path * identifier +val dirpath : full_path -> dir_path +val basename : full_path -> identifier (* Parsing and printing of section path as ["coq_root.module.id"] *) -val path_of_string : string -> section_path -val string_of_path : section_path -> string -val pr_sp : section_path -> std_ppcmds - -module Sppred : Predicate.S with type elt = section_path -module Spmap : Map.S with type key = section_path +val path_of_string : string -> full_path +val string_of_path : full_path -> string +val pr_path : full_path -> std_ppcmds -val restrict_path : int -> section_path -> section_path +module Sppred : Predicate.S with type elt = full_path +module Spmap : Map.S with type key = full_path -type extended_global_reference = - | TrueGlobal of global_reference - | SyntacticDef of kernel_name +val restrict_path : int -> full_path -> full_path (*s Temporary function to brutally form kernel names from section paths *) -val encode_kn : dir_path -> identifier -> kernel_name -val decode_kn : kernel_name -> dir_path * identifier +val encode_mind : dir_path -> identifier -> mutual_inductive +val decode_mind : mutual_inductive -> dir_path * identifier val encode_con : dir_path -> identifier -> constant val decode_con : constant -> dir_path * identifier (*s A [qualid] is a partially qualified ident; it includes fully qualified names (= absolute names) and all intermediate partial - qualifications of absolute names, including single identifiers *) + qualifications of absolute names, including single identifiers. + The [qualid] are used to access the name table. *) + type qualid val make_qualid : dir_path -> identifier -> qualid val repr_qualid : qualid -> dir_path * identifier -val string_of_qualid : qualid -> string val pr_qualid : qualid -> std_ppcmds - +val string_of_qualid : qualid -> string val qualid_of_string : string -> qualid -(* Turns an absolute name into a qualified name denoting the same name *) -val qualid_of_sp : section_path -> qualid +(* Turns an absolute name, a dirpath, or an identifier into a + qualified name denoting the same name *) +val qualid_of_path : full_path -> qualid val qualid_of_dirpath : dir_path -> qualid - -val make_short_qualid : identifier -> qualid +val qualid_of_ident : identifier -> qualid (* Both names are passed to objects: a "semantic" [kernel_name], which - can be substituted and a "syntactic" [section_path] which can be printed + can be substituted and a "syntactic" [full_path] which can be printed *) -type object_name = section_path * kernel_name +type object_name = full_path * kernel_name type object_prefix = dir_path * (module_path * dir_path) val make_oname : object_prefix -> identifier -> object_name (* to this type are mapped [dir_path]'s in the nametab *) -type global_dir_reference = +type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix @@ -137,7 +164,11 @@ type global_dir_reference = | DirClosedSection of dir_path (* this won't last long I hope! *) -type reference = +(*s A [reference] is the user-level notion of name. It denotes either a + global name (referred either by a qualified name or by a single + name) or a variable *) + +type reference = | Qualid of qualid located | Ident of identifier located @@ -146,8 +177,13 @@ val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc -(* popping one level of section in global names *) +(*s Popping one level of section in global names *) val pop_con : constant -> constant -val pop_kn : kernel_name -> kernel_name +val pop_kn : mutual_inductive-> mutual_inductive val pop_global_reference : global_reference -> global_reference + +(* Deprecated synonyms *) + +val make_short_qualid : identifier -> qualid (* = qualid_of_ident *) +val qualid_of_sp : full_path -> qualid (* = qualid_of_path *) -- cgit v1.2.3