Skip to content

Commit d6fda2f

Browse files
coqbot-app[bot]SkySkimmer
coqbot-app[bot]
and
SkySkimmer
authored
Merge PR rocq-prover#21558: ltac2: operations to manipulate transparent states
Reviewed-by: SkySkimmer Ack-by: ppedrot Ack-by: thomas-lamiaux Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
2 parents 53a055c + b1221ca commit d6fda2f

File tree

3 files changed

+148
-3
lines changed

3 files changed

+148
-3
lines changed

‎doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
- **Added:**
2+
Low-level operations to manipulate transparent states:
3+
1. Set-like operations (union, intersection, difference).
4+
2. Operations to add/remove/test membership of constants, variables, and primitive projections.
5+
(`#21558 <https://github.com/rocq-prover/rocq/pull/21558>`_,
6+
by Mathis Bouverot-Dupuis).

‎plugins/ltac2/tac2stdlib.ml‎

Lines changed: 80 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -710,16 +710,94 @@ let () =
710710

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

713+
let () =
714+
define "empty_transparent_state" (ret transparent_state) TransparentState.empty
715+
716+
let () =
717+
define "full_transparent_state" (ret transparent_state) TransparentState.full
718+
713719
let () =
714720
define "current_transparent_state"
715721
(unit @-> tac transparent_state)
716722
Tac2tactics.current_transparent_state
717723

