[coqchk] Fix #5030

When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).

Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.

9 files changed, 87 insertions, 50 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 6d307b3c5e..1ff1425dea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -119,11 +119,12 @@ let check_one_lib admit senv (dir,m) =
     if LibrarySet.mem dir admit then
       (Flags.if_verbose Feedback.msg_notice
          (str "Admitting library: " ++ pr_dirpath dir);
-       Safe_checking.unsafe_import senv md m.library_extra_univs dig)
+       Safe_checking.unsafe_import (fst senv) md m.library_extra_univs dig),
+      (snd senv)
     else
       (Flags.if_verbose Feedback.msg_notice
          (str "Checking library: " ++ pr_dirpath dir);
-       Safe_checking.import senv md m.library_extra_univs dig)
+       Safe_checking.import (fst senv) (snd senv) md m.library_extra_univs dig)
   in
     register_loaded_library m; senv
 
@@ -435,6 +436,6 @@ let recheck_library senv ~norec ~admit ~check =
   Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
-  let senv = List.fold_left (check_one_lib nochk) senv needed in
+  let senv = List.fold_left (check_one_lib nochk) (senv, Cmap.empty) needed in
   Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked");
   senv
diff --git a/checker/check.mli b/checker/check.mli
index bb19f09d2e..93274204a3 100644
--- a/checker/check.mli
+++ b/checker/check.mli
@@ -30,4 +30,4 @@ val add_load_path : physical_path * logical_path -> unit
 val recheck_library : safe_environment ->
   norec:object_file list ->
   admit:object_file list ->
-  check:object_file list -> safe_environment
+  check:object_file list -> safe_environment * Cset.t Cmap.t
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index a9136a225d..0a2da7435c 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -38,8 +38,13 @@ let pr_assumptions ass axs =
   else
     hv 2 (str ass ++ str ":" ++ fnl() ++ prlist_with_sep fnl str axs)
 
-let pr_axioms env =
-  let csts = fold_constants (fun c cb acc -> if not (Declareops.constant_has_body cb) then Cset.add c acc else acc) env Cset.empty in
+let pr_axioms env opac =
+  let add c cb acc =
+    if Declareops.constant_has_body cb then acc else
+      match Cmap.find_opt c opac with
+      | None -> Cset.add c acc
+      | Some s -> Cset.union s acc in
+  let csts = fold_constants add env Cset.empty in
   let csts = Cset.fold (fun c acc -> Constant.to_string c :: acc) csts [] in
   pr_assumptions "Axioms" csts
 
@@ -57,20 +62,20 @@ let pr_nonpositive env =
   let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in
   pr_assumptions "Inductives whose positivity is assumed" inds
 
-let print_context env =
+let print_context env opac =
   if !output_context then begin
     Feedback.msg_notice
       (hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
-      str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_axioms env opac ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_nonpositive env ++ fnl()))
       )
   end
 
-let stats env =
-  print_context env;
+let stats env opac =
+  print_context env opac;
   print_memory_stat ()
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 8796bcda76..987d50b469 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -10,4 +10,4 @@
 val memory_stat : bool ref
 val output_context : bool ref
 
-val stats : Environ.env -> unit
+val stats : Environ.env -> Names.Cset.t Names.Cmap.t -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index 0522d43417..086acc482c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -407,6 +407,6 @@ let run senv =
 
 let start () =
   let senv = init() in
