diff --git a/doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst b/doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst new file mode 100644 index 000000000000..4f18a15bcdde --- /dev/null +++ b/doc/changelog/06-Ltac2-language/22260-ltac2-constr-is-kind-Added.rst @@ -0,0 +1,4 @@ +- **Added:** + Ltac2 functions ``Constr.is_rel``, ``Constr.is_meta``, ``Constr.is_cast``, ``Constr.is_prod``, ``Constr.is_lambda``, ``Constr.is_letin``, ``Constr.is_app`` and ``Constr.is_case`` + (`#22260 `_, + by Jason Gross). diff --git a/test-suite/ltac2/constr_is_kind.v b/test-suite/ltac2/constr_is_kind.v new file mode 100644 index 000000000000..9fabadc4dbf2 --- /dev/null +++ b/test-suite/ltac2/constr_is_kind.v @@ -0,0 +1,20 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Type exn ::= [ Regression_Test_Failure ]. +Ltac2 check (b : bool) := if b then () else Control.throw Regression_Test_Failure. + +Ltac2 Eval check (Constr.is_prod constr:(nat -> nat)). +Ltac2 Eval check (Constr.is_prod constr:(forall n : nat, n = n)). +Ltac2 Eval check (Bool.neg (Constr.is_prod constr:(fun n : nat => n))). +Ltac2 Eval check (Constr.is_lambda constr:(fun n : nat => n)). +Ltac2 Eval check (Bool.neg (Constr.is_lambda constr:(nat -> nat))). +Ltac2 Eval check (Constr.is_letin constr:(let x := 1 in x)). +Ltac2 Eval check (Bool.neg (Constr.is_letin constr:(S 0))). +Ltac2 Eval check (Constr.is_app constr:(S 0)). +Ltac2 Eval check (Bool.neg (Constr.is_app constr:(S))). +Ltac2 Eval check (Constr.is_case constr:(match 0 with 0 => 0 | S n => n end)). +Ltac2 Eval check (Bool.neg (Constr.is_case constr:(S 0))). +Ltac2 Eval check (Constr.is_rel (Constr.Unsafe.make (Constr.Unsafe.Rel 1))). +Ltac2 Eval check (Bool.neg (Constr.is_rel constr:(0))). +Ltac2 Eval check (Bool.neg (Constr.is_meta constr:(0))). +Ltac2 Eval check (Bool.neg (Constr.is_cast constr:(S 0))). diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v index ce39400e7082..bae4c954caa0 100644 --- a/theories/Ltac2/Constr.v +++ b/theories/Ltac2/Constr.v @@ -600,3 +600,51 @@ Ltac2 is_sort(c: constr) := | Unsafe.Sort _ => true | _ => false end. + +Ltac2 is_rel(c: constr) := + match Unsafe.kind c with + | Unsafe.Rel _ => true + | _ => false + end. + +Ltac2 is_meta(c: constr) := + match Unsafe.kind c with + | Unsafe.Meta _ => true + | _ => false + end. + +Ltac2 is_cast(c: constr) := + match Unsafe.kind c with + | Unsafe.Cast _ _ _ => true + | _ => false + end. + +Ltac2 is_prod(c: constr) := + match Unsafe.kind c with + | Unsafe.Prod _ _ => true + | _ => false + end. + +Ltac2 is_lambda(c: constr) := + match Unsafe.kind c with + | Unsafe.Lambda _ _ => true + | _ => false + end. + +Ltac2 is_letin(c: constr) := + match Unsafe.kind c with + | Unsafe.LetIn _ _ _ => true + | _ => false + end. + +Ltac2 is_app(c: constr) := + match Unsafe.kind c with + | Unsafe.App _ _ => true + | _ => false + end. + +Ltac2 is_case(c: constr) := + match Unsafe.kind c with + | Unsafe.Case _ _ _ _ _ => true + | _ => false + end.