aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/merge.ml
blob: 7634437171dc66b695f503a77b03065c47102a35 (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Merging of induction principles. *)

open Globnames
open Tactics
open Indfun_common
open CErrors
open Util
open Constrexpr
open Vernacexpr
open Pp
open Names
open Term
open Vars
open Declarations
open Glob_term
open Glob_termops
open Decl_kinds
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration

(** {1 Utilities}  *)

(** {2 Useful operations on constr and glob_constr} *)

let pop c = Vars.lift (-1) c
let rec popn i c = if i<=0 then c else pop (popn (i-1) c)

(** Substitutions in constr *)
let compare_constr_nosub t1 t2 =
  if compare_constr (fun _ _ -> false) t1 t2
  then true
  else false

let rec compare_constr' t1 t2 =
  if compare_constr_nosub t1 t2
  then true
  else (compare_constr (compare_constr') t1 t2)

let rec substitterm prof t by_t in_u =
  if (compare_constr' (lift prof t) in_u)
  then (lift prof by_t)
  else map_constr_with_binders succ
    (fun i -> substitterm i t by_t) prof in_u

let lift_ldecl n ldecl = List.map (fun (x,y) -> x,lift n y) ldecl

let understand = Pretyping.understand (Global.env()) Evd.empty

(** Operations on names and identifiers *)
let id_of_name = function
    Anonymous -> Id.of_string "H"
  | Name id   -> id;;
let name_of_string = Id.of_string %> Name.mk_name
let string_of_name = id_of_name %> Id.to_string

(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
let isVarf f x =
    match x with
      | { CAst.v = GVar x } -> Id.equal x f
      | _ -> false

(** [ident_global_exist id] returns true if identifier [id] is linked
    in global environment. *)
let ident_global_exist id =
  try
    let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in
    let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
    true
  with e when CErrors.noncritical e -> false

(** [next_ident_fresh id] returns a fresh identifier (ie not linked in
    global env) with base [id]. *)
let next_ident_fresh (id:Id.t) =
    let res = ref id in
    while ident_global_exist !res do res := Nameops.increment_subscript !res done;
    !res


(** {2 Debugging} *)
(* comment this line to see debug msgs *)
let msg x = () ;; let pr_lconstr c = str ""
(* uncomment this to see debugging *)
let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c)
let prconstrnl c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
let prlistconstr lc = List.iter prconstr lc
let prstr s = msg(str s)
let prNamedConstr s c =
  begin
    msg(str "");
    msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
    msg(str "");
  end
let prNamedRConstr s c =
  begin
    msg(str "");
    msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} ");
    msg(str "");
  end
let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
let prNamedLConstr s lc =
  begin
    prstr "[§§§ ";
    prstr s;
    prNamedLConstr_aux lc;
    prstr " §§§]\n";
  end
let prNamedLDecl s lc =
  begin
    prstr s; prstr "\n";
    List.iter (fun (nm,_,tp) -> prNamedConstr (string_of_name nm) tp) lc;
    prstr "\n";
  end
let prNamedRLDecl s lc =
  begin
    prstr s; prstr "\n"; prstr "{§§ ";
    List.iter
      (fun x ->
        match x with
          | (nm,None,Some tp) -> prNamedRConstr (string_of_name nm) tp
          | (nm,Some bdy,None) -> prNamedRConstr ("(letin) "^string_of_name nm) bdy
          | _ -> assert false
        ) lc;
    prstr " §§}\n";
    prstr "\n";
  end

(** {2 Misc} *)

exception Found of int

(* Array scanning *)

let array_prfx (arr: 'a array) (pred: int -> 'a -> bool): int =
match Array.findi pred arr with
| None -> Array.length arr (* all elt are positive *)
| Some i -> i

(* Like List.chop but except that [i] is the size of the suffix of [l]. *)
let list_chop_end i l =
  let size_prefix = List.length l -i in
  if size_prefix < 0 then failwith "list_chop_end"
  else List.chop size_prefix l

let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a =
  let i = ref 0 in
  List.fold_left
    (fun acc x ->
      let res = f !i acc x in i := !i + 1; res)
    acc arr

let list_filteri (f: int -> 'a -> bool) (l:'a list):'a list =
  let i = ref 0 in
  List.filter (fun x -> let res = f !i x in i := !i + 1; res) l


(** Iteration module *)
module For =
struct
  let rec map i j (f: int -> 'a)  = if i>j then [] else f i :: (map (i+1) j f)
  let rec foldup i j (f: 'a -> int -> 'a) acc =
    if i>j then acc else let newacc = f acc i in foldup (i+1) j f newacc
  let rec folddown i j (f: 'a -> int -> 'a) acc =
    if i>j then acc else let newacc = f acc j in folddown i (j-1) f newacc
  let fold i j = if i<j then foldup i j else folddown i j
end


(** {1 Parameters shifting and linking information} *)

(** This type is used to deal with debruijn linked indices. When a
    variable is linked to a previous one, we will ignore it and refer
    to previous one. *)
type linked_var =
    | Linked of int
    | Unlinked
    | Funres

(** When merging two graphs, parameters may become regular arguments,
    and thus be shifted. This type describes the result of computing
    the changes. *)
type 'a shifted_params =
    {
      nprm1:'a;
      nprm2:'a;
      prm2_unlinked:'a list; (* ranks of unlinked params in nprms2 *)
      nuprm1:'a;
      nuprm2:'a;
      nargs1:'a;
      nargs2:'a;
    }


let prlinked x =
  match x with
    | Linked i -> Printf.sprintf "Linked %d" i
    | Unlinked -> Printf.sprintf "Unlinked"
    | Funres -> Printf.sprintf "Funres"

let linkmonad f lnkvar =
  match lnkvar with
    | Linked i -> Linked (f i)
    | Unlinked -> Unlinked
    | Funres -> Funres

let linklift lnkvar i = linkmonad (fun x -> x+i) lnkvar

(* This map is used to deal with debruijn linked indices. *)
module Link = Map.Make (Int)

let pr_links l =
  Printf.printf "links:\n";
  Link.iter (fun k e -> Printf.printf "%d : %s\n" k (prlinked e)) l;
  Printf.printf "_____________\n"

type 'a merged_arg =
    | Prm_stable of 'a
    | Prm_linked of 'a
    | Prm_arg of 'a
    | Arg_stable of 'a
    | Arg_linked of 'a
    | Arg_funres

(** Information about graph merging of two inductives.
   All rel_decl list are IN REVERSE ORDER (ie well suited for compose) *)

type merge_infos =
    {
      ident:Id.t; (** new inductive name *)
      mib1: mutual_inductive_body;
      oib1: one_inductive_body;
      mib2: mutual_inductive_body;
      oib2: one_inductive_body;

      (** Array of links of the first inductive (should be all stable) *)
      lnk1: int merged_arg array;

      (** Array of links of the second inductive (point to the first ind param/args) *)
      lnk2: int merged_arg array;

      (** rec params which remain rec param (ie not linked) *)
      recprms1: Context.Rel.Declaration.t list;
      recprms2: Context.Rel.Declaration.t list;
      nrecprms1: int;
      nrecprms2: int;

      (** rec parms which became non parm (either linked to something
         or because after a rec parm that became non parm) *)
      otherprms1: Context.Rel.Declaration.t list;
      otherprms2: Context.Rel.Declaration.t list;
      notherprms1:int;
      notherprms2:int;

      (** args which remain args in merge *)
      args1:Context.Rel.Declaration.t list;
      args2:Context.Rel.Declaration.t list;
      nargs1:int;
      nargs2:int;

      (** functional result args *)
      funresprms1: Context.Rel.Declaration.t list;
      funresprms2: Context.Rel.Declaration.t list;
      nfunresprms1:int;
      nfunresprms2:int;
    }


let pr_merginfo x =
  let i,s=
    match x with
      | Prm_linked i -> Some i,"Prm_linked"
      | Arg_linked i -> Some i,"Arg_linked"
      | Prm_stable i -> Some i,"Prm_stable"
      | Prm_arg i -> Some i,"Prm_arg"
      | Arg_stable i -> Some i,"Arg_stable"
      | Arg_funres -> None , "Arg_funres" in
  match i with
    | Some i -> Printf.sprintf "%s(%d)" s i
    | None -> Printf.sprintf "%s" s

let isPrm_stable x = match x with Prm_stable _ -> true | _ -> false

(* ?? prm_linked?? *)
let isArg_stable x = match x with Arg_stable _ | Prm_arg _ -> true | _ -> false

let is_stable x =
  match x with Arg_stable _ | Prm_stable _ | Prm_arg _ -> true | _ -> false

let isArg_funres x = match x with Arg_funres -> true | _ -> false

let filter_shift_stable (lnk:int merged_arg array) (l:'a list): 'a list =
  let prms = list_filteri (fun i _ -> isPrm_stable lnk.(i)) l in
  let args = list_filteri (fun i _ -> isArg_stable lnk.(i)) l in
  let fres = list_filteri (fun i _ -> isArg_funres lnk.(i)) l in
  prms@args@fres

(** Reverse the link map, keeping only linked vars, elements are list
    of int as several vars may be linked to the same var. *)
let revlinked lnk =
  For.fold 0 (Array.length lnk - 1)
    (fun acc k ->
      match lnk.(k) with
        | Unlinked | Funres -> acc
        | Linked i ->
            let old = try Link.find i acc with Not_found -> [] in
            Link.add i (k::old) acc)
    Link.empty

let array_switch arr i j =
  let aux = arr.(j) in arr.(j) <- arr.(i); arr.(i) <- aux

let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
  let larr = Array.of_list l in
  let _ =
    Array.iteri
      (fun j x ->
        match x with
          | Prm_linked i -> array_switch larr i j
          | Arg_linked i -> array_switch larr i j
          | Prm_stable i -> ()
          | Prm_arg i -> ()
          | Arg_stable i -> ()
          | Arg_funres -> ()
      ) lnk in
  filter_shift_stable lnk (Array.to_list larr)


let error msg = user_err Pp.(str msg)

(** {1 Utilities for merging} *)

let ind1name = Id.of_string "__ind1"
let ind2name = Id.of_string "__ind2"

(** Performs verifications on two graphs before merging: they must not
    be co-inductive, and for the moment they must not be mutual
    either. *)
let verify_inds mib1 mib2 =
  if mib1.mind_finite == Decl_kinds.CoFinite then error "First argument is coinductive";
  if mib2.mind_finite == Decl_kinds.CoFinite then error "Second argument is coinductive";
  if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
  if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
  ()

(*
(** [build_raw_params prms_decl avoid] returns a list of variables
    attributed to the list of decl [prms_decl], avoiding names in
    [avoid]. *)
let build_raw_params prms_decl avoid =
  let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in
  let _ = prNamedConstr "DUMMY" dummy_constr in
  let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in
  let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
  let res,_ = glob_decompose_prod dummy_glob_constr in
  let comblist = List.combine prms_decl res in
  comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr)))
*)

let ids_of_rawlist avoid rawl =
    List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl)



