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
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
open Names
open Univ
open Term
open Reduction
open Sign
open Declarations
open Inductive
open Environ
open Type_errors
open Typeops
open Indtypes
type judgment = unsafe_judgment
let j_val j = j.uj_val
let j_type j = body_of_type j.uj_type
let vect_lift = Array.mapi lift
let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
(* The typing machine without information. *)
(* ATTENTION : faudra faire le typage du contexte des Const,
MutInd et MutConstructsi un jour cela devient des constructions
arbitraires et non plus des variables *)
let univ_combinator (cst,univ) (j,c') =
(j,(Constraint.union cst c', merge_constraints c' univ))
let rec execute env cstr cu =
match kind_of_term cstr with
| IsMeta _ ->
anomaly "the kernel does not understand metas"
| IsEvar _ ->
anomaly "the kernel does not understand existential variables"
| IsSort (Prop c) ->
(judge_of_prop_contents c, cu)
| IsSort (Type u) ->
univ_combinator cu (judge_of_type u)
| IsApp (f,args) ->
let (j,cu1) = execute env f cu in
let (jl,cu2) = execute_array env args cu1 in
univ_combinator cu2
(apply_rel_list env Evd.empty false (Array.to_list jl) j)
| IsLambda (name,c1,c2) ->
let (j,cu1) = execute env c1 cu in
let var = assumption_of_judgment env Evd.empty j in
let env1 = push_rel_assum (name,var) env in
let (j',cu2) = execute env1 c2 cu1 in
univ_combinator cu2 (abs_rel env1 Evd.empty name var j')
| IsProd (name,c1,c2) ->
let (j,cu1) = execute env c1 cu in
let varj = type_judgment env Evd.empty j in
let env1 = push_rel_assum (name,varj.utj_val) env in
let (j',cu2) = execute env1 c2 cu1 in
let varj' = type_judgment env Evd.empty j' in
univ_combinator cu2
(gen_rel env1 Evd.empty name varj varj')
| IsLetIn (name,c1,c2,c3) ->
let (j,cu1) = execute env (mkCast(c1,c2)) cu in
let env1 = push_rel_def (name,j.uj_val,j.uj_type) env in
let (j',cu2) = execute env1 c3 cu1 in
univ_combinator cu2
(judge_of_letin env1 Evd.empty name j j')
| IsCast (c,t) ->
let (cj,cu1) = execute env c cu in
let (tj,cu2) = execute env t cu1 in
let tj = assumption_of_judgment env Evd.empty tj in
univ_combinator cu2
(cast_rel env Evd.empty cj tj)
| IsRel n ->
(relative env n, cu)
| IsVar id ->
(make_judge cstr (lookup_named_type id env), cu)
| IsConst c ->
(make_judge cstr (type_of_constant env Evd.empty c), cu)
(* Inductive types *)
| IsMutInd ind ->
(make_judge cstr (type_of_inductive env Evd.empty ind), cu)
| IsMutConstruct c ->
(make_judge cstr (type_of_constructor env Evd.empty c), cu)
| IsMutCase (ci,p,c,lf) ->
let (cj,cu1) = execute env c cu in
let (pj,cu2) = execute env p cu1 in
let (lfj,cu3) = execute_array env lf cu2 in
univ_combinator cu3
(judge_of_case env Evd.empty ci pj cj lfj)
| IsFix ((vn,i as vni),recdef) ->
if array_exists (fun n -> n < 0) vn then
error "General Fixpoints not allowed";
let ((_,tys,_ as recdef'),cu1) = execute_fix env recdef cu in
let fix = (vni,recdef') in
check_fix env Evd.empty fix;
(make_judge (mkFix fix) tys.(i), cu1)
| IsCoFix (i,recdef) ->
let ((_,tys,_ as recdef'),cu1) = execute_fix env recdef cu in
let cofix = (i,recdef') in
check_cofix env Evd.empty cofix;
(make_judge (mkCoFix cofix) tys.(i), cu1)
and execute_fix env (names,lar,vdef) cu =
let (larj,cu1) = execute_array env lar cu in
let lara = Array.map (assumption_of_judgment env Evd.empty) larj in
let env1 = push_rec_types (names,lara,vdef) env in
let (vdefj,cu2) = execute_array env1 vdef cu1 in
let vdefv = Array.map j_val vdefj in
let cst = type_fixpoint env1 Evd.empty names lara vdefj in
univ_combinator cu2 ((names,lara,vdefv),cst)
and execute_array env v cu =
let (jl,cu1) = execute_list env (Array.to_list v) cu in
(Array.of_list jl, cu1)
and execute_list env l cu =
match l with
| [] ->
([], cu)
| c::r ->
let (j,cu1) = execute env c cu in
let (jr,cu2) = execute_list env r cu1 in
(j::jr, cu2)
(* The typed type of a judgment. *)
let execute_type env constr cu =
let (j,cu1) = execute env constr cu in
(type_judgment env Evd.empty j, cu1)
(* Exported machines. *)
let safe_infer env constr =
let (j,(cst,_)) =
execute env constr (Constraint.empty, universes env) in
(j, cst)
let safe_infer_type env constr =
let (j,(cst,_)) =
execute_type env constr (Constraint.empty, universes env) in
(j, cst)
(* Typing of several terms. *)
let safe_infer_l env cl =
let type_one (cst,l) c =
let (j,cst') = safe_infer env c in
(Constraint.union cst cst', j::l)
in
List.fold_left type_one (Constraint.empty,[]) cl
let safe_infer_v env cv =
let type_one (cst,l) c =
let (j,cst') = safe_infer env c in
(Constraint.union cst cst', j::l)
in
let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in
(cst', Array.of_list l)
(*s Safe environments. *)
type safe_environment = env
let empty_environment = empty_env
let universes = universes
let context = context
let named_context = named_context
let lookup_named_type = lookup_named_type
let lookup_rel_type = lookup_rel_type
let lookup_named = lookup_named
let lookup_constant = lookup_constant
let lookup_mind = lookup_mind
let lookup_mind_specif = lookup_mind_specif
(* Insertion of variables (named and de Bruijn'ed). They are now typed before
being added to the environment. *)
let push_rel_or_named_def push (id,b) env =
let (j,cst) = safe_infer env b in
let env' = add_constraints cst env in
push (id,j.uj_val,j.uj_type) env'
let push_named_def = push_rel_or_named_def push_named_def
let push_rel_def = push_rel_or_named_def push_rel_def
let push_rel_or_named_assum push (id,t) env =
let (j,cst) = safe_infer env t in
let env' = add_constraints cst env in
let t = assumption_of_judgment env Evd.empty j in
push (id,t) env'
let push_named_assum = push_rel_or_named_assum push_named_assum
let push_rel_assum = push_rel_or_named_assum push_rel_assum
let check_and_push_named_def (id,b) env =
let (j,cst) = safe_infer env b in
let env' = add_constraints cst env in
let env'' = Environ.push_named_def (id,j.uj_val,j.uj_type) env' in
(Some j.uj_val,j.uj_type,cst),env''
let check_and_push_named_assum (id,t) env =
let (j,cst) = safe_infer env t in
let env' = add_constraints cst env in
let t = assumption_of_judgment env Evd.empty j in
let env'' = Environ.push_named_assum (id,t) env' in
(None,t,cst),env''
let push_rels_with_univ vars env =
List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
let safe_infer_local_decl env id = function
| LocalDef c ->
let (j,cst) = safe_infer env c in
(Name id, Some j.uj_val, j.uj_type), cst
| LocalAssum c ->
let (j,cst) = safe_infer env c in
(Name id, None, assumption_of_judgment env Evd.empty j), cst
let safe_infer_local_decls env decls =
let rec inferec env = function
| (id, d) :: l ->
let env, l, cst1 = inferec env l in
let d, cst2 = safe_infer_local_decl env id d in
push_rel d env, d :: l, Constraint.union cst1 cst2
| [] -> env, [], Constraint.empty in
inferec env decls
(* Insertion of constants and parameters in environment. *)
type global_declaration = Def of constr | Assum of constr
let safe_infer_declaration env = function
| Def c ->
let (j,cst) = safe_infer env c in
Some j.uj_val, j.uj_type, cst
| Assum t ->
let (j,cst) = safe_infer env t in
None, assumption_of_judgment env Evd.empty j, cst
type local_names = (identifier * variable) list
let add_global_declaration sp env locals (body,typ,cst) op =
let env' = add_constraints cst env in
let ids = match body with
| None -> global_vars_set env typ
| Some b ->
Idset.union (global_vars_set env b) (global_vars_set env typ) in
let hyps = keep_hyps env ids (named_context env) in
let sp_hyps = List.map (fun (id,b,t) -> (List.assoc id locals, b, t)) hyps in
let cb = {
const_kind = kind_of_path sp;
const_body = body;
const_type = typ;
const_hyps = sp_hyps;
const_constraints = cst;
const_opaque = op }
in
Environ.add_constant sp cb env'
let add_parameter sp t locals env =
add_global_declaration
sp env locals (safe_infer_declaration env (Assum t)) false
let add_constant sp ce locals env =
let { const_entry_body = body;
const_entry_type = typ;
const_entry_opaque = op } = ce in
let body' =
match typ with
| None -> body
| Some ty -> mkCast (body, ty) in
add_global_declaration
sp env locals (safe_infer_declaration env (Def body')) op
let add_discharged_constant sp r locals env =
let (body,typ,cst,op) = Cooking.cook_constant env r in
let env' = add_constraints cst env in
match body with
| None ->
add_parameter sp typ locals (* Bricolage avant poubelle *) env'
| Some c ->
(* let c = hcons1_constr c in *)
let ids =
Idset.union (global_vars_set env c) (global_vars_set env typ) in
let hyps = keep_hyps env ids (named_context env') in
let sp_hyps =
List.map (fun (id,b,t) -> (List.assoc id locals,b,t)) hyps in
let cb =
{ const_kind = kind_of_path sp;
const_body = Some c;
const_type = typ;
const_hyps = sp_hyps;
const_constraints = cst;
const_opaque = op }
in
Environ.add_constant sp cb env'
(* Insertion of inductive types. *)
(* Only the case where at least s1 or s2 is a [Type] is taken into account *)
let max_universe (s1,cst1) (s2,cst2) g =
match s1,s2 with
| Type u1, Type u2 ->
let (u12,cst) = sup u1 u2 g in
Type u12, Constraint.union cst (Constraint.union cst1 cst2)
| Type u1, _ -> s1, cst1
| _, _ -> s2, cst2
(* This (re)computes informations relevant to extraction and the sort of an
arity or type constructor; we do not to recompute universes constraints *)
let rec infos_and_sort env t =
match kind_of_term t with
| IsProd (name,c1,c2) ->
let (varj,_) = safe_infer_type env c1 in
let env1 = Environ.push_rel_assum (name,varj.utj_val) env in
let s1 = varj.utj_type in
let logic = not (is_info_type env Evd.empty varj) in
let small = is_small s1 in
(logic,small) :: (infos_and_sort env1 c2)
| IsCast (c,_) -> infos_and_sort env c
| _ -> []
(* [infos] is a sequence of pair [islogic,issmall] for each type in
the product of a constructor or arity *)
let is_small infos = List.for_all (fun (logic,small) -> small) infos
let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
let is_logic_arity infos =
List.for_all (fun (logic,small) -> logic || small) infos
let is_unit arinfos constrsinfos =
match constrsinfos with (* One info = One constructor *)
| [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
| _ -> false
let small_unit constrsinfos (env_ar_par,short_arity) =
let issmall = List.for_all is_small constrsinfos in
let arinfos = infos_and_sort env_ar_par short_arity in
let isunit = is_unit arinfos constrsinfos in
issmall, isunit
(* [smax] is the max of the sorts of the products of the constructor type *)
let enforce_type_constructor arsort smax cst =
match smax, arsort with
| Type uc, Type ua -> enforce_geq ua uc cst
| _,_ -> cst
let type_one_constructor env_ar_par params arsort c =
let infos = infos_and_sort env_ar_par c in
(* Each constructor is typed-checked here *)
let (j,cst) = safe_infer_type env_ar_par c in
let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in
(* If the arity is at some level Type arsort, then the sort of the
constructor must be below arsort; here we consider constructors with the
global parameters (which add a priori more constraints on their sort) *)
let cst2 = enforce_type_constructor arsort j.utj_type cst in
(infos, full_cstr_type, cst2)
let infer_constructor_packet env_ar params short_arity arsort vc =
let env_ar_par = push_rels params env_ar in
let (constrsinfos,jlc,cst) =
List.fold_right
(fun c (infosl,l,cst) ->
let (infos,ct,cst') =
type_one_constructor env_ar_par params arsort c in
(infos::infosl,ct::l, Constraint.union cst cst'))
vc
([],[],Constraint.empty) in
let vc' = Array.of_list jlc in
let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
(issmall,isunit,vc', cst)
let add_mind sp mie locals env =
mind_check_wellformed env mie;
(* We first type params and arity of each inductive definition *)
(* This allows to build the environment of arities and to share *)
(* the set of constraints *)
let cst, env_arities, rev_params_arity_list =
List.fold_left
(fun (cst,env_arities,l) ind ->
(* Params are typed-checked here *)
let params = ind.mind_entry_params in
let env_params, params, cst1 = safe_infer_local_decls env params in
(* Arities (without params) are typed-checked here *)
let arity, cst2 = safe_infer_type env_params ind.mind_entry_arity in
(* We do not need to generate the universe of full_arity; if
later, after the validation of the inductive definition,
full_arity is used as argument or subject to cast, an
upper universe will be generated *)
let id = ind.mind_entry_typename in
let full_arity = it_mkProd_or_LetIn arity.utj_val params in
Constraint.union cst (Constraint.union cst1 cst2),
push_rel_assum (Name id, full_arity) env_arities,
(params, id, full_arity, arity.utj_val)::l)
(Constraint.empty,env,[])
mie.mind_entry_inds in
let params_arity_list = List.rev rev_params_arity_list in
(* Now, we type the constructors (without params) *)
let inds,cst =
List.fold_right2
(fun ind (params,id,full_arity,short_arity) (inds,cst) ->
let arsort = sort_of_arity env full_arity in
let lc = ind.mind_entry_lc in
let (issmall,isunit,lc',cst') =
infer_constructor_packet env_arities params short_arity arsort lc
in
let nparams = ind.mind_entry_nparams in
let consnames = ind.mind_entry_consnames in
let ind' = (params,nparams,id,full_arity,consnames,issmall,isunit,lc')
in
(ind'::inds, Constraint.union cst cst'))
mie.mind_entry_inds
params_arity_list
([],cst) in
(* Finally, we build the inductive packet and push it to env *)
let kind = kind_of_path sp in
let mib = cci_inductive locals env env_arities kind mie.mind_entry_finite inds cst
in
add_mind sp mib (add_constraints cst env)
let add_constraints = add_constraints
let rec pop_named_decls idl env =
match idl with
| [] -> env
| id::l -> pop_named_decls l (Environ.pop_named_decl id env)
let export = export
let import = import
let env_of_safe_env e = e
(* Exported typing functions *)
let typing env c =
let (j,cst) = safe_infer env c in
j
let typing_in_unsafe_env = typing
|