package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file glob_term_to_relation.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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
open Printer
open Pp
open Names
open Constr
open Context
open Vars
open Glob_term
open Glob_ops
open Indfun_common
open CErrors
open Util
open Glob_termops
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

let observe strm = if do_observe () then Feedback.msg_debug strm else ()

(*let observennl strm =
  if do_observe ()
  then Pp.msg strm
  else ()*)

type binder_type = Lambda of Name.t | Prod of Name.t | LetIn of Name.t
type glob_context = (binder_type * glob_constr) list

let rec solve_trivial_holes pat_as_term e =
  match (DAst.get pat_as_term, DAst.get e) with
  | GHole _, _ -> e
  | GApp (fp, argsp), GApp (fe, argse) when glob_constr_eq fp fe ->
    DAst.make
      (GApp
         (solve_trivial_holes fp fe, List.map2 solve_trivial_holes argsp argse))
  | _, _ -> pat_as_term

(*
   compose_glob_context [(bt_1,n_1,t_1);......] rt returns
   b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
   binders corresponding to the bt_i's
*)
let compose_glob_context =
  let compose_binder (bt, t) acc =
    match bt with
    | Lambda n -> mkGLambda (n, t, acc)
    | Prod n -> mkGProd (n, t, acc)
    | LetIn n -> mkGLetIn (n, t, None, acc)
  in
  List.fold_right compose_binder

(*
   The main part deals with building a list of globalized constructor expressions
   from the rhs of a fixpoint equation.
*)

