forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 1
/
constr.ml
1649 lines (1454 loc) · 60.2 KB
/
constr.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
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)
(* Extension to mutual inductive constructions by Christine Paulin for
Coq V5.10.2 *)
(* Extension to co-inductive constructions by Eduardo Gimenez *)
(* Optimization of substitution functions by Chet Murthy *)
(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
(* Hash-consing by Bruno Barras in Feb 1998 *)
(* Restructuration of Coq of the type-checking kernel by Jean-Christophe
Filliâtre, 1999 *)
(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
(* This file defines the internal syntax of the Calculus of
Inductive Constructions (CIC) terms together with constructors,
destructors, iterators and basic functions *)
open Util
open Names
open Univ
open Context
open Stages
open SVars
open Stage
open Annot
open Constraints
type existential_key = Evar.t
type metavariable = int
(* This defines the strategy to use for verifiying a Cast *)
(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *)
(* come after the vo-exported cast_kind so as to be compatible with coqchk *)
type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
(* This defines Cases annotations *)
type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
type case_printing =
{ ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
style : case_style }
(* INVARIANT:
* - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs
* - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)),
* ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i)
*)
type case_info =
{ ci_ind : inductive; (* inductive type to which belongs the value that is being matched *)
ci_npar : int; (* number of parameters of the above inductive type *)
ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines
the number of values that can be bound in a match-construct.
NOTE: parameters of the inductive type are therefore excluded from the count *)
ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines
the number of values that can be applied to the constructor,
in addition to the parameters of the related inductive type
NOTE: "lets" are therefore excluded from the count
NOTE: parameters of the inductive type are also excluded from the count *)
ci_relevance : Sorts.relevance;
ci_pp_info : case_printing (* not interpreted by the kernel *)
}
(********************************************************************)
(* Constructions as implemented *)
(********************************************************************)
(* [constr array] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
type 'constr pexistential = existential_key * 'constr array
type ('constr, 'types) prec_declaration =
Name.t binder_annot array * 'types array * 'constr array
type ('constr, 'types) pfixpoint =
(int option array * int) * ('constr, 'types) prec_declaration
type ('constr, 'types) pfixpoint_nopt =
(int array * int) * ('constr, 'types) prec_declaration
type ('constr, 'types) pcofixpoint =
int * ('constr, 'types) prec_declaration
type 'a puniverses = 'a Univ.puniverses
type pconstant = Constant.t puniverses
type pinductive = inductive puniverses
type pconstructor = constructor puniverses
(* [Var] is used for named variables and [Rel] for variables as
de Bruijn indices. *)
type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Rel of int * Annot.t list option
| Var of Id.t
| Meta of metavariable
| Evar of 'constr pexistential
| Sort of 'sort
| Cast of 'constr * cast_kind * 'types
| Prod of Name.t binder_annot * 'types * 'types
| Lambda of Name.t binder_annot * 'types * 'constr
| LetIn of Name.t binder_annot * 'constr * 'types * 'constr
| App of 'constr * 'constr array
| Const of (Constant.t * 'univs) * Annot.t list option
| Ind of (inductive * 'univs) * Annot.t
| Construct of (constructor * 'univs)
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
| Proj of Projection.t * 'constr
| Int of Uint63.t
(* constr is the fixpoint of the previous type. Requires option
-rectypes of the Caml compiler to be set *)
type t = (t, t, Sorts.t, Instance.t) kind_of_term
type constr = t
type existential = existential_key * constr array
type types = constr
type rec_declaration = (constr, types) prec_declaration
type fixpoint = (constr, types) pfixpoint
type fixpoint_nopt = (constr, types) pfixpoint_nopt
type cofixpoint = (constr, types) pcofixpoint
(*********************)
(* Term constructors *)
(*********************)
(* Constructs a de Bruijn index with number n *)
let rels =
let mkRel n = Rel (n, None) in
[|mkRel 1;mkRel 2;mkRel 3;mkRel 4;mkRel 5;mkRel 6;mkRel 7;mkRel 8;
mkRel 9;mkRel 10;mkRel 11;mkRel 12;mkRel 13;mkRel 14;mkRel 15;mkRel 16|]
let mkRel n = if 0<n && n<=16 then rels.(n-1) else Rel (n, None)
let mkRelA n ans = Rel (n, ans)
(* Construct a type *)
let mkSProp = Sort Sorts.sprop
let mkProp = Sort Sorts.prop
let mkSet = Sort Sorts.set
let mkType u = Sort (Sorts.sort_of_univ u)
let mkSort = function
| Sorts.SProp -> mkSProp
| Sorts.Prop -> mkProp (* Easy sharing *)
| Sorts.Set -> mkSet
| Sorts.Type _ as s -> Sort s
(* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
(* (that means t2 is declared as the type of t1) *)
let mkCast (t1,k2,t2) =
match t1 with
| Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2)
| _ -> Cast (t1,k2,t2)
(* Constructs the product (x:t1)t2 *)
let mkProd (x,t1,t2) = Prod (x,t1,t2)
(* Constructs the abstraction [x:t1]t2 *)
let mkLambda (x,t1,t2) = Lambda (x,t1,t2)
(* Constructs [x=c_1:t]c_2 *)
let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2)
(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
(* We ensure applicative terms have at least one argument and the
function is not itself an applicative term *)
let mkApp (f, a) =
if Int.equal (Array.length a) 0 then f else
match f with
| App (g, cl) -> App (g, Array.append cl a)
| _ -> App (f, a)
let map_puniverses f (x,u) = (f x, u)
let in_punivs a = (a, Univ.Instance.empty)
(* Constructs a constant *)
let mkConst c = Const ((in_punivs c), None)
let mkConstU c = Const (c, None)
let mkConstUA c ans = Const (c, ans)
(* Constructs an applied projection *)
let mkProj (p,c) = Proj (p,c)
(* Constructs an existential variable *)
let mkEvar e = Evar e
(* Constructs the ith (co)inductive type of the block named kn *)
let mkInd m = Ind ((in_punivs m), Empty)
let mkIndU m = Ind (m, Empty)
let mkIndUS m stg = Ind (m, stg)
(* Constructs the jth constructor of the ith (co)inductive type of the
block named kn. *)
let mkConstruct c = Construct (in_punivs c)
let mkConstructU c = Construct c
let mkConstructUi ((ind,u),i) = Construct ((ind,i),u)
(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
let mkCase (ci, p, c, ac) = Case (ci, p, c, ac)
(* If recindxs = [|i1,...in|]
funnames = [|f1,...fn|]
typarray = [|t1,...tn|]
bodies = [|b1,...bn|]
then
mkFix ((recindxs,i),(funnames,typarray,bodies))
constructs the ith function of the block
Fixpoint f1 [ctx1] : t1 := b1
with f2 [ctx2] : t2 := b2
...
with fn [ctxn] : tn := bn.
where the length of the jth context is ij.
*)
let mkFix fix = Fix fix
let mkFixOpt ((vn, i), rec_decl) =
mkFix ((Array.map (fun i -> Some i) vn, i), rec_decl)
(* If funnames = [|f1,...fn|]
typarray = [|t1,...tn|]
bodies = [|b1,...bn|]
then
mkCoFix (i,(funnames,typsarray,bodies))
constructs the ith function of the block
CoFixpoint f1 : t1 := b1
with f2 : t2 := b2
...
with fn : tn := bn.
*)
let mkCoFix cofix= CoFix cofix
(* Constructs an existential variable named "?n" *)
let mkMeta n = Meta n
(* Constructs a Variable named id *)
let mkVar id = Var id
let mkRef (gr,u) = let open GlobRef in match gr with
| ConstRef c -> mkConstU (c,u)
| IndRef ind -> mkIndU (ind,u)
| ConstructRef c -> mkConstructU (c,u)
| VarRef x -> mkVar x
(* Constructs a primitive integer *)
let mkInt i = Int i
(************************************************************************)
(* kind_of_term = constructions as seen by the user *)
(************************************************************************)
(* User view of [constr]. For [App], it is ensured there is at
least one argument and the function is not itself an applicative
term *)
let kind c = c
let rec kind_nocast_gen kind c =
match kind c with
| Cast (c, _, _) -> kind_nocast_gen kind c
| App (h, outer) as k ->
(match kind_nocast_gen kind h with
| App (h, inner) -> App (h, Array.append inner outer)
| _ -> k)
| k -> k
let kind_nocast c = kind_nocast_gen kind c
(* The other way around. We treat specifically smart constructors *)
let of_kind = function
| App (f, a) -> mkApp (f, a)
| Cast (c, knd, t) -> mkCast (c, knd, t)
| k -> k
(**********************************************************************)
(* Non primitive term destructors *)
(**********************************************************************)
(* Destructor operations : partial functions
Raise [DestKO] if the const has not the expected form *)
exception DestKO
let isMeta c = match kind c with Meta _ -> true | _ -> false
(* Destructs a type *)
let isSort c = match kind c with
| Sort _ -> true
| _ -> false
let rec isprop c = match kind c with
| Sort (Sorts.Prop | Sorts.Set) -> true
| Cast (c,_,_) -> isprop c
| _ -> false
let rec is_Prop c = match kind c with
| Sort Sorts.Prop -> true
| Cast (c,_,_) -> is_Prop c
| _ -> false
let rec is_Set c = match kind c with
| Sort Sorts.Set -> true
| Cast (c,_,_) -> is_Set c
| _ -> false
let rec is_Type c = match kind c with
| Sort (Sorts.Type _) -> true
| Cast (c,_,_) -> is_Type c
| _ -> false
let is_small = Sorts.is_small
let iskind c = isprop c || is_Type c
(* Tests if an evar *)
let isEvar c = match kind c with Evar _ -> true | _ -> false
let isEvar_or_Meta c = match kind c with
| Evar _ | Meta _ -> true
| _ -> false
let isCast c = match kind c with Cast _ -> true | _ -> false
(* Tests if a de Bruijn index *)
let isRel c = match kind c with Rel _ -> true | _ -> false
let isRelN n c =
match kind c with Rel (n', _) -> Int.equal n n' | _ -> false
(* Tests if a variable *)
let isVar c = match kind c with Var _ -> true | _ -> false
let isVarId id c = match kind c with Var id' -> Id.equal id id' | _ -> false
(* Tests if an inductive *)
let isInd c = match kind c with Ind _ -> true | _ -> false
let isProd c = match kind c with | Prod _ -> true | _ -> false
let isLambda c = match kind c with | Lambda _ -> true | _ -> false
let isLetIn c = match kind c with LetIn _ -> true | _ -> false
let isApp c = match kind c with App _ -> true | _ -> false
let isConst c = match kind c with Const _ -> true | _ -> false
let isConstruct c = match kind c with Construct _ -> true | _ -> false
let isCase c = match kind c with Case _ -> true | _ -> false
let isProj c = match kind c with Proj _ -> true | _ -> false
let isFix c = match kind c with Fix _ -> true | _ -> false
let isCoFix c = match kind c with CoFix _ -> true | _ -> false
(* Destructs a de Bruijn index *)
let destRel c = match kind c with
| Rel (n, _) -> n
| _ -> raise DestKO
(* Destructs an existential variable *)
let destMeta c = match kind c with
| Meta n -> n
| _ -> raise DestKO
(* Destructs a variable *)
let destVar c = match kind c with
| Var id -> id
| _ -> raise DestKO
let destSort c = match kind c with
| Sort s -> s
| _ -> raise DestKO
(* Destructs a casted term *)
let destCast c = match kind c with
| Cast (t1,k,t2) -> (t1,k,t2)
| _ -> raise DestKO
(* Destructs the product (x:t1)t2 *)
let destProd c = match kind c with
| Prod (x,t1,t2) -> (x,t1,t2)
| _ -> raise DestKO
(* Destructs the abstraction [x:t1]t2 *)
let destLambda c = match kind c with
| Lambda (x,t1,t2) -> (x,t1,t2)
| _ -> raise DestKO
(* Destructs the let [x:=b:t1]t2 *)
let destLetIn c = match kind c with
| LetIn (x,b,t1,t2) -> (x,b,t1,t2)
| _ -> raise DestKO
(* Destructs an application *)
let destApp c = match kind c with
| App (f,a) -> (f, a)
| _ -> raise DestKO
(* Destructs a constant *)
let destConst c = match kind c with
| Const (kn, _) -> kn
| _ -> raise DestKO
(* Destructs an existential variable *)
let destEvar c = match kind c with
| Evar (_kn, _a as r) -> r
| _ -> raise DestKO
(* Destructs a (co)inductive type named kn *)
let destInd c = match kind c with
| Ind ((_kn, _a as r), _) -> r
| _ -> raise DestKO
(* Destructs a constructor *)
let destConstruct c = match kind c with
| Construct (_kn, _a as r) -> r
| _ -> raise DestKO
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
let destCase c = match kind c with
| Case (ci,p,c,v) -> (ci,p,c,v)
| _ -> raise DestKO
let destProj c = match kind c with
| Proj (p, c) -> (p, c)
| _ -> raise DestKO
let destFix c = match kind c with
| Fix fix -> fix
| _ -> raise DestKO
let destCoFix c = match kind c with
| CoFix cofix -> cofix
| _ -> raise DestKO
let destRef c = let open GlobRef in match kind c with
| Var x -> VarRef x, Univ.Instance.empty
| Const ((c,u), _) -> ConstRef c, u
| Ind ((ind,u), _) -> IndRef ind, u
| Construct (c,u) -> ConstructRef c, u
| _ -> raise DestKO
(******************************************************************)
(* Flattening and unflattening of embedded applications and casts *)
(******************************************************************)
let decompose_app c =
match kind c with
| App (f,cl) -> (f, Array.to_list cl)
| _ -> (c,[])
let decompose_appvect c =
match kind c with
| App (f,cl) -> (f, cl)
| _ -> (c,[||])
(****************************************************************************)
(* Functions to recur through subterms *)
(****************************************************************************)
(* [fold f acc c] folds [f] on the immediate subterms of [c]
starting from [acc] and proceeding from left to right according to
the usual representation of the constructions; it is not recursive *)
let fold f acc c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> acc
| Cast (c,_,t) -> f (f acc c) t
| Prod (_,t,c) -> f (f acc t) c
| Lambda (_,t,c) -> f (f acc t) c
| LetIn (_,b,t,c) -> f (f (f acc b) t) c
| App (c,l) -> Array.fold_left f (f acc c) l
| Proj (_p,c) -> f acc c
| Evar (_,l) -> Array.fold_left f acc l
| Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
| Fix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
| CoFix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
(* [iter f c] iters [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
let iter f c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> ()
| Cast (c,_,t) -> f c; f t
| Prod (_,t,c) -> f t; f c
| Lambda (_,t,c) -> f t; f c
| LetIn (_,b,t,c) -> f b; f t; f c
| App (c,l) -> f c; Array.iter f l
| Proj (_p,c) -> f c
| Evar (_,l) -> Array.iter f l
| Case (_,p,c,bl) -> f p; f c; Array.iter f bl
| Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
| CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
(* [iter_with_binders g f n c] iters [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive and the order with which
subterms are processed is not specified *)
let iter_with_binders g f n c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> ()
| Cast (c,_,t) -> f n c; f n t
| Prod (_,t,c) -> f n t; f (g n) c
| Lambda (_,t,c) -> f n t; f (g n) c
| LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
| App (c,l) -> f n c; Array.Fun1.iter f n l
| Evar (_,l) -> Array.Fun1.iter f n l
| Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (_p,c) -> f n c
| Fix (_,(_,tl,bl)) ->
Array.Fun1.iter f n tl;
Array.Fun1.iter f (iterate g (Array.length tl) n) bl
| CoFix (_,(_,tl,bl)) ->
Array.Fun1.iter f n tl;
Array.Fun1.iter f (iterate g (Array.length tl) n) bl
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
right according to the usual representation of the constructions as
[fold_constr] but it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive *)
let fold_constr_with_binders g f n acc c =
match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> acc
| Cast (c,_, t) -> f n (f n acc c) t
| Prod (_na,t,c) -> f (g n) (f n acc t) c
| Lambda (_na,t,c) -> f (g n) (f n acc t) c
| LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (_p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(_,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
| CoFix (_,(_,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
(* [map f c] maps [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
let rec map_under_context f n d =
if n = 0 then f d else
match kind d with
| LetIn (na,b,t,c) ->
let b' = f b in
let t' = f t in
let c' = map_under_context f (n-1) c in
if b' == b && t' == t && c' == c then d
else mkLetIn (na,b',t',c')
| Lambda (na,t,b) ->
let t' = f t in
let b' = map_under_context f (n-1) b in
if t' == t && b' == b then d
else mkLambda (na,t',b')
| _ -> CErrors.anomaly (Pp.str "Ill-formed context")
let map_branches f ci bl =
let nl = Array.map List.length ci.ci_pp_info.cstr_tags in
let bl' = Array.map2 (map_under_context f) nl bl in
if Array.for_all2 (==) bl' bl then bl else bl'
let map_return_predicate f ci p =
map_under_context f (List.length ci.ci_pp_info.ind_tags) p
let rec map_under_context_with_binders g f l n d =
if n = 0 then f l d else
match kind d with
| LetIn (na,b,t,c) ->
let b' = f l b in
let t' = f l t in
let c' = map_under_context_with_binders g f (g l) (n-1) c in
if b' == b && t' == t && c' == c then d
else mkLetIn (na,b',t',c')
| Lambda (na,t,b) ->
let t' = f l t in
let b' = map_under_context_with_binders g f (g l) (n-1) b in
if t' == t && b' == b then d
else mkLambda (na,t',b')
| _ -> CErrors.anomaly (Pp.str "Ill-formed context")
let map_branches_with_binders g f l ci bl =
let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in
if Array.for_all2 (==) bl' bl then bl else bl'
let map_return_predicate_with_binders g f l ci p =
map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p
let rec map_under_context_with_full_binders g f l n d =
if n = 0 then f l d else
match kind d with
| LetIn (na,b,t,c) ->
let b' = f l b in
let t' = f l t in
let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
if b' == b && t' == t && c' == c then d
else mkLetIn (na,b',t',c')
| Lambda (na,t,b) ->
let t' = f l t in
let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
if t' == t && b' == b then d
else mkLambda (na,t',b')
| _ -> CErrors.anomaly (Pp.str "Ill-formed context")
let map_branches_with_full_binders g f l ci bl =
let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in
if Array.for_all2 (==) bl' bl then bl else bl'
let map_return_predicate_with_full_binders g f l ci p =
map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p
let map_gen userview f c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> c
| Cast (b,k,t) ->
let b' = f b in
let t' = f t in
if b'==b && t' == t then c
else mkCast (b', k, t')
| Prod (na,t,b) ->
let b' = f b in
let t' = f t in
if b'==b && t' == t then c
else mkProd (na, t', b')
| Lambda (na,t,b) ->
let b' = f b in
let t' = f t in
if b'==b && t' == t then c
else mkLambda (na, t', b')
| LetIn (na,b,t,k) ->
let b' = f b in
let t' = f t in
let k' = f k in
if b'==b && t' == t && k'==k then c
else mkLetIn (na, b', t', k')
| App (b,l) ->
let b' = f b in
let l' = Array.Smart.map f l in
if b'==b && l'==l then c
else mkApp (b', l')
| Proj (p,t) ->
let t' = f t in
if t' == t then c
else mkProj (p, t')
| Evar (e,l) ->
let l' = Array.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
| Case (ci,p,b,bl) when userview ->
let b' = f b in
let p' = map_return_predicate f ci p in
let bl' = map_branches f ci bl in
if b'==b && p'==p && bl'==bl then c
else mkCase (ci, p', b', bl')
| Case (ci,p,b,bl) ->
let b' = f b in
let p' = f p in
let bl' = Array.Smart.map f bl in
if b'==b && p'==p && bl'==bl then c
else mkCase (ci, p', b', bl')
| Fix (ln,(lna,tl,bl)) ->
let tl' = Array.Smart.map f tl in
let bl' = Array.Smart.map f bl in
if tl'==tl && bl'==bl then c
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
let tl' = Array.Smart.map f tl in
let bl' = Array.Smart.map f bl in
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
let map_user_view = map_gen true
let map = map_gen false
(* Like {!map} but with an accumulator. *)
let fold_map f accu c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> accu, c
| Cast (b,k,t) ->
let accu, b' = f accu b in
let accu, t' = f accu t in
if b'==b && t' == t then accu, c
else accu, mkCast (b', k, t')
| Prod (na,t,b) ->
let accu, b' = f accu b in
let accu, t' = f accu t in
if b'==b && t' == t then accu, c
else accu, mkProd (na, t', b')
| Lambda (na,t,b) ->
let accu, b' = f accu b in
let accu, t' = f accu t in
if b'==b && t' == t then accu, c
else accu, mkLambda (na, t', b')
| LetIn (na,b,t,k) ->
let accu, b' = f accu b in
let accu, t' = f accu t in
let accu, k' = f accu k in
if b'==b && t' == t && k'==k then accu, c
else accu, mkLetIn (na, b', t', k')
| App (b,l) ->
let accu, b' = f accu b in
let accu, l' = Array.Smart.fold_left_map f accu l in
if b'==b && l'==l then accu, c
else accu, mkApp (b', l')
| Proj (p,t) ->
let accu, t' = f accu t in
if t' == t then accu, c
else accu, mkProj (p, t')
| Evar (e,l) ->
let accu, l' = Array.Smart.fold_left_map f accu l in
if l'==l then accu, c
else accu, mkEvar (e, l')
| Case (ci,p,b,bl) ->
let accu, b' = f accu b in
let accu, p' = f accu p in
let accu, bl' = Array.Smart.fold_left_map f accu bl in
if b'==b && p'==p && bl'==bl then accu, c
else accu, mkCase (ci, p', b', bl')
| Fix (ln,(lna,tl,bl)) ->
let accu, tl' = Array.Smart.fold_left_map f accu tl in
let accu, bl' = Array.Smart.fold_left_map f accu bl in
if tl'==tl && bl'==bl then accu, c
else accu, mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
let accu, tl' = Array.Smart.fold_left_map f accu tl in
let accu, bl' = Array.Smart.fold_left_map f accu bl in
if tl'==tl && bl'==bl then accu, c
else accu, mkCoFix (ln,(lna,tl',bl'))
(* [map_with_binders g f n c] maps [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive and the order with which
subterms are processed is not specified *)
let map_with_binders g f l c0 = match kind c0 with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _) -> c0
| Cast (c, k, t) ->
let c' = f l c in
let t' = f l t in
if c' == c && t' == t then c0
else mkCast (c', k, t')
| Prod (na, t, c) ->
let t' = f l t in
let c' = f (g l) c in
if t' == t && c' == c then c0
else mkProd (na, t', c')
| Lambda (na, t, c) ->
let t' = f l t in
let c' = f (g l) c in
if t' == t && c' == c then c0
else mkLambda (na, t', c')
| LetIn (na, b, t, c) ->
let b' = f l b in
let t' = f l t in
let c' = f (g l) c in
if b' == b && t' == t && c' == c then c0
else mkLetIn (na, b', t', c')
| App (c, al) ->
let c' = f l c in
let al' = Array.Fun1.Smart.map f l al in
if c' == c && al' == al then c0
else mkApp (c', al')
| Proj (p, t) ->
let t' = f l t in
if t' == t then c0
else mkProj (p, t')
| Evar (e, al) ->
let al' = Array.Fun1.Smart.map f l al in
if al' == al then c0
else mkEvar (e, al')
| Case (ci, p, c, bl) ->
let p' = f l p in
let c' = f l c in
let bl' = Array.Fun1.Smart.map f l bl in
if p' == p && c' == c && bl' == bl then c0
else mkCase (ci, p', c', bl')
| Fix (ln, (lna, tl, bl)) ->
let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
let bl' = Array.Fun1.Smart.map f l' bl in
if tl' == tl && bl' == bl then c0
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
(*********************)
(* Stage annotations *)
(*********************)
(** fold-type functions on stage annotations of constrs *)
let rec count_annots cstr =
match cstr with
| Ind _ -> 1
| Rel (_, la) -> List.length (Option.default [] la)
| Cast (c, _, _)
| Lambda (_, _, c) ->
count_annots c
| LetIn (_, b, _, c) ->
count_annots b + count_annots c
| Const (_, la) -> List.length (Option.default [] la)
| Case (_, _, c, lf) ->
Array.fold_left (fun count c -> count + count_annots c) (count_annots c) lf
| Fix (_, (_, _, bl))
| CoFix (_, (_, _, bl)) ->
Array.fold_left (fun count c -> count + count_annots c) 0 bl
| _ ->
fold (fun count c -> count + count_annots c) 0 cstr
let rec collect_annots c =
match c with
| Ind (_, Stage (StageVar (na, _))) -> SVars.add na SVars.empty
| _ -> fold (fun vars c -> SVars.union vars (collect_annots c)) SVars.empty c
let rec any_annot f c =
match c with
| Ind (_, a) -> f a
| _ -> fold (fun acc c -> acc || any_annot f c) false c
(** map-type functions on stage annotations of constrs *)
let rec map_annots f g cstr =
match cstr with
| Ind (iu, a) -> f iu a cstr
| Rel _ -> g cstr
| Cast (c, k, t) ->
let c' = map_annots f g c in
if c == c' then cstr else
mkCast (c', k, t)
| Lambda (n, t, c) ->
let c' = map_annots f g c in
if c == c' then cstr else
mkLambda (n, t, c')
| LetIn (n, b, t, c) ->
let b' = map_annots f g b in
let c' = map_annots f g c in
if b == b' && c == c' then cstr else
mkLetIn (n, b', t, c')
| Const _ -> g cstr
| Case (ci, p, c, lf) ->
let c' = map_annots f g c in
let lf' = Array.Smart.map (map_annots f g) lf in
if c == c' && lf == lf' then cstr else
mkCase (ci, p, c', lf')
| Fix (ln, (nl, tl, bl)) ->
let bl' = Array.Smart.map (map_annots f g) bl in
if bl == bl' then cstr else
mkFix (ln, (nl, tl, bl'))
| CoFix (ln, (nl, tl, bl)) ->
let bl' = Array.Smart.map (map_annots f g) bl in
if bl == bl' then cstr else
mkCoFix (ln, (nl, tl, bl'))
| _ -> map (map_annots f g) cstr
let make_annots_list annot la =
List.make (List.length la) annot
let map_annots_list g cstr =
match cstr with
| Rel (n, Some la) ->
let la = g la in
mkRelA n (Some la)
| Const (c, Some la) ->
let la = g la in
mkConstUA c (Some la)
| _ -> cstr
let erase =
let f iu a c =
match a with
| Empty -> c
| _ -> mkIndUS iu Empty in
map_annots f (map_annots_list (make_annots_list Empty))
let erase_infty =
let f iu a c =
match a with
| Stage Infty -> c
| _ -> mkIndUS iu infty in
map_annots f (map_annots_list (make_annots_list infty))
let erase_glob vars =
let f iu a c =
match a with
| Stage (StageVar (na, _))
when mem na vars ->
mkIndUS iu Glob
| Stage Infty -> c
| _ -> mkIndUS iu infty in
map_annots f (map_annots_list (make_annots_list Empty))
let erase_star vars =
let f iu a c =
match a with
| Stage (StageVar (na, _))
when SVars.mem na vars ->
mkIndUS iu Star
| Empty -> c
| _ -> mkIndUS iu Empty in
map_annots f (map_annots_list (make_annots_list Empty))
let annotate ind s =
let f (((i, _), _) as iu) _ c =
if MutInd.equal ind i then
mkIndUS iu s
else c in
map_annots f identity
let annotate_fresh annots =
let annots_ref = ref annots in
let f iu _ _ =
let annots = !annots_ref in
annots_ref := List.tl annots;
mkIndUS iu (List.hd annots) in
let g la =
let annots = !annots_ref in
let la, annots = List.chop (List.length la) annots in
annots_ref := annots; la in
map_annots f (map_annots_list g)
let annotate_glob s =
let f iu a c =
match a with
| Glob -> mkIndUS iu s
| _ -> c in
map_annots f identity
let annotate_succ vars =
let f iu a c =
match a with
| Stage (StageVar (na, _))
when mem na vars ->
mkIndUS iu (hat a)
| _ -> c in
map_annots f identity
(*********************)
(* Lifting *)
(*********************)
(* The generic lifting function *)
let rec exliftn el c =
let open Esubst in
match kind c with
| Rel (i, ans) -> mkRelA (reloc_rel i el) ans
| _ -> map_with_binders el_lift exliftn el c
(* Lifting the binding depth across k bindings *)
let liftn n k c =
let open Esubst in
match el_liftn (pred k) (el_shft n el_id) with
| ELID -> c
| el -> exliftn el c
let lift n = liftn n 1
let fold_with_full_binders g f n acc c =
let open Context.Rel.Declaration in
match kind c with
| Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ -> acc
| Cast (c,_, t) -> f n (f n acc c) t
| Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
| Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
| LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (_,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(lna,tl,bl)) ->
let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
| CoFix (_,(lna,tl,bl)) ->
let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
type 'univs instance_compare_fn = GlobRef.t -> int ->
'univs -> 'univs -> bool