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

Fixes #13963

4 files changed, 66 insertions, 0 deletions

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