type 'a build_entry_pre_return =
  { context : glob_context
  ; (* the binding context of the result *)
    value : 'a (* The value *) }

type 'a build_entry_return =
  {result : 'a build_entry_pre_return list; to_avoid : Id.t list}

(*
  [combine_results combine_fun res1 res2] combine two results [res1] and [res2]
  w.r.t. [combine_fun].

  Informally, both [res1] and [res2] are lists of "constructors"  [res1_1;...]
  and [res2_1,....] and we need to produce
  [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
*)

let combine_results
    (combine_fun :
         'a build_entry_pre_return
      -> 'b build_entry_pre_return
      -> 'c build_entry_pre_return) (res1 : 'a build_entry_return)
    (res2 : 'b build_entry_return) : 'c build_entry_return =
  let pre_result =
    List.map
      (fun res1 ->
        (* for each result in arg_res *)
        List.map (* we add it in each args_res *)
          (fun res2 -> combine_fun res1 res2)
          res2.result)
      res1.result
  in
  (* and then we flatten the map *)
  { result = List.concat pre_result
  ; to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid }

(*
   The combination function for an argument with a list of argument
*)

let combine_args arg args =
  { context = arg.context @ args.context
  ; (* Note that the binding context of [arg] MUST be placed before the one of
       [args] in order to preserve possible type dependencies
    *)
    value = arg.value :: args.value }

let ids_of_binder = function
  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty
  | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id

let rec change_vars_in_binder mapping = function
  | [] -> []
  | (bt, t) :: l ->
    let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
    (bt, change_vars mapping t)
    ::
    ( if Id.Map.is_empty new_mapping then l
    else change_vars_in_binder new_mapping l )

let rec replace_var_by_term_in_binder x_id term = function
  | [] -> []
  | (bt, t) :: l ->
    (bt, replace_var_by_term x_id term t)
    ::
    ( if Id.Set.mem x_id (ids_of_binder bt) then l
    else replace_var_by_term_in_binder x_id term l )

let add_bt_names bt = Id.Set.union (ids_of_binder bt)

let apply_args ctxt body args =
  let need_convert_id avoid id =
    List.exists (is_free_in id) args || Id.Set.mem id avoid
  in
  let need_convert avoid bt =
    Id.Set.exists (need_convert_id avoid) (ids_of_binder bt)
  in
  let next_name_away (na : Name.t) (mapping : Id.t Id.Map.t) (avoid : Id.Set.t)
      =
    match na with
    | Name id when Id.Set.mem id avoid ->
      let new_id = Namegen.next_ident_away id avoid in
      (Name new_id, Id.Map.add id new_id mapping, Id.Set.add new_id avoid)
    | _ -> (na, mapping, avoid)
  in
  let next_bt_away bt (avoid : Id.Set.t) =
    match bt with
    | LetIn na ->
      let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
      (LetIn new_na, mapping, new_avoid)
    | Prod na ->
      let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
      (Prod new_na, mapping, new_avoid)
    | Lambda na ->
      let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
      (Lambda new_na, mapping, new_avoid)
  in
  let rec do_apply avoid ctxt body args =
    match (ctxt, args) with
    | _, [] ->
      (* No more args *)
      (ctxt, body)
    | [], _ ->
      (* no more fun *)
      let f, args' = glob_decompose_app body in
      (ctxt, mkGApp (f, args' @ args))
    | (Lambda Anonymous, t) :: ctxt', arg :: args' ->
      do_apply avoid ctxt' body args'
    | (Lambda (Name id), t) :: ctxt', arg :: args' ->
      let new_avoid, new_ctxt', new_body, new_id =
        if need_convert_id avoid id then
          let new_avoid = Id.Set.add id avoid in
          let new_id = Namegen.next_ident_away id new_avoid in
          let new_avoid' = Id.Set.add new_id new_avoid in
          let mapping = Id.Map.add id new_id Id.Map.empty in
          let new_ctxt' = change_vars_in_binder mapping ctxt' in
          let new_body = change_vars mapping body in
          (new_avoid', new_ctxt', new_body, new_id)
        else (Id.Set.add id avoid, ctxt', body, id)
      in
      let new_body = replace_var_by_term new_id arg new_body in
      let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
      do_apply avoid new_ctxt' new_body args'
    | (bt, t) :: ctxt', _ ->
      let new_avoid, new_ctxt', new_body, new_bt =
        let new_avoid = add_bt_names bt avoid in
        if need_convert avoid bt then
          let new_bt, mapping, new_avoid = next_bt_away bt new_avoid in
          ( new_avoid
          , change_vars_in_binder mapping ctxt'
          , change_vars mapping body
          , new_bt )
        else (new_avoid, ctxt', body, bt)
      in
      let new_ctxt', new_body = do_apply new_avoid new_ctxt' new_body args in
      ((new_bt, t) :: new_ctxt', new_body)
  in
  do_apply Id.Set.empty ctxt body args

let combine_app f args =
  let new_ctxt, new_value = apply_args f.context f.value args.value in
  { (* Note that the binding context of [args] MUST be placed before the one of
       the applied value in order to preserve possible type dependencies
    *)
    context = args.context @ new_ctxt
  ; value = new_value }

let combine_lam n t b =
  { context = []
  ; value =
      mkGLambda
        ( n
        , compose_glob_context t.context t.value
        , compose_glob_context b.context b.value ) }

let combine_prod2 n t b =
  { context = []
  ; value =
      mkGProd
        ( n
        , compose_glob_context t.context t.value
        , compose_glob_context b.context b.value ) }

let combine_prod n t b =
  {context = t.context @ ((Prod n, t.value) :: b.context); value = b.value}

let combine_letin n t b =
  {context = t.context @ ((LetIn n, t.value) :: b.context); value = b.value}

let mk_result ctxt value avoid =
  {result = [{context = ctxt; value}]; to_avoid = avoid}

(*************************************************
  Some functions to deal with overlapping patterns
**************************************************)

let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type")
let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type")

(*
  [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
  (the list of expressions on which we will do the matching)
 *)
let make_discr_match_el = List.map (fun e -> (e, (Anonymous, None)))

(*
  [make_discr_match_brl i \[pat_1,...,pat_n\]]  constructs a discrimination pattern matching on the ith expression.
  that is.
  match ?????? with \\
  | pat_1 => False  \\
  | pat_{i-1} => False \\
  | pat_i => True \\
  | pat_{i+1} => False \\
  \vdots
  | pat_n => False
  end
*)
let make_discr_match_brl i =
  List.map_i
    (fun j {CAst.v = idl, patl, _} ->
      CAst.make
      @@
      if Int.equal j i then (idl, patl, mkGRef (Lazy.force coq_True_ref))
      else (idl, patl, mkGRef (Lazy.force coq_False_ref)))
    0

(*
   [make_discr_match brl el i] generates an hypothesis such that it reduce to true iff
   brl_{i} is the first branch matched by [el]

   Used when we want to simulate the coq pattern matching algorithm
*)
let make_discr_match brl el i =
  mkGCases (None, make_discr_match_el el, make_discr_match_brl i brl)

(**********************************************************************)
(*  functions used to build case expression from lettuple and if ones *)
(**********************************************************************)

(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
let build_constructors_of_type ind' argl =
  let mib, ind = Inductive.lookup_mind_specif (Global.env ()) ind' in
  let npar = mib.Declarations.mind_nparams in
  Array.mapi
    (fun i _ ->
      let construct = (ind', i + 1) in
      let constructref = GlobRef.ConstructRef construct in
      let _implicit_positions_of_cst =
        Impargs.implicits_of_global constructref
      in
      let cst_narg =
        Inductiveops.constructor_nallargs (Global.env ()) construct
      in
      let argl =
        if List.is_empty argl then List.make cst_narg (mkGHole ())
        else List.make npar (mkGHole ()) @ argl
      in
      let pat_as_term =
        mkGApp (mkGRef (GlobRef.ConstructRef (ind', i + 1)), argl)
      in
      cases_pattern_of_glob_constr (Global.env ()) Anonymous pat_as_term)
    ind.Declarations.mind_consnames

(******************)
(* Main functions *)
(******************)

let raw_push_named (na, raw_value, raw_typ) env =
  match na with
  | Anonymous -> env
  | Name id -> (
    let typ, _ =
      Pretyping.understand env (Evd.from_env env)
        ~expected_type:Pretyping.IsType raw_typ
    in
    let na = make_annot id Sorts.Relevant in
    (* TODO relevance *)
    match raw_value with
    | None -> EConstr.push_named (NamedDecl.LocalAssum (na, typ)) env
    | Some value -> EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env
    )

let add_pat_variables sigma pat typ env : Environ.env =
  let rec add_pat_variables env pat typ : Environ.env =
    observe
      (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
    match DAst.get pat with
    | PatVar na ->
      Environ.push_rel
        (RelDecl.LocalAssum (make_annot na Sorts.Relevant, typ))
        env
    | PatCstr (c, patl, na) ->
      let (Inductiveops.IndType (indf, indargs)) =
        try
          Inductiveops.find_rectype env (Evd.from_env env)
            (EConstr.of_constr typ)
        with Not_found -> assert false
      in
      let constructors = Inductiveops.get_constructors env indf in
      let constructor : Inductiveops.constructor_summary =
        List.find
          (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr))
          (Array.to_list constructors)
      in
      let cs_args_types : types list =
        List.map RelDecl.get_type constructor.Inductiveops.cs_args
      in
      List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
  in
  let new_env = add_pat_variables env pat typ in
  let res =
    fst
      (Context.Rel.fold_outside
         (fun decl (env, ctxt) ->
           let open Context.Rel.Declaration in
           match decl with
           | LocalAssum ({binder_name = Anonymous}, _)
            |LocalDef ({binder_name = Anonymous}, _, _) ->
             assert false
           | LocalAssum (({binder_name = Name id} as na), t) ->
             let na = {na with binder_name = id} in
             let new_t = substl ctxt t in
             observe
               ( str "for variable " ++ Ppconstr.pr_id id ++ fnl ()
               ++ str "old type := "
               ++ Printer.pr_lconstr_env env sigma t
               ++ fnl () ++ str "new type := "
               ++ Printer.pr_lconstr_env env sigma new_t
               ++ fnl () );
             let open Context.Named.Declaration in
             (Environ.push_named (LocalAssum (na, new_t)) env, mkVar id :: ctxt)
           | LocalDef (({binder_name = Name id} as na), v, t) ->
             let na = {na with binder_name = id} in
             let new_t = substl ctxt t in
             let new_v = substl ctxt v in
             observe
               ( str "for variable " ++ Ppconstr.pr_id id ++ fnl ()
               ++ str "old type := "
               ++ Printer.pr_lconstr_env env sigma t
               ++ fnl () ++ str "new type := "
               ++ Printer.pr_lconstr_env env sigma new_t
               ++ fnl () ++ str "old value := "
               ++ Printer.pr_lconstr_env env sigma v
               ++ fnl () ++ str "new value := "
               ++ Printer.pr_lconstr_env env sigma new_v
               ++ fnl () );
             let open Context.Named.Declaration in
             ( Environ.push_named (LocalDef (na, new_v, new_t)) env
             , mkVar id :: ctxt ))
         (Environ.rel_context new_env)
         ~init:(env, []))
  in
  observe
    (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
  res

let rec pattern_to_term_and_type env typ =
  DAst.with_val (function
    | PatVar Anonymous -> assert false
    | PatVar (Name id) -> mkGVar id
    | PatCstr (constr, patternl, _) ->
      let cst_narg = Inductiveops.constructor_nallargs (Global.env ()) constr in
      let (Inductiveops.IndType (indf, indargs)) =
        try
          Inductiveops.find_rectype env (Evd.from_env env)
            (EConstr.of_constr typ)
        with Not_found -> assert false
      in
      let constructors = Inductiveops.get_constructors env indf in
      let constructor =
        List.find
          (fun cs ->
            Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr)
          (Array.to_list constructors)
      in
      let cs_args_types : types list =
        List.map RelDecl.get_type constructor.Inductiveops.cs_args
      in
      let _, cstl = Inductiveops.dest_ind_family indf in
      let csta = Array.of_list cstl in
      let implicit_args =
        Array.to_list
          (Array.init
             (cst_narg - List.length patternl)
             (fun i ->
               Detyping.detype Detyping.Now false Id.Set.empty env
                 (Evd.from_env env)
                 (EConstr.of_constr csta.(i))))
      in
      let patl_as_term =
        List.map2
          (pattern_to_term_and_type env)
          (List.rev cs_args_types) patternl
      in
      mkGApp (mkGRef (GlobRef.ConstructRef constr), implicit_args @ patl_as_term))

(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
   of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
   corresponding graphs.


   The idea to transform a term [t] into a list of constructors [lc] is the following:
   \begin{itemize}
   \item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding
   to [body] and add (bind x. _) to each elements of [lc]
   \item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames)
   then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
   then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn],
   [g c1 ... cn] is an element of [lc]
   \item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then
   compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
   then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
   create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
   \item if the term is a cast just treat its body part
   \item
   if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case
   and concatenate them (informally, each branch of a match produces a new constructor)
   \end{itemize}

   WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed.
   We must wait to have complete all the current calculi to set the recursive calls.
   At this point, each term [f t1 ... tn]  (where f appears in [funnames]) is replaced by
   a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later.
   We in fact not create a constructor list since then end of each constructor has not the expected form
   but only the value of the function
*)

let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x

let rec build_entry_lc env sigma funnames avoid rt :
    glob_constr build_entry_return =
  observe (str " Entering : " ++ pr_glob_constr_env env rt);
  let open CAst in
  match DAst.get rt with
  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _
   |GFloat _ ->
    (* do nothing (except changing type of course) *)
    mk_result [] rt avoid
  | GApp (_, _) -> (
    let f, args = glob_decompose_app rt in
    let args_res : glob_constr list build_entry_return =
      List.fold_right
        (* create the arguments lists of constructors and combine them *)
          (fun arg ctxt_argsl ->
          let arg_res =
            build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg
          in
          combine_results combine_args arg_res ctxt_argsl)
        args (mk_result [] [] avoid)
    in
    match DAst.get f with
    | GLambda _ ->
      let rec aux t l =
        match l with
        | [] -> t
        | u :: l -> (
          DAst.make
          @@
          match DAst.get t with
          | GLambda (na, _, nat, b) -> GLetIn (na, u, None, aux b l)
          | _ -> GApp (t, l) )
      in
      build_entry_lc env sigma funnames avoid (aux f args)
    | GVar id when Id.Set.mem id funnames ->
      (* if we have [f t1 ... tn] with [f]$\in$[fnames]
         then we create a fresh variable [res],
         add [res] and its "value" (i.e. [res v1 ... vn]) to each
         pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
         a pseudo value "v1 ... vn".
         The "value" of this branch is then simply [res]
      *)
      (* XXX here and other [understand] calls drop the ctx *)
      let rt_as_constr, ctx = Pretyping.understand env (Evd.from_env env) rt in
      let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
      let res_raw_type =
        Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env)
          rt_typ
      in
      let res = fresh_id args_res.to_avoid "_res" in
      let new_avoid = res :: args_res.to_avoid in
      let res_rt = mkGVar res in
      let new_result =
        List.map
          (fun arg_res ->
            let new_hyps =
              [ (Prod (Name res), res_raw_type)
              ; (Prod Anonymous, mkGApp (res_rt, mkGVar id :: arg_res.value)) ]
            in
            {context = arg_res.context @ new_hyps; value = res_rt})
          args_res.result
      in
      {result = new_result; to_avoid = new_avoid}
    | GVar _ | GEvar _ | GPatVar _ | GHole _ | GSort _ | GRef _ ->
      (* if have [g t1 ... tn] with [g] not appearing in [funnames]
         then
         foreach [ctxt,v1 ... vn] in [args_res] we return
         [ctxt, g v1 .... vn]
      *)
      { args_res with
        result =
          List.map
            (fun args_res -> {args_res with value = mkGApp (f, args_res.value)})
            args_res.result }
    | GApp _ ->
      assert false (* we have collected all the app in [glob_decompose_app] *)
    | GLetIn (n, v, t, b) ->
      (* if we have [(let x := v in b) t1 ... tn] ,
         we discard our work and compute the list of constructor for
         [let x = v in (b t1 ... tn)] up to alpha conversion
      *)
      let new_n, new_b, new_avoid =
        match n with
        | Name id when List.exists (is_free_in id) args ->
          (* need to alpha-convert the name *)
          let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
          let new_avoid = id :: avoid in
          let new_b = replace_var_by_term id (DAst.make @@ GVar id) b in
          (Name new_id, new_b, new_avoid)
        | _ -> (n, b, avoid)
      in
      build_entry_lc env sigma funnames avoid
        (mkGLetIn (new_n, v, t, mkGApp (new_b, args)))
    | GCases _ | GIf _ | GLetTuple _ | GProj _ ->
      (* we have [(match e1, ...., en with ..... end) t1 tn]
         we first compute the result from the case and
         then combine each of them with each of args one
      *)
      let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
      combine_results combine_app f_res args_res
    | GCast (b, _, _) ->
      (* for an applied cast we just trash the cast part
         and restart the work.

         WARNING: We need to restart since [b] itself should be an application term
      *)
      build_entry_lc env sigma funnames avoid (mkGApp (b, args))
    | GRec _ -> user_err Pp.(str "Not handled GRec")
    | GProd _ -> user_err Pp.(str "Cannot apply a type")
    | GInt _ -> user_err Pp.(str "Cannot apply an integer")
    | GFloat _ -> user_err Pp.(str "Cannot apply a float")
    | GArray _ -> user_err Pp.(str "Cannot apply an array")
    (* end of the application treatement *) )
  | GProj (f, params, c) ->
    let args_res : glob_constr list build_entry_return =
      List.fold_right
        (* create the arguments lists of constructors and combine them *)
          (fun arg ctxt_argsl ->
          let arg_res =
            build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg
          in
          combine_results combine_args arg_res ctxt_argsl)
        (params@[c]) (mk_result [] [] avoid) in
      { args_res with
        result =
          List.map
            (fun args_res ->
              let c, params = List.sep_last args_res.value in
              {args_res with value = DAst.make (GProj (f, params, c))})
            args_res.result }
  | GLambda (n, _, t, b) ->
    (* we first compute the list of constructor
       corresponding to the body of the function,
       then the one corresponding to the type
       and combine the two result
    *)
    let t_res = build_entry_lc env sigma funnames avoid t in
    let new_n =
      match n with
      | Name _ -> n
      | Anonymous -> Name (Indfun_common.fresh_id [] "_x")
    in
    let new_env = raw_push_named (new_n, None, t) env in
    let b_res = build_entry_lc new_env sigma funnames avoid b in
    combine_results (combine_lam new_n) t_res b_res
  | GProd (n, _, t, b) ->
    (* we first compute the list of constructor
       corresponding to the body of the function,
       then the one corresponding to the type
       and combine the two result
    *)
    let t_res = build_entry_lc env sigma funnames avoid t in
    let new_env = raw_push_named (n, None, t) env in
    let b_res = build_entry_lc new_env sigma funnames avoid b in
    if List.length t_res.result = 1 && List.length b_res.result = 1 then
      combine_results (combine_prod2 n) t_res b_res
    else combine_results (combine_prod n) t_res b_res
  | GLetIn (n, v, typ, b) ->
    (* we first compute the list of constructor
       corresponding to the body of the function,
       then the one corresponding to the value [t]
       and combine the two result
    *)
    let v =
      match typ with
      | None -> v
      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, DEFAULTcast, t)
    in
    let v_res = build_entry_lc env sigma funnames avoid v in
    let v_as_constr, ctx = Pretyping.understand env (Evd.from_env env) v in
    let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
    let v_r = Sorts.Relevant in
    (* TODO relevance *)
    let new_env =
      match n with
      | Anonymous -> env
      | Name id ->
        EConstr.push_named
          (NamedDecl.LocalDef (make_annot id v_r, v_as_constr, v_type))
          env
    in
    let b_res = build_entry_lc new_env sigma funnames avoid b in
    combine_results (combine_letin n) v_res b_res
  | GCases (_, _, el, brl) ->
    (* we create the discrimination function
       and treat the case itself
    *)
    let make_discr = make_discr_match brl in
    build_entry_lc_from_case env sigma funnames make_discr el brl avoid
  | GIf (b, (na, e_option), lhs, rhs) ->
    let b_as_constr, ctx = Pretyping.understand env (Evd.from_env env) b in
    let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
    let ind, _ =
      try Inductiveops.find_inductive env (Evd.from_env env) b_typ
      with Not_found ->
        user_err
          ( str "Cannot find the inductive associated to "
          ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
          ++ str ". try again with a cast" )
    in
    let case_pats = build_constructors_of_type (fst ind) [] in
    assert (Int.equal (Array.length case_pats) 2);
    let brl =
      List.map_i (fun i x -> CAst.make ([], [case_pats.(i)], x)) 0 [lhs; rhs]
    in
    let match_expr = mkGCases (None, [(b, (Anonymous, None))], brl) in
    (* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
    build_entry_lc env sigma funnames avoid match_expr
  | GLetTuple (nal, _, b, e) ->
    let nal_as_glob_constr =
      List.map (function Name id -> mkGVar id | Anonymous -> mkGHole ()) nal
    in
    let b_as_constr, ctx = Pretyping.understand env (Evd.from_env env) b in
    let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
    let ind, _ =
      try Inductiveops.find_inductive env (Evd.from_env env) b_typ
      with Not_found ->
        user_err
          ( str "Cannot find the inductive associated to "
          ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
          ++ str ". try again with a cast" )
    in
    let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
    assert (Int.equal (Array.length case_pats) 1);
    let br = CAst.make ([], [case_pats.(0)], e) in
    let match_expr = mkGCases (None, [(b, (Anonymous, None))], [br]) in
    build_entry_lc env sigma funnames avoid match_expr
  | GRec _ -> user_err Pp.(str "Not handled GRec")
  | GCast (b, _, _) -> build_entry_lc env sigma funnames avoid b
  | GArray _ -> user_err Pp.(str "Not handled GArray")

and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
    (brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return =
  match el with
  | [] -> assert false (* this case correspond to match <nothing> with .... !*)
  | el ->
    (* this case correspond to
       match el with brl end
       we first compute the list of lists corresponding to [el] and
       combine them .
       Then for each element of the combinations,
       we compute the result we compute one list per branch in [brl] and
       finally we just concatenate those list
    *)
    let case_resl =
      List.fold_right
        (fun (case_arg, _) ctxt_argsl ->
          let arg_res =
            build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg
          in
          combine_results combine_args arg_res ctxt_argsl)
        el (mk_result [] [] avoid)
    in
    let types =
      List.map
        (fun (case_arg, _) ->
          let case_arg_as_constr, ctx =
            Pretyping.understand env (Evd.from_env env) case_arg
          in
          EConstr.Unsafe.to_constr
            (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr))
        el
    in
    (****** The next works only if the match is not dependent ****)
    let results =
      List.map
        (fun ca ->
          let res =
            build_entry_lc_from_case_term env sigma types funname make_discr []
              brl case_resl.to_avoid ca
          in
          res)
        case_resl.result
    in
    { result = List.concat (List.map (fun r -> r.result) results)
    ; to_avoid =
        List.fold_left
          (fun acc r -> List.union Id.equal acc r.to_avoid)
          [] results }

and build_entry_lc_from_case_term env sigma types funname make_discr
    patterns_to_prevent brl avoid matched_expr =
  match brl with
  | [] -> (* computed_branches  *) {result = []; to_avoid = avoid}
  | br :: brl' ->
    (* alpha conversion to prevent name clashes *)
    let {CAst.v = idl, patl, return} = alpha_br avoid br in
    let new_avoid = idl @ avoid in
    (* for now we can no more use idl as an identifier *)
    (* building a list of precondition stating that we are not in this branch
       (will be used in the following recursive calls)
    *)
    let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
    let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
      List.map2
        (fun pat typ avoid pat'_as_term ->
          let renamed_pat, _, _ = alpha_pat avoid pat in
          let pat_ids = get_pattern_id renamed_pat in
          let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
          List.fold_right
            (fun id acc ->
              let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
              let raw_typ_of_id =
                Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids
                  (Evd.from_env env) typ_of_id
              in
              mkGProd (Name id, raw_typ_of_id, acc))
            pat_ids
            (glob_make_neq pat'_as_term (pattern_to_term renamed_pat)))
        patl types
    in
    (* Checking if we can be in this branch
       (will be used in the following recursive calls)
    *)
    let unify_with_those_patterns : (cases_pattern -> bool * bool) list =
      List.map
        (fun pat pat' -> (are_unifiable pat pat', eq_cases_pattern pat pat'))
        patl
    in
    (*
           we first compute the other branch result (in ordrer to keep the order of the matching
           as much as possible)
        *)
    let brl'_res =
      build_entry_lc_from_case_term env sigma types funname make_discr
        ((unify_with_those_patterns, not_those_patterns) :: patterns_to_prevent)
        brl' avoid matched_expr
    in
    (* We now create the precondition of this branch i.e.
       1- the list of variable appearing in the different patterns of this branch and
          the list of equation stating than el = patl (List.flatten ...)
       2- If there exists a previous branch which pattern unify with the one of this branch
          then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
    *)
    let those_pattern_preconds =
      List.flatten
        (List.map3
           (fun pat e typ_as_constr ->
             let this_pat_ids = ids_of_pat pat in
             let typ_as_constr = EConstr.of_constr typ_as_constr in
             let typ =
               Detyping.detype Detyping.Now false Id.Set.empty new_env
                 (Evd.from_env env) typ_as_constr
             in
             let pat_as_term = pattern_to_term pat in
             (* removing trivial holes *)
             let pat_as_term = solve_trivial_holes pat_as_term e in
             (* observe (str "those_pattern_preconds" ++ spc () ++ *)
             (*            str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
             (*            str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
             (*            str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
             List.fold_right
               (fun id acc ->
                 if Id.Set.mem id this_pat_ids then
                   ( Prod (Name id)
                   , let typ_of_id = Typing.type_of_variable new_env id in
                     let raw_typ_of_id =
                       Detyping.detype Detyping.Now false Id.Set.empty new_env
                         (Evd.from_env env) typ_of_id
                     in
                     raw_typ_of_id )
                   :: acc
                 else acc)
               idl
               [(Prod Anonymous, glob_make_eq ~typ pat_as_term e)])
           patl matched_expr.value types)
      @
      if
        List.exists
          (function
            | unifl, _ ->
              let unif, _ =
                List.split (List.map2 (fun x y -> x y) unifl patl)
              in
              List.for_all (fun x -> x) unif)
          patterns_to_prevent
      then
        let i = List.length patterns_to_prevent in
        let pats_as_constr =
          List.map2 (pattern_to_term_and_type new_env) types patl
        in
        [(Prod Anonymous, make_discr pats_as_constr i)]
      else []
    in
    (* We compute the result of the value returned by the branch*)
    let return_res = build_entry_lc new_env sigma funname new_avoid return in
    (* and combine it with the preconds computed for this branch *)
    let this_branch_res =
      List.map
        (fun res ->
          { context = matched_expr.context @ those_pattern_preconds @ res.context
          ; value = res.value })
        return_res.result
    in
    {brl'_res with result = this_branch_res @ brl'_res.result}

let is_res r =
  match DAst.get r with
  | GVar id -> (
    try String.equal (String.sub (Id.to_string id) 0 4) "_res"
    with Invalid_argument _ -> false )
  | _ -> false

let is_gr c gr =
  match DAst.get c with GRef (r, _) -> GlobRef.equal r gr | _ -> false

let is_gvar c = match DAst.get c with GVar id -> true | _ -> false

let same_raw_term rt1 rt2 =
  match (DAst.get rt1, DAst.get rt2) with
  | GRef (r1, _), GRef (r2, _) -> GlobRef.equal r1 r2
  | GHole _, GHole _ -> true
  | _ -> false

let decompose_raw_eq env lhs rhs =
  let rec decompose_raw_eq lhs rhs acc =
    observe
      ( str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " "
      ++ pr_glob_constr_env env rhs );
    let rhd, lrhs = glob_decompose_app rhs in
    let lhd, llhs = glob_decompose_app lhs in
    observe (str "lhd := " ++ pr_glob_constr_env env lhd);
    observe (str "rhd := " ++ pr_glob_constr_env env rhd);
    observe (str "llhs := " ++ int (List.length llhs));
    observe (str "lrhs := " ++ int (List.length lrhs));
    let sllhs = List.length llhs in
    let slrhs = List.length lrhs in
    if same_raw_term lhd rhd && Int.equal sllhs slrhs then
      (* let _ = assert false in  *)
      List.fold_right2 decompose_raw_eq llhs lrhs acc
    else (lhs, rhs) :: acc
  in
  decompose_raw_eq lhs rhs []

exception Continue

(*
   The second phase which reconstruct the real type of the constructor.
   rebuild the globalized constructors expression.
   eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
  observe (str "rebuilding : " ++ pr_glob_constr_env env rt);
  let open Context.Rel.Declaration in
  let open CAst in
  match DAst.get rt with
  | GProd (n, k, t, b) -> (
    let not_free_in_t id = not (is_free_in id t) in
    let new_crossed_types = t :: crossed_types in
    match DAst.get t with
    | GApp (res_rt, args') when is_res res_rt -> (
      let arg = List.hd args' in
      match DAst.get arg with
      | GVar this_relname ->
        (*i The next call to mk_rel_id is
          valid since we are constructing the graph
          Ensures by: obvious
          i*)
        let new_t =
          mkGApp (mkGVar (mk_rel_id this_relname), List.tl args' @ [res_rt])
        in
        let t', ctx = Pretyping.understand env (Evd.from_env env) new_t in
        let r = Sorts.Relevant in
        (* TODO relevance *)
        let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
        let new_b, id_to_exclude =
          rebuild_cons new_env nb_args relname args new_crossed_types
            (depth + 1) b
        in
        (mkGProd (n, new_t, new_b), Id.Set.filter not_free_in_t id_to_exclude)
      | _ ->
        (* the first args is the name of the function! *)
        assert false )
    | GApp (eq_as_ref, [ty; id; rt])
      when is_gvar id
           && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type")
           && n == Anonymous -> (
      let loc1 = rt.CAst.loc in
      let loc2 = eq_as_ref.CAst.loc in
      let loc3 = id.CAst.loc in
      let id = match DAst.get id with GVar id -> id | _ -> assert false in
      try
        observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
        let t' =
          try fst (Pretyping.understand env (Evd.from_env env) t) (*FIXME*)
          with e when CErrors.noncritical e -> raise Continue
        in
        let is_in_b = is_free_in id b in
        let _keep_eq =
          (not (List.exists (is_free_in id) args))
          || is_in_b
          || List.exists (is_free_in id) crossed_types
        in
        let new_args = List.map (replace_var_by_term id rt) args in
        let subst_b = if is_in_b then b else replace_var_by_term id rt b in
        let r = Sorts.Relevant in
        (* TODO relevance *)
        let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
        let new_b, id_to_exclude =
          rebuild_cons new_env nb_args relname new_args new_crossed_types
            (depth + 1) subst_b
        in
        (mkGProd (n, t, new_b), id_to_exclude)
      with Continue ->
        let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
        let ty', ctx = Pretyping.understand env (Evd.from_env env) ty in
        let ind, args' =
          Inductiveops.find_inductive env Evd.(from_env env) ty'
        in
        let mib, _ = Global.lookup_inductive (fst ind) in
        let nparam = mib.Declarations.mind_nparams in
        let params, arg' = Util.List.chop nparam args' in
        let rt_typ =
          DAst.make
          @@ GApp
               ( DAst.make @@ GRef (GlobRef.IndRef (fst ind), None)
               , List.map
                   (fun p ->
                     Detyping.detype Detyping.Now false Id.Set.empty env
                       (Evd.from_env env) (EConstr.of_constr p))
                   params
                 @ Array.to_list
                     (Array.make (List.length args' - nparam) (mkGHole ())) )
        in
        let eq' =
          DAst.make ?loc:loc1
          @@ GApp
               ( DAst.make ?loc:loc2 @@ GRef (jmeq, None)
               , [ty; DAst.make ?loc:loc3 @@ GVar id; rt_typ; rt] )
        in
        observe
          (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
        let eq'_as_constr, ctx =
          Pretyping.understand env (Evd.from_env env) eq'
        in
        observe (str " computing new type for jmeq : done");
        let sigma = Evd.(from_env env) in
        let new_args =
          match EConstr.kind sigma eq'_as_constr with
          | App (_, [|_; _; ty; _|]) ->
            let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in
            let ty' = snd (Util.List.chop nparam ty) in
            List.fold_left2
              (fun acc var_as_constr arg ->
                if isRel var_as_constr then
                  let na =
                    RelDecl.get_name
                      (Environ.lookup_rel (destRel var_as_constr) env)
                  in
                  match na with
                  | Anonymous -> acc
                  | Name id' ->
                    ( id'
                    , Detyping.detype Detyping.Now false Id.Set.empty env
                        (Evd.from_env env) arg )
                    :: acc
                else if isVar var_as_constr then
                  ( destVar var_as_constr
                  , Detyping.detype Detyping.Now false Id.Set.empty env
                      (Evd.from_env env) arg )
                  :: acc
                else acc)
              [] arg' ty'
          | _ -> assert false
        in
        let is_in_b = is_free_in id b in
        let _keep_eq =
          (not (List.exists (is_free_in id) args))
          || is_in_b
          || List.exists (is_free_in id) crossed_types
        in
        let new_args =
          List.fold_left
            (fun args (id, rt) -> List.map (replace_var_by_term id rt) args)
            args ((id, rt) :: new_args)
        in
        let subst_b = if is_in_b then b else replace_var_by_term id rt b in
        let new_env =
          let t', ctx = Pretyping.understand env (Evd.from_env env) eq' in
          let r = Sorts.Relevant in
          (* TODO relevance *)
          EConstr.push_rel (LocalAssum (make_annot n r, t')) env
        in
        let new_b, id_to_exclude =
          rebuild_cons new_env nb_args relname new_args new_crossed_types
            (depth + 1) subst_b
        in
        (mkGProd (n, eq', new_b), id_to_exclude)
      (* J.F:. keep this comment  it explain how to remove some meaningless equalities
         if keep_eq then
         mkGProd(n,t,new_b),id_to_exclude
         else new_b, Id.Set.add id id_to_exclude
      *) )
    | GApp (eq_as_ref, [ty; rt1; rt2])
      when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous
      -> (
      try
        let l = decompose_raw_eq env rt1 rt2 in
        if List.length l > 1 then
          let new_rt =
            List.fold_left
              (fun acc (lhs, rhs) ->
                mkGProd
                  ( Anonymous
                  , mkGApp
                      ( mkGRef Coqlib.(lib_ref "core.eq.type")
                      , [mkGHole (); lhs; rhs] )
                  , acc ))
              b l
          in
          rebuild_cons env nb_args relname args crossed_types depth new_rt
        else raise Continue
      with Continue -> (
        observe
          (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
        let t', ctx = Pretyping.understand env (Evd.from_env env) t in
        let r = Sorts.Relevant in
        (* TODO relevance *)
        let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
        let new_b, id_to_exclude =
          rebuild_cons new_env nb_args relname args new_crossed_types
            (depth + 1) b
        in
        match n with
        | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
          (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
        | _ -> (mkGProd (n, t, new_b), Id.Set.filter not_free_in_t id_to_exclude) )
      )
    | _ -> (
      observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
      let t', ctx = Pretyping.understand env (Evd.from_env env) t in
      let r = Sorts.Relevant in
      (* TODO relevance *)
      let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
      let new_b, id_to_exclude =
        rebuild_cons new_env nb_args relname args new_crossed_types (depth + 1)
          b
      in
      match n with
      | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
        (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
      | _ -> (mkGProd (n, t, new_b), Id.Set.filter not_free_in_t id_to_exclude)
      ) )
  | GLambda (n, k, t, b) -> (
    let not_free_in_t id = not (is_free_in id t) in
    let new_crossed_types = t :: crossed_types in
    observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
    let t', ctx = Pretyping.understand env (Evd.from_env env) t in
    match n with
    | Name id ->
      let r = Sorts.Relevant in
      (* TODO relevance *)
      let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
      let new_b, id_to_exclude =
        rebuild_cons new_env nb_args relname
          (args @ [mkGVar id])
          new_crossed_types (depth + 1) b
      in
      if Id.Set.mem id id_to_exclude && depth >= nb_args then
        (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
      else
        ( DAst.make @@ GProd (n, k, t, new_b)
        , Id.Set.filter not_free_in_t id_to_exclude )
    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
    (* We have renamed all the anonymous functions during alpha_renaming phase *)
    )
  | GLetIn (n, v, t, b) -> (
    let t =
      match t with
      | None -> v
      | Some t -> DAst.make ?loc:rt.loc @@ GCast (v, DEFAULTcast, t)
    in
    let not_free_in_t id = not (is_free_in id t) in
    let evd = Evd.from_env env in
    let t', ctx = Pretyping.understand env evd t in
    let evd = Evd.from_ctx ctx in
    let type_t' = Retyping.get_type_of env evd t' in
    let t' = EConstr.Unsafe.to_constr t' in
    let type_t' = EConstr.Unsafe.to_constr type_t' in
    let new_env =
      Environ.push_rel (LocalDef (make_annot n Sorts.Relevant, t', type_t')) env
    in
    let new_b, id_to_exclude =
      rebuild_cons new_env nb_args relname args (t :: crossed_types) (depth + 1)
        b
    in
    match n with
    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
      (new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude))
    | _ ->
      ( DAst.make @@ GLetIn (n, t, None, new_b)
      , (* HOPING IT WOULD WORK *)
        Id.Set.filter not_free_in_t id_to_exclude ) )
  | GLetTuple (nal, (na, rto), t, b) ->
    assert (Option.is_empty rto);
    let not_free_in_t id = not (is_free_in id t) in
    let new_t, id_to_exclude' =
      rebuild_cons env nb_args relname args crossed_types depth t
    in
    let t', ctx = Pretyping.understand env (Evd.from_env env) new_t in
    let r = Sorts.Relevant in
    (* TODO relevance *)
    let new_env = EConstr.push_rel (LocalAssum (make_annot na r, t')) env in
    let new_b, id_to_exclude =
      rebuild_cons new_env nb_args relname args (t :: crossed_types) (depth + 1)
        b
    in
    (* 	  match n with  *)
    (* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
    (* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
    (* 	    | _ -> *)
    ( DAst.make @@ GLetTuple (nal, (na, None), t, new_b)
    , Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') )
  | _ -> (mkGApp (mkGVar relname, args @ [rt]), Id.Set.empty)

(* debugging wrapper *)
let rebuild_cons env nb_args relname args crossed_types rt =
  (*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
  (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
  let res = rebuild_cons env nb_args relname args crossed_types 0 rt in
  (*   observe (str " leads to "++ pr_glob_constr (fst res)); *)
  res

(* naive implementation of parameter detection.

   A parameter is an argument which is only preceded by parameters and whose
   calls are all syntactically equal.

   TODO: Find a valid way to deal with implicit arguments here!
*)
let rec compute_cst_params relnames params gt =
  DAst.with_val
    (function
      | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params
      | GApp (f, args) -> (
        match DAst.get f with
        | GVar relname' when Id.Set.mem relname' relnames ->
          compute_cst_params_from_app [] (params, args)
        | _ -> List.fold_left (compute_cst_params relnames) params (f :: args) )
      | GProj (f, args, c) ->
        List.fold_left (compute_cst_params relnames) params (args @ [c])
      | GLambda (_, _, t, b) | GProd (_, _, t, b) | GLetTuple (_, _, t, b) ->
        let t_params = compute_cst_params relnames params t in
        compute_cst_params relnames t_params b
      | GLetIn (_, v, t, b) ->
        let v_params = compute_cst_params relnames params v in
        let t_params =
          Option.fold_left (compute_cst_params relnames) v_params t
        in
        compute_cst_params relnames t_params b
      | GCases _ ->
        params
        (* If there is still cases at this point they can only be
           discrimination ones *)
      | GSort _ -> params
      | GHole _ -> params
      | GIf _ | GRec _ | GCast _ | GArray _ ->
        CErrors.user_err (str "Unhandled case."))
    gt

and compute_cst_params_from_app acc (params, rtl) =
  let is_gid id c =
    match DAst.get c with GVar id' -> Id.equal id id' | _ -> false
  in
  match (params, rtl) with
  | _ :: _, [] -> assert false (* the rel has at least nargs + 1 arguments ! *)
  | ((Name id, _, None) as param) :: params', c :: rtl' when is_gid id c ->
    compute_cst_params_from_app (param :: acc) (params', rtl')
  | _ -> List.rev acc

let compute_params_name relnames
    (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array)
    csts =
  let rels_params =
    Array.mapi
      (fun i args ->
        List.fold_left
          (fun params (_, cst) -> compute_cst_params relnames params cst)
          args csts.(i))
      args
  in
  let l = ref [] in
  let _ =
    try
      List.iteri
        (fun i ((n, nt, typ) as param) ->
          if
            Array.for_all
              (fun l ->
                let n', nt', typ' = List.nth l i in
                Name.equal n n' && glob_constr_eq nt nt'
                && Option.equal glob_constr_eq typ typ')
              rels_params
          then l := param :: !l)
        rels_params.(0)
    with e when CErrors.noncritical e -> ()
  in
  List.rev !l

let rec rebuild_return_type rt =
  let loc = rt.CAst.loc in
  match rt.CAst.v with
  | Constrexpr.CProdN (n, t') ->
    CAst.make ?loc @@ Constrexpr.CProdN (n, rebuild_return_type t')
  | Constrexpr.CLetIn (na, v, t, t') ->
    CAst.make ?loc @@ Constrexpr.CLetIn (na, v, t, rebuild_return_type t')
  | _ ->
    CAst.make ?loc
    @@ Constrexpr.CProdN
         ( [ Constrexpr.CLocalAssum
               ([CAst.make Anonymous], Constrexpr.Default Explicit, rt) ]
         , CAst.make @@ Constrexpr.CSort (UAnonymous {rigid = true}) )

let do_build_inductive evd (funconstants : pconstant list)
    (funsargs : (Name.t * glob_constr * glob_constr option) list list)
    returned_types (rtl : glob_constr list) =
  let _time1 = System.get_time () in
  let funnames =
    List.map
      (fun c -> Label.to_id (KerName.label (Constant.canonical (fst c))))
      funconstants
  in
  (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
  let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
  let funnames = Array.of_list funnames in
  let funsargs = Array.of_list funsargs in
  let returned_types = Array.of_list returned_types in
  (* alpha_renaming of the body to prevent variable capture during manipulation *)
  let rtl_alpha = List.map (function rt -> expand_as (alpha_rt [] rt)) rtl in
  let rta = Array.of_list rtl_alpha in
  (*i The next call to mk_rel_id is valid since we are constructing the graph
    Ensures by: obvious
    i*)
  let relnames = Array.map mk_rel_id funnames in
  let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
  (* Construction of the pseudo constructors *)
  let open Context.Named.Declaration in
  let evd, env =
    Array.fold_right2
      (fun id (c, u) (evd, env) ->
        let u = EConstr.EInstance.make u in
        let evd, t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
        let t = EConstr.Unsafe.to_constr t in
        ( evd
        , Environ.push_named (LocalAssum (make_annot id Sorts.Relevant, t)) env
        ))
      funnames
      (Array.of_list funconstants)
      (evd, Global.env ())
  in
  (* we solve and replace the implicits *)
  let rta =
    Array.mapi
      (fun i rt ->
        let _, t =
          Typing.type_of env evd
            (EConstr.of_constr (mkConstU (Array.of_list funconstants).(i)))
        in
        resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env
          evd rt)
      rta
  in
  let resa = Array.map (build_entry_lc env evd funnames_as_set []) rta in
  let env_with_graphs =
    let rel_arity i funargs =
      (* Rebuilding arities (with parameters) *)
      let rel_first_args :
          (Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list =
        funargs
      in
      List.fold_right
        (fun (n, t, typ) acc ->
          match typ with
          | Some typ ->
            CAst.make
            @@ Constrexpr.CLetIn
                 ( CAst.make n
                 , with_full_print
                     Constrextern.(extern_glob_constr empty_extern_env)
                     t
                 , Some
                     (with_full_print
                        Constrextern.(extern_glob_constr empty_extern_env)
                        typ)
                 , acc )
          | None ->
            CAst.make
            @@ Constrexpr.CProdN
                 ( [ Constrexpr.CLocalAssum
                       ( [CAst.make n]
                       , Constrexpr_ops.default_binder_kind
                       , with_full_print
                           Constrextern.(extern_glob_constr empty_extern_env)
                           t ) ]
                 , acc ))
        rel_first_args
        (rebuild_return_type returned_types.(i))
    in
    (* We need to lift back our work topconstr but only with all information
       We mimic a Set Printing All.
       Then save the graphs and reset Printing options to their primitive values
    *)
    let rel_arities = Array.mapi rel_arity funsargs in
    Util.Array.fold_left2
      (fun env rel_name rel_ar ->
        let rex =
          fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)
        in
        let rex = EConstr.Unsafe.to_constr rex in
        let r = Sorts.Relevant in
        (* TODO relevance *)
        Environ.push_named (LocalAssum (make_annot rel_name r, rex)) env)
      env relnames rel_arities
  in
  (* and of the real constructors*)
  let constr i res =
    List.map
      (function
        | result (* (args',concl') *) ->
          let rt = compose_glob_context result.context result.value in
          let nb_args = List.length funsargs.(i) in
          (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_glob_constr rt)) rt; *)
          fst (rebuild_cons env_with_graphs nb_args relnames.(i) [] [] rt))
      res.result
  in
  (* adding names to constructors  *)
  let next_constructor_id = ref (-1) in
  let mk_constructor_id i =
    incr next_constructor_id;
    (*i The next call to mk_rel_id is valid since we are constructing the graph
      Ensures by: obvious
      i*)
    Id.of_string
      ( Id.to_string (mk_rel_id funnames.(i))
      ^ "_"
      ^ string_of_int !next_constructor_id )
  in
  let rel_constructors i rt : (Id.t * glob_constr) list =
    next_constructor_id := -1;
    List.map (fun constr -> (mk_constructor_id i, constr)) (constr i rt)
  in
  let rel_constructors = Array.mapi rel_constructors resa in
  (* Computing the set of parameters if asked *)
  let rels_params =
    compute_params_name relnames_as_set funsargs rel_constructors
  in
  let nrel_params = List.length rels_params in
  let rel_constructors =
    (* Taking into account the parameters in constructors *)
    Array.map
      (List.map (fun (id, rt) -> (id, snd (chop_rprod_n nrel_params rt))))
      rel_constructors
  in
  let rel_arity i funargs =
    (* Reduilding arities (with parameters) *)
    let rel_first_args :
        (Name.t * Glob_term.glob_constr * Glob_term.glob_constr option) list =
      snd (List.chop nrel_params funargs)
    in
    List.fold_right
      (fun (n, t, typ) acc ->
        match typ with
        | Some typ ->
          CAst.make
          @@ Constrexpr.CLetIn
               ( CAst.make n
               , with_full_print
                   Constrextern.(extern_glob_constr empty_extern_env)
                   t
               , Some
                   (with_full_print
                      Constrextern.(extern_glob_constr empty_extern_env)
                      typ)
               , acc )
        | None ->
          CAst.make
          @@ Constrexpr.CProdN
               ( [ Constrexpr.CLocalAssum
                     ( [CAst.make n]
                     , Constrexpr_ops.default_binder_kind
                     , with_full_print
                         Constrextern.(extern_glob_constr empty_extern_env)
                         t ) ]
               , acc ))
      rel_first_args
      (rebuild_return_type returned_types.(i))
  in
  (* We need to lift back our work topconstr but only with all information
     We mimic a Set Printing All.
     Then save the graphs and reset Printing options to their primitive values
  *)
  let rel_arities = Array.mapi rel_arity funsargs in
  let rel_params_ids =
    List.fold_left
      (fun acc (na, _, _) ->
        match na with Anonymous -> acc | Name id -> id :: acc)
      [] rels_params
  in
  let rel_params =
    List.map
      (fun (n, t, typ) ->
        match typ with
        | Some typ ->
          Constrexpr.CLocalDef
            ( CAst.make n
            , Constrextern.(extern_glob_constr empty_extern_env) t
            , Some
                (with_full_print
                   Constrextern.(extern_glob_constr empty_extern_env)
                   typ) )
        | None ->
          Constrexpr.CLocalAssum
            ( [CAst.make n]
            , Constrexpr_ops.default_binder_kind
            , Constrextern.(extern_glob_constr empty_extern_env) t ))
      rels_params
  in
  let ext_rels_constructors =
    Array.map
      (List.map (fun (id, t) ->
           ( Vernacexpr.(NoCoercion, NoInstance)
           , ( CAst.make id
             , with_full_print
                 Constrextern.(extern_glob_type empty_extern_env)
                 ((* zeta_normalize *) alpha_rt rel_params_ids t) ) )))
      rel_constructors
  in
  let rel_ind i ext_rel_constructors =
    ( ( CAst.make @@ relnames.(i)
      , (rel_params, None)
      , Some rel_arities.(i)
      , ext_rel_constructors )
    , [] )
  in
  let ext_rel_constructors = Array.mapi rel_ind ext_rels_constructors in
  let rel_inds = Array.to_list ext_rel_constructors in
  (*   let _ =  *)
  (*   Pp.msgnl  (\* observe *\) ( *)
  (*       str "Inductive" ++ spc () ++ *)
  (* 	prlist_with_sep  *)
  (* 	(fun () -> fnl ()++spc () ++ str "with" ++ spc ())  *)
  (* 	(function ((_,id),_,params,ar,constr) ->  *)
  (* 	   Ppconstr.pr_id id ++ spc () ++  *)
  (* 	     Ppconstr.pr_binders params ++ spc () ++ *)
  (* 	     str ":" ++ spc () ++  *)
  (* 	     Ppconstr.pr_lconstr_expr ar ++ spc () ++ str ":=" ++ *)
  (* 	     prlist_with_sep  *)
  (* 	     (fun _ -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
  (* 	     (function (_,((_,id),t)) ->  *)
  (* 		Ppconstr.pr_id id ++ spc () ++ str ":" ++ spc () ++ *)
  (* 		  Ppconstr.pr_lconstr_expr t) *)
  (* 	     constr *)
  (* 	) *)
  (* 	rel_inds *)
  (*     ) *)
  (*   in *)
  let _time2 = System.get_time () in
  try
    with_full_print
      (Flags.silently
         (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds
            ~cumulative:false ~poly:false ~private_ind:false
            ~uniform:ComInductive.NonUniformParameters))
      Declarations.Finite
  with
  | UserError msg as e ->
    let _time3 = System.get_time () in
    (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
    let repacked_rel_inds =
      List.map
        (fun ((a, b, c, l), ntn) ->
          (Vernacexpr.((NoCoercion, (a, None)), b, c, Constructors l), ntn))
        rel_inds
    in
    let msg =
      str "while trying to define"
      ++ spc ()
      ++ Ppvernac.pr_vernac
           (CAst.make
              Vernacexpr.
                { control = []
                ; attrs = []
                ; expr =
                    VernacInductive (Vernacexpr.Inductive_kw, repacked_rel_inds)
                })
      ++ fnl () ++ msg
    in
    observe msg; raise e
  | reraise ->
    let _time3 = System.get_time () in
    (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
    let repacked_rel_inds =
      List.map
        (fun ((a, b, c, l), ntn) ->
          (Vernacexpr.((NoCoercion, (a, None)), b, c, Constructors l), ntn))
        rel_inds
    in
    let msg =
      str "while trying to define"
      ++ spc ()
      ++ Ppvernac.pr_vernac
           ( CAst.make
           @@ Vernacexpr.
                { control = []
                ; attrs = []
                ; expr =
                    VernacInductive (Vernacexpr.Inductive_kw, repacked_rel_inds)
                } )
      ++ fnl () ++ CErrors.print reraise
    in
    observe msg; raise reraise

let build_inductive evd funconstants funsargs returned_types rtl =
  let pu = !Detyping.print_universes in
  let cu = !Constrextern.print_universes in
  try
    Detyping.print_universes := true;
    Constrextern.print_universes := true;
    do_build_inductive evd funconstants funsargs returned_types rtl;
    Detyping.print_universes := pu;
    Constrextern.print_universes := cu
  with e when CErrors.noncritical e ->
    Detyping.print_universes := pu;
    Constrextern.print_universes := cu;
    raise (Building_graph e)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct