[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.

1 files changed, 63 insertions, 32 deletions

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