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
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Sorts
open Names
open Constr
open Univ
open UVars
module QualityOrSet = struct
type t = Qual of Quality.t | Set
let equal a b = match a, b with
| Qual a, Qual b -> Quality.equal a b
| Set, Set -> true
| Qual _, Set | Set, Qual _ -> false
let compare a b = match a, b with
| Qual a, Qual b -> Quality.compare a b
| Set, Set -> 0
| Qual _, Set -> 1
| Set, Qual _ -> -1
let eliminates_to a b =
let to_qual = function
| Set -> Quality.qtype
| Qual q -> q
in Quality.eliminates_to (to_qual a) (to_qual b)
let of_quality q = Qual q
let of_sort s = match s with
| Sorts.Set -> Set
| s -> of_quality (Sorts.quality s)
let quality q = match q with
| Set -> Quality.qtype
| Qual q -> q
let set = Set
let qtype = Qual Quality.qtype
let prop = Qual Quality.qprop
let sprop = Qual Quality.qsprop
let is_type q = match q with
| Set -> false
| Qual q -> Quality.is_qtype q
let is_set q = match q with
| Set -> true
| Qual _ -> false
let is_prop q = match q with
| Set -> false
| Qual q -> Quality.is_qprop q
let is_sprop q = match q with
| Set -> false
| Qual q -> Quality.is_qsprop q
let pr prv q = match q with
| Set -> Pp.str"Set"
| Qual q -> Quality.pr prv q
let raw_pr = pr Sorts.QVar.raw_pr
let all_constants = Set :: List.map (fun q -> Qual q) Quality.all_constants
let all = Set :: List.map (fun q -> Qual q) Quality.all
end
type sort_context_set = (Sorts.QVar.Set.t * Univ.Level.Set.t) * Univ.Constraints.t
type 'a in_sort_context_set = 'a * sort_context_set
let empty_sort_context = (QVar.Set.empty, Level.Set.empty), Constraints.empty
let is_empty_sort_context ((qs,us),csts) =
QVar.Set.is_empty qs && Level.Set.is_empty us && Constraints.is_empty csts
let sort_context_union ((qs,us),csts) ((qs',us'),csts') =
((QVar.Set.union qs qs', Level.Set.union us us'),Constraints.union csts csts')
let diff_sort_context ((qs,us),csts) ((qs',us'),csts') =
(QVar.Set.diff qs qs', Level.Set.diff us us'), Constraints.diff csts csts'
type univ_length_mismatch = {
gref : GlobRef.t;
actual : int * int;
expect : int * int;
}
(* Due to an OCaml bug ocaml/ocaml#10027 inlining this record will cause
compliation with -rectypes to crash. *)
exception UniverseLengthMismatch of univ_length_mismatch
let () = CErrors.register_handler (function
| UniverseLengthMismatch { gref; actual=(aq,au); expect=(eq,eu) } ->
let ppreal, ppexpected =
if aq = 0 && eq = 0 then Pp.(int au, int eu)
else Pp.(str "(" ++ int aq ++ str " | " ++ int au ++ str ")"
, str "(" ++ int eq ++ str " | " ++ int eu ++ str ")")
in
Some Pp.(str "Universe instance length for " ++ Nametab.pr_global_env Id.Set.empty gref ++
spc() ++ str "is " ++ ppreal ++
spc() ++ str "but should be " ++ ppexpected ++ str".")
| _ -> None)
(* Generator of levels *)
let new_univ_id =
let cnt = ref 0 in
fun () -> incr cnt; !cnt
let new_univ_global () =
let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
Univ.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ())
let fresh_level () =
Univ.Level.make (new_univ_global ())
let new_sort_id =
let cnt = ref 0 in
fun () -> incr cnt; !cnt
let new_sort_global id =
Sorts.QGlobal.make (Global.current_dirpath ()) id
let fresh_sort_quality () =
let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
Sorts.QVar.make_unif s (new_sort_id ())
let fresh_instance auctx : _ in_sort_context_set =
let qlen, ulen = AbstractContext.size auctx in
let qinst = Array.init qlen (fun _ -> Sorts.Quality.QVar (fresh_sort_quality ())) in
let uinst = Array.init ulen (fun _ -> fresh_level()) in
let qctx = Array.fold_left (fun qctx q -> match q with
| Sorts.Quality.QVar q -> Sorts.QVar.Set.add q qctx
| _ -> assert false)
Sorts.QVar.Set.empty
qinst
in
let uctx = Array.fold_right Level.Set.add uinst Level.Set.empty in
let inst = Instance.of_array (qinst,uinst) in
inst, ((qctx,uctx), AbstractContext.instantiate inst auctx)
let existing_instance ?loc ~gref auctx inst =
let () =
let actual = Instance.length inst
and expect = AbstractContext.size auctx in
if not (UVars.eq_sizes actual expect) then
Loc.raise ?loc (UniverseLengthMismatch { gref; actual; expect })
else ()
in
inst, ((Sorts.QVar.Set.empty,Level.Set.empty), AbstractContext.instantiate inst auctx)
let fresh_instance_from ?loc ctx = function
| Some (gref,inst) -> existing_instance ?loc ~gref ctx inst
| None -> fresh_instance ctx
(** Fresh universe polymorphic construction *)
let fresh_global_instance ?loc ?names env gr =
let auctx = Environ.universes_of_global env gr in
let names = Option.map (fun x -> gr, x) names in
let u, ctx = fresh_instance_from ?loc auctx names in
u, ctx
let fresh_constant_instance env c =
let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in
(c, u), ctx
let fresh_inductive_instance env ind =
let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in
(ind, u), ctx
let fresh_constructor_instance env c =
let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
(c, u), ctx
let fresh_array_instance env =
let auctx = CPrimitives.typ_univs CPrimitives.PT_array in
let u, ctx = fresh_instance_from auctx None in
u, ctx
let fresh_global_instance ?loc ?names env gr =
let u, ctx = fresh_global_instance ?loc ?names env gr in
mkRef (gr, u), ctx
let constr_of_monomorphic_global env gr =
if not (Environ.is_polymorphic env gr) then
fst (fresh_global_instance env gr)
else CErrors.user_err
Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
str " would forget universes.")
let fresh_sort_in_quality =
let open QualityOrSet in
function
| Qual (QConstant QSProp) -> Sorts.sprop, empty_sort_context
| Qual (QConstant QProp) -> Sorts.prop, empty_sort_context
| Set -> Sorts.set, empty_sort_context
| Qual (QConstant QType | QVar _ (* Treat as Type *)) ->
let u = fresh_level () in
sort_of_univ (Univ.Universe.make u), ((QVar.Set.empty,Level.Set.singleton u), Constraints.empty)
let new_global_univ () =
let u = fresh_level () in
(Univ.Universe.make u, ContextSet.singleton u)
let fresh_universe_context_set_instance ctx =
if ContextSet.is_empty ctx then Level.Map.empty, ctx
else
let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
let univs',subst = Level.Set.fold
(fun u (univs',subst) ->
let u' = fresh_level () in
(Level.Set.add u' univs', Level.Map.add u u' subst))
univs (Level.Set.empty, Level.Map.empty)
in
let cst' = subst_univs_level_constraints subst cst in
subst, (univs', cst')
let fresh_sort_context_instance ((qs,us),csts) =
let usubst, (us, csts) = fresh_universe_context_set_instance (us,csts) in
let qsubst, qs = QVar.Set.fold (fun q (qsubst,qs) ->
let q' = fresh_sort_quality () in
QVar.Map.add q (Sorts.Quality.QVar q') qsubst, QVar.Set.add q' qs)
qs
(QVar.Map.empty, QVar.Set.empty)
in
(qsubst, usubst), ((qs, us), csts)
|
