implement is_const, is_var, ... etc and has_evar for Ltac2

Fixes #13963

6 files changed, 84 insertions, 3 deletions

diff --git a/test-suite/ltac2/evar.v b/test-suite/ltac2/evar.v
new file mode 100644
index 0000000000..2c82673edd
--- /dev/null
+++ b/test-suite/ltac2/evar.v
@@ -0,0 +1,17 @@
+Require Import Ltac2.Ltac2.
+
+Goal exists (a: nat), a = 1.
+Proof.
+  match! goal with
+  | [ |- ?g ] => Control.assert_false (Constr.has_evar g)
+  end.
+  eexists.
+  match! goal with
+  | [ |- ?g ] => Control.assert_true (Constr.has_evar g)
+  end.
+  match! goal with
+  | [ |- ?x = ?y ] =>
+    Control.assert_true (Constr.is_evar x);
+    Control.assert_false (Constr.is_evar y)
+  end.
+Abort.
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v
index 7b3a460c8c..9108871e28 100644
--- a/test-suite/ltac2/rebind.v
+++ b/test-suite/ltac2/rebind.v
@@ -26,12 +26,10 @@ Ltac2 rec nat_eq n m :=
   | S n => match m with | O => false | S m => nat_eq n m end
   end.
 
-Ltac2 Type exn ::= [ Assertion_failed ].
-
 Ltac2 assert_eq n m :=
   match nat_eq n m with
   | true => ()
-  | false => Control.throw Assertion_failed end.
+  | false => Control.throw Assertion_failure end.
 
 Ltac2 mutable x := O.
 Ltac2 y := x.
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 72cac900cd..fa056910b8 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -96,3 +96,54 @@ Ltac2 @ external in_context : ident -> constr -> (unit -> unit) -> constr := "lt
 
 Ltac2 @ external pretype : preterm -> constr := "ltac2" "constr_pretype".
 (** Pretype the provided preterm. Assumes the goal to be focussed. *)
+
+
+Ltac2 is_evar(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Evar _ _ => true
+  | _ => false
+  end.
+
+Ltac2 @ external has_evar : constr -> bool := "ltac2" "constr_has_evar".
+
+Ltac2 is_var(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Var _ => true
+  | _ => false
+  end.
+
+Ltac2 is_fix(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Fix _ _ _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_cofix(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.CoFix _ _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_ind(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Ind _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_constructor(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Constructor _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_proj(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Proj _ _ => true
+  | _ => false
+  end.
+
+Ltac2 is_const(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Constant _ _ => true
+  | _ => false
+  end.
diff --git a/user-contrib/Ltac2/Control.v b/user-contrib/Ltac2/Control.v
index 8b9d53a433..31c8871ff8 100644
--- a/user-contrib/Ltac2/Control.v
+++ b/user-contrib/Ltac2/Control.v
@@ -98,6 +98,12 @@ Ltac2 assert_bounds (msg : string) (test : bool) :=
   | false => throw_out_of_bounds msg
   end.
 
+Ltac2 assert_true b :=
+  if b then () else throw Assertion_failure.
+
+Ltac2 assert_false b :=
+  if b then throw Assertion_failure else ().
+
 (** Short form backtracks *)
 
 Ltac2 backtrack_tactic_failure (msg : string) :=
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index 097a0ca25f..19c89d7266 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -80,3 +80,6 @@ Ltac2 Type exn ::= [ Invalid_argument (message option) ].
 
 Ltac2 Type exn ::= [ Tactic_failure (message option) ].
 (** Generic error for tactic failure. *)
+
+Ltac2 Type exn ::= [ Assertion_failure ].
+(** Used to indicate that an Ltac2 function ran into a situation that should never occcur. *)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index bcf9ece7c8..fa7df5dfeb 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -755,6 +755,12 @@ let () = define1 "constr_binder_type" (repr_ext val_binder) begin fun (bnd, ty)
   return (of_constr ty)
 end
 
+let () = define1 "constr_has_evar" constr begin fun c ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = Evarutil.has_undefined_evars sigma c in
+  Proofview.tclUNIT (Value.of_bool b)
+end
+
 (** Patterns *)
 
 let empty_context = EConstr.mkMeta Constr_matching.special_meta