aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/ltac2/array_lib.v181
-rw-r--r--test-suite/output/Notations.out68
-rw-r--r--test-suite/output/Notations.v62
-rw-r--r--test-suite/output/Notations4.out8
-rw-r--r--test-suite/output/Notations4.v26
5 files changed, 343 insertions, 2 deletions
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/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..b870fa6f6f 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -137,3 +137,71 @@ end = p
: forall x : nat, x = x -> Prop
bar 0
: nat
+let k := rew [P] p in v in k
+ : P y
+let k := rew [P] p in v in k
+ : P y
+let k := rew <- [P] p in v' in k
+ : P x
+let k := rew [P] p in v in k
+ : P y
+let k := rew [P] p in v in k
+ : P y
+let k := rew <- [P] p in v' in k
+ : P x
+let k := rew [fun y : A => P y] p in v in k
+ : P y
+let k := rew [fun y : A => P y] p in v in k
+ : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+ : P x
+let k := rew [fun y : A => P y] p in v in k
+ : P y
+let k := rew [fun y : A => P y] p in v in k
+ : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+ : P x
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent <- [P'] p in v' in k
+ : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent <- [P'] p in v' in k
+ : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent <- [P'] p in v' in k
+ : P' x (eq_sym p)
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+ : P y p
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+ : P y p
+let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k
+ : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent [P] p in v in k
+ : P y p
+let k := rew dependent <- [P'] p in v' in k
+ : P' x (eq_sym p)
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+ : P y p
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+ : P y p
+let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k
+ : P' x (eq_sym p)
+rew dependent [P] p in v
+ : P y p
+rew dependent <- [P'] p in v'
+ : P' x (eq_sym p)
+rew dependent [fun a x => id (P a x)] p in v
+ : id (P y p)
+rew dependent <- [fun a p' => id (P' a p')] p in v'
+ : id (P' x (eq_sym p))
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adab324cf0..7d2f1e9ba8 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -251,11 +251,11 @@ Notation NONE := None.
Check (fun x => match x with SOME x => x | NONE => 0 end).
Notation NONE2 := (@None _).
-Notation SOME2 := (@Some _).
+Notation SOME2 := (@Some _).
Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
Notation NONE3 := @None.
-Notation SOME3 := @Some.
+Notation SOME3 := @Some.
Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end).
Notation "a :'" := (cons a) (at level 12).
@@ -300,3 +300,61 @@ Definition bar (a b : nat) := plus a b.
Notation "" := A (format "", only printing).
Check (bar A 0).
End M.
+
+(* Check eq notations *)
+Module EqNotationsCheck.
+ Import EqNotations.
+ Section nd.
+ Context (A : Type) (x : A) (P : A -> Type)
+ (y : A) (p : x = y) (v : P x) (v' : P y).
+
+ Check let k : P y := rew p in v in k.
+ Check let k : P y := rew -> p in v in k.
+ Check let k : P x := rew <- p in v' in k.
+ Check let k : P y := rew [P] p in v in k.
+ Check let k : P y := rew -> [P] p in v in k.
+ Check let k : P x := rew <- [P] p in v' in k.
+ Check let k : P y := rew [fun y => P y] p in v in k.
+ Check let k : P y := rew -> [fun y => P y] p in v in k.
+ Check let k : P x := rew <- [fun y => P y] p in v' in k.
+ Check let k : P y := rew [fun (y : A) => P y] p in v in k.
+ Check let k : P y := rew -> [fun (y : A) => P y] p in v in k.
+ Check let k : P x := rew <- [fun (y : A) => P y] p in v' in k.
+ End nd.
+ Section dep.
+ Context (A : Type) (x : A) (P : forall y, x = y -> Type)
+ (y : A) (p : x = y) (P' : forall x, y = x -> Type)
+ (v : P x eq_refl) (v' : P' y eq_refl).
+
+ Check let k : P y p := rew dependent p in v in k.
+ Check let k : P y p := rew dependent -> p in v in k.
+ Check let k : P' x (eq_sym p) := rew dependent <- p in v' in k.
+ Check let k : P y p := rew dependent [P] p in v in k.
+ Check let k : P y p := rew dependent -> [P] p in v in k.
+ Check let k : P' x (eq_sym p) := rew dependent <- [P'] p in v' in k.
+ Check let k : P y p := rew dependent [fun y p => P y p] p in v in k.
+ Check let k : P y p := rew dependent -> [fun y p => P y p] p in v in k.
+ Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => P' y p] p in v' in k.
+ Check let k : P y p := rew dependent [fun y p => id (P y p)] p in v in k.
+ Check let k : P y p := rew dependent -> [fun y p => id (P y p)] p in v in k.
+ Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => id (P' y p)] p in v' in k.
+ Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+ Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+ Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => P' x p)] p in v' in k.
+ Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+ Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+ Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => id (P' x p))] p in v' in k.
+ Check match p as x in _ = a return P a x with
+ | eq_refl => v
+ end.
+ Check match eq_sym p as p' in _ = a return P' a p' with
+ | eq_refl => v'
+ end.
+ Check match p as x in _ = a return id (P a x) with
+ | eq_refl => v
+ end.
+ Check match eq_sym p as p' in _ = a return id (P' a p') with
+ | eq_refl => v'
+ end.
+ End dep.
+End EqNotationsCheck.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 799d310fa7..43f88f42a5 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -63,3 +63,11 @@ fun '{| |} => true
: R -> bool
b = a
: Prop
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 26c7840a16..4de6ce19b4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -158,3 +158,29 @@ Check b = a.
End Test.
End L.
+
+Module M.
+
+(* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
+
+Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+ (and T1 (and T2 .. (and Tn True)..))
+ (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+ (and T1 (and T2 .. (and Tn True)..))
+ (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+ (and T1 (and T2 .. (and Tn True)..))
+ (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[v' Tn ']' } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+ (and T1 (and T2 .. (and Tn True)..))
+ (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+ (and T1 (and T2 .. (and Tn True)..))
+ (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'").
+
+End M.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:29:56 +0000