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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \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 Univ
open Term
open Context
open Declarations
open Environ
open Entries
open Typeops
let constrain_type env j cst1 = function
| `None ->
make_polymorphic_if_constant_for_ind env j, cst1
| `Some t ->
let (tj,cst2) = infer_type env t in
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (eq_constr t tj.utj_val);
let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
NonPolymorphicType t, cstrs
| `SomeWJ (t, tj, cst2) ->
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (eq_constr t tj.utj_val);
let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
NonPolymorphicType t, cstrs
let map_option_typ = function None -> `None | Some x -> `Some x
let translate_local_assum env t =
let (j,cst) = infer env t in
let t = Typeops.assumption_of_judgment env j in
(t,cst)
(* Insertion of constants and parameters in environment. *)
let handle_side_effects env body side_eff =
let handle_sideff t se =
let cbl = match se with
| SEsubproof (c,cb) -> [c,cb]
| SEscheme (cl,_) -> List.map (fun (_,c,cb) -> c,cb) cl 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 fix_body (c,cb) t =
match cb.const_body with
| Undef _ -> assert false
| Def b ->
let b = Mod_subst.force_constr b in
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)
| OpaqueDef b ->
let b = Opaqueproof.force_proof b in
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|]) in
List.fold_right fix_body cbl t
in
(* CAVEAT: we assure a proper order *)
Declareops.fold_side_effects handle_sideff body
(Declareops.uniquize_side_effects side_eff)
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 Interface.Complete)
let infer_declaration env dcl =
match dcl with
| ParameterEntry (ctx,t,nl) ->
let j, cst = infer env t in
let t = hcons_constr (Typeops.assumption_of_judgment env j) in
Undef nl, NonPolymorphicType t, cst, false, ctx
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true } as c) ->
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj, tycst = infer_type env typ in
let proofterm =
Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
let body = handle_side_effects env body side_eff in
let j, cst = infer env body in
let j = hcons_j j in
let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
feedback_completion_typecheck feedback_id;
j.uj_val, cst) in
let def = OpaqueDef (Opaqueproof.create proofterm) in
let typ = NonPolymorphicType typ in
def, typ, tycst, 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, side_eff = Future.join body in
let body = handle_side_effects env body side_eff in
let j, cst = infer env body in
let j = hcons_j j in
let typ, cst = constrain_type env j cst (map_option_typ typ) in
feedback_completion_typecheck feedback_id;
let def = Def (Mod_subst.from_val j.uj_val) in
def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
| PolymorphicArity (ctx,_) ->
Context.fold_rel_context
(fold_rel_declaration
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
let record_aux env s1 s2 =
let v =
String.concat " "
(List.map (fun (id, _,_) -> Id.to_string id)
(keep_hyps env (Id.Set.union s1 s2))) in
Aux_file.record_in_aux "context_used" v
let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
let set_suggest_proof_using f = suggest_proof_using := f
let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
let check declared inferred =
let mk_set l = List.fold_right Id.Set.add (List.map pi1 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
error ("The following section variable are used but not declared:\n"^
(String.concat ", " (List.map Id.to_string
(Id.Set.elements (Idset.diff inferred_set declared_set))))) in
(* We try to postpone the computation of used section variables *)
let hyps, def =
let context_ids = List.map pi1 (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 lc) in
!suggest_proof_using kn env vars ids_typ context_ids;
if !Flags.compilation_mode = Flags.BuildVo then
record_aux env ids_typ vars;
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 *)
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
{ const_hyps = hyps;
const_body = def;
const_type = typ;
const_body_code = Cemitcodes.from_val (compile_constant_body env def);
const_constraints = cst;
const_inline_code = inline_code }
(*s Global and local constant declaration. *)
let translate_constant env kn ce =
build_constant_declaration kn env (infer_declaration env ce)
let translate_recipe env kn r =
let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
build_constant_declaration kn env (def,typ,cst,inline_code,hyps)
let translate_local_def env id centry =
let def,typ,cst,inline_code,ctx =
infer_declaration env (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
def, typ, cst
(* Insertion of inductive types. *)
let translate_mind env kn mie = Indtypes.check_inductive env kn mie
let handle_side_effects env ce = { ce with
const_entry_body = Future.chain ~greedy:true ~pure:true
ce.const_entry_body (fun (body, side_eff) ->
handle_side_effects env body side_eff, Declareops.no_seff);
}
|
