Proper record type and accessors for transparent states.

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

dev/doc/changes.md

@@ -19,6 +19,10 @@ Names
   Constant.make3 has been removed, use Constant.make2
   Constant.repr3 has been removed, use Constant.repr2
 
+- `Names.transparent_state` has been moved to its own module `TranspState`.
+  This module gathers utility functions that used to be defined in several
+  places.
+
 Coqlib:
 
 - Most functions from the `Coqlib` module have been deprecated in favor of

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

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

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

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

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

plugins/firstorder/ground.ml

@@ -18,16 +18,16 @@ open Tacticals.New
 open Globnames
 
 let update_flags ()=
-  let f acc coe =
-    match coe.Classops.coe_value with
-    | ConstRef c -> Names.Cpred.add c acc
-    | _ -> acc
+  let open TranspState in
+  let f accu coe = match coe.Classops.coe_value with
+    | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+    | _ -> accu
   in
-    let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
+  let flags = List.fold_left f TranspState.full (Classops.coercions ()) in
     red_flags:=
     CClosure.RedFlags.red_add_transparent
       CClosure.betaiotazeta
-      (Names.Id.Pred.full,Names.Cpred.complement pred)
+      flags
 
 let ground_tac solver startseq =
   Proofview.Goal.enter begin fun gl ->

plugins/ltac/rewrite.ml

@@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) =
 
 let rewrite_db = "rewrite"
 
-let conv_transparent_state = (Id.Pred.empty, Cpred.full)
+let conv_transparent_state = TranspState.cst_full
 
 let rewrite_transparent_state () =
   Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)

pretyping/evarconv.ml

@@ -16,7 +16,6 @@ open Termops
 open Environ
 open EConstr
 open Vars
-open CClosure
 open Reduction
 open Reductionops
 open Recordops
@@ -74,14 +73,14 @@ let coq_unit_judge =
 
 let unfold_projection env evd ts p c =
   let cst = Projection.constant p in
-    if is_transparent_constant ts cst then
+    if TranspState.is_transparent_constant ts cst then
       Some (mkProj (Projection.unfold p, c))
     else None
 
 let eval_flexible_term ts env evd c =
   match EConstr.kind evd c with
   | Const (c, u) ->
-      if is_transparent_constant ts c
+      if TranspState.is_transparent_constant ts c
       then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
       else None
   | Rel n ->
@@ -91,7 +90,7 @@ let eval_flexible_term ts env evd c =
        with Not_found -> None)
   | Var id ->
       (try
-	 if is_transparent_variable ts id then
+         if TranspState.is_transparent_variable ts id then
 	   env |> lookup_named id |> NamedDecl.get_value
 	 else None
        with Not_found -> None)

pretyping/reductionops.ml

@@ -675,10 +675,6 @@ let apply_subst recfun env sigma refold cst_l t stack =
 let stacklam recfun env sigma t stack =
   apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
 
-let beta_app sigma (c,l) =
-  let zip s = Stack.zip sigma s in
-  stacklam zip [] sigma c (Stack.append_app l Stack.empty)
-
 let beta_applist sigma (c,l) =
   let zip s = Stack.zip sigma s in
   stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)
@@ -1681,25 +1677,6 @@ let meta_reducible_instance evd b =
   if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
   else irec b.rebus
 
-
-let head_unfold_under_prod ts env sigma c =
-  let unfold (cst,u) =
-    let cstu = (cst, EInstance.kind sigma u) in
-    if Cpred.mem cst (snd ts) then
-      match constant_opt_value_in env cstu with
-	| Some c -> EConstr.of_constr c
-	| None -> mkConstU (cst, u)
-    else mkConstU (cst, u) in
-  let rec aux c =
-    match EConstr.kind sigma c with
-      | Prod (n,t,c) -> mkProd (n,aux t, aux c)
-      | _ ->
-	  let (h,l) = decompose_app_vect sigma c in
-	  match EConstr.kind sigma h with
-	    | Const cst -> beta_app sigma (unfold cst, l)
-	    | _ -> c in
-  aux c
-
 let betazetaevar_applist sigma n c l =
   let rec stacklam n env t stack =
     if Int.equal n 0 then applist (substl env t, stack) else

pretyping/reductionops.mli

@@ -302,7 +302,6 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TranspState.t ->
 val whd_meta : local_reduction_function
 val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
 val instance : evar_map -> constr Metamap.t -> constr -> constr
-val head_unfold_under_prod : TranspState.t -> reduction_function
 val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)

pretyping/tacred.ml

