Merge PR coq#17777: Expose [Evarconv.unify] as an Ltac2 primitive.

Reviewed-by: ppedrot
Reviewed-by: SkySkimmer
Ack-by: Janno
Ack-by: Blaisorblade
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

doc/changelog/06-Ltac2-language/17777-evarconv-and-transparent-state.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  new standard library modules `Ltac2.Unification` and `Ltac2.TransparentState`
+  providing access to "Evarconv" unification, including the configuration of the
+  transparency state
+  (`#17777 <https://github.com/coq/coq/pull/17777>`_,
+  by Rodolphe Lepigre).

doc/stdlib/index-list.html.template

@@ -697,7 +697,9 @@ through the <tt>Require Import</tt> command.</p>
     user-contrib/Ltac2/Proj.v
     user-contrib/Ltac2/Std.v
     user-contrib/Ltac2/String.v
+    user-contrib/Ltac2/TransparentState.v
     user-contrib/Ltac2/Uint63.v
+    user-contrib/Ltac2/Unification.v
   </dd>
 
   <dt> <b>Unicode</b>:

plugins/ltac2/tac2ffi.ml

@@ -114,6 +114,7 @@ let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1"
 let val_uint63 = Val.create "uint63"
 let val_float = Val.create "float"
 let val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag = Val.create "ind_data"
+let val_transparent_state : TransparentState.t Val.tag = Val.create "transparent_state"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with

plugins/ltac2/tac2ffi.mli

@@ -219,6 +219,7 @@ val val_float : Float64.t Val.tag
 val val_ltac1 : Geninterp.Val.t Val.tag
 
 val val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag
+val val_transparent_state : TransparentState.t Val.tag
 
 val val_exn : Exninfo.iexn Tac2dyn.Val.tag
 (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]

plugins/ltac2/tac2stdlib.ml

@@ -572,3 +572,26 @@ end
 let () = define_prim2 "tac_unify" constr constr begin fun x y ->
   Tac2tactics.unify x y
 end
+
+(** Tactics for [Ltac2/TransparentState.v]. *)
+
+let transparent_state = Tac2ffi.repr_ext Tac2ffi.val_transparent_state
+
+let () =
+  let tac _ =
+    Tac2tactics.current_transparent_state () >>= fun ts ->
+    return (Tac2ffi.of_ext Tac2ffi.val_transparent_state ts)
+  in
+  Tac2env.define_primitive (pname "current_transparent_state") (mk_closure_val arity_one tac)
+
+let () =
+  let v = Tac2ffi.of_ext Tac2ffi.val_transparent_state TransparentState.full in
+  Tac2env.define_primitive (pname "full_transparent_state") v
+
+let () =
+  let v = Tac2ffi.of_ext Tac2ffi.val_transparent_state TransparentState.empty in
+  Tac2env.define_primitive (pname "empty_transparent_state") v
+
+(** Tactics around Evarconv unification (in [Ltac2/Unification.v]). *)
+
+let () = define_prim3 "evarconv_unify" transparent_state constr constr Tac2tactics.evarconv_unify

plugins/ltac2/tac2tactics.ml

@@ -405,6 +405,13 @@ let typeclasses_eauto strategy depth dbs =
 
 let unify x y = Tactics.unify x y
 
+let current_transparent_state () =
+  Proofview.tclENV >>= fun env ->
+  let state = Conv_oracle.get_transp_state (Environ.oracle env) in
+  Proofview.tclUNIT state
+
+let evarconv_unify state x y = Tactics.evarconv_unify ~state x y
+
 (** Inversion *)
 
 let inversion knd arg pat ids =

plugins/ltac2/tac2tactics.mli

@@ -121,3 +121,7 @@ val unify : constr -> constr -> unit tactic
 val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic
+
+val current_transparent_state : unit -> TransparentState.t tactic
+
+val evarconv_unify : TransparentState.t -> constr -> constr -> unit tactic

tactics/tactics.ml

@@ -5323,6 +5323,19 @@ let unify ?(state=TransparentState.full) x y =
     Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
