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
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <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 *)
(************************************************************************)
open Util
open Pp
open Names
open Term
open Context
open Environ
open Locus
open Univ
(** Universes *)
type universe_names =
Univ.universe_level Idmap.t * Id.t Univ.LMap.t
val global_universe_names : unit -> universe_names
val set_global_universe_names : universe_names -> unit
(** The global universe counter *)
val set_remote_new_univ_level : universe_level RemoteCounter.installer
(** Side-effecting functions creating new universe levels. *)
val new_univ_level : Names.dir_path -> universe_level
val new_univ : Names.dir_path -> universe
val new_Type : Names.dir_path -> types
val new_Type_sort : Names.dir_path -> sorts
val new_global_univ : unit -> universe in_universe_context_set
val new_sort_in_family : sorts_family -> sorts
(** {6 Constraints for type inference}
When doing conversion of universes, not only do we have =/<= constraints but
also Lub constraints which correspond to unification of two levels which might
not be necessary if unfolding is performed.
*)
type universe_constraint_type = ULe | UEq | ULub
type universe_constraint = universe * universe_constraint_type * universe
module Constraints : sig
include Set.S with type elt = universe_constraint
val pr : t -> Pp.std_ppcmds
end
type universe_constraints = Constraints.t
type 'a universe_constrained = 'a * universe_constraints
type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
val subst_univs_universe_constraints : universe_subst_fn ->
universe_constraints -> universe_constraints
val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
val to_constraints : universes -> universe_constraints -> constraints
(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
application grouping, the universe constraints in [u] and additional constraints [c]. *)
val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
modulo alpha, casts, application grouping, the universe constraints
in [u] and additional constraints [c]. *)
val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and the universe constraints in [c]. *)
val eq_constr_universes : constr -> constr -> bool universe_constrained
(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
alpha, casts, application grouping and the universe constraints in [c]. *)
val leq_constr_universes : constr -> constr -> bool universe_constrained
(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and the universe constraints in [c]. *)
val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
val fresh_instance_from_context : universe_context ->
universe_instance constrained
val fresh_instance_from : universe_context -> universe_instance option ->
universe_instance in_universe_context_set
val fresh_sort_in_family : env -> sorts_family ->
sorts in_universe_context_set
val fresh_constant_instance : env -> constant ->
pconstant in_universe_context_set
val fresh_inductive_instance : env -> inductive ->
pinductive in_universe_context_set
val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference ->
constr in_universe_context_set
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
constr in_universe_context_set
(** Get fresh variables for the universe context.
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
val fresh_universe_context_set_instance : universe_context_set ->
universe_level_subst * universe_context_set
(** Raises [Not_found] if not a global reference. *)
val global_of_constr : constr -> Globnames.global_reference puniverses
val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option
val constr_of_global_univ : Globnames.global_reference puniverses -> constr
val extend_context : 'a in_universe_context_set -> universe_context_set ->
'a in_universe_context_set
(** Simplification and pruning of constraints:
[normalize_context_set ctx us]
- Instantiate the variables in [us] with their most precise
universe levels respecting the constraints.
- Normalizes the context [ctx] w.r.t. equality constraints,
choosing a canonical universe in each equivalence class
(a global one if there is one) and transitively saturate
the constraints w.r.t to the equalities. *)
module UF : Unionfind.PartitionSig with type elt = universe_level
type universe_opt_subst = universe option universe_map
val make_opt_subst : universe_opt_subst -> universe_subst_fn
val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
val normalize_context_set : universe_context_set ->
universe_opt_subst (* The defined and undefined variables *) ->
universe_set (* univ variables that can be substituted by algebraics *) ->
(universe_opt_subst * universe_set) in_universe_context_set
val normalize_univ_variables : universe_opt_subst ->
universe_opt_subst * universe_set * universe_set * universe_subst
val normalize_univ_variable :
find:(universe_level -> universe) ->
update:(universe_level -> universe -> universe) ->
universe_level -> universe
val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
(universe_level -> universe)
val normalize_univ_variable_subst : universe_subst ref ->
(universe_level -> universe)
val normalize_universe_opt_subst : universe_opt_subst ref ->
(universe -> universe)
val normalize_universe_subst : universe_subst ref ->
(universe -> universe)
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
the constraints should be properly added to an evd.
See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
the proper way to get a fresh copy of a global reference. *)
val constr_of_global : Globnames.global_reference -> constr
(** ** DEPRECATED ** synonym of [constr_of_global] *)
val constr_of_reference : Globnames.global_reference -> constr
(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
references by taking the original universe instance that is not recorded
anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
(** Returns the type of the global reference, by creating a fresh instance of polymorphic
references and computing their instantiated universe context. (side-effect on the
universe counter, use with care). *)
val type_of_global : Globnames.global_reference -> types in_universe_context_set
(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
references by taking the original universe instance that is not recorded
anywhere. The constraints are forgotten as well.
USE with care. *)
val unsafe_type_of_global : Globnames.global_reference -> types
(** Full universes substitutions into terms *)
val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
universe_opt_subst -> constr -> constr
(** Shrink a universe context to a restricted set of variables *)
val universes_of_constr : constr -> universe_set
val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
val simplify_universe_context : universe_context_set ->
universe_context_set * universe_level_subst
val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
(** Pretty-printing *)
val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
(* For tracing *)
type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
val pr_constraints_map : constraints_map -> Pp.std_ppcmds
val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set ->
universe_level * (universe_set * universe_set * universe_set)
val compute_lbound : (constraint_type * Univ.universe) list -> universe option
val instantiate_with_lbound :
Univ.LMap.key ->
Univ.universe ->
bool ->
bool ->
Univ.LSet.t * Univ.universe option Univ.LMap.t *
Univ.LSet.t *
(bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
(Univ.LSet.t * Univ.universe option Univ.LMap.t *
Univ.LSet.t *
(bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
(bool * bool * Univ.universe)
val minimize_univ_variables :
Univ.LSet.t ->
Univ.universe option Univ.LMap.t ->
Univ.LSet.t ->
constraints_map -> constraints_map ->
Univ.constraints ->
Univ.LSet.t * Univ.universe option Univ.LMap.t *
Univ.LSet.t *
(bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
(** {6 Support for old-style sort-polymorphism } *)
val solve_constraints_system : universe option array -> universe array -> universe array ->
universe array
|
