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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** Universes. *)
module Level :
sig
type t
(** Type of universe levels. A universe level is essentially a unique name
that will be associated to constraints later on. *)
val make : Names.DirPath.t -> int -> t
(** Create a new universe level from a unique identifier and an associated
module path. *)
val equal : t -> t -> bool
end
type universe_level = Level.t
(** Alias name. *)
module Universe :
sig
type t
(** Type of universes. A universe is defined as a set of level expressions.
A level expression is built from levels and successors of level expressions, i.e.:
le ::= l + n, n \in N.
A universe is said atomic if it consists of a single level expression with
no increment, and algebraic otherwise (think the least upper bound of a set of
level expressions).
*)
val equal : t -> t -> bool
(** Equality function on formal universes *)
val make : Level.t -> t
(** Create a universe representing the given level. *)
end
type universe = Universe.t
(** Alias name. *)
val pr_uni : universe -> Pp.std_ppcmds
(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ...
Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
val type0m_univ : universe
val type0_univ : universe
val type1_univ : universe
val is_type0_univ : universe -> bool
val is_type0m_univ : universe -> bool
val is_univ_variable : universe -> bool
val sup : universe -> universe -> universe
val super : universe -> universe
(** {6 Graphs of universes. } *)
type universes
type 'a check_function = universes -> 'a -> 'a -> bool
val check_leq : universe check_function
val check_eq : universe check_function
(** The initial graph of universes: Prop < Set *)
val initial_universes : universes
(** {6 Constraints. } *)
type constraint_type = Lt | Le | Eq
type univ_constraint = universe_level * constraint_type * universe_level
module Constraint : Set.S with type elt = univ_constraint
type constraints = Constraint.t
val empty_constraint : constraints
(** A value with universe constraints. *)
type 'a constrained = 'a * constraints
(** Enforcing constraints. *)
type 'a constraint_function = 'a -> 'a -> constraints -> constraints
val enforce_leq : universe constraint_function
(** {6 ... } *)
(** Merge of constraints in a universes graph.
The function [merge_constraints] merges a set of constraints in a given
universes graph. It raises the exception [UniverseInconsistency] if the
constraints are not satisfiable. *)
(** Type explanation is used to decorate error messages to provide
useful explanation why a given constraint is rejected. It is composed
of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
.. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol
denoted by ri, currently only < and <=). The lowest end of the chain
is supposed known (see UniverseInconsistency exn). The upper end may
differ from the second univ of UniverseInconsistency because all
universes in the path are canonical. Note that each step does not
necessarily correspond to an actual constraint, but reflect how the
system stores the graph and may result from combination of several
constraints...
*)
type univ_inconsistency = constraint_type * universe * universe
exception UniverseInconsistency of univ_inconsistency
val merge_constraints : constraints -> universes -> universes
val check_constraints : constraints -> universes -> bool
(** {6 Support for old-style sort-polymorphism } *)
val subst_large_constraints :
(universe_level * universe) list -> universe -> universe
(** {6 Support for universe polymorphism } *)
(** Polymorphic maps from universe levels to 'a *)
module LMap : Map.S with type key = universe_level
type 'a universe_map = 'a LMap.t
(** {6 Substitution} *)
type universe_subst_fn = universe_level -> universe
type universe_level_subst_fn = universe_level -> universe_level
(** A full substitution, might involve algebraic universes *)
type universe_subst = universe universe_map
type universe_level_subst = universe_level universe_map
val level_subst_of : universe_subst_fn -> universe_level_subst_fn
(** {6 Universe instances} *)
module Instance :
sig
type t
(** A universe instance represents a vector of argument universes
to a polymorphic definition (constant, inductive or constructor). *)
val empty : t
val is_empty : t -> bool
val equal : t -> t -> bool
(** Equality (note: instances are hash-consed, this is O(1)) *)
val subst_fn : universe_level_subst_fn -> t -> t
(** Substitution by a level-to-level function. *)
val subst : universe_level_subst -> t -> t
(** Substitution by a level-to-level function. *)
val pr : t -> Pp.std_ppcmds
(** Pretty-printing, no comments *)
val check_eq : t check_function
(** Check equality of instances w.r.t. a universe graph *)
end
type universe_instance = Instance.t
type 'a puniverses = 'a * universe_instance
(** A vector of universe levels with universe constraints,
representiong local universe variables and associated constraints *)
module UContext :
sig
type t
val empty : t
val instance : t -> Instance.t
val constraints : t -> constraints
end
type universe_context = UContext.t
val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
(** Substitution of universes. *)
val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
val subst_univs_level_universe : universe_level_subst -> universe -> universe
(** Level to universe substitutions. *)
val is_empty_subst : universe_subst -> bool
val make_subst : universe_subst -> universe_subst_fn
val subst_univs_universe : universe_subst_fn -> universe -> universe
(** Substitution of instances *)
val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
val subst_instance_universe : universe_instance -> universe -> universe
val subst_instance_constraints : universe_instance -> constraints -> constraints
(* val make_instance_subst : universe_instance -> universe_level_subst *)
(* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
(** Get the instantiated graph. *)
val instantiate_univ_context : universe_context -> universe_context
val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
(** {6 Pretty-printing of universes. } *)
val pr_universes : universes -> Pp.std_ppcmds
|
