aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
blob: 3839135a86dba56d074c11e24415ea50b1dd1f5e (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
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
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
(************************************************************************)
(*  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        *)
(************************************************************************)

(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
   the Coq module system *)

(* This module provides the main entry points for type-checking basic
   declarations *)

open Errors
open Util
open Names
open Term
open Declarations
open Environ
open Entries
open Typeops
open Fast_typeops

let constrain_type env j poly subst = function
  | `None -> 
    if not poly then (* Old-style polymorphism *)
      make_polymorphic_if_constant_for_ind env j
    else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
  | `Some t ->
      let tj = infer_type env t in
      let _ = judge_of_cast env j DEFAULTcast tj in
	assert (eq_constr t tj.utj_val);
	RegularArity (Vars.subst_univs_level_constr subst t)
  | `SomeWJ (t, tj) ->
      let tj = infer_type env t in
      let _ = judge_of_cast env j DEFAULTcast tj in
	assert (eq_constr t tj.utj_val);
	RegularArity (Vars.subst_univs_level_constr subst t)

let map_option_typ = function None -> `None | Some x -> `Some x

(* Insertion of constants and parameters in environment. *)

let mk_pure_proof c = (c, Univ.ContextSet.empty), []

let equal_eff e1 e2 =
  let open Entries in
  match e1, e2 with
  | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
        Names.Constant.equal c1 c2
  | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
        CList.for_all2eq
          (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
          cl1 cl2
  | _ -> false

let rec uniq_seff = function
  | [] -> []
  | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
(* The list of side effects is in reverse order (most recent first).
 * To keep the "topological" order between effects we have to uniq-ize from
 * the tail *)
let uniq_seff l = List.rev (uniq_seff (List.rev l))

let inline_side_effects env body ctx side_eff =
  let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
    let cbl = match se with
      | SEsubproof (c,cb,b) -> [c,cb,b]
      | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
    let not_exists (c,_,_) =
      try ignore(Environ.lookup_constant c env); false
      with Not_found -> true in 
    let cbl = List.filter not_exists cbl in
    let cname c = 
      let name = string_of_con c in
      for i = 0 to String.length name - 1 do
        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
      Name (id_of_string name) in
    let rec sub c i x = match kind_of_term x with
      | Const (c', _) when eq_constant c c' -> mkRel i
      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
    let rec sub_body c u b i x = match kind_of_term x with
      | Const (c',u') when eq_constant c c' -> 
	Vars.subst_instance_constr u' b
      | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
    let fix_body (c,cb,b) (t,ctx) =
      match cb.const_body, b with
      | Def b, _ ->
          let b = Mod_subst.force_constr b in
	  let poly = cb.const_polymorphic in
	    if not poly then
              let b_ty = Typeops.type_of_constant_type env cb.const_type in
              let t = sub c 1 (Vars.lift 1 t) in
	        mkLetIn (cname c, b, b_ty, t),
		Univ.ContextSet.union ctx
		  (Univ.ContextSet.of_context cb.const_universes)
	    else 
	      let univs = cb.const_universes in
		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
      | OpaqueDef _, `Opaque (b,_) -> 
	  let poly = cb.const_polymorphic in
	    if not poly then
              let b_ty = Typeops.type_of_constant_type env cb.const_type in
              let t = sub c 1 (Vars.lift 1 t) in
	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
		Univ.ContextSet.union ctx
		  (Univ.ContextSet.of_context cb.const_universes)
	    else
	      let univs = cb.const_universes in
		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
      | _ -> assert false
    in
    let t, ctx = List.fold_right fix_body cbl (t,ctx) in
    t, ctx, (mb,List.length cbl) :: sl
  in
  (* CAVEAT: we assure a proper order *)
  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)

(* Given the list of signatures of side effects, checks if they match.
 * I.e. if they are ordered descendants of the current revstruct *)
let check_signatures curmb sl =
  let is_direct_ancestor (sl, curmb) (mb, how_many) =
    match curmb with
    | None -> None, None
    | Some curmb ->
        try
          let mb = CEphemeron.get mb in
          match sl with
          | None -> sl, None
          | Some n ->
              if List.length mb >= how_many && CList.skipn how_many mb == curmb
              then Some (n + how_many), Some mb
              else None, None
        with CEphemeron.InvalidKey -> None, None in
  let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
  sl

