aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/typeops.ml
blob: d49c40a8bdc7023eefc89ac1a7c0388b6e50dc04 (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Errors
open Util
open Names
open Cic
open Term
open Reduction
open Type_errors
open Inductive
open Environ

let inductive_of_constructor = fst

let conv_leq_vecti env v1 v2 =
  Array.fold_left2_i
    (fun i _ t1 t2 ->
      (try conv_leq env t1 t2
      with NotConvertible -> raise (NotConvertibleVect i)); ())
    ()
    v1
    v2

let check_constraints cst env = 
  if Environ.check_constraints cst env then ()
  else error_unsatisfied_constraints env cst

(* This should be a type (a priori without intension to be an assumption) *)
let type_judgment env (c,ty as j) =
  match whd_betadeltaiota env ty with
    | Sort s -> (c,s)
    | _ -> error_not_type env j

(* This should be a type intended to be assumed. The error message is *)
(* not as useful as for [type_judgment]. *)
let assumption_of_judgment env j =
  try fst(type_judgment env j)
  with TypeError _ ->
    error_assumption env j

(************************************************)
(* Incremental typing rules: builds a typing judgement given the *)
(* judgements for the subterms. *)

(*s Type of sorts *)

(* Prop and Set *)

let judge_of_prop = Sort (Type Univ.type1_univ)

(* Type of Type(i). *)

let judge_of_type u = Sort (Type (Univ.super u))

(*s Type of a de Bruijn index. *)

let judge_of_relative env n =
  try
    let (_,_,typ) = lookup_rel n env in
    lift n typ
  with Not_found ->
    error_unbound_rel env n

(* Type of constants *)


let type_of_constant_type_knowing_parameters env t paramtyps =
  match t with
  | RegularArity t -> t
  | TemplateArity (sign,ar) ->
      let ctx = List.rev sign in
      let ctx,s = instantiate_universes env ctx ar paramtyps in
      mkArity (List.rev ctx,s)

let type_of_constant_knowing_parameters env cst paramtyps =
  let ty, cu = constant_type env cst in
    type_of_constant_type_knowing_parameters env ty paramtyps, cu

let type_of_constant_type env t =
  type_of_constant_type_knowing_parameters env t [||]

let type_of_constant env cst =
  type_of_constant_knowing_parameters env cst [||]

let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
  let _cb =
    try lookup_constant kn env
    with Not_found ->
      failwith ("Cannot find constant: "^string_of_con kn)
  in
  let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
  let () = check_constraints cu env in
    ty

let judge_of_constant env cst =
  judge_of_constant_knowing_parameters env cst [||]

(* Type of an application. *)

let judge_of_apply env (f,funj) argjv =
  let rec apply_rec n typ = function
    | [] -> typ
    | (h,hj)::restjl ->
        (match whd_betadeltaiota env typ with
          | Prod (_,c1,c2) ->
	      (try conv_leq env hj c1
	      with NotConvertible ->
		error_cant_apply_bad_type env (n,c1, hj) (f,funj) argjv);
	      apply_rec (n+1) (subst1 h c2) restjl
          | _ ->
	      error_cant_apply_not_functional env (f,funj) argjv)
  in
  apply_rec 1 funj (Array.to_list argjv)

(* Type of product *)

let sort_of_product env domsort rangsort =
  match (domsort, rangsort) with
    (* Product rule (s,Prop,Prop) *)
    | (_,       Prop Null)  -> rangsort
    (* Product rule (Prop/Set,Set,Set) *)
    | (Prop _,  Prop Pos) -> rangsort
    (* Product rule (Type,Set,?) *)
    | (Type u1, Prop Pos) ->
        if fst (engagement env) = ImpredicativeSet then
          (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
          rangsort
        else
          (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
          Type (Univ.sup u1 Univ.type0_univ)
    (* Product rule (Prop,Type_i,Type_i) *)
    | (Prop Pos,  Type u2)  -> Type (Univ.sup Univ.type0_univ u2)
    (* Product rule (Prop,Type_i,Type_i) *)
    | (Prop Null, Type _)  -> rangsort
    (* Product rule (Type_i,Type_i,Type_i) *)
    | (Type u1, Type u2) -> Type (Univ.sup u1 u2)

(* Type of a type cast *)

(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule

    env |- c:typ1    env |- typ2:s    env |- typ1 <= typ2
    ---------------------------------------------------------------------
         env |- c:typ2
*)

let judge_of_cast env (c,cj) k tj =
  let conversion =
    match k with
    | VMcast | NATIVEcast -> vm_conv CUMUL
    | DEFAULTcast -> conv_leq in
  try
    conversion env cj tj
  with NotConvertible ->
    error_actual_type env (c,cj) tj

(* Inductive types. *)

(* The type is parametric over the uniform parameters whose conclusion
   is in Type; to enforce the internal constraints between the
   parameters and the instances of Type occurring in the type of the
   constructors, we use the level variables _statically_ assigned to
   the conclusions of the parameters as mediators: e.g. if a parameter
   has conclusion Type(alpha), static constraints of the form alpha<=v
   exist between alpha and the Type's occurring in the constructor
   types; when the parameters is finally instantiated by a term of
   conclusion Type(u), then the constraints u<=alpha is computed in
   the App case of execute; from this constraints, the expected
   dynamic constraints of the form u<=v are enforced *)

let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
  let specif =
    try lookup_mind_specif env ind
    with Not_found ->
      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
  in
  type_of_inductive_knowing_parameters env (specif,u) paramstyp

let judge_of_inductive env ind =
  judge_of_inductive_knowing_parameters env ind [||]

(* Constructors. *)

let judge_of_constructor env (c,u) =
  let ind = inductive_of_constructor c in
  let specif =
    try lookup_mind_specif env ind
    with Not_found ->
      failwith ("Cannot find inductive: "^string_of_mind (fst ind))
  in
  type_of_constructor (c,u) specif

(* Case. *)

let check_branch_types env (c,cj) (lfj,explft) =
  try conv_leq_vecti env lfj explft
  with
      NotConvertibleVect i ->
        error_ill_formed_branch env c i lfj.(i) explft.(i)
    | Invalid_argument _ ->
        error_number_branches env (c,cj) (Array.length explft)

let judge_of_case env ci pj (c,cj) lfj =
  let indspec =
    try find_rectype env cj
    with Not_found -> error_case_not_inductive env (c,cj) in
  let _ = check_case_info env (fst (fst indspec)) ci in
  let (bty,rslty) = type_case_branches env indspec pj c in
  check_branch_types env (c,cj) (lfj,bty);
  rslty

(* Projection. *)

let judge_of_projection env p c ct =
  let pb = lookup_projection p env in
  let (ind,u), args =
    try find_rectype env ct
    with Not_found -> error_case_not_inductive env (c, ct)
  in
    assert(eq_mind pb.proj_ind (fst ind));
    let ty = subst_instance_constr u pb.proj_type in
      substl (c :: List.rev args) ty

(* Fixpoints. *)

(* Checks the type of a general (co)fixpoint, i.e. without checking *)
(* the specific guard condition. *)

let type_fixpoint env lna lar lbody vdefj =
  let lt = Array.length vdefj in
  assert (Array.length lar = lt && Array.length lbody = lt);
  try
    conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar)
  with NotConvertibleVect i ->
    let vdefj = Array.map2 (fun b ty -> b,ty) lbody vdefj in
    error_ill_typed_rec_body env i lna vdefj lar

(************************************************************************)
(************************************************************************)


(* let refresh_arity env ar = *)
(*   let ctxt, hd = decompose_prod_assum ar in *)
(*   match hd with *)
(*       Sort (Type u) when not (is_univ_variable u) -> *)
(*         let u' = fresh_local_univ() in *)
(*         let env' = add_constraints (enforce_leq u u' empty_constraint) env in *)
(*         env', mkArity (ctxt,Type u') *)
(*     | _ -> env, ar *)


(* The typing machine. *)
let rec execute env cstr =
  match cstr with
    (* Atomic terms *)
    | Sort (Prop _) -> judge_of_prop

    | Sort (Type u) -> judge_of_type u

    | Rel n -> judge_of_relative env n

    | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")

    | Const c -> judge_of_constant env c

    (* Lambda calculus operators *)
    | App (App (f,args),args') ->
        execute env (App(f,Array.append args args'))

    | App (f,args) ->
        let jl = execute_array env args in
	let j =
	  match f with
	    | Ind ind ->
		(* Sort-polymorphism of inductive types *)
		judge_of_inductive_knowing_parameters env ind jl
	    | Const cst ->
		(* Sort-polymorphism of constant *)
		judge_of_constant_knowing_parameters env cst jl
	    | _ ->
		(* No sort-polymorphism *)
		execute env f
	in
        let jl = Array.map2 (fun c ty -> c,ty) args jl in
	judge_of_apply env (f,j) jl

    | Proj (p, c) ->
        let ct = execute env c in
          judge_of_projection env p c ct

    | Lambda (name,c1,c2) ->
        let _ = execute_type env c1 in
	let env1 = push_rel (name,None,c1) env in
        let j' = execute env1 c2 in
        Prod(name,c1,j')

    | Prod (name,c1,c2) ->
        let varj = execute_type env c1 in
	let env1 = push_rel (name,None,c1) env in
        let varj' = execute_type env1 c2 in
	Sort (sort_of_product env varj varj')

    | LetIn (name,c1,c2,c3) ->
        let j1 = execute env c1 in
        (* /!\ c2 can be an inferred type => refresh
           (but the pushed type is still c2) *)
        let _ =
          let env',c2' = (* refresh_arity env *) env, c2 in
          let _ = execute_type env' c2' in
          judge_of_cast env' (c1,j1) DEFAULTcast c2' in
        let env1 = push_rel (name,Some c1,c2) env in
        let j' = execute env1 c3 in
        subst1 c1 j'

    | Cast (c,k,t) ->
        let cj = execute env c in
        let _ = execute_type env t in
	judge_of_cast env (c,cj) k t;
        t

    (* Inductive types *)
    | Ind ind -> judge_of_inductive env ind

    | Construct c -> judge_of_constructor env c

    | Case (ci,p,c,lf) ->
        let cj = execute env c in
        let pj = execute env p in
        let lfj = execute_array env lf in
        judge_of_case env ci (p,pj) (c,cj) lfj

    | Fix ((_,i as vni),recdef) ->
        let fix_ty = execute_recdef env recdef i in
        let fix = (vni,recdef) in
        check_fix env fix;
	fix_ty

    | CoFix (i,recdef) ->
        let fix_ty = execute_recdef env recdef i in
        let cofix = (i,recdef) in
        check_cofix env cofix;
	fix_ty

    (* Partial proofs: unsupported by the kernel *)
    | Meta _ ->
	anomaly (Pp.str "the kernel does not support metavariables")

    | Evar _ ->
	anomaly (Pp.str "the kernel does not support existential variables")

and execute_type env constr =
  let j = execute env constr in
  snd (type_judgment env (constr,j))

and execute_recdef env (names,lar,vdef) i =
  let larj = execute_array env lar in
  let larj = Array.map2 (fun c ty -> c,ty) lar larj in
  let lara = Array.map (assumption_of_judgment env) larj in
  let env1 = push_rec_types (names,lara,vdef) env in
  let vdefj = execute_array env1 vdef in
  type_fixpoint env1 names lara vdef vdefj;
  lara.(i)

and execute_array env = Array.map (execute env)

(* Derived functions *)
let infer env constr = execute env constr
let infer_type env constr = execute_type env constr

(* Typing of several terms. *)

let check_ctxt env rels =
  fold_rel_context (fun d env ->
    match d with
        (_,None,ty) ->
          let _ = infer_type env ty in
          push_rel d env
      | (_,Some bd,ty) ->
          let j1 = infer env bd in
          let _ = infer env ty in
          conv_leq env j1 ty;
          push_rel d env)
    rels ~init:env

(* Polymorphic arities utils *)

let check_kind env ar u =
  match (snd (dest_prod env ar)) with
  | Sort (Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> ()
  | _ -> failwith "not the correct sort"

let check_polymorphic_arity env params par =
  let pl = par.template_param_levels in
  let rec check_p env pl params =
    match pl, params with
        Some u::pl, (na,None,ty)::params ->
          check_kind env ty u;
          check_p (push_rel (na,None,ty) env) pl params
      | None::pl,d::params -> check_p (push_rel d env) pl params
      | [], _ -> ()
      | _ -> failwith "check_poly: not the right number of params" in
  check_p env pl (List.rev params)