(** {1 Merging function graphs} *)

(** [shift_linked_params mib1 mib2 lnk] Computes which parameters (rec
    uniform and ordinary ones) of mutual inductives [mib1] and [mib2]
    remain uniform when linked by [lnk]. All parameters are
    considered, ie we take parameters of the first inductive body of
    [mib1] and [mib2].

    Explanation: The two inductives have parameters, some of the first
    are recursively uniform, some of the last are functional result of
    the functional graph.

   (I x1 x2 ... xk ... xk' ... xn)
   (J y1 y2 ... xl ... yl' ... ym)

   Problem is, if some rec unif params are linked to non rec unif
   ones, they become non rec (and the following too). And functinal
   argument have to be shifted at the end *)
let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array) id =
  let _ = prstr "\nYOUHOU shift\n" in
  let linked_targets = revlinked lnk2 in
  let is_param_of_mib1 x = x < mib1.mind_nparams_rec in
  let is_param_of_mib2 x = x < mib2.mind_nparams_rec in
  let is_targetted_by_non_recparam_lnk1 i =
    try
      let targets = Link.find i linked_targets in
      List.exists (fun x -> not (is_param_of_mib2 x)) targets
    with Not_found -> false in
  let mlnk1 =
    Array.mapi
      (fun i lkv ->
        let isprm = is_param_of_mib1 i in
        let prmlost = is_targetted_by_non_recparam_lnk1 i in
        match isprm , prmlost, lnk1.(i) with
          | true , true , _ -> Prm_arg i (* recparam becoming ordinary *)
          | true , false , _-> Prm_stable i (* recparam remains recparam*)
          | false , false , Funres -> Arg_funres
          | _ , _ , Funres -> assert false (* fun res cannot be a rec param or lost *)
          | false , _ , _ -> Arg_stable i) (* Args of lnk1 are not linked *)
      lnk1 in
  let mlnk2 =
    Array.mapi
      (fun i lkv ->
        (* Is this correct if some param of ind2 is lost? *)
        let isprm = is_param_of_mib2 i in
        match isprm , lnk2.(i) with
          | true , Linked j when not (is_param_of_mib1 j) ->
              Prm_arg j (* recparam becoming ordinary *)
          | true , Linked j -> Prm_linked j (*recparam linked to recparam*)
          | true , Unlinked -> Prm_stable i (* recparam remains recparam*)
          | false , Linked j -> Arg_linked j (* Args of lnk2 lost *)
          | false , Unlinked -> Arg_stable i (* Args of lnk2 remains *)
          | false , Funres -> Arg_funres
          | true , Funres -> assert false (* fun res cannot be a rec param *)
      )
      lnk2 in
  let oib1 = mib1.mind_packets.(0) in
  let oib2 = mib2.mind_packets.(0) in
  (* count params remaining params *)
  let n_params1 = array_prfx mlnk1 (fun i x -> not (isPrm_stable x)) in
  let n_params2 = array_prfx mlnk2 (fun i x -> not (isPrm_stable x)) in
  let bldprms arity_ctxt mlnk =
    list_fold_lefti
      (fun i (acc1,acc2,acc3,acc4) x ->
        prstr (pr_merginfo mlnk.(i));prstr "\n";
        match mlnk.(i) with
          | Prm_stable _ -> x::acc1 , acc2 , acc3, acc4
          | Prm_arg _ -> acc1 , x::acc2 , acc3, acc4
          | Arg_stable _ -> acc1 , acc2 , x::acc3, acc4
          | Arg_funres -> acc1 , acc2 , acc3, x::acc4
          | _ -> acc1 , acc2 , acc3, acc4)
      ([],[],[],[]) arity_ctxt in
(*  let arity_ctxt2 =
    build_raw_params oib2.mind_arity_ctxt
      (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
  let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
  let _ = prstr "\n\n\n" in
  let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
  let _ = prstr "\notherprms1:\n" in
  let _ =
    List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : ");
			   prconstr (RelDecl.get_type decl); prstr "\n")
    otherprms1 in
  let _ = prstr "\notherprms2:\n" in
  let _ =
    List.iter (fun decl -> prstr (string_of_name (RelDecl.get_name decl) ^ " : "); prconstr (RelDecl.get_type decl); prstr "\n")
    otherprms2 in
  {
    ident=id;
    mib1=mib1;
    oib1 = oib1;
    mib2=mib2;
    oib2 = oib2;
    lnk1 = mlnk1;
    lnk2 = mlnk2;
    nrecprms1 = n_params1;
    recprms1 = recprms1;
    otherprms1 = otherprms1;
    args1 = args1;
    funresprms1 = funresprms1;
    notherprms1 = Array.length mlnk1 - n_params1;
    nfunresprms1 = List.length funresprms1;
    nargs1 = List.length args1;
    nrecprms2 = n_params2;
    recprms2 = recprms2;
    otherprms2 = otherprms2;
    args2 = args2;
    funresprms2 = funresprms2;
    notherprms2 = Array.length mlnk2 - n_params2;
    nargs2 = List.length args2;
    nfunresprms2 = List.length funresprms2;
  }




(** {1 Merging functions} *)

exception NoMerge

let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
  let lnk = Array.append shift.lnk1 shift.lnk2 in
  match CAst.(c1.v, c2.v) with
    | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
        let _ = prstr "\nICI1!\n" in
        let args = filter_shift_stable lnk (arr1 @ arr2) in
        CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args)
    | GApp(f1, arr1), GApp(f2,arr2)  -> raise NoMerge
    | GLetIn(nme,bdy,typ,trm) , _ ->
        let _ = prstr "\nICI2!\n" in
        let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
    | _, GLetIn(nme,bdy,typ,trm) ->
        let _ = prstr "\nICI3!\n" in
        let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
    | _ -> let _ = prstr "\nICI4!\n" in
           raise NoMerge

let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
  let lnk = Array.append shift.lnk1 shift.lnk2 in
  match CAst.(c1.v, c2.v) with
    | GApp(f1, arr1), GApp(f2,arr2) ->
        let args = filter_shift_stable lnk (arr1 @ arr2) in
        CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args)
          (* FIXME: what if the function appears in the body of the let? *)
    | GLetIn(nme,bdy,typ,trm) , _ ->
      let _ = prstr "\nICI2 '!\n" in
        let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
    | _, GLetIn(nme,bdy,typ,trm) ->
        let _ = prstr "\nICI3 '!\n" in
        let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
    | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge



(* Heuristic when merging two lists of hypothesis: merge every rec
   calls of branch 1 with all rec calls of branch 2. *)
(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
let rec merge_rec_hyps shift accrec
    (ltyp:(Name.t * glob_constr option * glob_constr option) list)
    filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
  let mergeonehyp t reldecl =
    match reldecl with
      | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind))
        -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
      | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
      | (nme,None,Some _) -> assert false
      | (nme,None,None) | (nme,Some _,Some _) -> assert false in
  match ltyp with
    | [] -> []
    | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f ->
        let rechyps = List.map (mergeonehyp t) accrec in
        rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
    | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable


let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift =
  List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec


let find_app (nme:Id.t) ltyp =
  try
    ignore
      (List.map
          (fun x ->
            match x with
              | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0)
              | _ -> ())
          ltyp);
    false
  with Found _ -> true

let prnt_prod_or_letin nm letbdy typ =
  match letbdy , typ with
    | Some lbdy , None -> prNamedRConstr ("(letin) " ^ string_of_name nm) lbdy
    | None , Some tp -> prNamedRConstr (string_of_name nm) tp
    | _ , _ -> assert false


let rec merge_types shift accrec1
    (ltyp1:(Name.t * glob_constr option * glob_constr option) list)
    (concl1:glob_constr) (ltyp2:(Name.t * glob_constr option * glob_constr option) list) concl2
    : (Name.t * glob_constr option * glob_constr option) list * glob_constr =
  let _ = prstr "MERGE_TYPES\n" in
  let _ = prstr "ltyp 1 : " in
  let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
  let _ = prstr "\nltyp 2 : " in
  let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp2 in
  let _ = prstr "\n" in
  let res =
    match ltyp1 with
      | [] ->
          let isrec1 = not (List.is_empty accrec1) in
          let isrec2 = find_app ind2name ltyp2 in
          let rechyps =
            if isrec1 && isrec2
            then (* merge_rec_hyps shift accrec1 ltyp2 filter_shift_stable *)
              merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
                filter_shift_stable_right
              @ merge_rec_hyps shift accrec1 [name_of_string "concl2",None, Some concl2]
                filter_shift_stable
            else if isrec1
                (* if rec calls in accrec1 and not in ltyp2, add one to ltyp2 *)
            then
              merge_rec_hyps shift accrec1
                (ltyp2@[name_of_string "concl2",None,Some concl2]) filter_shift_stable
            else if isrec2
            then merge_rec_hyps shift [name_of_string "concl1",None,Some concl1] ltyp2
              filter_shift_stable_right
            else ltyp2 in
          let _ = prstr"\nrechyps : " in
          let _ = List.iter(fun (nm,lbdy,tp)-> prnt_prod_or_letin nm lbdy tp) rechyps in
          let _ = prstr "MERGE CONCL :  " in
          let _ = prNamedRConstr "concl1" concl1 in
          let _ = prstr " with " in
          let _ = prNamedRConstr "concl2" concl2 in
          let _ = prstr "\n" in
          let concl =
            merge_app concl1 concl2 ind1name ind2name shift filter_shift_stable in
          let _ = prstr "FIN " in
          let _ = prNamedRConstr "concl" concl in
          let _ = prstr "\n" in

          rechyps , concl
      | (nme,None, Some t1)as e ::lt1 ->
          (match t1.CAst.v with
            | GApp(f,carr) when isVarf ind1name f ->
                merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
            | _ ->
                let recres, recconcl2 =
                  merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
                ((nme,None,Some t1) :: recres) , recconcl2)
      | (nme,Some bd, None) ::lt1 ->
          (* FIXME: what if ind1name appears in bd? *)
          let recres, recconcl2 =
            merge_types shift accrec1 lt1 concl1 ltyp2 concl2 in
          ((nme,Some bd,None) :: recres) , recconcl2
      | (_,None,None)::_ | (_,Some _,Some _)::_ -> assert false
  in
  res