-  let senv = run senv in
-  Check_stat.stats (Safe_typing.env_of_safe_env senv);
+  let senv, opac = run senv in
+  Check_stat.stats (Safe_typing.env_of_safe_env senv) opac;
   exit 0
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 2f795ff8d9..c2b486c371 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -15,7 +15,20 @@ let indirect_accessor = ref {
 
 let set_indirect_accessor f = indirect_accessor := f
 
-let check_constant_declaration env kn cb =
+let register_opacified_constant env opac kn =
+  let wo_body =
+    fold_constants
+      (fun kn cb s ->
+        if Declareops.constant_has_body cb then s else
+          match Cmap.find_opt kn opac with
+          | None -> Cset.add kn s
+          | Some s' -> Cset.union s' s)
+      env
+      Cset.empty
+  in
+  Cmap.add kn wo_body opac
+
+let check_constant_declaration env opac kn cb opacify =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   let env = CheckFlags.set_local_flags cb.const_typing_flags env in
   let poly, env =
@@ -54,11 +67,13 @@ let check_constant_declaration env kn cb =
        with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()
   in
-  ()
+  match body with
+  | Some _ when opacify -> register_opacified_constant env opac kn
+  | Some _ | None -> opac
 
-let check_constant_declaration env kn cb =
-  let () = check_constant_declaration env kn cb in
-  Environ.add_constant kn cb env
+let check_constant_declaration env opac kn cb opacify =
+  let opac = check_constant_declaration env opac kn cb opacify in
+  Environ.add_constant kn cb env, opac
 
 (** {6 Checking modules } *)
 
@@ -80,18 +95,32 @@ let mk_mtb mp sign delta =
     mod_delta = delta;
     mod_retroknowledge = ModTypeRK; }
 
-let rec check_module env mp mb =
+let collect_constants_without_body sign mp =
+  let collect_sf s lab = function
+  | SFBconst cb ->
+     let c = Constant.make2 mp lab in
+     if Declareops.constant_has_body cb then s else Cset.add c s
+  | SFBmind _ | SFBmodule _ | SFBmodtype _ -> s in
+  match sign with
+  | MoreFunctor _ -> Cset.empty  (* currently ignored *)
+  | NoFunctor struc ->
+     List.fold_left (fun s (lab,mb) -> collect_sf s lab mb) Cset.empty struc
+
+let rec check_module env opac mp mb =
   Flags.if_verbose Feedback.msg_notice (str "  checking module: " ++ str (ModPath.to_string mp));
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
-  let (_:module_signature) =
-    check_signature env mb.mod_type mb.mod_mp mb.mod_delta
+  let sign, opac =
+    check_signature env opac mb.mod_type mb.mod_mp mb.mod_delta Cset.empty
   in
-  let optsign = match mb.mod_expr with
-    |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta)
-    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
-    |Abstract|FullStruct -> None
+  let optsign, opac = match mb.mod_expr with
+    |Struct sign_struct ->
+      let opacify = collect_constants_without_body sign mb.mod_mp in
+      let sign, opac = check_signature env opac sign_struct mb.mod_mp mb.mod_delta opacify in
+      Some (sign, mb.mod_delta), opac
+    |Algebraic me -> Some (check_mexpression env opac me mb.mod_mp mb.mod_delta), opac
+    |Abstract|FullStruct -> None, opac
   in
-  match optsign with
+  let () = match optsign with
   |None -> ()
   |Some (sign,delta) ->
     let mtb1 = mk_mtb mp sign delta
@@ -100,35 +129,37 @@ let rec check_module env mp mb =
     let cu = Subtyping.check_subtypes env mtb1 mtb2 in
     if not (Environ.check_constraints cu env) then
       CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping");
+  in
+  opac
 
 and check_module_type env mty =
   Flags.if_verbose Feedback.msg_notice (str "  checking module type: " ++ str (ModPath.to_string mty.mod_mp));
-  let (_:module_signature) =
-    check_signature env mty.mod_type mty.mod_mp mty.mod_delta in
+  let (_:module_signature), _ =
+    check_signature env Cmap.empty mty.mod_type mty.mod_mp mty.mod_delta Cset.empty in
   ()
 
-and check_structure_field env mp lab res = function
+and check_structure_field env opac mp lab res opacify = function
   | SFBconst cb ->
       let c = Constant.make2 mp lab in
