Source file context.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
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
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
(** The modules defined below represent a {e local context}
as defined by Chapter 4 in the Reference Manual:
A {e local context} is an ordered list of of {e local declarations}
of names that we call {e variables}.
A {e local declaration} of some variable can be either:
- a {e local assumption}, or
- a {e local definition}.
*)
open Util
open Names
type ('a,'r) pbinder_annot = { binder_name : 'a; binder_relevance : 'r }
let eq_annot eq eqr {binder_name=na1;binder_relevance=r1} {binder_name=na2;binder_relevance=r2} =
eq na1 na2 && eqr r1 r2
let hash_annot h {binder_name=n;binder_relevance=r} =
Hashset.Combine.combinesmall (Sorts.relevance_hash r) (h n)
let map_annot f {binder_name=na;binder_relevance} =
let na' = f na in
{binder_name=na';binder_relevance}
let map_annot_relevance_smart fr ({binder_name=na;binder_relevance=r} as a) =
let r' = fr r in
if r == r' then a else {binder_name=na;binder_relevance=r'}
let map_annot_relevance fr {binder_name=na;binder_relevance=r} =
let r' = fr r in
{binder_name=na;binder_relevance=r'}
let make_annot x r = {binder_name=x;binder_relevance=r}
let binder_name x = x.binder_name
let binder_relevance x = x.binder_relevance
let annotR x = make_annot x Sorts.Relevant
let nameR x = annotR (Name x)
let anonR = annotR Anonymous
(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
Individual declarations are then designated by de Bruijn indexes. *)
module Rel =
struct
(** Representation of {e local declarations}. *)
module Declaration =
struct
type ('constr, 'types, 'r) pt =
| LocalAssum of (Name.t,'r) pbinder_annot * 'types (** name, type *)
| LocalDef of (Name.t,'r) pbinder_annot * 'constr * 'types (** name, value, type *)
let get_annot = function
| LocalAssum (na,_) | LocalDef (na,_,_) -> na
(** Return the name bound by a given declaration. *)
let get_name x = (get_annot x).binder_name
(** Return [Some value] for local-declarations and [None] for local-assumptions. *)
let get_value = function
| LocalAssum _ -> None
| LocalDef (_,v,_) -> Some v
(** Return the type of the name bound by a given declaration. *)
let get_type = function
| LocalAssum (_,ty)
| LocalDef (_,_,ty) -> ty
let get_relevance x = (get_annot x).binder_relevance
let set_annot x d =
if get_annot d == x then d else match d with
| LocalAssum (_,ty) -> LocalAssum (x, ty)
| LocalDef (_,v,ty) -> LocalDef (x, v, ty)
(** Set the name that is bound by a given declaration. *)
let set_name na = function
| LocalAssum (x,ty) -> LocalAssum ({x with binder_name=na}, ty)
| LocalDef (x,v,ty) -> LocalDef ({x with binder_name=na}, v, ty)
let set_relevance r = function
| LocalAssum (x,ty) -> LocalAssum ({x with binder_relevance=r}, ty)
| LocalDef (x,v,ty) -> LocalDef ({x with binder_relevance=r}, v, ty)
(** Set the type of the bound variable in a given declaration. *)
let set_type ty = function
| LocalAssum (na,_) -> LocalAssum (na, ty)
| LocalDef (na,v,_) -> LocalDef (na, v, ty)
(** Return [true] iff a given declaration is a local assumption. *)
let is_local_assum = function
| LocalAssum _ -> true
| LocalDef _ -> false
(** Return [true] iff a given declaration is a local definition. *)
let is_local_def = function
| LocalAssum _ -> false
| LocalDef _ -> true
(** Check whether any term in a given declaration satisfies a given predicate. *)
let exists f = function
| LocalAssum (_, ty) -> f ty
| LocalDef (_, v, ty) -> f v || f ty
(** Check whether all terms in a given declaration satisfy a given predicate. *)
let for_all f = function
| LocalAssum (_, ty) -> f ty
| LocalDef (_, v, ty) -> f v && f ty
(** Check whether the two given declarations are equal. *)
let equal eqr eq decl1 decl2 =
match decl1, decl2 with
| LocalAssum (n1,ty1), LocalAssum (n2, ty2) ->
eq_annot Name.equal eqr n1 n2 && eq ty1 ty2
| LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) ->
eq_annot Name.equal eqr n1 n2 && eq v1 v2 && eq ty1 ty2
| _ ->
false
(** Map the name bound by a given declaration. *)
let map_name f x =
let na = get_name x in
let na' = f na in
if na == na' then x else set_name na' x
let map_relevance f x =
let r = get_relevance x in
let r' = f r in
if r == r' then x else set_relevance r' x
(** For local assumptions, this function returns the original local assumptions.
For local definitions, this function maps the value in the local definition. *)
let map_value f = function
| LocalAssum _ as decl -> decl
| LocalDef (na, v, t) as decl ->
let v' = f v in
if v == v' then decl else LocalDef (na, v', t)
(** Map the type of the name bound by a given declaration. *)
let map_type f = function
| LocalAssum (na, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalAssum (na, ty')
| LocalDef (na, v, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalDef (na, v, ty')
(** Map all terms in a given declaration. *)
let map_constr f = function
| LocalAssum (na, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalAssum (na, ty')
| LocalDef (na, v, ty) as decl ->
let v' = f v in
let ty' = f ty in
if v == v' && ty == ty' then decl else LocalDef (na, v', ty')
(** Map all terms in a given declaration. *)
let map_constr_with_relevance g f = function
| LocalAssum (na, ty) as decl ->
let na' = map_annot_relevance_smart g na in
let ty' = f ty in
if na == na' && ty == ty' then decl else LocalAssum (na', ty')
| LocalDef (na, v, ty) as decl ->
let na' = map_annot_relevance_smart g na in
let v' = f v in
let ty' = f ty in
if na == na' && v == v' && ty == ty' then decl else LocalDef (na', v', ty')
let map_constr_het fr f = function
| LocalAssum (na, ty) ->
let ty' = f ty in
LocalAssum (map_annot_relevance fr na, ty')
| LocalDef (na, v, ty) ->
let v' = f v in
let ty' = f ty in
LocalDef (map_annot_relevance fr na, v', ty')
(** Perform a given action on all terms in a given declaration. *)
let iter_constr f = function
| LocalAssum (_,ty) -> f ty
| LocalDef (_,v,ty) -> f v; f ty
(** Reduce all terms in a given declaration to a single value. *)
let fold_constr f decl acc =
match decl with
| LocalAssum (_n,ty) -> f ty acc
| LocalDef (_n,v,ty) -> f ty (f v acc)
let to_tuple = function
| LocalAssum (na, ty) -> na, None, ty
| LocalDef (na, v, ty) -> na, Some v, ty
let drop_body = function
| LocalAssum _ as d -> d
| LocalDef (na, _v, ty) -> LocalAssum (na, ty)
end
(** Rel-context is represented as a list of declarations.
Inner-most declarations are at the beginning of the list.
Outer-most declarations are at the end of the list. *)
type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
(** empty rel-context *)
let empty = []
(** Return a new rel-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
(** Return the number of {e local declarations} in a given rel-context. *)
let length = List.length
(** Return the number of {e local assumptions} in a given rel-context. *)
let nhyps ctx =
let open Declaration in
let rec nhyps acc = function
| [] -> acc
| LocalAssum _ :: hyps -> nhyps (succ acc) hyps
| LocalDef _ :: hyps -> nhyps acc hyps
in
nhyps 0 ctx
(** Return a declaration designated by a given de Bruijn index.
@raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
let rec lookup n ctx =
match n, ctx with
| 1, decl :: _ -> decl
| n, _ :: sign -> lookup (n-1) sign
| _, [] -> raise Not_found
(** Check whether given two rel-contexts are equal. *)
let equal eqr eq l = List.equal (fun c -> Declaration.equal eqr eq c) l
(** Map all terms in a given rel-context. *)
let map f = List.Smart.map (Declaration.map_constr f)
let map_with_relevance g f = List.Smart.map (Declaration.map_constr_with_relevance g f)
let map_het fr f = List.map (Declaration.map_constr_het fr f)
(** Map all terms in a given rel-context. *)
let map_with_binders f ctx =
let rec aux k = function
| decl :: ctx as l ->
let decl' = Declaration.map_constr (f k) decl in
let ctx' = aux (k-1) ctx in
if decl == decl' && ctx == ctx' then l else decl' :: ctx'
| [] -> []
in
aux (length ctx) ctx
(** Perform a given action on every declaration in a given rel-context. *)
let iter f = List.iter (Declaration.iter_constr f)
(** Reduce all terms in a given rel-context to a single value.
Innermost declarations are processed first. *)
let fold_inside f ~init = List.fold_left f init
(** Reduce all terms in a given rel-context to a single value.
Outermost declarations are processed first. *)
let fold_outside f l ~init = List.fold_right f l init
(** Return the set of all named variables bound in a given rel-context. *)
let to_vars l =
List.fold_left (fun accu decl ->
match Declaration.get_name decl with
| Name id -> Id.Set.add id accu
| Anonymous -> accu)
Id.Set.empty l
(** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
and each {e local definition} is mapped to [false]. *)
let to_tags l =
let rec aux l = function
| [] -> l
| Declaration.LocalDef _ :: ctx -> aux (true::l) ctx
| Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
in aux [] l
let drop_bodies l = List.Smart.map Declaration.drop_body l
(** Split a context so that the second part contains [n]
[LocalAssum], keeping all [LocalDef] in the middle in the first part *)
let chop_nhyps n l =
let rec aux l' = function
| (0, l) -> (List.rev l', l)
| (n, (Declaration.LocalDef _ as h) :: l) -> aux (h::l') (n, l)
| (n, (Declaration.LocalAssum _ as h) :: l) -> aux (h::l') (n-1, l)
| (_, []) -> CErrors.anomaly (Pp.str "chop_nhyps: not enough hypotheses.")
in aux [] (n,l)
(** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
with n = |Δ| and with the {e local definitions} of [Γ] skipped in
[args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
let to_extended_list mk n l =
let rec reln l p = function
| Declaration.LocalAssum _ :: hyps -> reln (mk (n+p) :: l) (p+1) hyps
| Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
| [] -> l
in
reln [] 1 l
(** [extended_vect n Γ] does the same, returning instead an array. *)
let to_extended_vect mk n hyps = Array.of_list (to_extended_list mk n hyps)
(** Consistency with terminology in Named *)
let instance = to_extended_vect
let instance_list = to_extended_list
end
(** This module represents contexts that can capture non-anonymous variables.
Individual declarations are then designated by the identifiers they bind. *)
module Named =
struct
(** Representation of {e local declarations}. *)
module Declaration =
struct
(** local declaration *)
type ('constr, 'types, 'r) pt =
| LocalAssum of (Id.t,'r) pbinder_annot * 'types (** identifier, type *)
| LocalDef of (Id.t,'r) pbinder_annot * 'constr * 'types (** identifier, value, type *)
let get_annot = function
| LocalAssum (na,_) | LocalDef (na,_,_) -> na
(** Return the identifier bound by a given declaration. *)
let get_id x = (get_annot x).binder_name
(** Return [Some value] for local-declarations and [None] for local-assumptions. *)
let get_value = function
| LocalAssum _ -> None
| LocalDef (_,v,_) -> Some v
(** Return the type of the name bound by a given declaration. *)
let get_type = function
| LocalAssum (_,ty)
| LocalDef (_,_,ty) -> ty
let get_relevance x = (get_annot x).binder_relevance
(** Set the identifier that is bound by a given declaration. *)
let set_id id =
let set x = {x with binder_name = id} in
function
| LocalAssum (x,ty) -> LocalAssum (set x, ty)
| LocalDef (x, v, ty) -> LocalDef (set x, v, ty)
(** Set the type of the bound variable in a given declaration. *)
let set_type ty = function
| LocalAssum (id,_) -> LocalAssum (id, ty)
| LocalDef (id,v,_) -> LocalDef (id, v, ty)
(** Return [true] iff a given declaration is a local assumption. *)
let is_local_assum = function
| LocalAssum _ -> true
| LocalDef _ -> false
(** Return [true] iff a given declaration is a local definition. *)
let is_local_def = function
| LocalDef _ -> true
| LocalAssum _ -> false
(** Check whether any term in a given declaration satisfies a given predicate. *)
let exists f = function
| LocalAssum (_, ty) -> f ty
| LocalDef (_, v, ty) -> f v || f ty
(** Check whether all terms in a given declaration satisfy a given predicate. *)
let for_all f = function
| LocalAssum (_, ty) -> f ty
| LocalDef (_, v, ty) -> f v && f ty
(** Check whether the two given declarations are equal. *)
let equal eqr eq decl1 decl2 =
match decl1, decl2 with
| LocalAssum (id1, ty1), LocalAssum (id2, ty2) ->
eq_annot Id.equal eqr id1 id2 && eq ty1 ty2
| LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) ->
eq_annot Id.equal eqr id1 id2 && eq v1 v2 && eq ty1 ty2
| _ ->
false
(** Map the identifier bound by a given declaration. *)
let map_id f x =
let id = get_id x in
let id' = f id in
if id == id' then x else set_id id' x
(** For local assumptions, this function returns the original local assumptions.
For local definitions, this function maps the value in the local definition. *)
let map_value f = function
| LocalAssum _ as decl -> decl
| LocalDef (na, v, t) as decl ->
let v' = f v in
if v == v' then decl else LocalDef (na, v', t)
(** Map the type of the name bound by a given declaration. *)
let map_type f = function
| LocalAssum (id, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalAssum (id, ty')
| LocalDef (id, v, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalDef (id, v, ty')
(** Map all terms in a given declaration. *)
let map_constr f = function
| LocalAssum (id, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalAssum (id, ty')
| LocalDef (id, v, ty) as decl ->
let v' = f v in
let ty' = f ty in
if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
(** Map all terms in a given declaration. *)
let map_constr_with_relevance g f = function
| LocalAssum (id, ty) as decl ->
let id' = map_annot_relevance_smart g id in
let ty' = f ty in
if id == id' && ty == ty' then decl else LocalAssum (id', ty')
| LocalDef (id, v, ty) as decl ->
let id' = map_annot_relevance_smart g id in
let v' = f v in
let ty' = f ty in
if id == id' && v == v' && ty == ty' then decl else LocalDef (id', v', ty')
let map_constr_het fr f = function
| LocalAssum (id, ty) ->
let ty' = f ty in
LocalAssum (map_annot_relevance fr id, ty')
| LocalDef (id, v, ty) ->
let v' = f v in
let ty' = f ty in
LocalDef (map_annot_relevance fr id, v', ty')
(** Perform a given action on all terms in a given declaration. *)
let iter_constr f = function
| LocalAssum (_, ty) -> f ty
| LocalDef (_, v, ty) -> f v; f ty
(** Reduce all terms in a given declaration to a single value. *)
let fold_constr f decl a =
match decl with
| LocalAssum (_, ty) -> f ty a
| LocalDef (_, v, ty) -> a |> f v |> f ty
let to_tuple = function
| LocalAssum (id, ty) -> id, None, ty
| LocalDef (id, v, ty) -> id, Some v, ty
let of_tuple = function
| id, None, ty -> LocalAssum (id, ty)
| id, Some v, ty -> LocalDef (id, v, ty)
let drop_body = function
| LocalAssum _ as d -> d
| LocalDef (id, _v, ty) -> LocalAssum (id, ty)
let of_rel_decl f = function
| Rel.Declaration.LocalAssum (na,t) ->
LocalAssum (map_annot f na, t)
| Rel.Declaration.LocalDef (na,v,t) ->
LocalDef (map_annot f na, v, t)
let to_rel_decl =
let name x = {binder_name=Name x.binder_name;binder_relevance=x.binder_relevance} in
function
| LocalAssum (id,t) ->
Rel.Declaration.LocalAssum (name id, t)
| LocalDef (id,v,t) ->
Rel.Declaration.LocalDef (name id,v,t)
end
(** Named-context is represented as a list of declarations.
Inner-most declarations are at the beginning of the list.
Outer-most declarations are at the end of the list. *)
type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
(** empty named-context *)
let empty = []
(** Return a new named-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
(** Return the number of {e local declarations} in a given named-context. *)
let length = List.length
(** Return a declaration designated by a given identifier
@raise Not_found if the designated identifier is not present in the designated named-context. *)
let rec lookup id = function
| decl :: _ when Id.equal id (Declaration.get_id decl) -> decl
| _ :: sign -> lookup id sign
| [] -> raise Not_found
(** Check whether given two named-contexts are equal. *)
let equal eqr eq l = List.equal (fun c -> Declaration.equal eqr eq c) l
(** Map all terms in a given named-context. *)
let map f = List.Smart.map (Declaration.map_constr f)
let map_with_relevance g f = List.Smart.map (Declaration.map_constr_with_relevance g f)
let map_het fr f = List.map (Declaration.map_constr_het fr f)
(** Perform a given action on every declaration in a given named-context. *)
let iter f = List.iter (Declaration.iter_constr f)
(** Reduce all terms in a given named-context to a single value.
Innermost declarations are processed first. *)
let fold_inside f ~init = List.fold_left f init
(** Reduce all terms in a given named-context to a single value.
Outermost declarations are processed first. *)
let fold_outside f l ~init = List.fold_right f l init
(** Return the set of all identifiers bound in a given named-context. *)
let to_vars l =
List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l
let drop_bodies l = List.Smart.map Declaration.drop_body l
(** [to_instance Ω] builds an instance [args] in reverse order such
that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
let to_instance mk l =
let filter = function
| Declaration.LocalAssum (id, _) -> Some (mk id.binder_name)
| _ -> None
in
List.map_filter filter l
(** [instance Ω] builds an instance [args] such
that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
let instance_list mk l =
let filter = function
| Declaration.LocalAssum (id, _) -> Some (mk id.binder_name)
| _ -> None
in
List.rev (List.map_filter filter l)
let instance mk l =
Array.of_list (instance_list mk l)
end
module Compacted =
struct
module Declaration =
struct
type ('constr, 'types, 'r) pt =
| LocalAssum of (Id.t,'r) pbinder_annot list * 'types
| LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types
let map_constr f = function
| LocalAssum (ids, ty) as decl ->
let ty' = f ty in
if ty == ty' then decl else LocalAssum (ids, ty')
| LocalDef (ids, c, ty) as decl ->
let ty' = f ty in
let c' = f c in
if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
let of_named_decl = function
| Named.Declaration.LocalAssum (id,t) ->
LocalAssum ([id],t)
| Named.Declaration.LocalDef (id,v,t) ->
LocalDef ([id],v,t)
let to_named_context = function
| LocalAssum (ids, t) ->
List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids
| LocalDef (ids, v, t) ->
List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids
end
type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
let fold f l ~init = List.fold_right f l init
end