diff options
| -rw-r--r-- | doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst | 4 | ||||
| -rw-r--r-- | test-suite/ltac2/array_lib.v | 181 | ||||
| -rw-r--r-- | user-contrib/Ltac2/Array.v | 211 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 26 |
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 -> |