718724
let () =
719-
define "full_transparent_state" (ret transparent_state) TransparentState.full
725+
define "union_transparent_state"
726+
(transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
727+
{ tr_var = Id.Pred.union ts1.tr_var ts2.tr_var ;
728+
tr_cst = Cpred.union ts1.tr_cst ts2.tr_cst ;
729+
tr_prj = PRpred.union ts1.tr_prj ts2.tr_prj }
720730

721731
let () =
722-
define "empty_transparent_state" (ret transparent_state) TransparentState.empty
732+
define "inter_transparent_state"
733+
(transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
734+
{ tr_var = Id.Pred.inter ts1.tr_var ts2.tr_var ;
735+
tr_cst = Cpred.inter ts1.tr_cst ts2.tr_cst ;
736+
tr_prj = PRpred.inter ts1.tr_prj ts2.tr_prj }
737+
738+
let () =
739+
define "diff_transparent_state"
740+
(transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
741+
{ tr_var = Id.Pred.diff ts1.tr_var ts2.tr_var ;
742+
tr_cst = Cpred.diff ts1.tr_cst ts2.tr_cst ;
743+
tr_prj = PRpred.diff ts1.tr_prj ts2.tr_prj }
744+
745+
let () =
746+
define "add_constant_transparent_state"
747+
(constant @-> transparent_state @-> ret transparent_state) @@ fun c ts ->
748+
{ tr_var = ts.tr_var ;
749+
tr_cst = Cpred.add c ts.tr_cst ;
750+
tr_prj = ts.tr_prj }
751+
752+
let () =
753+
define "add_proj_transparent_state"
754+
(projection @-> transparent_state @-> ret transparent_state) @@ fun p ts ->
755+
{ tr_var = ts.tr_var ;
756+
tr_cst = ts.tr_cst ;
757+
tr_prj = PRpred.add (Projection.repr p) ts.tr_prj }
758+
759+
let () =
760+
define "add_var_transparent_state"
761+
(ident @-> transparent_state @-> ret transparent_state) @@ fun v ts ->
762+
{ tr_var = Id.Pred.add v ts.tr_var ;
763+
tr_cst = ts.tr_cst ;
764+
tr_prj = ts.tr_prj }
765+
766+
let () =
767+
define "remove_constant_transparent_state"
768+
(constant @-> transparent_state @-> ret transparent_state) @@ fun c ts ->
769+
{ tr_var = ts.tr_var ;
770+
tr_cst = Cpred.remove c ts.tr_cst ;
771+
tr_prj = ts.tr_prj }
772+
773+
let () =
774+
define "remove_proj_transparent_state"
775+
(projection @-> transparent_state @-> ret transparent_state) @@ fun p ts ->
776+
{ tr_var = ts.tr_var ;
777+
tr_cst = ts.tr_cst ;
778+
tr_prj = PRpred.remove (Projection.repr p) ts.tr_prj }
779+
780+
let () =
781+
define "remove_var_transparent_state"
782+
(ident @-> transparent_state @-> ret transparent_state) @@ fun v ts ->
783+
{ tr_var = Id.Pred.remove v ts.tr_var ;
784+
tr_cst = ts.tr_cst ;
785+
tr_prj = ts.tr_prj }
786+
787+
let () =
788+
define "mem_constant_transparent_state"
789+
(constant @-> transparent_state @-> ret bool) @@ fun c ts ->
790+
Cpred.mem c ts.tr_cst
791+
792+
let () =
793+
define "mem_proj_transparent_state"
794+
(projection @-> transparent_state @-> ret bool) @@ fun p ts ->
795+
PRpred.mem (Projection.repr p) ts.tr_prj
796+
797+
let () =
798+
define "mem_var_transparent_state"
799+
(ident @-> transparent_state @-> ret bool) @@ fun v ts ->
800+
Id.Pred.mem v ts.tr_var
723801

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

‎theories/Ltac2/TransparentState.v‎

Lines changed: 62 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010

1111
Require Import Ltac2.Init.
1212

13-
(** Abstract type representing a transparency state. *)
13+
(** Abstract type representing a transparency state. A transparency state
14+
is a set of variables, constants, and primitive projections. *)
1415
Ltac2 Type t.
1516

1617
(** [empty] is the empty transparency state (all constants are opaque). *)
@@ -25,3 +26,63 @@ Ltac2 @ external full : t :=
2526
by, e.g., the [Strategy] command, or the [with_strategy] Ltac tactic. *)
2627
Ltac2 @ external current : unit -> t :=
2728
"rocq-runtime.plugins.ltac2" "current_transparent_state".
29+
30+
(** [union t1 t2] builds a transparency state containing all the variables,
31+
constants, and primitive projections which are either in [t1] or in [t2]. *)
32+
Ltac2 @ external union : t -> t -> t :=
33+
"rocq-runtime.plugins.ltac2" "union_transparent_state".
34+
35+
(** [inter t1 t2] builds a transparency state containing all the variables,
36+
constants, and primitive projections which are both in [t1] and in [t2]. *)
37+
Ltac2 @ external inter : t -> t -> t :=
38+
"rocq-runtime.plugins.ltac2" "inter_transparent_state".
39+
40+
(** [diff t1 t2] builds a transparency state containing all the variables,
41+
constants, and primitive projections which are in [t1] but not in [t2]. *)
42+
Ltac2 @ external diff : t -> t -> t :=
43+
"rocq-runtime.plugins.ltac2" "diff_transparent_state".
44+
45+
(** [add_constant c t] adds the constant [c] to the transparency state [t].
46+
Does nothing if the constant is already present. *)
47+
Ltac2 @ external add_constant : constant -> t -> t :=
48+
"rocq-runtime.plugins.ltac2" "add_constant_transparent_state".
49+
50+
(** [add_proj p t] adds the primitive projection [p] to the transparency
51+
state [t]. Does nothing if the projection is already present. *)
52+
Ltac2 @ external add_proj : projection -> t -> t :=
53+
"rocq-runtime.plugins.ltac2" "add_proj_transparent_state".
54+
55+
(** [add_var p t] adds the local variable [v] to the transparency state [t].
56+
Does nothing if the variable is already present. *)
57+
Ltac2 @ external add_var : ident -> t -> t :=
58+
"rocq-runtime.plugins.ltac2" "add_var_transparent_state".
59+
60+
(** [remove_constant c t] removes the constant [c] from the transparency
61+
state [t]. Does nothing if the constant is not present. *)
62+
Ltac2 @ external remove_constant : constant -> t -> t :=
63+
"rocq-runtime.plugins.ltac2" "remove_constant_transparent_state".
64+
65+
(** [remove_proj p t] removes the primitive projection [p] from the
66+
transparency state [t]. Does nothing if the projection is not present. *)
67+
Ltac2 @ external remove_proj : projection -> t -> t :=
68+
"rocq-runtime.plugins.ltac2" "remove_proj_transparent_state".
69+
70+
(** [remove_var p t] removes the local variable [v] from the transparency
71+
state [t]. Does nothing if the variable is not present. *)
72+
Ltac2 @ external remove_var : ident -> t -> t :=
73+
"rocq-runtime.plugins.ltac2" "remove_var_transparent_state".
74+
75+
(** [mem_constant c t] checks whether the constant [c] is present in the
76+
transparency state [t]. *)
77+
Ltac2 @ external mem_constant : constant -> t -> bool :=
78+
"rocq-runtime.plugins.ltac2" "mem_constant_transparent_state".
79+
80+
(** [mem_proj p t] checks whether the primitive projection [p] is present in the
81+
transparency state [t]. *)
82+
Ltac2 @ external mem_proj : projection -> t -> bool :=
83+
"rocq-runtime.plugins.ltac2" "mem_proj_transparent_state".
84+
85+
(** [mem_var v t] checks whether the local variable [v] is present in the
86+
transparency state [t]. *)
87+
Ltac2 @ external mem_var : ident -> t -> bool :=
88+
"rocq-runtime.plugins.ltac2" "mem_var_transparent_state".

0 commit comments

Comments
 (0)