Add Ltac2 Constr.is_prop, is_set, is_sprop, is_type and is_type_or_set

doc/changelog/06-Ltac2-language/22264-ltac2-constr-sort-predicates-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 functions ``Constr.is_prop``, ``Constr.is_set``, ``Constr.is_sprop``, ``Constr.is_type`` and ``Constr.is_type_or_set``
+  (`#22264 <https://github.com/rocq-prover/rocq/pull/22264>`_,
+  by Jason Gross).

test-suite/ltac2/constr_sort_predicates.v

@@ -0,0 +1,21 @@
+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_prop constr:(Prop)).
+Ltac2 Eval check (Bool.neg (Constr.is_prop constr:(Set))).
+Ltac2 Eval check (Bool.neg (Constr.is_prop constr:(Type))).
+Ltac2 Eval check (Constr.is_set constr:(Set)).
+Ltac2 Eval check (Bool.neg (Constr.is_set constr:(Prop))).
+Ltac2 Eval check (Constr.is_sprop constr:(SProp)).
+Ltac2 Eval check (Bool.neg (Constr.is_sprop constr:(Prop))).
+Ltac2 Eval check (Constr.is_type constr:(Type)).
+Ltac2 Eval check (Bool.neg (Constr.is_type constr:(Prop))).
+Ltac2 Eval check (Bool.neg (Constr.is_type constr:(Set))).
+Ltac2 Eval check (Bool.neg (Constr.is_type constr:(SProp))).
+Ltac2 Eval check (Bool.neg (Constr.is_type constr:(nat))).
+Ltac2 Eval check (Constr.is_type_or_set constr:(Set)).
+Ltac2 Eval check (Constr.is_type_or_set constr:(Type)).
+Ltac2 Eval check (Bool.neg (Constr.is_type_or_set constr:(Prop))).
+Ltac2 Eval check (Bool.neg (Constr.is_prop constr:(0))).

theories/Ltac2/Constr.v

@@ -600,3 +600,27 @@ Ltac2 is_sort(c: constr) :=
   | Unsafe.Sort _ => true
   | _ => false
   end.
+
+(** [is_prop c] returns [true] iff [c] is the sort [Prop]. *)
+Ltac2 is_prop (c : constr) : bool := equal c constr:(Prop).
+
+(** [is_set c] returns [true] iff [c] is the sort [Set]. *)
+Ltac2 is_set (c : constr) : bool := equal c constr:(Set).
+
+(** [is_sprop c] returns [true] iff [c] is the sort [SProp]. *)
+Ltac2 is_sprop (c : constr) : bool := equal c constr:(SProp).
+
+(** [is_type c] returns [true] iff [c] is a sort of the form
+    [Type@{u}], i.e. a sort other than [Prop], [Set] and [SProp]. *)
+Ltac2 is_type (c : constr) : bool :=
+  if is_sort c
+  then if is_prop c then false
+       else if is_set c then false
+       else if is_sprop c then false
+       else true
+  else false.
+
+(** [is_type_or_set c] returns [true] iff [c] is [Set] or a sort of
+    the form [Type@{u}]. *)
+Ltac2 is_type_or_set (c : constr) : bool :=
+  if is_type c then true else is_set c.