blob: 0e45778d0ac6cae2c5835486fd1c9cdfc79a82f2 (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*s Identifiers *)
type identifier
type name = Name of identifier | Anonymous
(* Parsing and printing of identifiers *)
val string_of_id : identifier -> string
val id_of_string : string -> identifier
val id_ord : identifier -> identifier -> int
(* Identifiers sets and maps *)
module Idset : Set.S with type elt = identifier
module Idpred : Predicate.S with type elt = identifier
module Idmap : Map.S with type key = identifier
(*s Directory paths = section names paths *)
type module_ident = identifier
module ModIdmap : Map.S with type key = module_ident
type dir_path
(* Inner modules idents on top of list (to improve sharing).
For instance: A.B.C is ["C";"B";"A"] *)
val make_dirpath : module_ident list -> dir_path
val repr_dirpath : dir_path -> module_ident list
val empty_dirpath : dir_path
(* Printing of directory paths as ["coq_root.module.submodule"] *)
val string_of_dirpath : dir_path -> string
(*s Unique identifier to be used as "self" in structures and
signatures - invisible for users *)
type mod_self_id
(* The first argument is a file name - to prevent conflict between
different files *)
val make_msid : dir_path -> string -> mod_self_id
val id_of_msid : mod_self_id -> identifier
val debug_string_of_msid : mod_self_id -> string
(*s Unique names for bound modules *)
type mod_bound_id
val make_mbid : dir_path -> string -> mod_bound_id
val id_of_mbid : mod_bound_id -> identifier
val debug_string_of_mbid : mod_bound_id -> string
(*s Names of structure elements *)
type label
val mk_label : string -> label
val string_of_label : label -> string
val label_of_id : identifier -> label
val id_of_label : label -> identifier
module Labset : Set.S with type elt = label
module Labmap : Map.S with type key = label
(*s The module part of the kernel name *)
type module_path =
| MPfile of dir_path
| MPbound of mod_bound_id
| MPself of mod_self_id
| MPdot of module_path * label
(*i | MPapply of module_path * module_path in the future (maybe) i*)
val string_of_mp : module_path -> string
module MPset : Set.S with type elt = module_path
module MPmap : Map.S with type key = module_path
(*s Substitutions *)
type substitution
val empty_subst : substitution
val add_msid :
mod_self_id -> module_path -> substitution -> substitution
val add_mbid :
mod_bound_id -> module_path -> substitution -> substitution
val map_msid : mod_self_id -> module_path -> substitution
val map_mbid : mod_bound_id -> module_path -> substitution
(* sequential composition:
[substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
*)
val join : substitution -> substitution -> substitution
(*i debugging *)
val debug_string_of_subst : substitution -> string
val debug_pr_subst : substitution -> Pp.std_ppcmds
(*i*)
(* [subst_mp sub mp] guarantees that whenever the result of the
substitution is structutally equal [mp], it is equal by pointers
as well [==] *)
val subst_mp :
substitution -> module_path -> module_path
(* [occur_*id id sub] returns true iff [id] occurs in [sub]
on either side *)
val occur_msid : mod_self_id -> substitution -> bool
val occur_mbid : mod_bound_id -> substitution -> bool
(* Name of the toplevel structure *)
val initial_msid : mod_self_id
val initial_path : module_path (* [= MPself initial_msid] *)
(* Initial "seed" of the unique identifier generator *)
val initial_dir : dir_path
(*s The absolute names of objects seen by kernel *)
type kernel_name
(* Constructor and destructor *)
val make_kn : module_path -> dir_path -> label -> kernel_name
val repr_kn : kernel_name -> module_path * dir_path * label
val modpath : kernel_name -> module_path
val label : kernel_name -> label
val string_of_kn : kernel_name -> string
val pr_kn : kernel_name -> Pp.std_ppcmds
val subst_kn : substitution -> kernel_name -> kernel_name
module KNset : Set.S with type elt = kernel_name
module KNpred : Predicate.S with type elt = kernel_name
module KNmap : Map.S with type key = kernel_name
(*s Specific paths for declarations *)
type variable = identifier
type constant = kernel_name
type mutual_inductive = kernel_name
(* Beware: first inductive has index 0 *)
type inductive = mutual_inductive * int
(* Beware: first constructor has index 1 *)
type constructor = inductive * int
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
val index_of_constructor : constructor -> int
(* Better to have it here that in Closure, since required in grammar.cma *)
type evaluable_global_reference =
| EvalVarRef of identifier
| EvalConstRef of constant
(* Hash-consing *)
val hcons_names : unit ->
(kernel_name -> kernel_name) * (dir_path -> dir_path) *
(name -> name) * (identifier -> identifier) * (string -> string)
|