+let evarconv_unify ?(state=TransparentState.full) ?(with_ho=true) x y =
+  Proofview.Goal.enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Proofview.Goal.sigma gl in
+  try
+    let flags = Evarconv.default_flags_of state in
+    let sigma = Evarconv.unify ~flags ~with_ho env sigma Conversion.CONV x y in
+    Proofview.Unsafe.tclEVARS sigma
+  with e when noncritical e ->
+    let e, info = Exninfo.capture e in
+    Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None)))
+  end
+
 (** [tclWRAPFINALLY before tac finally] runs [before] before each
     entry-point of [tac] and passes the result of [before] to
     [finally], which is then run at each exit-point of [tac],

tactics/tactics.mli

@@ -405,6 +405,7 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
 
 val unify           : ?state:TransparentState.t -> constr -> constr -> unit Proofview.tactic
+val evarconv_unify : ?state:TransparentState.t -> ?with_ho:bool -> constr -> constr -> unit Proofview.tactic
 
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> unit Proofview.tactic

test-suite/ltac2/std_tactics.v

@@ -28,6 +28,28 @@ Proof.
   end.
 Abort.
 
+Goal forall (x: nat), exists y, f x = g y.
+Proof.
+  intros.
+  eexists.
+  Unification.unify TransparentState.full 'f 'g.
+  lazy_match! goal with
+  | [ |- ?a ?b = ?rhs ] => Unification.unify_with_full_ts '($a $b) rhs
+  end.
+Abort.
+
+Goal True.
+Proof.
+  Fail Unification.unify TransparentState.empty '(1 + 1) '2.
+  Unification.unify TransparentState.full '(1 + 1) '2.
+  Unification.unify (TransparentState.current ()) '(1 + 1) '2.
+  Opaque Nat.add.
+  Fail Unification.unify (TransparentState.current ()) '(1 + 1) '2.
+  Succeed Unification.unify TransparentState.full '(1 + 1) '2.
+  exact I.
+Qed.
+
+
 (* Test that by clause of assert doesn't eat all semicolons:
    https://github.com/coq/coq/issues/17491 *)
 Goal forall (a: nat), a = a.

user-contrib/Ltac2/Ltac2.v

@@ -37,5 +37,7 @@ Require Ltac2.String.
 Require Ltac2.Uint63.
 Require Ltac2.FSet.
 Require Ltac2.FMap.
+Require Ltac2.TransparentState.
+Require Ltac2.Unification.
 
 Require Export Ltac2.Notations.

user-contrib/Ltac2/TransparentState.v

@@ -0,0 +1,27 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+(** Abstract type representing a transparency state. *)
+Ltac2 Type t.
+
+(** [empty] is the empty transparency state (all constants are opaque). *)
+Ltac2 @ external empty : t :=
+  "coq-core.plugins.ltac2" "empty_transparent_state".
+
+(** [full] is the full transparency state (all constants are transparent). *)
+Ltac2 @ external full : t :=
+  "coq-core.plugins.ltac2" "full_transparent_state".
+
+(** [current ()] gives the transparency state of the goal, which is influenced
+    by, e.g., the [Strategy] command, or the [with_strategy] Ltac tactic. *)
+Ltac2 @ external current : unit -> t :=
+  "coq-core.plugins.ltac2" "current_transparent_state".

user-contrib/Ltac2/Unification.v

@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+Require Ltac2.TransparentState.
+
+(** [unify ts c1 c2] unifies [c1] and [c2] (using Evarconv unification), which
+    may have the effect of instantiating evars. If the [c1] and [c2] cannot be
+    unified, an [Internal] exception is raised. *)
+Ltac2 @ external unify : TransparentState.t -> constr -> constr -> unit :=
+  "coq-core.plugins.ltac2" "evarconv_unify".
+
+(** [unify_with_full_ts] is like [unify TransparentState.full]. *)
+Ltac2 unify_with_full_ts : constr -> constr -> unit := fun c1 c2 =>
+  unify TransparentState.full c1 c2.
+
+(** [unify_with_current_ts] is like [unify (TransparentState.current ())]. *)
+Ltac2 unify_with_current_ts : constr -> constr -> unit := fun c1 c2 =>
+  unify (TransparentState.current ()) c1 c2.