aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
blob: bffe36eea338945a8fff971cdab38b1da7c4164a (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
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
(************************************************************************)
(*         *   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 env 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 pj = Retyping.get_judgment_of env sigma p in
  let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
  let specif = Global.lookup_inductive (fst ind) in
  let sorts = elim_sorts specif 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_prop_contents = function
  | Null -> judge_of_prop
  | Pos -> judge_of_set

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 c ->
        sigma, judge_of_prop_contents c
      | 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)