let skip_trusted_seff sl b e =
  let rec aux sl b e acc =
    let open Context.Rel.Declaration in
    match sl, kind_of_term b with
    | (None|Some 0), _ -> b, e, acc
    | Some sl, LetIn (n,c,ty,bo) ->
       aux (Some (sl-1)) bo
         (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc)
    | Some sl, App(hd,arg) ->
       begin match kind_of_term hd with
       | Lambda (n,ty,bo) ->
           aux (Some (sl-1)) bo
             (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc)
       | _ -> assert false
       end
    | _ -> assert false
    in
  aux sl b e []

let rec unzip ctx j =
  match ctx with
  | [] -> j
  | `Let (n,c,ty) :: ctx ->
      unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) }
  | `Cut (n,ty,arg) :: ctx ->
      unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }

let hcons_j j =
  { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 

let feedback_completion_typecheck =
  Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
	      
let infer_declaration ~trust env kn dcl =
  match dcl with
  | ParameterEntry (ctx,poly,(t,uctx),nl) ->
      let env = push_context ~strict:(not poly) uctx env in
      let j = infer env t in
      let abstract = poly && not (Option.is_empty kn) in
      let usubst, univs = Univ.abstract_universes abstract uctx in
      let c = Typeops.assumption_of_judgment env j in
      let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
	Undef nl, RegularArity t, None, poly, univs, false, ctx

  | DefinitionEntry ({ const_entry_type = Some typ;
                       const_entry_opaque = true;
		       const_entry_polymorphic = false} as c) ->
      let env = push_context ~strict:true c.const_entry_universes env in
      let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
      let tyj = infer_type env typ in
      let proofterm =
        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
          let body, uctx, signatures =
            inline_side_effects env body uctx side_eff in
          let valid_signatures = check_signatures trust signatures in
	  let env' = push_context_set uctx env in
          let j =
            let body,env',ectx = skip_trusted_seff valid_signatures body env' in
            let j = infer env' body in
            unzip ectx j in
          let j = hcons_j j in
	  let subst = Univ.LMap.empty in
          let _typ = constrain_type env' j c.const_entry_polymorphic subst
	    (`SomeWJ (typ,tyj)) in
          feedback_completion_typecheck feedback_id;
          j.uj_val, uctx) in
      let def = OpaqueDef (Opaqueproof.create proofterm) in
      def, RegularArity typ, None, c.const_entry_polymorphic, 
	c.const_entry_universes,
	c.const_entry_inline_code, c.const_entry_secctx

  | DefinitionEntry c ->
      let { const_entry_type = typ; const_entry_opaque = opaque } = c in
      let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
      let (body, ctx), side_eff = Future.join body in
      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
      let body, ctx, _ = inline_side_effects env body
        (Univ.ContextSet.union univsctx ctx) side_eff in
      let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
      let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
      let usubst, univs =
	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
      let j = infer env body in
      let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
      let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
      let def = 
	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
	else Def (Mod_subst.from_val def) 
      in
	feedback_completion_typecheck feedback_id;
	def, typ, None, c.const_entry_polymorphic,
        univs, c.const_entry_inline_code, c.const_entry_secctx

  | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
    let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
    let kn, pb = 
      match mib.mind_record with
      | Some (Some (id, kns, pbs)) -> 
	if i < Array.length pbs then
	  kns.(i), pbs.(i)
	else assert false
      | _ -> assert false
    in
    let term, typ = pb.proj_eta in
      Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
      mib.mind_polymorphic, mib.mind_universes, false, None

let global_vars_set_constant_type env = function
  | RegularArity t -> global_vars_set env t
  | TemplateArity (ctx,_) ->
      Context.Rel.fold_outside
        (Context.Rel.Declaration.fold
	  (fun t c -> Id.Set.union (global_vars_set env t) c))
      ctx ~init:Id.Set.empty

let record_aux env s_ty s_bo suggested_expr =
  let open Context.Named.Declaration in
  let in_ty = keep_hyps env s_ty in
  let v =
    String.concat " "
      (CList.map_filter (fun decl ->
          let id = get_id decl in
          if List.exists (Id.equal id % get_id) in_ty then None
          else Some (Id.to_string id))
        (keep_hyps env s_bo)) in
  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)

let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f

let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
  let open Context.Named.Declaration in
  let check declared inferred =
    let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
    let inferred_set, declared_set = mk_set inferred, mk_set declared in
    if not (Id.Set.subset inferred_set declared_set) then
      let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
      let n = List.length l in
      errorlabstrm "" (Pp.(str "The following section " ++
        str (String.plural n "variable") ++
        str " " ++ str (String.conjugate_verb_to_be n) ++
        str " used but not declared:" ++
        fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
  let sort evn l =
    List.filter (fun decl ->
      let id = get_id decl in
      List.exists (Names.Id.equal id % get_id) l)
    (named_context env) in
  (* We try to postpone the computation of used section variables *)
  let hyps, def =
    let context_ids = List.map get_id (named_context env) in
    match ctx with
    | None when not (List.is_empty context_ids) -> 
        (* No declared section vars, and non-empty section context:
           we must look at the body NOW, if any *)
        let ids_typ = global_vars_set_constant_type env typ in
        let ids_def = match def with
        | Undef _ -> Idset.empty
        | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
        | OpaqueDef lc ->
            let vars =
              global_vars_set env
                (Opaqueproof.force_proof (opaque_tables env) lc) in
            (* we force so that cst are added to the env immediately after *)
            ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
            let expr =
              !suggest_proof_using (Constant.to_string kn)
                env vars ids_typ context_ids in
            if !Flags.compilation_mode = Flags.BuildVo then
              record_aux env ids_typ vars expr;
            vars
        in
        keep_hyps env (Idset.union ids_typ ids_def), def
    | None ->
        if !Flags.compilation_mode = Flags.BuildVo then
          record_aux env Id.Set.empty Id.Set.empty "";
        [], def (* Empty section context: no need to check *)
    | Some declared ->
        (* We use the declared set and chain a check of correctness *)
        sort env declared,
        match def with
        | Undef _ as x -> x (* nothing to check *)
        | Def cs as x ->
            let ids_typ = global_vars_set_constant_type env typ in
            let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
            let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
            check declared inferred;
            x
        | OpaqueDef lc -> (* In this case we can postpone the check *)
            OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
              let ids_typ = global_vars_set_constant_type env typ in
              let ids_def = global_vars_set env c in
              let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
              check declared inferred) lc) in
  let tps = 
    let res =
      let comp_univs = if poly then Some univs else None in
      match proj with
      | None -> compile_constant_body env comp_univs def
      | Some pb ->
	(* The compilation of primitive projections is a bit tricky, because
           they refer to themselves (the body of p looks like fun c =>
           Proj(p,c)). We break the cycle by building an ad-hoc compilation
           environment. A cleaner solution would be that kernel projections are
           simply Proj(i,c) with i an int and c a constr, but we would have to
           get rid of the compatibility layer. *)
	let cb =
	  { const_hyps = hyps;
	    const_body = def;
	    const_type = typ;
	    const_proj = proj;
	    const_body_code = None;
	    const_polymorphic = poly;
	    const_universes = univs;
	    const_inline_code = inline_code }
	in
	let env = add_constant kn cb env in
	compile_constant_body env comp_univs def
    in Option.map Cemitcodes.from_val res
  in
  { const_hyps = hyps;
    const_body = def;
    const_type = typ;
    const_proj = proj;
    const_body_code = tps;
    const_polymorphic = poly;
    const_universes = univs;
    const_inline_code = inline_code }

(*s Global and local constant declaration. *)

let translate_constant mb env kn ce =
  build_constant_declaration kn env
    (infer_declaration ~trust:mb env (Some kn) ce)

let constant_entry_of_side_effect cb u =
  let pt =
    match cb.const_body, u with
    | OpaqueDef _, `Opaque (b, c) -> b, c
    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
    | _ -> assert false in
  DefinitionEntry {
    const_entry_body = Future.from_val (pt, []);
    const_entry_secctx = None;
    const_entry_feedback = None;
    const_entry_type =
      (match cb.const_type with RegularArity t -> Some t | _ -> None);
    const_entry_polymorphic = cb.const_polymorphic;
    const_entry_universes = cb.const_universes;
    const_entry_opaque = Declareops.is_opaque cb;
    const_entry_inline_code = cb.const_inline_code }
;;

let turn_direct (kn,cb,u,r as orig) =
  match cb.const_body, u with
  | OpaqueDef _, `Opaque (b,c) ->
      let pt = Future.from_val (b,c) in
      kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
   | _ -> orig
;;

type side_effect_role =
  | Subproof
  | Schema of inductive * string

type exported_side_effect = 
  constant * constant_body * side_effects constant_entry * side_effect_role

let export_side_effects mb env ce =
  match ce with
  | ParameterEntry _ | ProjectionEntry _ -> [], ce
  | DefinitionEntry c ->
      let { const_entry_body = body } = c in
      let _, eff = Future.force body in
      let ce = DefinitionEntry { c with
        const_entry_body = Future.chain ~greedy:true ~pure:true body
          (fun (b_ctx, _) -> b_ctx, []) } in
      let not_exists (c,_,_,_) =
        try ignore(Environ.lookup_constant c env); false
        with Not_found -> true in 
      let aux (acc,sl) { eff = se; from_env = mb } =
        let cbl = match se with
          | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
          | SEscheme (cl,k) ->
              List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
        let cbl = List.filter not_exists cbl in
        if cbl = [] then acc, sl
        else cbl :: acc, (mb,List.length cbl) :: sl in
      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
      let trusted = check_signatures mb signatures in
      let push_seff env = function
        | kn, cb, `Nothing, _ ->
           let env = Environ.add_constant kn cb env in
	   if not cb.const_polymorphic then
	     Environ.push_context ~strict:true cb.const_universes env
	   else env
        | kn, cb, `Opaque(_, ctx), _ -> 
           let env = Environ.add_constant kn cb env in
	   if not cb.const_polymorphic then
	     let env = Environ.push_context ~strict:true cb.const_universes env in
             Environ.push_context_set ~strict:true ctx env
	   else env in
      let rec translate_seff sl seff acc env =
        match sl, seff with
        | _, [] -> List.rev acc, ce
        | (None | Some 0), cbs :: rest ->
           let env, cbs =
             List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
               let ce = constant_entry_of_side_effect ocb u in
               let cb = translate_constant mb env kn ce in
               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
             (env,[]) cbs in
           translate_seff sl rest (cbs @ acc) env
        | Some sl, cbs :: rest ->
           let cbs_len = List.length cbs in
           let cbs = List.map turn_direct cbs in
           let env = List.fold_left push_seff env cbs in
           let ecbs = List.map (fun (kn,cb,u,r) ->
             kn, cb, constant_entry_of_side_effect cb u, r) cbs in
           translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
     in
       translate_seff trusted seff [] env
;;

let translate_local_assum env t =
  let j = infer env t in
  let t = Typeops.assumption_of_judgment env j in
    t

let translate_recipe env kn r =
  build_constant_declaration kn env (Cooking.cook_constant env r)

let translate_local_def mb env id centry =
  let def,typ,proj,poly,univs,inline_code,ctx =
    infer_declaration ~trust:mb env None (DefinitionEntry centry) in
  let typ = type_of_constant_type env typ in
  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
    match def with
    | Undef _ -> ()
    | Def _ -> ()
    | OpaqueDef lc ->
       let open Context.Named.Declaration in
       let context_ids = List.map get_id (named_context env) in
       let ids_typ = global_vars_set env typ in
       let ids_def = global_vars_set env
         (Opaqueproof.force_proof (opaque_tables env) lc) in
       let expr =
         !suggest_proof_using (Id.to_string id)
           env ids_def ids_typ context_ids in
       record_aux env ids_typ ids_def expr
  end;
  def, typ, univs

(* Insertion of inductive types. *)

let translate_mind env kn mie = Indtypes.check_inductive env kn mie

let inline_entry_side_effects env ce = { ce with
  const_entry_body = Future.chain ~greedy:true ~pure:true
    ce.const_entry_body (fun ((body, ctx), side_eff) ->
      let body, ctx',_ = inline_side_effects env body ctx side_eff in
      (body, ctx'), []);
}

let inline_side_effects env body side_eff =
  pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff)