Merge PR #10429: Perform the opaque section variable inference outside of the kernel

Reviewed-by: SkySkimmer
Reviewed-by: gares

4 files changed, 56 insertions, 50 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 2d29c3ee19..ca08ba485e 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -80,7 +80,7 @@ type section_def_entry = {
 type 'a opaque_entry = {
   opaque_entry_body   : 'a;
   (* List of section variables *)
-  opaque_entry_secctx : Constr.named_context option;
+  opaque_entry_secctx : Constr.named_context;
   (* State id on which the completion of type checking is reported *)
   opaque_entry_feedback : Stateid.t option;
   opaque_entry_type        : types;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a0cc2974d9..7526508c4e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -691,7 +691,7 @@ let constant_entry_of_side_effect eff =
   if Declareops.is_opaque cb then
   OpaqueEntry {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    opaque_entry_secctx = None;
+    opaque_entry_secctx = cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
@@ -699,7 +699,7 @@ let constant_entry_of_side_effect eff =
   else
   DefinitionEntry {
     const_entry_body = (p, Univ.ContextSet.empty);
-    const_entry_secctx = None;
+    const_entry_secctx = Some cb.const_hyps;
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index eca22869d2..b3c3dcbf45 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -151,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_universes = Monomorphic univs;
         cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
         cook_inline = false;
-        cook_context = c.opaque_entry_secctx;
+        cook_context = Some c.opaque_entry_secctx;
       }
 
   (** Similar case for polymorphic entries. *)
@@ -188,7 +188,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_universes = Polymorphic auctx;
         cook_relevance = Sorts.relevance_of_sort tj.utj_type;
         cook_inline = false;
-        cook_context = c.opaque_entry_secctx;
+        cook_context = Some c.opaque_entry_secctx;
       }
 
   (** Other definitions have to be processed immediately. *)
@@ -237,17 +237,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
         cook_context = c.const_entry_secctx;
       }
 
-let record_aux env s_ty s_bo =
-  let in_ty = keep_hyps env s_ty in
-  let v =
-    String.concat " "
-      (CList.map_filter (fun decl ->
-          let id = NamedDecl.get_id decl in
-          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
-          else Some (Id.to_string id))
-        (keep_hyps env s_bo)) in
-  Aux_file.record_in_aux "context_used" v
-
 let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
@@ -279,24 +268,22 @@ let build_constant_declaration env result =
     let context_ids = List.map NamedDecl.get_id (named_context env) in
     let def = result.cook_body in
     match result.cook_context with
-    | None when not (List.is_empty context_ids) -> 
+    | None ->
+      if List.is_empty context_ids then
+        (* Empty section context: no need to check *)
+        [], def
+      else
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
         let ids_typ = global_vars_set env typ in
         let ids_def = match def with
         | Undef _ | Primitive _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
-        | OpaqueDef lc ->
-            let (lc, _) = Future.force lc in
-            let vars = global_vars_set env lc in
-            if !Flags.record_aux_file then record_aux env ids_typ vars;
-            vars
+        | OpaqueDef _ ->
+          (* Opaque definitions always come with their section variables *)
+          assert false
         in
         keep_hyps env (Id.Set.union ids_typ ids_def), def
-    | None ->
-        if !Flags.record_aux_file then
-          record_aux env Id.Set.empty Id.Set.empty;
-        [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
         sort declared,
@@ -371,31 +358,12 @@ let translate_local_def env _id centry =
   } in
   let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
   let typ = decl.cook_type in
-  if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
-    match decl.cook_body with
-    | Undef _ -> ()
-    | Primitive _ -> ()
-    | Def _ -> ()
-    | OpaqueDef lc ->
-       let ids_typ = global_vars_set env typ in
-       let ids_def = global_vars_set env (fst (Future.force lc)) in
-       record_aux env ids_typ ids_def
-  end;
   let () = match decl.cook_universes with
   | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
   | Polymorphic _ -> assert false
   in
   let c = match decl.cook_body with
   | Def c -> Mod_subst.force_constr c
-  | OpaqueDef o ->
-    let (p, cst) = Future.force o in
-    (** Let definitions are ensured to have no extra constraints coming from
-        the body by virtue of the typing of [Entries.section_def_entry]. *)
-    let () = match cst with
-    | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
-    | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx)
-    in
-    p
-  | Undef _ | Primitive _ -> assert false
+  | Undef _ | Primitive _ | OpaqueDef _ -> assert false
   in
   c, decl.cook_relevance, typ
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 668026500d..74196bb875 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -27,6 +27,8 @@ open Cooking
 open Decls
 open Decl_kinds
 
+module NamedDecl = Context.Named.Declaration
+
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Declaration of constants and parameters *)
@@ -144,6 +146,18 @@ let register_side_effect (c, role) =
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
 
+let record_aux env s_ty s_bo =
+  let open Environ in
+  let in_ty = keep_hyps env s_ty in
+  let v =
+    String.concat " "
+      (CList.map_filter (fun decl ->
+          let id = NamedDecl.get_id decl in
+          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" v
+
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
@@ -168,15 +182,39 @@ let cast_proof_entry e =
     const_entry_inline_code = e.proof_entry_inline_code;
   }
 
-let cast_opaque_proof_entry e =
+let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Proof_global.proof_entry) =
   let open Proof_global in
   let typ = match e.proof_entry_type with
   | None -> assert false
   | Some typ -> typ
   in
+  let secctx = match e.proof_entry_secctx with
+  | None ->
+    let open Environ in
+    let env = Global.env () in
+    let hyp_typ, hyp_def =
+      if List.is_empty (Environ.named_context env) then
+        Id.Set.empty, Id.Set.empty
+      else
+        let ids_typ = global_vars_set env typ in
+        let pf, env = match pure with
+        | PureEntry ->
+          let (pf, _), () = Future.force e.proof_entry_body in
+          pf, env
+        | EffectEntry ->
+          let (pf, _), eff = Future.force e.proof_entry_body in
+          pf, Safe_typing.push_private_constants env eff
+        in
+        let vars = global_vars_set env pf in
+        ids_typ, vars
+    in
+    let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in
+    keep_hyps env (Id.Set.union hyp_typ hyp_def)
+  | Some hyps -> hyps
+  in
   {
     opaque_entry_body = e.proof_entry_body;
-    opaque_entry_secctx = e.proof_entry_secctx;
+    opaque_entry_secctx = secctx;
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
     opaque_entry_universes = e.proof_entry_universes;
@@ -208,7 +246,7 @@ let define_constant ~side_effect id cd =
       let export = get_roles export eff in
       let de = { de with proof_entry_body = Future.from_val (body, ()) } in
       let cd = match de.proof_entry_opaque with
-      | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de)
+      | true -> Entries.OpaqueEntry (cast_opaque_proof_entry PureEntry de)
       | false -> Entries.DefinitionEntry (cast_proof_entry de)
       in
       export, ConstantEntry (PureEntry, cd)
@@ -217,7 +255,7 @@ let define_constant ~side_effect id cd =
       let map (body, eff) = body, eff.Evd.seff_private in
       let body = Future.chain de.proof_entry_body map in
       let de = { de with proof_entry_body = body } in
-      let de = cast_opaque_proof_entry de in
+      let de = cast_opaque_proof_entry EffectEntry de in
       [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
     | ParameterEntry e ->
       [], ConstantEntry (PureEntry, Entries.ParameterEntry e)