Merge PR #7925: Clean transparent state

12 files changed, 112 insertions, 57 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95546a83e1..7e73609996 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 = TransparentState.empty
+let all_transparent = TransparentState.full
 
 module type RedFlagsSig = sig
   type reds
@@ -93,8 +90,8 @@ module type RedFlagsSig = sig
   val no_red : reds
   val red_add : reds -> red_kind -> reds
   val red_sub : reds -> red_kind -> reds
-  val red_add_transparent : reds -> transparent_state -> reds
-  val red_transparent : reds -> transparent_state
+  val red_add_transparent : reds -> TransparentState.t -> reds
+  val red_transparent : reds -> TransparentState.t
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
   val red_projection : reds -> Projection.t -> bool
@@ -106,11 +103,13 @@ module RedFlags = (struct
   (* [r_const=(false,cl)] means only those in [cl] *)
   (* [r_delta=true] just mean [r_const=(true,[])] *)
 
+  open TransparentState
+
   type reds = {
     r_beta : bool;
     r_delta : bool;
     r_eta : bool;
-    r_const : transparent_state;
+    r_const : TransparentState.t;
     r_zeta : bool;
     r_match : bool;
     r_fix : 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 1ee4bccc25..b6c87b3732 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      : transparent_state
-val all_transparent : transparent_state
-
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> Constant.t -> bool
-
 (** Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
@@ -60,10 +52,10 @@ module type RedFlagsSig = sig
   val red_sub : reds -> red_kind -> reds
 
   (** Adds a reduction kind to a set *)
-  val red_add_transparent : reds -> transparent_state -> reds
+  val red_add_transparent : reds -> TransparentState.t -> reds
 
   (** Retrieve the transparent state of the reduction flags *)
-  val red_transparent : reds -> transparent_state
+  val red_transparent : reds -> TransparentState.t
 
   (** Build a reduction set from scratch = iter [red_add] on [no_red] *)
   val mkflags : red_kind list -> reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index ac78064235..fe82353b70 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; _ } =
+  { TransparentState.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/conv_oracle.mli b/kernel/conv_oracle.mli
index 67add5dd35..bc06cc21b6 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -41,5 +41,5 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle
 (** Fold over the non-transparent levels of the oracle. Order unspecified. *)
 val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
 
-val get_transp_state : oracle -> transparent_state
+val get_transp_state : oracle -> TransparentState.t
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index a18c5d1e20..54c239349d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,4 +1,5 @@
 Names
+TransparentState
 Uint31
 Univ
 UGraph
diff --git a/kernel/names.ml b/kernel/names.ml
index 18560d5f8d..b2d6a489a6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -715,13 +715,6 @@ let hcons_construct = Hashcons.simple_hcons Hconstruct.generate Hconstruct.hcons
 
 (*****************)
 
-type transparent_state = Id.Pred.t * Cpred.t
-
-let empty_transparent_state = (Id.Pred.empty, Cpred.empty)
-let full_transparent_state = (Id.Pred.full, Cpred.full)
-let var_full_transparent_state = (Id.Pred.full, Cpred.empty)
-let cst_full_transparent_state = (Id.Pred.empty, Cpred.full)
-
 type 'a tableKey =
   | ConstKey of 'a
   | VarKey of Id.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 98995752a2..350db871d5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -510,14 +510,6 @@ type 'a tableKey =
   | VarKey of Id.t
   | RelKey of Int.t
 
-(** Sets of names *)
-type transparent_state = Id.Pred.t * Cpred.t
-
-val empty_transparent_state : transparent_state
-val full_transparent_state : transparent_state
-val var_full_transparent_state : transparent_state
-val cst_full_transparent_state : transparent_state
-
 type inv_rel_key = int (** index in the [rel_context] part of environment
 			  starting by the end, {e inverse}
 			  of de Bruijn indice *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5515ff9767..fbb481424f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -177,7 +177,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 
 (* functions of this type can be called from outside the kernel *)
 type 'a extended_conversion_function =
-  ?l2r:bool -> ?reds:Names.transparent_state -> env ->
+  ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
 
@@ -758,7 +758,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
 	()
 
 (* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
   let evars, univs = evars in
   if Flags.profile then
     let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
@@ -792,11 +792,11 @@ let infer_conv_universes =
       CProfile.profile8 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state)
+let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
     env univs t1 t2 = 
   infer_conv_universes CONV l2r evars ts env univs t1 t2
 
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) 
+let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 581e8bd88a..0408dbf057 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -31,7 +31,7 @@ exception NotConvertibleVect of int
 
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 type 'a extended_conversion_function = 
-  ?l2r:bool -> ?reds:Names.transparent_state -> env ->
+  ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
 
@@ -77,15 +77,15 @@ val conv_leq : types extended_conversion_function
 (** These conversion functions are used by module subtyping, which needs to infer
     universe constraints inside the kernel *)
 val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:Names.transparent_state -> constr infer_conversion_function
+  ?ts:TransparentState.t -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
-  ?ts:Names.transparent_state -> types infer_conversion_function
+  ?ts:TransparentState.t -> types infer_conversion_function
 
 (** Depending on the universe state functions, this might raise
   [UniverseInconsistency] in addition to [NotConvertible] (for better error
   messages). *)
 val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
-  Names.transparent_state -> (constr,'a) generic_conversion_function
+  TransparentState.t -> (constr,'a) generic_conversion_function
 
 val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
 val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
diff --git a/kernel/transparentState.ml b/kernel/transparentState.ml
new file mode 100644
index 0000000000..9661dace6a
--- /dev/null
+++ b/kernel/transparentState.ml
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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)         *)
+(************************************************************************)
+
+open Names
+
+type t = {
+  tr_var : Id.Pred.t;
+  tr_cst : Cpred.t;
+}
+
+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/transparentState.mli b/kernel/transparentState.mli
new file mode 100644
index 0000000000..f2999c6869
--- /dev/null
+++ b/kernel/transparentState.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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)         *)
+(************************************************************************)
+
+open Names
+
+(** Sets of names *)
+type t = {
+  tr_var : Id.Pred.t;
+  tr_cst : Cpred.t;
+}
+
+val empty : t
+(** Everything opaque *)
+
+val full : t
+(** Everything transparent *)
+
+val var_full : t
+(** All variables transparent *)
+
+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
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index c1130e62c9..246c90c09d 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -191,7 +191,7 @@ let warn_bytecode_compiler_failed =
 let vm_conv_gen cv_pb env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      full_transparent_state env univs t1 t2
+      TransparentState.full env univs t1 t2
   else
   try
     let v1 = val_of_constr env t1 in
@@ -200,7 +200,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
   with Not_found | Invalid_argument _ ->
     warn_bytecode_compiler_failed ();
     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-      full_transparent_state env univs t1 t2
+      TransparentState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in