(** [build_link_map_aux allargs1 allargs2 shift] returns the mapping of
    linked args [allargs2] to target args of [allargs1] as specified
    in [shift]. [allargs1] and [allargs2] are in reverse order.  Also
    returns the list of unlinked vars of [allargs2]. *)
let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array)
    (lnk:int merged_arg array) =
  Array.fold_left_i
    (fun i acc e ->
      if Int.equal i (Array.length lnk - 1) then acc (* functional arg, not in allargs *)
      else
        match e with
          | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc
          | _ -> acc)
    Id.Map.empty lnk

let build_link_map allargs1 allargs2 lnk =
  let allargs1 =
    Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in
  let allargs2 =
    Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs2) in
  build_link_map_aux allargs1 allargs2 lnk


(** [merge_one_constructor lnk shift typcstr1 typcstr2] merges the two
    constructor rawtypes [typcstr1] and [typcstr2].  [typcstr1] and
    [typcstr2] contain all parameters (including rec. unif. ones) of
    their inductive.

    if  [typcstr1] and [typcstr2] are of the form:

    forall recparams1, forall ordparams1, H1a -> H2a... (I1 x1 y1 ... z1)
    forall recparams2, forall ordparams2, H2b -> H2b... (I2 x2 y2 ... z2)

    we build:

    forall recparams1 (recparams2 without linked params),
     forall ordparams1 (ordparams2 without linked params),
      H1a' -> H2a' -> ...  -> H2a' -> H2b'(shifted) -> ...
        -> (newI x1 ... z1 x2 y2 ...z2 without linked params)

    where Hix' have been adapted, ie:
      - linked vars have been changed,
      - rec calls to I1 and I2 have been replaced by rec calls to
        newI. More precisely calls to I1 and I2 have been merge by an
        experimental heuristic (in particular if n o rec calls for I1
        or I2 is found, we use the conclusion as a rec call). See
        [merge_types] above.

    Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint.

    TODO: return nothing if equalities (after linking) are contradictory. *)
