blob: f881f4b38b8ee04d70cda1dcb5181c523c75d8b9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Names
open Term
open Mod_subst
(** {6 Global reference is a kernel side type for all references together } *)
type global_reference =
| VarRef of variable
| ConstRef of constant
| IndRef of inductive
| 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
(** Turn a global reference into a construction *)
val constr_of_global : global_reference -> constr
(** Turn a construction denoting a global reference into a global reference;
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> global_reference
(** Obsolete synonyms for constr_of_global and global_of_constr *)
val constr_of_reference : global_reference -> constr
val reference_of_constr : constr -> 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
(** {6 Extended global references } *)
type syndef_name = kernel_name
type extended_global_reference =
| TrueGlobal of global_reference
| SynDef of syndef_name
(** {6 Dirpaths } *)
val pr_dirpath : dir_path -> Pp.std_ppcmds
val dirpath_of_string : string -> dir_path
val string_of_dirpath : dir_path -> string
(** 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 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 is_dirpath_prefix_of : dir_path -> dir_path -> bool
module Dirset : Set.S with type elt = dir_path
module Dirmap : Map.S with type key = dir_path
(** {6 Full paths are {e absolute} paths of declarations } *)
type full_path
(** Constructors of [full_path] *)
val make_path : dir_path -> identifier -> full_path
(** 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 -> full_path
val string_of_path : full_path -> string
val pr_path : full_path -> std_ppcmds
module Sppred : Predicate.S with type elt = full_path
module Spmap : Map.S with type key = full_path
val restrict_path : int -> full_path -> full_path
(** {6 Temporary function to brutally form kernel names from section paths } *)
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
(** {6 ... } *)
(** 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.
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 pr_qualid : qualid -> std_ppcmds
val string_of_qualid : qualid -> string
val qualid_of_string : string -> 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 qualid_of_ident : identifier -> qualid
(** Both names are passed to objects: a "semantic" [kernel_name], which
can be substituted and a "syntactic" [full_path] which can be printed
*)
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 =
| DirOpenModule of object_prefix
| DirOpenModtype of object_prefix
| DirOpenSection of object_prefix
| DirModule of object_prefix
| DirClosedSection of dir_path
(** this won't last long I hope! *)
(** {6 ... } *)
(** 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
val qualid_of_reference : reference -> qualid located
val string_of_reference : reference -> string
val pr_reference : reference -> std_ppcmds
val loc_of_reference : reference -> loc
(** {6 Popping one level of section in global names } *)
val pop_con : constant -> constant
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 *)
|
