Skip to content

ltac2: operations to manipulate transparent states #21558

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 1 commit into from
Feb 3, 2026
Merged

ltac2: operations to manipulate transparent states #21558

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
- **Added:**
Low-level operations to manipulate transparent states:
1. Set-like operations (union, intersection, difference).
2. Operations to add/remove/test membership of constants, variables, and primitive projections.
(`#21558 <https://github.com/rocq-prover/rocq/pull/21558>`_,
by Mathis Bouverot-Dupuis).
82 changes: 80 additions & 2 deletions plugins/ltac2/tac2stdlib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -710,16 +710,94 @@ let () =

(** Tactics for [Ltac2/TransparentState.v]. *)

let () =
define "empty_transparent_state" (ret transparent_state) TransparentState.empty

let () =
define "full_transparent_state" (ret transparent_state) TransparentState.full

let () =
define "current_transparent_state"
(unit @-> tac transparent_state)
Tac2tactics.current_transparent_state

let () =
define "full_transparent_state" (ret transparent_state) TransparentState.full
define "union_transparent_state"
(transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
{ tr_var = Id.Pred.union ts1.tr_var ts2.tr_var ;
tr_cst = Cpred.union ts1.tr_cst ts2.tr_cst ;
tr_prj = PRpred.union ts1.tr_prj ts2.tr_prj }

let () =
define "empty_transparent_state" (ret transparent_state) TransparentState.empty
define "inter_transparent_state"
(transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
{ tr_var = Id.Pred.inter ts1.tr_var ts2.tr_var ;
tr_cst = Cpred.inter ts1.tr_cst ts2.tr_cst ;
tr_prj = PRpred.inter ts1.tr_prj ts2.tr_prj }

let () =
define "diff_transparent_state"
(transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
{ tr_var = Id.Pred.diff ts1.tr_var ts2.tr_var ;
tr_cst = Cpred.diff ts1.tr_cst ts2.tr_cst ;
tr_prj = PRpred.diff ts1.tr_prj ts2.tr_prj }

let () =
define "add_constant_transparent_state"
(constant @-> transparent_state @-> ret transparent_state) @@ fun c ts ->
{ tr_var = ts.tr_var ;
tr_cst = Cpred.add c ts.tr_cst ;
tr_prj = ts.tr_prj }

let () =
define "add_proj_transparent_state"
(projection @-> transparent_state @-> ret transparent_state) @@ fun p ts ->
{ tr_var = ts.tr_var ;
tr_cst = ts.tr_cst ;
tr_prj = PRpred.add (Projection.repr p) ts.tr_prj }

let () =
define "add_var_transparent_state"
(ident @-> transparent_state @-> ret transparent_state) @@ fun v ts ->
{ tr_var = Id.Pred.add v ts.tr_var ;
tr_cst = ts.tr_cst ;
tr_prj = ts.tr_prj }

let () =
define "remove_constant_transparent_state"
(constant @-> transparent_state @-> ret transparent_state) @@ fun c ts ->
{ tr_var = ts.tr_var ;
tr_cst = Cpred.remove c ts.tr_cst ;
tr_prj = ts.tr_prj }

let () =
define "remove_proj_transparent_state"
(projection @-> transparent_state @-> ret transparent_state) @@ fun p ts ->
{ tr_var = ts.tr_var ;
tr_cst = ts.tr_cst ;
tr_prj = PRpred.remove (Projection.repr p) ts.tr_prj }

let () =
define "remove_var_transparent_state"
(ident @-> transparent_state @-> ret transparent_state) @@ fun v ts ->
{ tr_var = Id.Pred.remove v ts.tr_var ;
tr_cst = ts.tr_cst ;
tr_prj = ts.tr_prj }

let () =
define "mem_constant_transparent_state"
(constant @-> transparent_state @-> ret bool) @@ fun c ts ->
Cpred.mem c ts.tr_cst

let () =
define "mem_proj_transparent_state"
(projection @-> transparent_state @-> ret bool) @@ fun p ts ->
PRpred.mem (Projection.repr p) ts.tr_prj

let () =
define "mem_var_transparent_state"
(ident @-> transparent_state @-> ret bool) @@ fun v ts ->
Id.Pred.mem v ts.tr_var

(** Tactics around Evarconv unification (in [Ltac2/Unification.v]). *)

Expand Down
63 changes: 62 additions & 1 deletion theories/Ltac2/TransparentState.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,8 @@

Require Import Ltac2.Init.

(** Abstract type representing a transparency state. *)
(** Abstract type representing a transparency state. A transparency state
is a set of variables, constants, and primitive projections. *)
Ltac2 Type t.

(** [empty] is the empty transparency state (all constants are opaque). *)
Expand All @@ -25,3 +26,63 @@ Ltac2 @ external full : t :=
by, e.g., the [Strategy] command, or the [with_strategy] Ltac tactic. *)
Ltac2 @ external current : unit -> t :=
"rocq-runtime.plugins.ltac2" "current_transparent_state".

(** [union t1 t2] builds a transparency state containing all the variables,
constants, and primitive projections which are either in [t1] or in [t2]. *)
Ltac2 @ external union : t -> t -> t :=
"rocq-runtime.plugins.ltac2" "union_transparent_state".

(** [inter t1 t2] builds a transparency state containing all the variables,
constants, and primitive projections which are both in [t1] and in [t2]. *)
Ltac2 @ external inter : t -> t -> t :=
"rocq-runtime.plugins.ltac2" "inter_transparent_state".

(** [diff t1 t2] builds a transparency state containing all the variables,
constants, and primitive projections which are in [t1] but not in [t2]. *)
Ltac2 @ external diff : t -> t -> t :=
"rocq-runtime.plugins.ltac2" "diff_transparent_state".
Comment on lines +30 to +43
Copy link
Contributor

@SkySkimmer SkySkimmer Jan 31, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if we should expose these operations. In #19117 there is some discussion about changing Hint Constants Opaque to set a default but not change constants which were explicitly set transparent, I'm not sure how well that would work with combining transparent states.

Copy link
Contributor

@thomas-lamiaux thomas-lamiaux Jan 31, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This low-level API are useful to a small minority of users that want a very fine control.
I would imagine, they would be interested in recovering the transparency state for some hint databases, and take the union or sth like that ? @andres-erbsen would you have such a need ?

Copy link
Member

@ppedrot ppedrot Jan 31, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@SkySkimmer this would typically be done at the HintDB API level, not the transparent state one AFAIU. I'm envisioning a system where we keep two different TS for each hintdb and switch one with the other with a flag. So I don't think exposing this kind of operations is problematic.


(** [add_constant c t] adds the constant [c] to the transparency state [t].
Does nothing if the constant is already present. *)
Ltac2 @ external add_constant : constant -> t -> t :=
"rocq-runtime.plugins.ltac2" "add_constant_transparent_state".

(** [add_proj p t] adds the primitive projection [p] to the transparency
state [t]. Does nothing if the projection is already present. *)
Ltac2 @ external add_proj : projection -> t -> t :=
"rocq-runtime.plugins.ltac2" "add_proj_transparent_state".

(** [add_var p t] adds the local variable [v] to the transparency state [t].
Does nothing if the variable is already present. *)
Ltac2 @ external add_var : ident -> t -> t :=
"rocq-runtime.plugins.ltac2" "add_var_transparent_state".

(** [remove_constant c t] removes the constant [c] from the transparency
state [t]. Does nothing if the constant is not present. *)
Ltac2 @ external remove_constant : constant -> t -> t :=
"rocq-runtime.plugins.ltac2" "remove_constant_transparent_state".

(** [remove_proj p t] removes the primitive projection [p] from the
transparency state [t]. Does nothing if the projection is not present. *)
Ltac2 @ external remove_proj : projection -> t -> t :=
"rocq-runtime.plugins.ltac2" "remove_proj_transparent_state".

(** [remove_var p t] removes the local variable [v] from the transparency
state [t]. Does nothing if the variable is not present. *)
Ltac2 @ external remove_var : ident -> t -> t :=
"rocq-runtime.plugins.ltac2" "remove_var_transparent_state".

(** [mem_constant c t] checks whether the constant [c] is present in the
transparency state [t]. *)
Ltac2 @ external mem_constant : constant -> t -> bool :=
"rocq-runtime.plugins.ltac2" "mem_constant_transparent_state".

(** [mem_proj p t] checks whether the primitive projection [p] is present in the
transparency state [t]. *)
Ltac2 @ external mem_proj : projection -> t -> bool :=
"rocq-runtime.plugins.ltac2" "mem_proj_transparent_state".

(** [mem_var v t] checks whether the local variable [v] is present in the
transparency state [t]. *)
Ltac2 @ external mem_var : ident -> t -> bool :=
"rocq-runtime.plugins.ltac2" "mem_var_transparent_state".