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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml
as part of the rebuilding of Coq around a purely functional
abstract type-checker, Nov 1999 *)
(* This module implements kernel-level discharching of local
declarations over global constants and inductive types *)
open CErrors
open Util
open Names
open Term
open Constr
open Declarations
open Univ
module NamedDecl = Context.Named.Declaration
(*s Cooking the constants. *)
let pop_dirpath p = match DirPath.repr p with
| [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.")
| _::l -> DirPath.make l
let pop_mind kn =
let (mp,dir,l) = MutInd.repr3 kn in
MutInd.make3 mp (pop_dirpath dir) l
let pop_con con =
let (mp,dir,l) = Constant.repr3 con in
Constant.make3 mp (pop_dirpath dir) l
type my_global_reference =
| ConstRef of Constant.t
| IndRef of inductive
| ConstructRef of constructor
module RefHash =
struct
type t = my_global_reference
let equal gr1 gr2 = match gr1, gr2 with
| ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
| IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
| ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
| _ -> false
open Hashset.Combine
let hash = function
| ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
| IndRef i -> combinesmall 2 (ind_syntactic_hash i)
| ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
end
module RefTable = Hashtbl.Make(RefHash)
let instantiate_my_gr gr u =
match gr with
| ConstRef c -> mkConstU (c, u)
| IndRef i -> mkIndU (i, u)
| ConstructRef c -> mkConstructU (c, u)
let share cache r (cstl,knl) =
try RefTable.find cache r
with Not_found ->
let f,(u,l) =
match r with
| IndRef (kn,i) ->
IndRef (pop_mind kn,i), Mindmap.find kn knl
| ConstructRef ((kn,i),j) ->
ConstructRef ((pop_mind kn,i),j), Mindmap.find kn knl
| ConstRef cst ->
ConstRef (pop_con cst), Cmap.find cst cstl in
let c = (f, (u, Array.map mkVar l)) in
RefTable.add cache r c;
c
let share_univs cache r u l =
let r', (u', args) = share cache r l in
mkApp (instantiate_my_gr r' (Instance.append u' u), args)
let update_case_info cache ci modlist =
try
let ind, n =
match share cache (IndRef ci.ci_ind) modlist with
| (IndRef f,(u,l)) -> (f, Array.length l)
| _ -> assert false in
{ ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
with Not_found ->
ci
let is_empty_modlist (cm, mm) =
Cmap.is_empty cm && Mindmap.is_empty mm
let expmod_constr cache modlist c =
let share_univs = share_univs cache in
let update_case_info = update_case_info cache in
let rec substrec c =
match kind c with
| Case (ci,p,t,br) ->
Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))
| Ind (ind,u) ->
(try
share_univs (IndRef ind) u modlist
with
| Not_found -> Constr.map substrec c)
| Construct (cstr,u) ->
(try
share_univs (ConstructRef cstr) u modlist
with
| Not_found -> Constr.map substrec c)
| Const (cst,u) ->
(try
share_univs (ConstRef cst) u modlist
with
| Not_found -> Constr.map substrec c)
| Proj (p, c') ->
(try
let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in
let make c = Projection.make c (Projection.unfolded p) in
match kind p' with
| Const (p',_) -> mkProj (make p', substrec c')
| App (f, args) ->
(match kind f with
| Const (p', _) -> mkProj (make p', substrec c')
| _ -> assert false)
| _ -> assert false
with Not_found -> Constr.map substrec c)
| _ -> Constr.map substrec c
in
if is_empty_modlist modlist then c
else substrec c
let abstract_constant_type =
List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
let abstract_constant_body =
List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
type recipe = { from : constant_body; info : Opaqueproof.cooking_info }
type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
cook_proj : projection_body option;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
}
let on_body ml hy f = function
| Undef _ as x -> x
| Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs)))
| OpaqueDef o ->
OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
{ Opaqueproof.modlist = ml; abstract = hy } o)
let expmod_constr_subst cache modlist subst c =
let subst = Univ.make_instance_subst subst in
let c = expmod_constr cache modlist c in
Vars.subst_univs_level_constr subst c
let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
let cache = RefTable.create 13 in
let expmod = expmod_constr_subst cache modlist subst in
let hyps = Context.Named.map expmod vars in
abstract_constant_body (expmod c) hyps
let lift_univs cb subst auctx0 =
match cb.const_universes with
| Monomorphic_const ctx ->
assert (AUContext.is_empty auctx0);
subst, (Monomorphic_const ctx)
| Polymorphic_const auctx ->
(** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
and another abstract context relative to the former context
[auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
construct the lifted abstract universe context
[0 ... n - 1 n ... n + m - 1 |=
C{0, ... n - 1} ∪
C'{0, ..., n - 1, n, ..., n + m - 1} ]
together with the instance
[u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
*)
if (Univ.Instance.is_empty subst) then
(** Still need to take the union for the constraints between globals *)
subst, (Polymorphic_const (AUContext.union auctx0 auctx))
else
let ainst = Univ.make_abstract_instance auctx in
let subst = Instance.append subst ainst in
let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
let cook_constant ~hcons env { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
let usubst, univs = lift_univs cb usubst abs_ctx in
let expmod = expmod_constr_subst cache modlist usubst in
let hyps = Context.Named.map expmod abstract in
let map c =
let c = abstract_constant_body (expmod c) hyps in
if hcons then Constr.hcons c else c
in
let body = on_body modlist (hyps, usubst, abs_ctx)
map
cb.const_body
in
let const_hyps =
Context.Named.fold_outside (fun decl hyps ->
List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
hyps)
hyps ~init:cb.const_hyps in
let typ = abstract_constant_type (expmod cb.const_type) hyps in
let projection pb =
let c' = abstract_constant_body (expmod pb.proj_body) hyps in
let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in
let ((mind, _), _), n' =
try
let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
match kind c' with
| App (f,l) -> (destInd f, Array.length l)
| Ind ind -> ind, 0
| _ -> assert false
with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
in
let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
{ proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
proj_eta = etab, etat;
proj_type = ty'; proj_body = c' }
in
{
cook_body = body;
cook_type = typ;
cook_proj = Option.map projection cb.const_proj;
cook_universes = univs;
cook_inline = cb.const_inline_code;
cook_context = Some const_hyps;
}
(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
|
