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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Environ
open Univ
(* Generator of levels *)
type universe_id = DirPath.t * int
let new_univ_id, set_remote_new_univ_id =
RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
~build:(fun n -> Global.current_dirpath (), n)
let new_univ_level () =
let dp, id = new_univ_id () in
Univ.Level.make dp id
let fresh_level () = new_univ_level ()
(* TODO: remove *)
let new_univ dp = Univ.Universe.make (new_univ_level dp)
let new_Type dp = mkType (new_univ dp)
let new_Type_sort dp = Type (new_univ dp)
let fresh_universe_instance ctx =
let init _ = new_univ_level () in
Instance.of_array (Array.init (AUContext.size ctx) init)
let fresh_instance_from_context ctx =
let inst = fresh_universe_instance ctx in
let constraints = AUContext.instantiate inst ctx in
inst, constraints
let fresh_instance ctx =
let ctx' = ref LSet.empty in
let init _ =
let u = new_univ_level () in
ctx' := LSet.add u !ctx'; u
in
let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
in !ctx', inst
let existing_instance ctx inst =
let () =
let len1 = Array.length (Instance.to_array inst)
and len2 = AUContext.size ctx in
if not (len1 == len2) then
CErrors.user_err ~hdr:"Universes"
Pp.(str "Polymorphic constant expected " ++ int len2 ++
str" levels but was given " ++ int len1)
else ()
in LSet.empty, inst
let fresh_instance_from ctx inst =
let ctx', inst =
match inst with
| Some inst -> existing_instance ctx inst
| None -> fresh_instance ctx
in
let constraints = AUContext.instantiate inst ctx in
inst, (ctx', constraints)
(** Fresh universe polymorphic construction *)
let fresh_constant_instance env c inst =
let cb = lookup_constant c env in
match cb.Declarations.const_universes with
| Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
| Declarations.Polymorphic_const auctx ->
let inst, ctx =
fresh_instance_from auctx inst
in
((c, inst), ctx)
let fresh_inductive_instance env ind inst =
let mib, mip = Inductive.lookup_mind_specif env ind in
match mib.Declarations.mind_universes with
| Declarations.Monomorphic_ind _ ->
((ind,Instance.empty), ContextSet.empty)
| Declarations.Polymorphic_ind uactx ->
let inst, ctx = (fresh_instance_from uactx) inst in
((ind,inst), ctx)
| Declarations.Cumulative_ind acumi ->
let inst, ctx =
fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
in ((ind,inst), ctx)
let fresh_constructor_instance env (ind,i) inst =
let mib, mip = Inductive.lookup_mind_specif env ind in
match mib.Declarations.mind_universes with
| Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
| Declarations.Polymorphic_ind auctx ->
let inst, ctx = fresh_instance_from auctx inst in
(((ind,i),inst), ctx)
| Declarations.Cumulative_ind acumi ->
let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
(((ind,i),inst), ctx)
open Globnames
let fresh_global_instance ?names env gr =
match gr with
| VarRef id -> mkVar id, ContextSet.empty
| ConstRef sp ->
let c, ctx = fresh_constant_instance env sp names in
mkConstU c, ctx
| ConstructRef sp ->
let c, ctx = fresh_constructor_instance env sp names in
mkConstructU c, ctx
| IndRef sp ->
let c, ctx = fresh_inductive_instance env sp names in
mkIndU c, ctx
let fresh_constant_instance env sp =
fresh_constant_instance env sp None
let fresh_inductive_instance env sp =
fresh_inductive_instance env sp None
let fresh_constructor_instance env sp =
fresh_constructor_instance env sp None
let constr_of_global gr =
let c, ctx = fresh_global_instance (Global.env ()) gr in
if not (Univ.ContextSet.is_empty ctx) then
if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
(* Should be an error as we might forget constraints, allow for now
to make firstorder work with "using" clauses *)
c
else CErrors.user_err ~hdr:"constr_of_global"
Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
str " would forget universes.")
else c
let constr_of_global_univ (gr,u) =
match gr with
| VarRef id -> mkVar id
| ConstRef sp -> mkConstU (sp,u)
| ConstructRef sp -> mkConstructU (sp,u)
| IndRef sp -> mkIndU (sp,u)
let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
| IsGlobal gr -> fresh_global_instance env gr
let global_of_constr c =
match kind c with
| Const (c, u) -> ConstRef c, u
| Ind (i, u) -> IndRef i, u
| Construct (c, u) -> ConstructRef c, u
| Var id -> VarRef id, Instance.empty
| _ -> raise Not_found
open Declarations
let type_of_reference env r =
match r with
| VarRef id -> Environ.named_type id env, ContextSet.empty
| ConstRef c ->
let cb = Environ.lookup_constant c env in
let ty = cb.const_type in
begin
match cb.const_universes with
| Monomorphic_const _ -> ty, ContextSet.empty
| Polymorphic_const auctx ->
let inst, ctx = fresh_instance_from auctx None in
Vars.subst_instance_constr inst ty, ctx
end
| IndRef ind ->
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
begin
match mib.mind_universes with
| Monomorphic_ind _ ->
let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
ty, ContextSet.empty
| Polymorphic_ind auctx ->
let inst, ctx = fresh_instance_from auctx None in
let ty = Inductive.type_of_inductive env (specif, inst) in
ty, ctx
| Cumulative_ind cumi ->
let inst, ctx =
fresh_instance_from (ACumulativityInfo.univ_context cumi) None
in
let ty = Inductive.type_of_inductive env (specif, inst) in
ty, ctx
end
| ConstructRef cstr ->
let (mib,oib as specif) =
Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
in
begin
match mib.mind_universes with
| Monomorphic_ind _ ->
Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
| Polymorphic_ind auctx ->
let inst, ctx = fresh_instance_from auctx None in
Inductive.type_of_constructor (cstr,inst) specif, ctx
| Cumulative_ind cumi ->
let inst, ctx =
fresh_instance_from (ACumulativityInfo.univ_context cumi) None
in
Inductive.type_of_constructor (cstr,inst) specif, ctx
end
let type_of_global t = type_of_reference (Global.env ()) t
let fresh_sort_in_family env = function
| InProp -> Sorts.prop, ContextSet.empty
| InSet -> Sorts.set, ContextSet.empty
| InType ->
let u = fresh_level () in
Type (Univ.Universe.make u), ContextSet.singleton u
let new_sort_in_family sf =
fst (fresh_sort_in_family (Global.env ()) sf)
let extend_context (a, ctx) (ctx') =
(a, ContextSet.union ctx ctx')
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 LMap.empty, ctx
else
let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
let univs',subst = LSet.fold
(fun u (univs',subst) ->
let u' = fresh_level () in
(LSet.add u' univs', LMap.add u u' subst))
univs (LSet.empty, LMap.empty)
in
let cst' = subst_univs_level_constraints subst cst in
subst, (univs', cst')
|
