Adding a Print Strategy vernacular command. It allows to check the

transparent status of variables and constants.

6 files changed, 55 insertions, 2 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 6a3c1165f..850f06f87 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -75,6 +75,7 @@ type printable =
   | PrintAbout of reference or_by_notation
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
+  | PrintStrategy of reference or_by_notation option
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 32aaacb62..4f2631a66 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -54,6 +54,12 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
           else Cmap.add c l cst_opacity }
   | RelKey _ -> Errors.error "set_strategy: RelKey"
 
+let fold_strategy f { var_opacity; cst_opacity; } accu =
+  let fvar id lvl accu = f (VarKey id) lvl accu in
+  let fcst cst lvl accu = f (ConstKey cst) lvl accu in
+  let accu = Id.Map.fold fvar var_opacity accu in
+  Cmap.fold fcst cst_opacity accu
+
 let get_transp_state { var_opacity; cst_opacity } =
   (Id.Map.fold
     (fun id l ts -> if  l=Opaque then Id.Pred.remove id ts else ts)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 24797238d..cd8cd2cf7 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -35,5 +35,8 @@ val get_strategy : oracle -> 'a tableKey -> level
  * Level of RelKey constant cannot be set. *)
 val set_strategy : oracle -> 'a tableKey -> level -> oracle
 
+(** Fold over the non-transparent levels of the oracle. Order unspecified. *)
+val fold_strategy : (unit tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a
+
 val get_transp_state : oracle -> transparent_state
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b52dcdbd6..73b26b02d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -878,8 +878,9 @@ GEXTEND Gram
       | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid)
       | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid)
       | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid)
-      | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid) ] ]
-
+      | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid)
+      | IDENT "Strategy"; qid = smart_global -> PrintStrategy (Some qid)
+      | IDENT "Strategies" -> PrintStrategy None ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 430dfab4d..ecc80c2cf 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -459,6 +459,8 @@ let pr_printable = function
   in
   str cmd ++ spc() ++ pr_smart_global qid
 | PrintNamespace dp -> str "Print Namespace" ++ pr_dirpath dp
+| PrintStrategy None -> str "Print Strategies"
+| PrintStrategy (Some qid) -> str "Print Strategy" ++ pr_smart_global qid
 in
 
 let pr_using e = str (Proof_using.to_string e) in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 395119083..b948a0535 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -274,6 +274,45 @@ let print_namespace ns =
   in
   msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace)
 
+let print_strategy r =
+  let open Conv_oracle in
+  let pr_level = function
+  | Expand -> str "expand"
+  | Level 0 -> str "transparent"
+  | Level n -> str "level" ++ spc() ++ int n
+  | Opaque -> str "opaque"
+  in
+  let pr_strategy (ref, lvl) = pr_global ref ++ str " : " ++ pr_level lvl in
+  let oracle = Environ.oracle (Global.env ()) in
+  match r with
+  | None ->
+    let fold key lvl (vacc, cacc) = match key with
+    | VarKey id -> ((VarRef id, lvl) :: vacc, cacc)
+    | ConstKey cst -> (vacc, (ConstRef cst, lvl) :: cacc)
+    | RelKey _ -> (vacc, cacc)
+    in
+    let var_lvl, cst_lvl = fold_strategy fold oracle ([], []) in
+    let var_msg =
+      if List.is_empty var_lvl then mt ()
+      else str "Variable strategies" ++ fnl () ++
+        hov 0 (prlist_with_sep fnl pr_strategy var_lvl) ++ fnl ()
+    in
+    let cst_msg =
+      if List.is_empty cst_lvl then mt ()
+      else str "Constant strategies" ++ fnl () ++
+        hov 0 (prlist_with_sep fnl pr_strategy cst_lvl)
+    in
+    msg_notice (var_msg ++ cst_msg)
+  | Some r ->
+    let r = Smartlocate.smart_global r in
+    let key = match r with
+    | VarRef id -> VarKey id
+    | ConstRef cst -> ConstKey cst
+    | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
+    in
+    let lvl = get_strategy oracle key in
+    msg_notice (pr_strategy (r, lvl))
+
 let dump_universes_gen g s =
   let output = open_out s in
   let output_constraint, close =
@@ -1417,6 +1456,7 @@ let vernac_print = function
       let nassums =
 	Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in
       msg_notice (Printer.pr_assumptionset (Global.env ()) nassums)
+  | PrintStrategy r -> print_strategy r
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in