-      check_constant_declaration env c cb
+      check_constant_declaration env opac c cb (Cset.mem c opacify)
   | SFBmind mib ->
       let kn = KerName.make mp lab in
       let kn = Mod_subst.mind_of_delta_kn res kn in
-      CheckInductive.check_inductive env kn mib
+      CheckInductive.check_inductive env kn mib, opac
   | SFBmodule msb ->
-      let () = check_module env (MPdot(mp,lab)) msb in
-      Modops.add_module msb env
+      let opac = check_module env opac (MPdot(mp,lab)) msb in
+      Modops.add_module msb env, opac
   | SFBmodtype mty ->
       check_module_type env mty;
-      add_modtype mty env
+      add_modtype mty env, opac
 
-and check_mexpr env mse mp_mse res = match mse with
+and check_mexpr env opac mse mp_mse res = match mse with
   | MEident mp ->
       let mb = lookup_module mp env in
       let mb = Modops.strengthen_and_subst_mb mb mp_mse false in
       mb.mod_type, mb.mod_delta
   | MEapply (f,mp) ->
-      let sign, delta = check_mexpr env f mp_mse res in
+      let sign, delta = check_mexpr env opac f mp_mse res in
       let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
       let mtb = Modops.module_type_of_module (lookup_module mp env) in
       let cu = Subtyping.check_subtypes env mtb farg_b in
@@ -139,22 +170,22 @@ and check_mexpr env mse mp_mse res = match mse with
   | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
 
-and check_mexpression env sign mp_mse res = match sign with
+and check_mexpression env opac sign mp_mse res = match sign with
   | MoreFunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
       let env' = Modops.add_module_type (MPbound arg_id) mtb env in
-      let body, delta = check_mexpression env' body mp_mse res in
+      let body, delta = check_mexpression env' opac body mp_mse res in
       MoreFunctor(arg_id,mtb,body), delta
-  | NoFunctor me -> check_mexpr env me mp_mse res
+  | NoFunctor me -> check_mexpr env opac me mp_mse res
 
-and check_signature env sign mp_mse res = match sign with
+and check_signature env opac sign mp_mse res opacify = match sign with
   | MoreFunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
       let env' = Modops.add_module_type (MPbound arg_id) mtb env in
-      let body = check_signature env' body mp_mse res in
-      MoreFunctor(arg_id,mtb,body)
+      let body, opac = check_signature env' opac body mp_mse res Cset.empty in
+      MoreFunctor(arg_id,mtb,body), opac
   | NoFunctor struc ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-        check_structure_field env mp_mse lab res mb) env struc
+      let (_:env), opac = List.fold_left (fun (env, opac) (lab,mb) ->
+        check_structure_field env opac mp_mse lab res opacify mb) (env, opac) struc
       in
-      NoFunctor struc
+      NoFunctor struc, opac
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index 58eb135b50..194f6c6e16 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -10,4 +10,4 @@
 
 val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit
 
-val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
+val check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.t
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index b5beab532e..55bfa36ce5 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -11,14 +11,14 @@
 open Declarations
 open Environ
 
-let import senv clib univs digest =
+let import senv opac clib univs digest =
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
   let env = push_context_set ~strict:true univs env in
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
-  Mod_checking.check_module env mb.mod_mp mb;
-  let (_,senv) = Safe_typing.import clib univs digest senv in senv
+  let opac = Mod_checking.check_module env opac mb.mod_mp mb in
+  let (_,senv) = Safe_typing.import clib univs digest senv in senv, opac
 
 let unsafe_import senv clib univs digest =
   let (_,senv) = Safe_typing.import clib univs digest senv in senv
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
index 21566555d4..b4abc52a74 100644
--- a/checker/safe_checking.mli
+++ b/checker/safe_checking.mli
@@ -12,5 +12,5 @@
 open Safe_typing
 (*i*)
 
-val import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
+val import : safe_environment -> Names.Cset.t Names.Cmap.t -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment * Names.Cset.t Names.Cmap.t
 val unsafe_import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment