Proper record type and accessors for transparent states.

This is documented in dev/doc/changes.md.

5 files changed, 57 insertions, 32 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c8028f713a..625a9a7277 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -72,11 +72,8 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = (Id.Pred.empty, Cpred.empty)
-let all_transparent = (Id.Pred.full, Cpred.full)
-
-let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
-let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+let all_opaque = TranspState.empty
+let all_transparent = TranspState.full
 
 module type RedFlagsSig = sig
   type reds
@@ -106,6 +103,8 @@ module RedFlags = (struct
   (* [r_const=(false,cl)] means only those in [cl] *)
   (* [r_delta=true] just mean [r_const=(true,[])] *)
 
+  open TranspState
+
   type reds = {
     r_beta : bool;
     r_delta : bool;
@@ -143,30 +142,30 @@ module RedFlags = (struct
     | ETA -> { red with r_eta = true }
     | DELTA -> { red with r_delta = true; r_const = all_transparent }
     | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.add kn l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } }
     | MATCH -> { red with r_match = true }
     | FIX -> { red with r_fix = true }
     | COFIX -> { red with r_cofix = true }
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.add id l1, l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } }
 
   let red_sub red = function
     | BETA -> { red with r_beta = false }
     | ETA -> { red with r_eta = false }
     | DELTA -> { red with r_delta = false }
     | CONST kn ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.remove kn l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } }
     | MATCH -> { red with r_match = false }
     | FIX -> { red with r_fix = false }
     | COFIX -> { red with r_cofix = false }
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Id.Pred.remove id l1, l2 }
+      let r = red.r_const in
+      { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } }
 
   let red_transparent red = red.r_const
 
@@ -179,12 +178,10 @@ module RedFlags = (struct
     | BETA -> incr_cnt red.r_beta beta
     | ETA -> incr_cnt red.r_eta eta
     | CONST kn ->
-	let (_,l) = red.r_const in
-	let c = Cpred.mem kn l in
+      let c = is_transparent_constant red.r_const kn in
 	incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
-	let (l,_) = red.r_const in
-	let c = Id.Pred.mem id l in
+      let c = is_transparent_variable red.r_const id in
 	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | MATCH -> incr_cnt red.r_match nb_match
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 9d41ee0695..26710a64d0 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
   a LetIn expression is Letin reduction *)
 
-
-
-val all_opaque      : TranspState.t
-val all_transparent : TranspState.t
-
-val is_transparent_variable : TranspState.t -> variable -> bool
-val is_transparent_constant : TranspState.t -> Constant.t -> bool
-
 (** Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ac78064235..c66beb49b8 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -81,7 +81,8 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu =
   let accu = Id.Map.fold fvar var_opacity accu in
   Cmap.fold fcst cst_opacity accu
 
-let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
+let get_transp_state { var_trstate; cst_trstate; _ } =
+  { TranspState.tr_var = var_trstate; tr_cst = cst_trstate }
 
 let dep_order l2r k1 k2 = match k1, k2 with
 | RelKey _, RelKey _ -> l2r
diff --git a/kernel/transpState.ml b/kernel/transpState.ml
index 9acb7244f7..9661dace6a 100644
--- a/kernel/transpState.ml
+++ b/kernel/transpState.ml
@@ -10,9 +10,36 @@
 
 open Names
 
-type t = Id.Pred.t * Cpred.t
+type t = {
+  tr_var : Id.Pred.t;
+  tr_cst : Cpred.t;
+}
 
-let empty = (Id.Pred.empty, Cpred.empty)
-let full = (Id.Pred.full, Cpred.full)
-let var_full = (Id.Pred.full, Cpred.empty)
-let cst_full = (Id.Pred.empty, Cpred.full)
+let empty = {
+  tr_var = Id.Pred.empty;
+  tr_cst = Cpred.empty;
+}
+
+let full = {
+  tr_var = Id.Pred.full;
+  tr_cst = Cpred.full;
+}
+
+let var_full = {
+  tr_var = Id.Pred.full;
+  tr_cst = Cpred.empty;
+}
+
+let cst_full = {
+  tr_var = Id.Pred.empty;
+  tr_cst = Cpred.full;
+}
+
+let is_empty ts =
+  Id.Pred.is_empty ts.tr_var && Cpred.is_empty ts.tr_cst
+
+let is_transparent_variable ts id =
+  Id.Pred.mem id ts.tr_var
+
+let is_transparent_constant ts cst =
+  Cpred.mem cst ts.tr_cst
diff --git a/kernel/transpState.mli b/kernel/transpState.mli
index a8d301549b..f2999c6869 100644
--- a/kernel/transpState.mli
+++ b/kernel/transpState.mli
@@ -11,7 +11,10 @@
 open Names
 
 (** Sets of names *)
-type t = Id.Pred.t * Cpred.t
+type t = {
+  tr_var : Id.Pred.t;
+  tr_cst : Cpred.t;
+}
 
 val empty : t
 (** Everything opaque *)
@@ -24,3 +27,8 @@ val var_full : t
 
 val cst_full : t
 (** All constant transparent *)
+
+val is_empty : t -> bool
+
+val is_transparent_variable : t -> Id.t -> bool
+val is_transparent_constant : t -> Constant.t -> bool