@@ -638,7 +638,7 @@ let whd_nothing_for_iota env sigma s =
       | Meta ev ->
         (try whrec (Evd.meta_value sigma ev, stack)
 	with Not_found -> s)
-      | Const (const, u) when is_transparent_constant TranspState.full const ->
+      | Const (const, u) ->
           let u = EInstance.kind sigma u in
 	  (match constant_opt_value_in env (const, u) with
 	     | Some  body -> whrec (EConstr.of_constr body, stack)

pretyping/unification.ml

@@ -504,16 +504,16 @@ let key_of env sigma b flags f =
   if subterm_restriction b flags then None else
   match EConstr.kind sigma f with
   | Const (cst, u) when is_transparent env (ConstKey cst) &&
-      (Cpred.mem cst (snd flags.modulo_delta)
+      (TranspState.is_transparent_constant flags.modulo_delta cst
        || Recordops.is_primitive_projection cst) ->
       let u = EInstance.kind sigma u in
       Some (IsKey (ConstKey (cst, u)))
   | Var id when is_transparent env (VarKey id) && 
-      Id.Pred.mem id (fst flags.modulo_delta) ->
+      TranspState.is_transparent_variable flags.modulo_delta id ->
     Some (IsKey (VarKey id))
   | Proj (p, c) when Projection.unfolded p
     || (is_transparent env (ConstKey (Projection.constant p)) &&
-       (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) ->
+       (TranspState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
     Some (IsProj (p, c))
   | _ -> None
 
@@ -550,7 +550,7 @@ let oracle_order env cf1 cf2 =
 
 let is_rigid_head sigma flags t =
   match EConstr.kind sigma t with
-  | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta))
+  | Const (cst,u) -> not (TranspState.is_transparent_constant flags.modulo_delta cst)
   | Ind (i,u) -> true
   | Construct _ -> true
   | Fix _ | CoFix _ -> true
@@ -633,11 +633,11 @@ let rec is_neutral env sigma ts t =
     | Const (c, u) ->
       not (Environ.evaluable_constant c env) ||
       not (is_transparent env (ConstKey c)) ||
-      not (Cpred.mem c (snd ts))
+      not (TranspState.is_transparent_constant ts c)
     | Var id -> 
       not (Environ.evaluable_named id env) ||
       not (is_transparent env (VarKey id)) ||
-      not (Id.Pred.mem id (fst ts))
+      not (TranspState.is_transparent_variable ts id)
     | Rel n -> true
     | Evar _ | Meta _ -> true
     | Case (_, p, c, cl) -> is_neutral env sigma ts c
@@ -1120,10 +1120,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       | Some sigma -> ans
       | None ->
         if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
-        | Some (cv_id, cv_k), (dl_id, dl_k) ->
-          Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
-        | None,(dl_id, dl_k) ->
-          Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
+        | Some cv, dl ->
+          let open TranspState in
+          Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst
+        | None, dl -> TranspState.is_empty dl)
 	then error_cannot_unify env sigma (m, n) else None
   in 
     let a = match res with 
@@ -1263,8 +1263,8 @@ let applyHead env evd n c  =
 
 let is_mimick_head sigma ts f =
   match EConstr.kind sigma f with
-  | Const (c,u) -> not (CClosure.is_transparent_constant ts c)
-  | Var id -> not (CClosure.is_transparent_variable ts id)
+  | Const (c,u) -> not (TranspState.is_transparent_constant ts c)
+  | Var id -> not (TranspState.is_transparent_variable ts id)
   | (Rel _|Construct _|Ind _) -> true
   | _ -> false
 

printing/printer.ml

@@ -445,9 +445,9 @@ let pr_predicate pr_elt (b, elts) =
 let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
 let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p)
 
-let pr_transparent_state (ids, csts) =
-  hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
-	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+let pr_transparent_state ts =
+  hv 0 (str"VARIABLES: " ++ pr_idpred ts.TranspState.tr_var ++ fnl () ++
+        str"CONSTANTS: " ++ pr_cpred ts.TranspState.tr_cst ++ fnl ())
 
 (* display complete goal
  og_s has goal+sigma on the previous proof step for diffs

proofs/redexpr.ml

@@ -160,7 +160,7 @@ let make_flag env f =
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
     else (* Only rConst *)
-        let red = red_add_transparent (red_add red fDELTA) all_opaque in
+        let red = red_add_transparent (red_add red fDELTA) TranspState.empty in
 	List.fold_right
 	  (fun v red -> red_add red (make_flag_constant v))
 	  f.rConst red