let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr)
    (typcstr2:glob_constr) : glob_constr =
  (* FIXME: les noms des parametres corerspondent en principe au
     parametres du niveau mib, mais il faudrait s'en assurer *)
  (* shift.nfunresprmsx last args are functional result *)
  let nargs1 =
    shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in
  let nargs2 =
    shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in
  let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in
  let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in
  (* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
  let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
  let rest2 = change_vars linked_map rest2 in
  let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in
  let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in
  let ltyp,concl2 =
    merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
  let _ = prNamedRLDecl "ltyp result:" ltyp in
  let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in
  let revargs1 =
    list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
  let _ = prNamedRLDecl "ltyp allargs1" allargs1 in
  let _ = prNamedRLDecl "ltyp revargs1" revargs1 in
  let revargs2 =
    list_filteri (fun i _ -> isArg_stable shift.lnk2.(i)) (List.rev allargs2) in
  let _ = prNamedRLDecl "ltyp allargs2" allargs2 in
  let _ = prNamedRLDecl "ltyp revargs2" revargs2 in
  let typwithprms =
    glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
  typwithprms


(** constructor numbering *)
let fresh_cstror_suffix , cstror_suffix_init =
  let cstror_num = ref 0 in
  (fun () ->
    let res = string_of_int !cstror_num in
    cstror_num := !cstror_num + 1;
    res) ,
  (fun () -> cstror_num := 0)

(** [merge_constructor_id id1 id2 shift] returns the identifier of the
    new constructor from the id of the two merged constructor and
    the merging info. *)
let merge_constructor_id id1 id2 shift:Id.t =
  let id = Id.to_string shift.ident ^ "_" ^ fresh_cstror_suffix () in
  next_ident_fresh (Id.of_string id)



(** [merge_constructors lnk shift avoid] merges the two list of
    constructor [(name*type)]. These are translated to glob_constr
    first, each of them having distinct var names. *)
let merge_constructors (shift:merge_infos) (avoid:Id.Set.t)
    (typcstr1:(Id.t * glob_constr) list)
    (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list =
  List.flatten
    (List.map
        (fun (id1,rawtyp1) ->
          List.map
            (fun (id2,rawtyp2) ->
              let typ = merge_one_constructor shift rawtyp1 rawtyp2 in
              let newcstror_id = merge_constructor_id id1 id2 shift in
              let _ = prstr "\n**************\n" in
              newcstror_id , typ)
            typcstr2)
        typcstr1)

(** [merge_inductive_body lnk shift avoid oib1 oib2] merges two
    inductive bodies [oib1] and [oib2], linking with [lnk], params
    info in [shift], avoiding identifiers in [avoid]. *)
let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
    (oib2:one_inductive_body) =
  (* building glob_constr type of constructors *)
  let mkrawcor nme avoid typ =
    (* first replace rel 1 by a varname *)
    let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
    let substindtyp = EConstr.of_constr substindtyp in
    Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
  let lcstr1: glob_constr list =
    Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
  (* add  to avoid all indentifiers of lcstr1 *)
  let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in
  let lcstr2 =
    Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in
  let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in

  let params1 =
    try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
    with e when CErrors.noncritical e -> [] in
  let params2 =
    try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
    with e when CErrors.noncritical e -> [] in

  let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
  let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in

  cstror_suffix_init();
  params1,params2,merge_constructors shift avoid3 lcstr1 lcstr2


(** [merge_mutual_inductive_body lnk mib1 mib2 shift] merge mutual
    inductive bodies [mib1] and [mib2] linking vars with
    [lnk]. [shift] information on parameters of the new inductive.
    For the moment, inductives are supposed to be non mutual.
*)
let merge_mutual_inductive_body
    (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) =
  (* Mutual not treated, we take first ind body of each. *)
  merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0)


let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
  Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x

let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
  let params = prms2 @ prms1 in
  let resparams =
    List.fold_left
      (fun acc (nme,tp) ->
        let _ = prstr "param :" in
        let _ = prNamedRConstr (string_of_name nme) tp in
        let _ = prstr "  ;  " in
        let typ = glob_constr_to_constr_expr tp in
        CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
      [] params in
  let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
  let arity,_ =
    List.fold_left
      (fun (acc,env) decl ->
        let nm = Context.Rel.Declaration.get_name decl in
        let c = RelDecl.get_type decl in
        let typ = Constrextern.extern_constr false env Evd.empty c in
        let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
        CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
      (concl,Global.env())
      (shift.funresprms2 @ shift.funresprms1
        @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
  resparams,arity



(** [glob_constr_list_to_inductive_expr ident rawlist] returns the
    induct_expr corresponding to the the list of constructor types
    [rawlist], named ident.
    FIXME: params et cstr_expr (arity) *)
let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
    (rawlist:(Id.t * glob_constr) list) =
  let lident = (Loc.tag shift.ident), None in
  let bindlist , cstr_expr = (* params , arities *)
    merge_rec_params_and_arity prms1 prms2 shift mkSet in
  let lcstor_expr : (bool * (lident * constr_expr)) list  =
    List.map (* zeta_normalize t ? *)
      (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t))
      rawlist in
  lident , bindlist , Some cstr_expr , lcstor_expr


let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
  match rdecl with
    | LocalAssum (nme,t) ->
        let t = EConstr.of_constr t in
        let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
        CAst.make @@ GProd (nme,Explicit,traw,t2)
    | LocalDef _ -> assert false


(** [merge_inductive ind1 ind2 lnk] merges two graphs, linking
    variables specified in [lnk]. Graphs are not supposed to be mutual
    inductives for the moment. *)
let merge_inductive (ind1: inductive) (ind2: inductive)
    (lnk1: linked_var array) (lnk2: linked_var array) id =
  let env = Global.env() in
  let mib1,_ = Inductive.lookup_mind_specif env ind1 in
  let mib2,_ = Inductive.lookup_mind_specif env ind2 in
  let _ = verify_inds mib1 mib2 in (* raises an exception if something wrong *)
  (* compute params that become ordinary args (because linked to ord. args) *)
  let shift_prm = shift_linked_params mib1 mib2 lnk1 lnk2 id in
  let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
  let _ = prstr "\nrawlist : " in
  let _ =
    List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in
  let _ = prstr "\nend rawlist\n" in
(* FIX: retransformer en constr ici
   let shift_prm =
    { shift_prm with
      recprms1=prms1;
      recprms1=prms1;
    } in *)
  let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
  (* Declare inductive *)
  let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
  let mie,pl,impls = Command.interp_mutual_inductive indl []
          false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
  (* Declare the mutual inductive block with its associated schemes *)
  ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)


(* Find infos on identifier id. *)
let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
  let kn_of_id x =
    let f_ref = Libnames.Ident (Loc.tag x) in
    locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
      locate_constant f_ref in
    try find_Function_infos (kn_of_id id)
    with Not_found ->
      user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme")

(** [merge id1 id2 args1 args2 id] builds and declares a new inductive
    type called [id], representing the merged graphs of both graphs
    [ind1] and [ind2]. identifiers occurring in both arrays [args1] and
    [args2] are considered linked (i.e. are the same variable) in the
    new graph.

    Warning: For the moment, repetitions of an id in [args1] or
    [args2] are not supported. *)
let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array)
    (args2:Id.t array) id : unit =
  let finfo1 = find_Function_infos_safe id1 in
  let finfo2 = find_Function_infos_safe id2 in
  (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *)
  (* We add one arg (functional arg of the graph) *)
  let lnk1 = Array.make (Array.length args1 + 1) Unlinked in
  let lnk2' = (* args2 may be linked to args1 members. FIXME: same
                 as above: vars may be linked inside args2?? *)
    Array.mapi
      (fun i c ->
        match Array.findi (fun i x -> Id.equal x c) args1 with
          | Some j -> Linked j
          | None -> Unlinked)
      args2 in
  (* We add one arg (functional arg of the graph) *)
  let lnk2 = Array.append lnk2' (Array.make 1 Unlinked) in
  (* setting functional results *)
  let _ = lnk1.(Array.length lnk1 - 1) <- Funres in
  let _ = lnk2.(Array.length lnk2 - 1) <- Funres in
  merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id


let remove_last_arg c =
  let (x,y) = decompose_prod c in
  let xnolast = List.rev (List.tl (List.rev x)) in
  compose_prod xnolast y

let rec remove_n_fst_list n l = if Int.equal n 0 then l else remove_n_fst_list (n-1) (List.tl l)
let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l))

