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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Reduction
open Declarations
open Constr
open Univ
open Util
(** Throughout this module we modify a map [variances] from local
universes to [Variance.t]. It starts as a trivial mapping to
[Irrelevant] and every time we encounter a local universe we
restrict it accordingly. *)
let infer_level_eq u variances =
if LMap.mem u variances
then LMap.set u Variance.Invariant variances
else variances
let infer_level_leq u variances =
match LMap.find u variances with
| exception Not_found -> variances
| varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances
let infer_generic_instance_eq variances u =
Array.fold_left (fun variances u -> infer_level_eq u variances)
variances (Instance.to_array u)
let variance_pb cv_pb var =
let open Variance in
match cv_pb, var with
| _, Irrelevant -> Irrelevant
| _, Invariant -> Invariant
| CONV, Covariant -> Invariant
| CUMUL, Covariant -> Covariant
let infer_cumulative_ind_instance cv_pb cumi variances u =
Array.fold_left2 (fun variances varu u ->
match LMap.find u variances with
| exception Not_found -> variances
| varu' ->
LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
let infer_inductive_instance cv_pb env variances ind nargs u =
let mind = Environ.lookup_mind (fst ind) env in
match mind.mind_universes with
| Monomorphic_ind _ -> assert (Instance.is_empty u); variances
| Polymorphic_ind _ -> infer_generic_instance_eq variances u
| Cumulative_ind cumi ->
if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
then infer_generic_instance_eq variances u
else infer_cumulative_ind_instance cv_pb cumi variances u
let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
let mind = Environ.lookup_mind mi env in
match mind.mind_universes with
| Monomorphic_ind _ -> assert (Instance.is_empty u); variances
| Polymorphic_ind _ -> infer_generic_instance_eq variances u
| Cumulative_ind cumi ->
if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
then infer_generic_instance_eq variances u
else infer_cumulative_ind_instance CONV cumi variances u
let infer_sort cv_pb variances s =
match cv_pb with
| CONV ->
LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances
| CUMUL ->
LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
let infer_table_key infos variances c =
let open Names in
match c with
| ConstKey (_, u) ->
infer_generic_instance_eq variances u
| VarKey _ | RelKey _ -> variances
let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk
let rec infer_fterm cv_pb infos variances hd stk =
Control.check_for_interrupt ();
let hd,stk = whd_stack infos hd stk in
let open CClosure in
match fterm_of hd with
| FAtom a ->
begin match kind a with
| Sort s -> infer_sort cv_pb variances s
| Meta _ -> infer_stack infos variances stk
| _ -> assert false
end
| FEvar ((_,args),e) ->
let variances = infer_stack infos variances stk in
infer_vect infos variances (Array.map (mk_clos e) args)
| FRel _ -> variances
| FFlex fl ->
let variances = infer_table_key infos variances fl in
infer_stack infos variances stk
| FProj (_,c) ->
let variances = infer_fterm CONV infos variances c [] in
infer_stack infos variances stk
| FLambda _ ->
let (_,ty,bd) = destFLambda mk_clos hd in
let variances = infer_fterm CONV infos variances ty [] in
infer_fterm CONV infos variances bd []
| FProd (_,dom,codom) ->
let variances = infer_fterm CONV infos variances dom [] in
infer_fterm cv_pb infos variances codom []
| FInd (ind, u) ->
let variances =
if Instance.is_empty u then variances
else
let nargs = stack_args_size stk in
infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u
in
infer_stack infos variances stk
| FConstruct (ctor,u) ->
let variances =
if Instance.is_empty u then variances
else
let nargs = stack_args_size stk in
infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u
in
infer_stack infos variances stk
| FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
let n = Array.length cl in
let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in
let le = Esubst.subs_liftn n e in
let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
infer_stack infos variances stk
(* Removed by whnf *)
| FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
and infer_stack infos variances (stk:CClosure.stack) =
match stk with
| [] -> variances
| z :: stk ->
let open CClosure in
let variances = match z with
| Zapp v -> infer_vect infos variances v
| Zproj _ -> variances
| Zfix (fx,a) ->
let variances = infer_fterm CONV infos variances fx [] in
infer_stack infos variances a
| ZcaseT (ci,p,br,e) ->
let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
infer_vect infos variances (Array.map (mk_clos e) br)
| Zshift _ -> variances
| Zupdate _ -> variances
in
infer_stack infos variances stk
and infer_vect infos variances v =
Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
let infer_term cv_pb env variances c =
let open CClosure in
let infos = (create_clos_infos all env, create_tab ()) in
infer_fterm cv_pb infos variances (CClosure.inject c) []
let infer_arity_constructor is_arity env variances arcn =
let infer_typ typ (env,variances) =
match typ with
| Context.Rel.Declaration.LocalAssum (_, typ') ->
(Environ.push_rel typ env, infer_term CUMUL env variances typ')
| Context.Rel.Declaration.LocalDef _ -> assert false
in
let typs, codom = Reduction.dest_prod env arcn in
let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
(* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
i is irrelevant, j is invariant. *)
if not is_arity then infer_term CUMUL env variances codom else variances
let infer_inductive env mie =
let open Entries in
let { mind_entry_params = params;
mind_entry_inds = entries; } = mie
in
let univs =
match mie.mind_entry_universes with
| Monomorphic_ind_entry _
| Polymorphic_ind_entry _ as univs -> univs
| Cumulative_ind_entry cumi ->
let uctx = CumulativityInfo.univ_context cumi in
let uarray = Instance.to_array @@ UContext.instance uctx in
let env = Environ.push_context uctx env in
let variances =
Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
LMap.empty uarray
in
let env, _ = Typeops.infer_local_decls env params in
let variances = List.fold_left (fun variances entry ->
let variances = infer_arity_constructor true
env variances entry.mind_entry_arity
in
List.fold_left (infer_arity_constructor false env)
variances entry.mind_entry_lc)
variances
entries
in
let variances = Array.map (fun u -> LMap.find u variances) uarray in
Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
in
{ mie with mind_entry_universes = univs }
|
