1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
21
let inductive_of_constructor = fst
23
let conv_leq_vecti env v1 v2 =
26
(try conv_leq env t1 t2
27
with NotConvertible -> raise (NotConvertibleVect i)); ())
32
(* This should be a type (a priori without intension to be an assumption) *)
33
let type_judgment env (c,ty as j) =
34
match whd_betadeltaiota env ty with
36
| _ -> error_not_type env j
38
(* This should be a type intended to be assumed. The error message is *)
39
(* not as useful as for [type_judgment]. *)
40
let assumption_of_judgment env j =
41
try fst(type_judgment env j)
43
error_assumption env j
45
(************************************************)
46
(* Incremental typing rules: builds a typing judgement given the *)
47
(* judgements for the subterms. *)
53
let judge_of_prop = Sort (Type type1_univ)
55
(* Type of Type(i). *)
57
let judge_of_type u = Sort (Type (super u))
59
(*s Type of a de Bruijn index. *)
61
let judge_of_relative env n =
63
let (_,_,typ) = lookup_rel n env in
66
error_unbound_rel env n
68
(* Type of variables *)
69
let judge_of_variable env id =
72
error_unbound_var env id
74
(* Management of context of variables. *)
76
(* Checks if a context of variable can be instantiated by the
77
variables of the current env *)
78
(* TODO: check order? *)
79
let rec check_hyps_inclusion env sign =
82
let ty2 = named_type id env in
83
if not (eq_constr ty2 ty1) then
84
error "types do not match")
89
let check_args env c hyps =
90
try check_hyps_inclusion env hyps
91
with UserError _ | Not_found ->
92
error_reference_variables env c
95
(* Checks if the given context of variables [hyps] is included in the
96
current context of [env]. *)
98
let check_hyps id env hyps =
99
let hyps' = named_context env in
100
if not (hyps_inclusion env hyps hyps') then
101
error_reference_variables env id
103
(* Instantiation of terms on real arguments. *)
105
(* Make a type polymorphic if an arity *)
107
let extract_level env p =
108
let _,c = dest_prod_assum env p in
109
match c with Sort (Type u) -> Some u | _ -> None
111
let extract_context_levels env =
113
(fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
115
let make_polymorphic_if_arity env t =
116
let params, ccl = dest_prod_assum env t in
119
let param_ccls = extract_context_levels env params in
120
let s = { poly_param_levels = param_ccls; poly_level = u} in
121
PolymorphicArity (params,s)
125
(* Type of constants *)
127
let type_of_constant_knowing_parameters env t paramtyps =
129
| NonPolymorphicType t -> t
130
| PolymorphicArity (sign,ar) ->
131
let ctx = List.rev sign in
132
let ctx,s = instantiate_universes env ctx ar paramtyps in
133
mkArity (List.rev ctx,s)
135
let type_of_constant_type env t =
136
type_of_constant_knowing_parameters env t [||]
138
let type_of_constant env cst =
139
type_of_constant_type env (constant_type env cst)
141
let judge_of_constant_knowing_parameters env cst paramstyp =
144
try lookup_constant cst env
146
failwith ("Cannot find constant: "^string_of_con cst) in
147
let _ = check_args env c cb.const_hyps in
148
type_of_constant_knowing_parameters env cb.const_type paramstyp
150
let judge_of_constant env cst =
151
judge_of_constant_knowing_parameters env cst [||]
153
(* Type of an application. *)
155
let judge_of_apply env (f,funj) argjv =
156
let rec apply_rec n typ = function
159
(match whd_betadeltaiota env typ with
161
(try conv_leq env hj c1
162
with NotConvertible ->
163
error_cant_apply_bad_type env (n,c1, hj) (f,funj) argjv);
164
apply_rec (n+1) (subst1 h c2) restjl
166
error_cant_apply_not_functional env (f,funj) argjv)
168
apply_rec 1 funj (Array.to_list argjv)
170
(* Type of product *)
172
let sort_of_product env domsort rangsort =
173
match (domsort, rangsort) with
174
(* Product rule (s,Prop,Prop) *)
175
| (_, Prop Null) -> rangsort
176
(* Product rule (Prop/Set,Set,Set) *)
177
| (Prop _, Prop Pos) -> rangsort
178
(* Product rule (Type,Set,?) *)
179
| (Type u1, Prop Pos) ->
180
if engagement env = Some ImpredicativeSet then
181
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
184
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
185
Type (sup u1 type0_univ)
186
(* Product rule (Prop,Type_i,Type_i) *)
187
| (Prop Pos, Type u2) -> Type (sup type0_univ u2)
188
(* Product rule (Prop,Type_i,Type_i) *)
189
| (Prop Null, Type _) -> rangsort
190
(* Product rule (Type_i,Type_i,Type_i) *)
191
| (Type u1, Type u2) -> Type (sup u1 u2)
193
(* Type of a type cast *)
195
(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule
197
env |- c:typ1 env |- typ2:s env |- typ1 <= typ2
198
---------------------------------------------------------------------
202
let judge_of_cast env (c,cj) k tj =
205
| VMcast -> vm_conv CUMUL
206
| DEFAULTcast -> conv_leq in
209
with NotConvertible ->
210
error_actual_type env (c,cj) tj
212
(* Inductive types. *)
214
(* The type is parametric over the uniform parameters whose conclusion
215
is in Type; to enforce the internal constraints between the
216
parameters and the instances of Type occurring in the type of the
217
constructors, we use the level variables _statically_ assigned to
218
the conclusions of the parameters as mediators: e.g. if a parameter
219
has conclusion Type(alpha), static constraints of the form alpha<=v
220
exist between alpha and the Type's occurring in the constructor
221
types; when the parameters is finally instantiated by a term of
222
conclusion Type(u), then the constraints u<=alpha is computed in
223
the App case of execute; from this constraints, the expected
224
dynamic constraints of the form u<=v are enforced *)
226
let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
229
try lookup_mind_specif env ind
231
failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in
232
check_args env c mib.mind_hyps;
233
type_of_inductive_knowing_parameters env mip paramstyp
235
let judge_of_inductive env ind =
236
judge_of_inductive_knowing_parameters env ind [||]
240
let judge_of_constructor env c =
241
let constr = Construct c in
243
let ((kn,_),_) = c in
245
try lookup_mind kn env
247
failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in
248
check_args env constr mib.mind_hyps in
249
let specif = lookup_mind_specif env (inductive_of_constructor c) in
250
type_of_constructor c specif
254
let check_branch_types env (c,cj) (lfj,explft) =
255
try conv_leq_vecti env lfj explft
257
NotConvertibleVect i ->
258
error_ill_formed_branch env c i lfj.(i) explft.(i)
259
| Invalid_argument _ ->
260
error_number_branches env (c,cj) (Array.length explft)
262
let judge_of_case env ci pj (c,cj) lfj =
264
try find_rectype env cj
265
with Not_found -> error_case_not_inductive env (c,cj) in
266
let _ = check_case_info env (fst indspec) ci in
267
let (bty,rslty) = type_case_branches env indspec pj c in
268
check_branch_types env (c,cj) (lfj,bty);
273
(* Checks the type of a general (co)fixpoint, i.e. without checking *)
274
(* the specific guard condition. *)
276
let type_fixpoint env lna lar lbody vdefj =
277
let lt = Array.length vdefj in
278
assert (Array.length lar = lt && Array.length lbody = lt);
280
conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar)
281
with NotConvertibleVect i ->
282
let vdefj = array_map2 (fun b ty -> b,ty) lbody vdefj in
283
error_ill_typed_rec_body env i lna vdefj lar
285
(************************************************************************)
286
(************************************************************************)
289
let refresh_arity env ar =
290
let ctxt, hd = decompose_prod_assum ar in
292
Sort (Type u) when not (is_univ_variable u) ->
293
let u' = fresh_local_univ() in
294
let env' = add_constraints (enforce_geq u' u Constraint.empty) env in
295
env', mkArity (ctxt,Type u')
299
(* The typing machine. *)
300
let rec execute env cstr =
303
| Sort (Prop _) -> judge_of_prop
305
| Sort (Type u) -> judge_of_type u
307
| Rel n -> judge_of_relative env n
309
| Var id -> judge_of_variable env id
311
| Const c -> judge_of_constant env c
313
(* Lambda calculus operators *)
314
| App (App (f,args),args') ->
315
execute env (App(f,Array.append args args'))
318
let jl = execute_array env args in
322
(* Sort-polymorphism of inductive types *)
323
judge_of_inductive_knowing_parameters env ind jl
325
(* Sort-polymorphism of constant *)
326
judge_of_constant_knowing_parameters env cst jl
328
(* No sort-polymorphism *)
331
let jl = array_map2 (fun c ty -> c,ty) args jl in
332
judge_of_apply env (f,j) jl
334
| Lambda (name,c1,c2) ->
335
let _ = execute_type env c1 in
336
let env1 = push_rel (name,None,c1) env in
337
let j' = execute env1 c2 in
340
| Prod (name,c1,c2) ->
341
let varj = execute_type env c1 in
342
let env1 = push_rel (name,None,c1) env in
343
let varj' = execute_type env1 c2 in
344
Sort (sort_of_product env varj varj')
346
| LetIn (name,c1,c2,c3) ->
347
let j1 = execute env c1 in
348
(* /!\ c2 can be an inferred type => refresh
349
(but the pushed type is still c2) *)
351
let env',c2' = refresh_arity env c2 in
352
let _ = execute_type env' c2' in
353
judge_of_cast env' (c1,j1) DEFAULTcast c2' in
354
let env1 = push_rel (name,Some c1,c2) env in
355
let j' = execute env1 c3 in
359
let cj = execute env c in
360
let _ = execute_type env t in
361
judge_of_cast env (c,cj) k t;
364
(* Inductive types *)
365
| Ind ind -> judge_of_inductive env ind
367
| Construct c -> judge_of_constructor env c
369
| Case (ci,p,c,lf) ->
370
let cj = execute env c in
371
let pj = execute env p in
372
let lfj = execute_array env lf in
373
judge_of_case env ci (p,pj) (c,cj) lfj
375
| Fix ((_,i as vni),recdef) ->
376
let fix_ty = execute_recdef env recdef i in
377
let fix = (vni,recdef) in
381
| CoFix (i,recdef) ->
382
let fix_ty = execute_recdef env recdef i in
383
let cofix = (i,recdef) in
384
check_cofix env cofix;
387
(* Partial proofs: unsupported by the kernel *)
389
anomaly "the kernel does not support metavariables"
392
anomaly "the kernel does not support existential variables"
394
and execute_type env constr =
395
let j = execute env constr in
396
snd (type_judgment env (constr,j))
398
and execute_recdef env (names,lar,vdef) i =
399
let larj = execute_array env lar in
400
let larj = array_map2 (fun c ty -> c,ty) lar larj in
401
let lara = Array.map (assumption_of_judgment env) larj in
402
let env1 = push_rec_types (names,lara,vdef) env in
403
let vdefj = execute_array env1 vdef in
404
type_fixpoint env1 names lara vdef vdefj;
407
and execute_array env = Array.map (execute env)
409
and execute_list env = List.map (execute env)
411
(* Derived functions *)
412
let infer env constr = execute env constr
413
let infer_type env constr = execute_type env constr
414
let infer_v env cv = execute_array env cv
416
(* Typing of several terms. *)
418
let check_ctxt env rels =
419
fold_rel_context (fun d env ->
422
let _ = infer_type env ty in
425
let j1 = infer env bd in
426
let _ = infer env ty in
431
let check_named_ctxt env ctxt =
432
fold_named_context (fun (id,_,_ as d) env ->
435
let _ = lookup_named id env in
436
failwith ("variable "^string_of_id id^" defined twice")
437
with Not_found -> () in
440
let _ = infer_type env ty in
443
let j1 = infer env bd in
444
let _ = infer env ty in
449
(* Polymorphic arities utils *)
451
let check_kind env ar u =
452
if snd (dest_prod env ar) = Sort(Type u) then ()
453
else failwith "not the correct sort"
455
let check_polymorphic_arity env params par =
456
let pl = par.poly_param_levels in
457
let rec check_p env pl params =
458
match pl, params with
459
Some u::pl, (na,None,ty)::params ->
461
check_p (push_rel (na,None,ty) env) pl params
462
| None::pl,d::params -> check_p (push_rel d env) pl params
464
| _ -> failwith "check_poly: not the right number of params" in
465
check_p env pl (List.rev params)
added
removed
checker/typeops.ml
