Adapt to coq/coq#18197 (List and Array fold argument order change)

Should be backwards compatible (by vendoring the new definition until
backward compat is dropped)

_CoqProject

@@ -151,6 +151,7 @@ theories/Util/Tactics/SpecializeAllWays.v
 theories/Util/Tactics/SpecializeBy.v
 theories/Util/Tactics/SplitInContext.v
 theories/Util/Tactics/UniquePose.v
+theories/Util/Tactics2/Array.v
 theories/Util/Tactics2/Constr.v
 theories/Util/Tactics2/FixNotationsForPerformance.v
 theories/Util/Tactics2/Ident.v

theories/Torch/Einsum.v

@@ -2,7 +2,7 @@ From Coq Require Import Sint63 Uint63 Utf8.
 From Ltac2 Require Ltac2 Constr List Ident String Fresh Printf.
 From NeuralNetInterp.Torch Require Import Tensor.
 From NeuralNetInterp.Util Require Import Wf_Uint63 Arrow.
-From NeuralNetInterp.Util.Tactics2 Require Constr FixNotationsForPerformance Constr.Unsafe.MakeAbbreviations List Ident.
+From NeuralNetInterp.Util.Tactics2 Require Constr FixNotationsForPerformance Constr.Unsafe.MakeAbbreviations Array List Ident.
 From NeuralNetInterp.Util Require Export Arith.Classes.
 
 Import Ltac2.
@@ -47,15 +47,15 @@ Module Import Internals.
        end.
 
   Ltac2 toplevel_rels (c : constr) : int list
-    := let rec aux (acc : int list) (c : constr)
+    := let rec aux (c : constr) (acc : int list)
          := match Constr.Unsafe.kind_nocast c with
             | Constr.Unsafe.Rel i => i :: acc
             | Constr.Unsafe.App f args
-              => let acc := aux acc f in
-                 Array.fold_right aux acc args
+              => let acc := aux f acc in
+                 Array.fold_right aux args acc
             | _ => acc
             end in
-       List.sort_uniq Int.compare (aux [] c).
+       List.sort_uniq Int.compare (aux c []).
 
   Local Notation try_tc := (ltac:(try typeclasses eauto)) (only parsing).
   (* inserts einsum for all binders *)

theories/Util/Tactics2/Array.v

@@ -0,0 +1,14 @@
+From Ltac2 Require Import Array Init.
+
+(** Definitions to be dropped when <8.19 compat is dropped *)
+
+Ltac2 rec fold_right_aux (f : 'a -> 'b -> 'b) (a : 'a array) (x : 'b) (pos : int) (len : int) :=
+  (* Note: one could compare pos<0.
+     We keep an extra len parameter so that the function can be used for any sub array *)
+  match Int.equal len 0 with
+  | true => x
+  | false => fold_right_aux f a (f (get a pos) x) (Int.sub pos 1) (Int.sub len 1)
+  end.
+
+Ltac2 fold_right (f : 'a -> 'b -> 'b) (a : 'a array) (x : 'b) : 'b :=
+  fold_right_aux f a x (Int.sub (length a) 1) (length a).

theories/Util/Tactics2/List.v

@@ -15,3 +15,17 @@ Ltac2 uniq (equal : 'a -> 'a -> bool) (ls : 'a list) : 'a list
                else aux xs (x :: acc)
           end in
      List.rev (aux ls []).
+
+(* drop when <8.19 compat is dropped *)
+Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (ls : 'a list) (a : 'b) : 'b :=
+  match ls with
+  | [] => a
+  | l :: ls => f l (fold_right f ls a)
+  end.
+
+(* drop when <8.19 compat is dropped *)
+Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (a : 'a) (xs : 'b list) : 'a :=
+  match xs with
+  | [] => a
+  | x :: xs => fold_left f (f a x) xs
+  end.