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
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
module CVars = Vars
open Pp
open CErrors
open Util
open Term
open Constr
open Environ
open EConstr
open Vars
open Reductionops
open Inductive
open Inductiveops
open Typeops
open Arguments_renaming
open Pretype_errors
open Context.Rel.Declaration
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
meta_instance evd ty
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
let type_judgment env sigma j =
match EConstr.kind sigma (whd_all env sigma j.uj_type) with
| Sort s -> sigma, {utj_val = j.uj_val; utj_type = ESorts.kind sigma s }
| Evar ev ->
let (sigma,s) = Evardefine.define_evar_as_sort env sigma ev in
sigma, { utj_val = j.uj_val; utj_type = s }
| _ -> error_not_a_type env sigma j
let assumption_of_judgment env sigma j =
try
let sigma, j = type_judgment env sigma j in
sigma, j.utj_val
with Type_errors.TypeError _ | PretypeError _ ->
error_assumption env sigma j
let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
let rec apply_rec sigma n typ = function
| [] ->
sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv);
uj_type =
let ar = inductive_type_knowing_parameters env sigma ind argjv in
hnf_prod_appvect env sigma (EConstr.of_constr ar) (Array.map j_val argjv) }
| hj::restjl ->
let sigma, (c1,c2) =
match EConstr.kind sigma (whd_all env sigma typ) with
| Prod (_,c1,c2) -> sigma, (c1,c2)
| Evar ev ->
let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
let (_,c1,c2) = destProd sigma t in
sigma, (c1,c2)
| _ ->
error_cant_apply_not_functional env sigma funj argjv
in
begin match Evarconv.cumul env sigma hj.uj_type c1 with
| Some sigma ->
apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
| None ->
error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
end
in
apply_rec sigma 1 funj.uj_type (Array.to_list argjv)
let judge_of_apply env sigma funj argjv =
let rec apply_rec sigma n typ = function
| [] ->
sigma, { uj_val = mkApp (j_val funj, Array.map j_val argjv);
uj_type = typ }
| hj::restjl ->
let sigma, (c1,c2) =
match EConstr.kind sigma (whd_all env sigma typ) with
| Prod (_,c1,c2) -> sigma, (c1,c2)
| Evar ev ->
let (sigma,t) = Evardefine.define_evar_as_product sigma ev in
let (_,c1,c2) = destProd sigma t in
sigma, (c1,c2)
| _ ->
error_cant_apply_not_functional env sigma funj argjv
in
begin match Evarconv.cumul env sigma hj.uj_type c1 with
| Some sigma ->
apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
| None ->
error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
end
in
apply_rec sigma 1 funj.uj_type (Array.to_list argjv)
let check_branch_types env sigma (ind,u) cj (lfj,explft) =
if not (Int.equal (Array.length lfj) (Array.length explft)) then
error_number_branches env sigma cj (Array.length explft);
Array.fold_left2_i (fun i sigma lfj explft ->
match Evarconv.cumul env sigma lfj.uj_type explft with
| Some sigma -> sigma
| None ->
error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft)
sigma lfj explft
let max_sort l =
if Sorts.List.mem InType l then InType else
if Sorts.List.mem InSet l then InSet else InProp
let is_correct_arity env sigma c pj ind specif params =
let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in
let allowed_sorts = elim_sorts specif in
let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in
let rec srec env sigma pt ar =
let pt' = whd_all env sigma pt in
match EConstr.kind sigma pt', ar with
| Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
begin match Evarconv.cumul env sigma a1 a1' with
| None -> error ()
| Some sigma ->
srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar'
end
| Sort s, [] ->
let s = ESorts.kind sigma s in
if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
then error ()
else sigma
| Evar (ev,_), [] ->
let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in
let sigma = Evd.define ev (mkSort s) sigma in
sigma
| _, (LocalDef _ as d)::ar' ->
srec (push_rel d env) sigma (lift 1 pt') ar'
| _ ->
error ()
in
srec env sigma pj.uj_type (List.rev arsign)
let lambda_applist_assum sigma n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
else anomaly (Pp.str "Not enough arguments.")
else match EConstr.kind sigma t, l with
| Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
| _ -> anomaly (Pp.str "Not enough lambda/let's.") in
app n [] c l
let type_case_branches env sigma (ind,largs) pj c =
let specif = lookup_mind_specif env (fst ind) in
let nparams = inductive_params specif in
let (params,realargs) = List.chop nparams largs in
let p = pj.uj_val in
let params = List.map EConstr.Unsafe.to_constr params in
let sigma = is_correct_arity env sigma c pj ind specif params in
let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
let lc = Array.map EConstr.of_constr lc in
let n = (snd specif).Declarations.mind_nrealdecls in
let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
sigma, (lc, ty)
let judge_of_case env sigma ci pj cj lfj =
let ((ind, u), spec) =
try find_mrectype env sigma cj.uj_type
with Not_found -> error_case_not_inductive env sigma cj in
let indspec = ((ind, EInstance.kind sigma u), spec) in
let _ = check_case_info env (fst indspec) ci in
let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in
let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in
sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
uj_type = rslty }
let check_type_fixpoint ?loc env sigma lna lar vdefj =
let lt = Array.length vdefj in
assert (Int.equal (Array.length lar) lt);
Array.fold_left2_i (fun i sigma defj ar ->
match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with
| Some sigma -> sigma
| None ->
error_ill_typed_rec_body ?loc env sigma
i lna vdefj lar)
sigma vdefj lar
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
let specif = Global.lookup_inductive (fst ind) in
let sorts = elim_sorts specif in
let pj = Retyping.get_judgment_of env sigma p in
let _, s = splay_prod env sigma pj.uj_type in
let ksort = match EConstr.kind sigma s with
| Sort s -> Sorts.family (ESorts.kind sigma s)
| _ -> error_elim_arity env sigma ind sorts c pj None in
if not (List.exists ((==) ksort) sorts) then
let s = inductive_sort_family (snd specif) in
error_elim_arity env sigma ind sorts c pj
(Some(ksort,s,Type_errors.error_elim_explain ksort s))
let judge_of_cast env sigma cj k tj =
let expected_type = tj.utj_val in
match Evarconv.cumul env sigma cj.uj_type expected_type with
| None ->
error_actual_type_core env sigma cj expected_type;
| Some sigma ->
sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
uj_type = expected_type }
let enrich_env env sigma =
set_universes env @@ Evd.universes sigma
let check_fix env sigma pfix =
let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let (idx, (ids, cs, ts)) = pfix in
check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
let check_cofix env sigma pcofix =
let inj c = EConstr.to_constr sigma c in
let (idx, (ids, cs, ts)) = pcofix in
check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
(* The typing machine with universes and existential variables. *)
let judge_of_prop =
{ uj_val = EConstr.mkProp;
uj_type = EConstr.mkSort Sorts.type1 }
let judge_of_set =
{ uj_val = EConstr.mkSet;
uj_type = EConstr.mkSort Sorts.type1 }
let judge_of_type u =
let uu = Univ.Universe.super u in
{ uj_val = EConstr.mkType u;
uj_type = EConstr.mkType uu }
let judge_of_relative env v =
Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
let judge_of_variable env id =
Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
let judge_of_projection env sigma p cj =
let pb = lookup_projection p env in
let (ind,u), args =
try find_mrectype env sigma cj.uj_type
with Not_found -> error_case_not_inductive env sigma cj
in
let u = EInstance.kind sigma u in
let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
let ty = substl (cj.uj_val :: List.rev args) ty in
{uj_val = EConstr.mkProj (p,cj.uj_val);
uj_type = ty}
let judge_of_abstraction env name var j =
{ uj_val = mkLambda (name, var.utj_val, j.uj_val);
uj_type = mkProd (name, var.utj_val, j.uj_type) }
let judge_of_product env name t1 t2 =
let s = sort_of_product env t1.utj_type t2.utj_type in
{ uj_val = mkProd (name, t1.utj_val, t2.utj_val);
uj_type = mkSort s }
let judge_of_letin env name defj typj j =
{ uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
uj_type = subst1 defj.uj_val j.uj_type }
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
let rec execute env sigma cstr =
let cstr = whd_evar sigma cstr in
match EConstr.kind sigma cstr with
| Meta n ->
sigma, { uj_val = cstr; uj_type = meta_type sigma n }
| Evar ev ->
let ty = EConstr.existential_type sigma ev in
let sigma, jty = execute env sigma ty in
let sigma, jty = assumption_of_judgment env sigma jty in
sigma, { uj_val = cstr; uj_type = jty }
| Rel n ->
sigma, judge_of_relative env n
| Var id ->
sigma, judge_of_variable env id
| Const (c, u) ->
let u = EInstance.kind sigma u in
sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
| Ind (ind, u) ->
let u = EInstance.kind sigma u in
sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
| Construct (cstruct, u) ->
let u = EInstance.kind sigma u in
sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
| Case (ci,p,c,lf) ->
let sigma, cj = execute env sigma c in
let sigma, pj = execute env sigma p in
let sigma, lfj = execute_array env sigma lf in
judge_of_case env sigma ci pj cj lfj
| Fix ((vn,i as vni),recdef) ->
let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
let fix = (vni,recdef') in
check_fix env sigma fix;
sigma, make_judge (mkFix fix) tys.(i)
| CoFix (i,recdef) ->
let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in
let cofix = (i,recdef') in
check_cofix env sigma cofix;
sigma, make_judge (mkCoFix cofix) tys.(i)
| Sort s ->
begin match ESorts.kind sigma s with
| Prop -> sigma, judge_of_prop
| Set -> sigma, judge_of_set
| Type u -> sigma, judge_of_type u
end
| Proj (p, c) ->
let sigma, cj = execute env sigma c in
sigma, judge_of_projection env sigma p cj
| App (f,args) ->
let sigma, jl = execute_array env sigma args in
(match EConstr.kind sigma f with
| Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env ->
let sigma, fj = execute env sigma f in
judge_of_applied_inductive_knowing_parameters env sigma fj (ind, u) jl
| _ ->
(* No template polymorphism *)
let sigma, fj = execute env sigma f in
judge_of_apply env sigma fj jl)
| Lambda (name,c1,c2) ->
let sigma, j = execute env sigma c1 in
let sigma, var = type_judgment env sigma j in
let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
let sigma, j' = execute env1 sigma c2 in
sigma, judge_of_abstraction env1 name var j'
| Prod (name,c1,c2) ->
let sigma, j = execute env sigma c1 in
let sigma, varj = type_judgment env sigma j in
let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
let sigma, j' = execute env1 sigma c2 in
let sigma, varj' = type_judgment env1 sigma j' in
sigma, judge_of_product env name varj varj'
| LetIn (name,c1,c2,c3) ->
let sigma, j1 = execute env sigma c1 in
let sigma, j2 = execute env sigma c2 in
let sigma, j2 = type_judgment env sigma j2 in
let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in
let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
let sigma, j3 = execute env1 sigma c3 in
sigma, judge_of_letin env name j1 j2 j3
| Cast (c,k,t) ->
let sigma, cj = execute env sigma c in
let sigma, tj = execute env sigma t in
let sigma, tj = type_judgment env sigma tj in
judge_of_cast env sigma cj k tj
and execute_recdef env sigma (names,lar,vdef) =
let sigma, larj = execute_array env sigma lar in
let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in
let env1 = push_rec_types (names,lara,vdef) env in
let sigma, vdefj = execute_array env1 sigma vdef in
let vdefv = Array.map j_val vdefj in
let sigma = check_type_fixpoint env1 sigma names lara vdefj in
sigma, (names,lara,vdefv)
and execute_array env = Array.fold_left_map (execute env)
let check env sigma c t =
let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
match Evarconv.cumul env sigma j.uj_type t with
| None ->
error_actual_type_core env sigma j t
| Some sigma -> sigma
let e_check env evdref c t =
evdref := check env !evdref c t
(* Type of a constr *)
let unsafe_type_of env sigma c =
let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
j.uj_type
(* Sort of a type *)
let sort_of env sigma c =
let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
let sigma, a = type_judgment env sigma j in
sigma, a.utj_type
let e_sort_of env evdref c =
Evarutil.evd_comb1 (sort_of env) evdref c
(* Try to solve the existential variables by typing *)
let type_of ?(refresh=false) env sigma c =
let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
if refresh then
Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type
else sigma, j.uj_type
let e_type_of ?refresh env evdref c =
Evarutil.evd_comb1 (type_of ?refresh env) evdref c
let solve_evars env sigma c =
let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
sigma, nf_evar sigma j.uj_val
let e_solve_evars env evdref c =
Evarutil.evd_comb1 (solve_evars env) evdref c
let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c)
|