Source file structures.ml
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
open CErrors
open Util
open Pp
open Names
open Constr
open Mod_subst
open Reductionops
module Structure = struct
type projection = {
proj_name : Names.Name.t;
proj_true : bool;
proj_canonical : bool;
proj_body : Names.Constant.t option;
}
type t = {
name : Names.inductive;
projections : projection list;
nparams : int;
}
let make env name projections =
let nparams = Inductiveops.inductive_nparams env name in
{ name; projections; nparams }
let structure_table =
Summary.ref (Indmap.empty : t Indmap.t) ~name:"record-structs"
let projection_table =
Summary.ref (Cmap.empty : t Cmap.t) ~name:"record-projs"
let register ({ name; projections; nparams } as s) =
structure_table := Indmap.add name s !structure_table;
projection_table :=
List.fold_right (fun { proj_body } m ->
Option.fold_right (fun proj -> Cmap.add proj s) proj_body m)
projections !projection_table
let subst subst ({ name; projections; nparams } as s) =
let subst_projection subst ({ proj_body } as p) =
let proj_body = Option.Smart.map (subst_constant subst) proj_body in
if proj_body == p.proj_body then p else
{ p with proj_body } in
let projections = List.Smart.map (subst_projection subst) projections in
let name = Mod_subst.subst_ind subst name in
if projections == s.projections &&
name == s.name
then s
else { name; projections; nparams }
let rebuild env s =
let mib = Environ.lookup_mind (fst s.name) env in
let nparams = mib.Declarations.mind_nparams in
{ s with nparams }
let find indsp = Indmap.find indsp !structure_table
let find_projections indsp =
(find indsp).projections |>
List.map (fun { proj_body } -> proj_body)
let find_from_projection cst = Cmap.find cst !projection_table
let projection_nparams cst = (Cmap.find cst !projection_table).nparams
let is_projection cst = Cmap.mem cst !projection_table
end
type obj_typ = {
o_ORIGIN : GlobRef.t;
o_DEF : constr;
o_CTX : Univ.AUContext.t;
o_INJ : int option;
o_TABS : constr list;
o_TPARAMS : constr list;
o_NPARAMS : int;
o_TCOMPS : constr list }
module ValuePattern = struct
type t =
Const_cs of GlobRef.t
| Proj_cs of Names.Projection.Repr.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs
let equal env p1 p2 = match p1, p2 with
| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
| Prod_cs, Prod_cs -> true
| Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
| Default_cs, Default_cs -> true
| _ -> false
let compare p1 p2 = match p1, p2 with
| Const_cs gr1, Const_cs gr2 -> GlobRef.CanOrd.compare gr1 gr2
| Proj_cs p1, Proj_cs p2 -> Projection.Repr.CanOrd.compare p1 p2
| Prod_cs, Prod_cs -> 0
| Sort_cs s1, Sort_cs s2 -> Sorts.family_compare s1 s2
| Default_cs, Default_cs -> 0
| _ -> pervasives_compare p1 p2
let rec of_constr env t =
match kind t with
| App (f,vargs) ->
let patt, n, args = of_constr env f in
patt, n, args @ Array.to_list vargs
| Rel n -> Default_cs, Some n, []
| Lambda (_, _, b) -> let patt, _, _ = of_constr env b in patt, None, []
| Prod (_,_,_) -> Prod_cs, None, [t]
| Proj (p, c) -> Proj_cs (Names.Projection.repr p), None, [c]
| Sort s -> Sort_cs (Sorts.family s), None, []
| _ -> Const_cs (fst @@ destRef t) , None, []
let print = function
Const_cs c -> Nametab.pr_global_env Id.Set.empty c
| Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Names.Projection.Repr.constant p))
| Prod_cs -> str "forall _, _"
| Default_cs -> str "_"
| Sort_cs s -> Sorts.pr_sort_family s
end
module PatMap = Map.Make(ValuePattern)
let object_table =
Summary.ref (GlobRef.Map.empty : (constr * obj_typ) PatMap.t GlobRef.Map.t)
~name:"record-canonical-structs"
let keep_true_projections projs =
let filter { Structure.proj_true ; proj_canonical; proj_body } = if proj_true then Some (proj_body, proj_canonical) else None in
List.map_filter filter projs
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
(fun (sign,env,t,ref,proji_sp) ->
let env = Termops.push_rels_assum sign env in
let con_pp = Nametab.pr_global_env Id.Set.empty ref in
let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in
let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
strbrk "Projection value has no head constant: "
++ term_pp ++ strbrk " in canonical instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
let compute_canonical_projections env ~warn (gref,ind) =
let o_CTX = Environ.universes_of_global env gref in
let o_DEF, c =
match gref with
| GlobRef.ConstRef con ->
let u = Univ.make_abstract_instance o_CTX in
mkConstU (con, u), Environ.constant_value_in env (con,u)
| GlobRef.VarRef id ->
mkVar id, Option.get (Environ.named_body id env)
| GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false
in
let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
let t = EConstr.Unsafe.to_constr t in
let o_TABS = List.rev_map snd sign in
let args = snd (decompose_app t) in
let { Structure.nparams = p; projections = lpj } =
Structure.find ind in
let o_TPARAMS, projs = List.chop p args in
let o_NPARAMS = List.length o_TPARAMS in
let lpj = keep_true_projections lpj in
let nenv = Termops.push_rels_assum sign env in
List.fold_left2 (fun acc (spopt, canonical) t ->
let t = EConstr.Unsafe.to_constr (shrink_eta env (EConstr.of_constr t)) in
if canonical
then
Option.cata (fun proji_sp ->
match ValuePattern.of_constr nenv t with
| patt, o_INJ, o_TCOMPS ->
((GlobRef.ConstRef proji_sp, (patt, t)),
{ o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
:: acc
| exception DestKO ->
if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
acc
) acc spopt
else acc
) [] lpj projs
let warn_redundant_canonical_projection =
CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
(fun (hd_val,prj,new_can_s,old_can_s) ->
strbrk "Ignoring canonical projection to " ++ hd_val
++ strbrk " by " ++ prj ++ strbrk " in "
++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
module Instance = struct
type t = GlobRef.t * inductive
let repr = fst
let subst subst (gref,ind as obj) =
match gref with
| GlobRef.ConstRef cst ->
let cst' = subst_constant subst cst in
let ind' = subst_ind subst ind in
if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind')
| _ -> assert false
let error_not_structure ref description =
user_err ~hdr:"object_declare"
(str"Could not declare a canonical structure " ++
(Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
description))
let make env sigma ref =
let vc =
match ref with
| GlobRef.ConstRef sp ->
let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
begin match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
| None -> error_not_structure ref (str "Could not find its value in the global environment.") end
| GlobRef.VarRef id ->
begin match Environ.named_body id env with
| Some b -> b
| None -> error_not_structure ref (str "Could not find its value in the global environment.") end
| GlobRef.IndRef _ | GlobRef.ConstructRef _ ->
error_not_structure ref (str "Expected an instance of a record or structure.")
in
let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
let body = EConstr.Unsafe.to_constr body in
let f,args = match kind body with
| App (f,args) -> f,args
| _ ->
error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in
let indsp = match kind f with
| Construct ((indsp,1),u) -> indsp
| _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in
let s =
try Structure.find indsp
with Not_found ->
error_not_structure ref
(str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
let ntrue_projs = List.count (fun { Structure.proj_true = x } -> x) s.Structure.projections in
if s.Structure.nparams + ntrue_projs > Array.length args then
error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
(ref,indsp)
let register ~warn env sigma o =
compute_canonical_projections env ~warn o |>
List.iter (fun ((proj, (cs_pat, t)), s) ->
let l = try GlobRef.Map.find proj !object_table with Not_found -> PatMap.empty in
match PatMap.find cs_pat l with
| exception Not_found ->
object_table := GlobRef.Map.add proj (PatMap.add cs_pat (t, s) l) !object_table
| _, cs ->
if warn
then
let old_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF) in
let new_can_s = Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF) in
let prj = Nametab.pr_global_env Id.Set.empty proj in
let hd_val = ValuePattern.print cs_pat in
warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
)
end
(** The canonical solution of a problem (proj,val) is a global
[constant = fun abs : abstractions_ty => body] and
[ body = RecodConstructor params canon_values ] and the canonical value
corresponding to val is [val cvalue_arguments].
It is possible that val is one of the [abs] abstractions, eg [Default_cs],
and in that case [cvalue_abstraction = Some i] *)
module CanonicalSolution = struct
type t = {
constant : EConstr.t;
abstractions_ty : EConstr.t list;
body : EConstr.t;
nparams : int;
params : EConstr.t list;
cvalue_abstraction : int option;
cvalue_arguments : EConstr.t list;
}
let find env sigma (proj,pat) =
let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = PatMap.find pat (GlobRef.Map.find proj !object_table) in
let us = List.map EConstr.of_constr us in
let params = List.map EConstr.of_constr params in
let u, ctx' = UnivGen.fresh_instance_from ctx None in
let subst = Univ.make_inverse_instance_subst u in
let c = EConstr.of_constr c in
let c' = EConstr.Vars.subst_univs_level_constr subst c in
let t' = EConstr.of_constr t' in
let t' = EConstr.Vars.subst_univs_level_constr subst t' in
let bs' = List.map (EConstr.of_constr %> EConstr.Vars.subst_univs_level_constr subst) bs in
let params = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) params in
let us = List.map (fun c -> EConstr.Vars.subst_univs_level_constr subst c) us in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
sigma, { body = t'; constant = c'; abstractions_ty = bs'; nparams; params; cvalue_arguments = us; cvalue_abstraction = n }
let rec get_nth n = function
| [] -> raise Not_found
| arg :: args ->
let len = Array.length arg in
if n < len then arg.(n)
else get_nth (n - len) args
let rec decompose_projection sigma c args =
match EConstr.kind sigma c with
| Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args
| Cast (c, _, _) -> decompose_projection sigma c args
| App (c, arg) -> decompose_projection sigma c (arg :: args)
| Const (c, u) ->
let n = Structure.projection_nparams c in
let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
get_nth n args
| Proj (p, c) ->
let _ = GlobRef.Map.find (GlobRef.ConstRef (Names.Projection.constant p)) !object_table in
c
| _ -> raise Not_found
let is_open_canonical_projection env sigma c =
let open EConstr in
try
let arg = decompose_projection sigma c [] in
try
let arg = whd_all env sigma arg in
let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
not (isConstruct sigma hd)
with Failure _ -> false
with Not_found -> false
end
module CSTable = struct
type entry = {
projection : Names.GlobRef.t;
value : ValuePattern.t;
solution : Names.GlobRef.t;
}
let canonical_entry_of_object projection value (_, { o_ORIGIN = solution }) =
{ projection; value; solution }
let entries () =
GlobRef.Map.fold (fun p ol acc ->
PatMap.fold (fun pat o acc -> canonical_entry_of_object p pat o :: acc) ol acc)
!object_table []
let entries_for ~projection:p =
try
GlobRef.Map.find p !object_table |>
PatMap.bindings |>
List.map (fun (pat, o) -> canonical_entry_of_object p pat o)
with Not_found -> []
end
module PrimitiveProjections = struct
let prim_table =
Summary.ref (Cmap_env.empty : Names.Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
let register p c =
prim_table := Cmap_env.add c p !prim_table
let mem c = Cmap_env.mem c !prim_table
let find_opt c =
try Some (Cmap_env.find c !prim_table) with Not_found -> None
end