Resolve #10342 : [Ltac2] Add array library

4 files changed, 422 insertions, 0 deletions

diff --git a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
new file mode 100644
index 0000000000..4acc423d10
--- /dev/null
+++ b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  An array library for ltac2 (OCaml standard library compatible where possible).
+  (`#10343 <https://github.com/coq/coq/pull/10343>`_,
+  by Michael Soegtrop).
diff --git a/test-suite/ltac2/array_lib.v b/test-suite/ltac2/array_lib.v
new file mode 100644
index 0000000000..31227eaddb
--- /dev/null
+++ b/test-suite/ltac2/array_lib.v
@@ -0,0 +1,181 @@
+Require Import Ltac2.Ltac2.
+Import Ltac2.Message.
+Import Ltac2.Array.
+Require Ltac2.List.
+Require Ltac2.Int.
+
+(* Array/List comparison functions which throw an exception on unequal *)
+
+Ltac2 Type exn ::= [ Regression_Test_Failure ].
+
+Ltac2 check_eq_int a l :=
+  List.iter2
+    (fun a b => match Int.equal a b with true => () | false => Control.throw Regression_Test_Failure end)
+    (to_list a) l.
+
+Ltac2 check_eq_bool a l :=
+  List.iter2
+    (fun a b => match Bool.eq a b with true => () | false => Control.throw Regression_Test_Failure end)
+    (to_list a) l.
+
+Ltac2 check_eq_int_matrix m ll :=
+  List.iter2 (fun a b => check_eq_int a b) (to_list m) ll.
+
+Ltac2 check_eq_bool_matrix m ll :=
+  List.iter2 (fun a b => check_eq_bool a b) (to_list m) ll.
+
+(* The below printing functions are mostly for debugging below test cases *)
+
+Ltac2 print2 m1 m2 := print (Message.concat m1 m2).
+Ltac2 print3 m1 m2 m3 := print2 m1 (Message.concat m2 m3).
+
+Ltac2 print_int_array a :=
+  iteri (fun i x => print3 (of_int i) (of_string "=") (of_int x)) a.
+
+Ltac2 of_bool b := match b with true=>of_string "true" | false=>of_string "false" end.
+
+Ltac2 print_bool_array a :=
+  iteri (fun i x => print3 (of_int i) (of_string "=") (of_bool x)) a.
+
+Ltac2 print_int_list a :=
+  List.iteri (fun i x => print3 (of_int i) (of_string "=") (of_int x)) a.
+
+Goal True.
+  (* Test failure *)
+  Fail check_eq_int ((init 3 (fun i => (Int.add i 10)))) [10;11;13].
+
+  (* test empty with int *)
+  check_eq_int (empty ()) [].
+  check_eq_int (append (empty ()) (init 3 (fun i => (Int.add i 10)))) [10;11;12].
+  check_eq_int (append (init 3 (fun i => (Int.add i 10))) (empty ())) [10;11;12].
+
+  (* test empty with bool *)
+  check_eq_bool (empty ()) [].
+  check_eq_bool (append (empty ()) (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
+  check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) (empty ())) [false;false;true].
+
+  (* test init with int *)
+  check_eq_int (init 0 (fun i => (Int.add i 10))) [].
+  check_eq_int (init 4 (fun i => (Int.add i 10))) [10;11;12;13].
+
+  (* test init with bool *)
+  check_eq_bool (init 0 (fun i => (Int.ge i 2))) [].
+  check_eq_bool (init 4 (fun i => (Int.ge i 2))) [false;false;true;true].
+
+  (* test make_matrix, set, get *)
+  let a := make_matrix 4 3 1 in
+  Array.set (Array.get a 1) 2 0;
+  check_eq_int_matrix a [[1;1;1];[1;1;0];[1;1;1];[1;1;1]].
+
+  let a := make_matrix 3 4 false in
+  Array.set (Array.get a 2) 1 true;
+  check_eq_bool_matrix a [[false;false;false;false];[false;false;false;false];[false;true;false;false]].
+
+  (* test copy *)
+  let a := init 4 (fun i => (Int.add i 10)) in
+  let b := copy a in
+  check_eq_int b [10;11;12;13].
+
+  (* test append *)
+  let a := init 3 (fun i => (Int.add i 10)) in
+  let b := init 4 (fun i => (Int.add i 20)) in
+  check_eq_int (append a b) [10;11;12;20;21;22;23].
+
+  (* test concat *)
+  let a := init 3 (fun i => (Int.add i 10)) in
+  let b := init 4 (fun i => (Int.add i 20)) in
+  let c := init 5 (fun i => (Int.add i 30)) in
+  check_eq_int (concat (a::b::c::[])) [10;11;12;20;21;22;23;30;31;32;33;34].
+
+  (* test sub *)
+  let a := init 10 (fun i => (Int.add i 10)) in
+  let b := (sub a 3 0) in
+  let c := (append b (init 3 (fun i => (Int.add i 10)))) in
+  check_eq_int b [];
+  check_eq_int c [10;11;12].
+
+  let a := init 10 (fun i => (Int.add i 10)) in
+  let b := (sub a 3 4) in
+  check_eq_int b [13;14;15;16].
+
+  (* test fill *)
+  let a := init 10 (fun i => (Int.add i 10)) in
+  fill a 3 4 0;
+  check_eq_int a [10;11;12;0;0;0;0;17;18;19].
+
+  (* test blit *)
+  let a := init 10 (fun i => (Int.add i 10)) in
+  let b := init 10 (fun i => (Int.add i 20)) in
+  blit a 5 b 3 4;
+  check_eq_int b [20;21;22;15;16;17;18;27;28;29].
+
+  (* test iter *)
+  let a := init 4 (fun i => (Int.add i 3)) in
+  let b := init 10 (fun i => 10) in
+  iter (fun x => Array.set b x x) a;
+  check_eq_int b [10;10;10;3;4;5;6;10;10;10].
+
+  (* test iter2 *)
+  let a := init 4 (fun i => (Int.add i 2)) in
+  let b := init 4 (fun i => (Int.add i 4)) in
+  let c := init 8 (fun i => 10) in
+  iter2 (fun x y => Array.set c x y) a b;
+  check_eq_int c [10;10;4;5;6;7;10;10].
+
+  (* test map *)
+  let a := init 4 (fun i => (Int.add i 10)) in
+  check_eq_bool (map (fun i => (Int.ge i 12)) a) [false;false;true;true].
+
+  (* test map2 *)
+  let a := init 4 (fun i => (Int.add 10 i)) in
+  let b := init 4 (fun i => (Int.sub 13 i)) in
+  check_eq_bool (map2 (fun x y => (Int.ge x y)) a b) [false;false;true;true].
+
+  (* test iteri *)
+  let a := init 4 (fun i => (Int.add i 10)) in
+  let m := make_matrix 4 2 100 in
+  iteri (fun i x => Array.set (Array.get m i) 0 i; Array.set (Array.get m i) 1 x) a;
+  check_eq_int_matrix m [[0;10];[1;11];[2;12];[3;13]].
+
+  (* test mapi *)
+  let a := init 4 (fun i => (Int.sub 3 i)) in
+  check_eq_bool (mapi (fun i x => (Int.ge i x)) a) [false;false;true;true].
+
+  (* to_list is already tested in check_eq_... *)
+
+  (* test of_list *)
+  check_eq_int (of_list ([0;1;2;3])) [0;1;2;3].
+
+  (* test fold_left *)
+  let a := init 4 (fun i => (Int.add 10 i)) in
+  check_eq_int (of_list (fold_left (fun a b => b::a) [] a)) [13;12;11;10].
+
+  (* 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].
+
+  (* test exist *)
+  let a := init 4 (fun i => (Int.add 10 i)) in
+  let l := [
+    exist (fun x => Int.equal x 10) a;
+    exist (fun x => Int.equal x 13) a;
+    exist (fun x => Int.equal x 14) a] in
+  check_eq_bool (of_list l) [true;true;false].
+
+  (* test for_all *)
+  let a := init 4 (fun i => (Int.add 10 i)) in
+  let l := [
+    for_all (fun x => Int.lt x 14) a;
+    for_all (fun x => Int.lt x 13) a] in
+  check_eq_bool (of_list l) [true;false].
+
+  (* test mem *)
+  let a := init 4 (fun i => (Int.add 10 i)) in
+  let l := [
+    mem Int.equal 10 a;
+    mem Int.equal 13 a;
+    mem Int.equal 14 a] in
+  check_eq_bool (of_list l) [true;true;false].
+
+exact I.
+Qed.
diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v
index c55e20bc88..ee3bf88647 100644
--- a/user-contrib/Ltac2/Array.v
+++ b/user-contrib/Ltac2/Array.v
@@ -8,9 +8,220 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* This is mostly a translation of OCaml stdlib/array.ml *)
+
+(**************************************************************************)
+(*                                                                        *)
+(*                                 OCaml                                  *)
+(*                                                                        *)
+(*             Xavier Leroy, projet Cristal, INRIA Rocquencourt           *)
+(*                                                                        *)
+(*   Copyright 1996 Institut National de Recherche en Informatique et     *)
+(*     en Automatique.                                                    *)
+(*                                                                        *)
+(*   All rights reserved.  This file is distributed under the terms of    *)
+(*   the GNU Lesser General Public License version 2.1, with the          *)
+(*   special exception on linking described in the file LICENSE.          *)
+(*                                                                        *)
+(**************************************************************************)
+
 Require Import Ltac2.Init.
+Require Ltac2.Int.
+Require Ltac2.Control.
+Require Ltac2.Bool.
+Require Ltac2.Message.
+
+(* Question: what is returned in case of an out of range value?
+   Answer:   Ltac2 throws a panic *)
 
+Ltac2 @external empty : unit -> 'a array := "ltac2" "array_empty".
 Ltac2 @external make : int -> 'a -> 'a array := "ltac2" "array_make".
 Ltac2 @external length : 'a array -> int := "ltac2" "array_length".
 Ltac2 @external get : 'a array -> int -> 'a := "ltac2" "array_get".
 Ltac2 @external set : 'a array -> int -> 'a -> unit := "ltac2" "array_set".
+Ltac2 @external lowlevel_blit : 'a array -> int -> 'a array -> int -> int -> unit := "ltac2" "array_blit".
+Ltac2 @external lowlevel_fill : 'a array -> int -> int -> 'a -> unit := "ltac2" "array_fill".
+Ltac2 @external concat : ('a array) list -> 'a array := "ltac2" "array_concat".
+
+(* Low level array operations *)
+
+Ltac2 lowlevel_sub (arr : 'a array) (start : int) (len : int) :=
+  let l := length arr in
+  match Int.equal l 0 with
+  | true => empty ()
+  | false =>
+      let newarr:=make len (get arr 0) in
+      lowlevel_blit arr start newarr 0 len;
+      newarr
+  end.
+
+(* Array functions as defined in the OCaml library *)
+
+Ltac2 init (l : int) (f : int->'a) :=
+  let rec init_aux (dst : 'a array) (pos : int) (len : int) (f : int->'a) :=
+    match Int.equal len 0 with
+    | true => ()
+    | false =>
+        set dst pos (f pos);
+        init_aux dst (Int.add pos 1) (Int.sub len 1) f
+    end
+  in
+  match Int.le l 0 with
+  | true => empty ()
+  | false =>
+      let arr:=make l (f 0) in
+      init_aux arr 0 (length arr) f;
+      arr
+  end.
+
+Ltac2 make_matrix (sx : int) (sy : int) (v : 'a) :=
+  let init1 i := v in
+  let initr i := init sy init1 in
+  init sx initr.
+
+Ltac2 copy a := lowlevel_sub a 0 (length a).
+
+Ltac2 append (a1 : 'a array) (a2 : 'a array) :=
+  match Int.equal (length a1) 0 with
+  | true => copy a2
+  | false => match Int.equal (length a2) 0 with
+             | true => copy a1
+             | false =>
+                 let newarr:=make (Int.add (length a1) (length a2)) (get a1 0) in
+                 lowlevel_blit a1 0 newarr 0 (length a1);
+                 lowlevel_blit a2 0 newarr (length a1) (length a2);
+                 newarr
+             end
+  end.
+
+Ltac2 sub (a : 'a array) (ofs : int) (len : int) :=
+  Control.assert_valid_argument "Array.sub ofs<0" (Int.ge ofs 0);
+  Control.assert_valid_argument "Array.sub len<0" (Int.ge len 0);
+  Control.assert_bounds "Array.sub" (Int.le ofs (Int.sub (length a) len));
+  lowlevel_sub a ofs len.
+
+Ltac2 fill (a : 'a array) (ofs : int) (len : int) (v : 'a) :=
+  Control.assert_valid_argument "Array.fill ofs<0" (Int.ge ofs 0);
+  Control.assert_valid_argument "Array.fill len<0" (Int.ge len 0);
+  Control.assert_bounds "Array.fill" (Int.le ofs (Int.sub (length a) len));
+  lowlevel_fill a ofs len v.
+
+Ltac2 blit (a1 : 'a array) (ofs1 : int) (a2 : 'a array) (ofs2 : int) (len : int) :=
+  Control.assert_valid_argument "Array.blit ofs1<0" (Int.ge ofs1 0);
+  Control.assert_valid_argument "Array.blit ofs2<0" (Int.ge ofs2 0);
+  Control.assert_valid_argument "Array.blit len<0" (Int.ge len 0);
+  Control.assert_bounds "Array.blit ofs1+len>len a1" (Int.le ofs1 (Int.sub (length a1) len));
+  Control.assert_bounds "Array.blit ofs2+len>len a2" (Int.le ofs2 (Int.sub (length a2) len));
+  lowlevel_blit a1 ofs1 a2 ofs2 len.
+
+Ltac2 rec iter_aux (f : 'a -> unit) (a : 'a array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => ()
+  | false => f (get a pos); iter_aux f a (Int.add pos 1) (Int.sub len 1)
+  end.
+
+Ltac2 iter (f : 'a -> unit) (a : 'a array) := iter_aux f a 0 (length a).
+
+Ltac2 rec iter2_aux (f : 'a -> 'b -> unit) (a : 'a array) (b : 'b array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => ()
+  | false => f (get a pos) (get b pos); iter2_aux f a b (Int.add pos 1) (Int.sub len 1)
+  end.
+
+Ltac2 rec iter2 (f : 'a -> 'b -> unit) (a : 'a array) (b : 'b array) :=
+  Control.assert_valid_argument "Array.iter2" (Int.equal (length a) (length b));
+  iter2_aux f a b 0 (length a).
+
+Ltac2 map (f : 'a -> 'b) (a : 'a array) :=
+  init (length a) (fun i => f (get a i)).
+
+Ltac2 map2 (f : 'a -> 'b -> 'c) (a : 'a array) (b : 'b array) :=
+  Control.assert_valid_argument "Array.map2" (Int.equal (length a) (length b));
+  init (length a) (fun i => f (get a i) (get b i)).
+
+Ltac2 rec iteri_aux (f : int -> 'a -> unit) (a : 'a array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => ()
+  | false => f pos (get a pos); iteri_aux f a (Int.add pos 1) (Int.sub len 1)
+  end.
+
+Ltac2 iteri (f : int -> 'a -> unit) (a : 'a array) := iteri_aux f a 0 (length a).
+
+Ltac2 mapi (f : int -> 'a -> 'b) (a : 'a array) :=
+  init (length a) (fun i => f i (get a i)).
+
+Ltac2 rec to_list_aux (a : 'a array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => []
+  | false => get a pos :: to_list_aux a (Int.add pos 1) (Int.sub len 1)
+  end.
+
+Ltac2 to_list (a : 'a array) := to_list_aux a 0 (length a).
+
+Ltac2 rec of_list_aux (ls : 'a list) (dst : 'a array) (pos : int) :=
+  match ls with
+  | [] => ()
+  | hd::tl =>
+      set dst pos hd;
+      of_list_aux tl dst (Int.add pos 1)
+  end.
+
+Ltac2 of_list (ls : 'a list) :=
+  (* Don't use List.length here because the List module might depend on Array some day *)
+  let rec list_length (ls : 'a list) :=
+    match ls with
+    | [] => 0
+    | _ :: tl => Int.add 1 (list_length tl)
+    end in
+  match ls with
+  | [] => empty ()
+  | hd::tl =>
+      let anew := make (list_length ls) hd in
+      of_list_aux ls anew 0;
+      anew
+  end.
+
+Ltac2 rec fold_left_aux (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => x
+  | 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 rec fold_right_aux (f : 'a -> 'b -> 'a) (x : 'a) (a : 'b array) (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)
+  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 rec exist_aux (p : 'a -> bool) (a : 'a array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => false
+  | false => match p (get a pos) with
+             | true => true
+             | false => exist_aux p a (Int.add pos 1) (Int.sub len 1)
+             end
+  end.
+
+(* Note: named exist (as in Coq library) rather than exists cause exists is a notation *)
+Ltac2 exist (p : 'a -> bool) (a : 'a array) := exist_aux p a 0 (length a).
+
+Ltac2 rec for_all_aux (p : 'a -> bool) (a : 'a array) (pos : int) (len : int) :=
+  match Int.equal len 0 with
+  | true => true
+  | false => match p (get a pos) with
+             | true => for_all_aux p a (Int.add pos 1) (Int.sub len 1)
+             | false => false
+             end
+  end.
+
+Ltac2 for_all (p : 'a -> bool) (a : 'a array) := for_all_aux p a 0 (length a).
+
+(* Note: we don't have (yet) a generic equality function in Ltac2 *)
+Ltac2 mem (eq : 'a -> 'a -> bool) (x : 'a) (a : 'a array) :=
+  exist (eq x) a.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 55cd7f7692..431589aa30 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -213,6 +213,14 @@ let define3 name r0 r1 r2 f = define_primitive name (arity_suc (arity_suc arity_
   f (Value.repr_to r0 x) (Value.repr_to r1 y) (Value.repr_to r2 z)
 end
 
+let define4 name r0 r1 r2 r3 f = define_primitive name (arity_suc (arity_suc (arity_suc arity_one))) begin fun x0 x1 x2 x3 ->
+  f (Value.repr_to r0 x0) (Value.repr_to r1 x1) (Value.repr_to r2 x2) (Value.repr_to r3 x3)
+end
+
+let define5 name r0 r1 r2 r3 r4 f = define_primitive name (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) begin fun x0 x1 x2 x3 x4 ->
+  f (Value.repr_to r0 x0) (Value.repr_to r1 x1) (Value.repr_to r2 x2) (Value.repr_to r3 x3) (Value.repr_to r4 x4)
+end
+
 (** Printing *)
 
 let () = define1 "print" pp begin fun pp ->
@@ -253,6 +261,10 @@ end
 
 (** Array *)
 
+let () = define0 "array_empty" begin
+  return (v_blk 0 (Array.of_list []))
+end
+
 let () = define2 "array_make" int valexpr begin fun n x ->
   if n < 0 || n > Sys.max_array_length then throw err_outofbounds
   else wrap (fun () -> v_blk 0 (Array.make n x))
@@ -272,6 +284,20 @@ let () = define2 "array_get" block int begin fun (_, v) n ->
   else wrap (fun () -> v.(n))
 end
 
+let () = define5 "array_blit" block int block int int begin fun (_, v0) s0 (_, v1) s1 l ->
+  if s0 < 0 || s0+l > Array.length v0 || s1 < 0 || s1+l > Array.length v1 || l<0 then throw err_outofbounds
+  else wrap_unit (fun () -> Array.blit v0 s0 v1 s1 l)
+end
+
+let () = define4 "array_fill" block int int valexpr begin fun (_, d) s l v ->
+  if s < 0 || s+l > Array.length d || l<0 then throw err_outofbounds
+  else wrap_unit (fun () -> Array.fill d s l v)
+end
+
+let () = define1 "array_concat" (list block) begin fun l ->
+  wrap (fun () -> v_blk 0 (Array.concat (List.map snd l)))
+end
+
 (** Ident *)
 
 let () = define2 "ident_equal" ident ident begin fun id1 id2 ->