let remove_last_n_arg n c =
  let (x,y) = decompose_prod c in
  let xnolast = remove_n_last_list n x in
  compose_prod xnolast y

(* [funify_branches relinfo nfuns branch] returns the branch [branch]
   of the relinfo [relinfo] modified to fit in a functional principle.
   Things to do:
    - remove indargs from rel applications
    - replace *variables only* corresponding to function (recursive)
      results by the actual function application. *)
let funify_branches relinfo nfuns branch =
  let mut_induct, induct =
    match relinfo.indref with
      | None -> assert false
      | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
      | _ -> assert false in
  let is_dom c =
    match kind_of_term c with
      | Ind(((u,_),_)) | Construct(((u,_),_),_) -> MutInd.equal u mut_induct
      | _ -> false in
  let _dom_i c =
    assert (is_dom c);
    match kind_of_term c with
      | Ind((u,i)) | Construct((u,_),i) -> i
      | _ -> assert false in
  let _is_pred c shift =
    match kind_of_term c with
      | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
      | _ -> false in
  (* FIXME: *)
  LocalDef (Anonymous,EConstr.mkProp,EConstr.mkProp)


let relprinctype_to_funprinctype relprinctype nfuns =
  let relprinctype = EConstr.of_constr relprinctype in
  let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in
  assert (not relinfo.farg_in_concl);
  assert (relinfo.indarg_in_concl);
  (* first remove indarg and indarg_in_concl *)
  let relinfo_noindarg = { relinfo with
    indarg_in_concl = false; indarg = None;
    concl = EConstr.of_constr (remove_last_arg (pop (EConstr.Unsafe.to_constr relinfo.concl))); } in
  (* the nfuns last induction arguments are functional ones: remove them *)
  let relinfo_argsok = { relinfo_noindarg with
    nargs = relinfo_noindarg.nargs - nfuns;
    (* args is in reverse order, so remove fst *)
    args = remove_n_fst_list nfuns relinfo_noindarg.args;
    concl = EConstr.of_constr (popn nfuns (EConstr.Unsafe.to_constr relinfo_noindarg.concl));
  } in
  let new_branches =
    List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
  let relinfo_branches = { relinfo_argsok with branches = new_branches } in
  relinfo_branches

(* @article{ bundy93rippling,
    author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
    title = "Rippling: A Heuristic for Guiding Inductive Proofs",
    journal = "Artificial Intelligence",
    volume = "62",
    number = "2",
    pages = "185-253",
    year = "1993",
    url = "citeseer.ist.psu.edu/bundy93rippling.html" }

 *)