Ltac2: make argument order of fold combinators same as OCaml

Fix #16485

doc/changelog/06-Ltac2-language/18197-ltac2-fold-order.rst

@@ -0,0 +1,6 @@
+- **Changed:**
+  argument order for the Ltac2 combinators `List.fold_left` `List.fold_right`
+  and `Array.fold_right` changed to be the same as in OCaml
+  (`#18197 <https://github.com/coq/coq/pull/18197>`_,
+  fixes `#16485 <https://github.com/coq/coq/issues/16485>`_,
+  by Gaëtan Gilbert).

test-suite/ltac2/array_lib.v

@@ -152,7 +152,7 @@ Goal True.
 
   (* test fold_right *)
   let a := init 4 (fun i => (Int.add 10 i)) in
-  check_eq_int (of_list (fold_right (fun a b => b::a) [] a)) [10;11;12;13].
+  check_eq_int (of_list (fold_right (fun a b => a::b) a [])) [10;11;12;13].
 
   (* test exist *)
   let a := init 4 (fun i => (Int.add 10 i)) in

test-suite/ltac2/map.v

@@ -6,7 +6,7 @@ Ltac2 ensure b := if b then () else Control.throw Regression_Test_Failure.
 
 Ltac2 sort_int_list l :=
   FSet.elements
-    (List.fold_left (fun acc x => FSet.add x acc) l (FSet.empty FSet.Tags.int_tag)).
+    (List.fold_left (fun acc x => FSet.add x acc) (FSet.empty FSet.Tags.int_tag) l).
 
 Ltac2 Eval
   ensure (List.equal Int.equal [1;2;5;8] (sort_int_list [2;5;1;8])).

user-contrib/Ltac2/Array.v

@@ -187,17 +187,19 @@ Ltac2 rec fold_left_aux (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) (pos : int)
   | false => fold_left_aux f (f x (get a pos)) a (Int.add pos 1) (Int.sub len 1)
   end.
 
-Ltac2 fold_left (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) := fold_left_aux f x a 0 (length a).
+Ltac2 fold_left (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) : 'a :=
+  fold_left_aux f x a 0 (length a).
 
-Ltac2 rec fold_right_aux (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) (pos : int) (len : int) :=
+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 (f x (get a pos)) a (Int.sub pos 1) (Int.sub len 1)
+  | 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 -> 'a) (x : 'a) (a : 'b array) := fold_right_aux f x a (Int.sub (length a) 1) (length a).
+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).
 
 Ltac2 rec exist_aux (p : 'a -> bool) (a : 'a array) (pos : int) (len : int) :=
   match Int.equal len 0 with

user-contrib/Ltac2/List.v

@@ -211,16 +211,16 @@ Ltac2 rev_map (f : 'a -> 'b) (ls : 'a list) :=
       end in
   rmap_f [] ls.
 
-Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) :=
+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 a ls)
+  | l :: ls => f l (fold_right f ls a)
   end.
 
-Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (xs : 'b list) (a : 'a) :=
+Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (a : 'a) (xs : 'b list) : 'a :=
   match xs with
   | [] => a
-  | x :: xs => fold_left f xs (f a x)
+  | x :: xs => fold_left f (f a x) xs
   end.
 
 Ltac2 fold_lefti (f : int -> 'a -> 'b -> 'a) (a : 'a) (xs : 'b list) : 'a :=