Merge PR #10817: Remove redundancy in section hypotheses of kernel entries.

Reviewed-by: SkySkimmer

11 files changed, 39 insertions, 49 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0951b07d49..b88a2e6194 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,7 +161,7 @@ type 'opaque result = {
   cook_universes : universes;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
-  cook_context : Constr.named_context option;
+  cook_context : Id.Set.t option;
 }
 
 let expmod_constr_subst cache modlist subst c =
@@ -242,11 +242,7 @@ let cook_constant { from = cb; info } =
     OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
-  let const_hyps =
-    Context.Named.fold_outside (fun decl hyps ->
-      List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
-		  hyps)
-      hyps0 ~init:cb.const_hyps in
+  let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
   let typ = abstract_constant_type (expmod cb.const_type) hyps in
   {
     cook_body = body;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 671cdf51fe..83a8b9edfc 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type 'opaque result = {
   cook_universes : universes;
   cook_relevance : Sorts.relevance;
   cook_inline : inline;
-  cook_context : Constr.named_context option;
+  cook_context : Names.Id.Set.t option;
 }
 
 val cook_constant : recipe -> Opaqueproof.opaque result
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 47e2f72b0e..1e6bc14935 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -61,7 +61,7 @@ type mutual_inductive_entry = {
 type definition_entry = {
   const_entry_body : constr;
   (* List of section variables *)
-  const_entry_secctx : Constr.named_context option;
+  const_entry_secctx : Id.Set.t option;
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type : types option;
@@ -70,7 +70,7 @@ type definition_entry = {
 
 type section_def_entry = {
   secdef_body : constr;
-  secdef_secctx : Constr.named_context option;
+  secdef_secctx : Id.Set.t option;
   secdef_feedback : Stateid.t option;
   secdef_type : types option;
 }
@@ -78,7 +78,7 @@ type section_def_entry = {
 type 'a opaque_entry = {
   opaque_entry_body   : 'a;
   (* List of section variables *)
-  opaque_entry_secctx : Constr.named_context;
+  opaque_entry_secctx : Id.Set.t;
   (* State id on which the completion of type checking is reported *)
   opaque_entry_feedback : Stateid.t option;
   opaque_entry_type        : types;
@@ -88,7 +88,7 @@ type 'a opaque_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Constr.named_context option * types in_universes_entry * inline
+    Id.Set.t option * types in_universes_entry * inline
 
 type primitive_entry = {
   prim_entry_type : types option;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4268f0a602..1069d9a62c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -733,7 +733,7 @@ let constant_entry_of_side_effect eff =
   if Declareops.is_opaque cb then
   OpaqueEff {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    opaque_entry_secctx = cb.const_hyps;
+    opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
@@ -741,7 +741,7 @@ let constant_entry_of_side_effect eff =
   else
   DefinitionEff {
     const_entry_body = p;
-    const_entry_secctx = Some cb.const_hyps;
+    const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps);
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
diff --git a/kernel/section.ml b/kernel/section.ml
index 4a9b222798..babd9fe7a1 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -146,19 +146,11 @@ let empty_segment = {
   abstr_uctx = AUContext.empty;
 }
 
-let extract_hyps sec vars hyps =
-  (* FIXME: this code is fishy. It is supposed to check that declared section
-     variables are an ordered subset of the ambient ones, but it doesn't check
-     e.g. uniqueness of naming nor convertibility of the section data. *)
-  let rec aux ids hyps = match ids, hyps with
-  | id :: ids, decl :: hyps when Names.Id.equal id (NamedDecl.get_id decl) ->
-    decl :: aux ids hyps
-  | _ :: ids, hyps ->
-    aux ids hyps
-  | [], _ -> []
-  in
-  let ids = List.map NamedDecl.get_id @@ List.firstn sec.sec_context vars in
-  aux ids hyps
+let extract_hyps sec vars used =
+  (* Keep the section-local segment of variables *)
+  let vars = List.firstn sec.sec_context vars in
+  (* Only keep the part that is used by the declaration *)
+  List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
 
 let section_segment_of_entry vars e hyps sections =
   (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
@@ -180,12 +172,14 @@ let section_segment_of_entry vars e hyps sections =
 let segment_of_constant env con s =
   let body = Environ.lookup_constant con env in
   let vars = Environ.named_context env in
-  section_segment_of_entry vars (SecDefinition con) body.Declarations.const_hyps s
+  let used = Context.Named.to_vars body.Declarations.const_hyps in
+  section_segment_of_entry vars (SecDefinition con) used s
 
 let segment_of_inductive env mind s =
   let mib = Environ.lookup_mind mind env in
   let vars = Environ.named_context env in
-  section_segment_of_entry vars (SecInductive mind) mib.Declarations.mind_hyps s
+  let used = Context.Named.to_vars mib.Declarations.mind_hyps in
+  section_segment_of_entry vars (SecInductive mind) used s
 
 let instance_from_variable_context =
   List.rev %> List.filter NamedDecl.is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b65e62ba30..f70b2960cf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -221,9 +221,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
 let build_constant_declaration env result =
   let open Cooking in
   let typ = result.cook_type in
-  let check declared inferred =
-    let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
-    let inferred_set, declared_set = mk_set inferred, mk_set declared in
+  let check declared_set inferred_set =
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
       let n = List.length l in
@@ -239,11 +237,6 @@ let build_constant_declaration env result =
          str "Proof using " ++ declared_vars ++ fnl () ++
          str "to" ++ fnl () ++
          str "Proof using " ++ inferred_vars) in
-  let sort l =
-    List.filter (fun decl ->
-      let id = NamedDecl.get_id decl in
-      List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
-    (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map NamedDecl.get_id (named_context env) in
@@ -252,7 +245,7 @@ let build_constant_declaration env result =
     | None ->
       if List.is_empty context_ids then
         (* Empty section context: no need to check *)
-        [], def
+        Id.Set.empty, def
       else
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
@@ -264,16 +257,19 @@ let build_constant_declaration env result =
           (* Opaque definitions always come with their section variables *)
           assert false
         in
-        keep_hyps env (Id.Set.union ids_typ ids_def), def
+        Environ.really_needed env (Id.Set.union ids_typ ids_def), def
     | Some declared ->
+      let needed = Environ.really_needed env declared in
+      (* Transitive closure ensured by the upper layers *)
+      let () = assert (Id.Set.equal needed declared) in
         (* We use the declared set and chain a check of correctness *)
-        sort declared,
+        declared,
         match def with
         | Undef _ | Primitive _ as x -> x (* nothing to check *)
         | Def cs as x ->
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
@@ -281,12 +277,13 @@ let build_constant_declaration env result =
           let kont c =
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env c in
-            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
+            let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in
             check declared inferred
           in
           OpaqueDef (iter kont lc)
   in
   let univs = result.cook_universes in
+  let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
   let tps = 
     let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
     Option.map Cemitcodes.from_val res
@@ -317,7 +314,10 @@ let translate_recipe env _kn r =
   let univs = result.cook_universes in
   let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
   let tps = Option.map Cemitcodes.from_val res in
-  { const_hyps = Option.get result.cook_context;
+  let hyps = Option.get result.cook_context in
+  (* Trust the set of section hypotheses generated by Cooking *)
+  let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
+  { const_hyps = hyps;
     const_body = result.cook_body;
     const_type = result.cook_type;
     const_body_code = tps;
diff --git a/tactics/declare.ml b/tactics/declare.ml
index e418240d3a..b6a0d9f39a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -72,7 +72,7 @@ type constant_obj = {
 type 'a proof_entry = {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
+  proof_entry_secctx : Id.Set.t option;
   (* State id on which the completion of type checking is reported *)
   proof_entry_feedback : Stateid.t option;
   proof_entry_type        : Constr.types option;
@@ -228,7 +228,7 @@ let cast_opaque_proof_entry e =
         ids_typ, vars
     in
     let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
-    keep_hyps env (Id.Set.union hyp_typ hyp_def)
+    Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
   | Some hyps -> hyps
   in
   {
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 4cb876cecb..da66a2713c 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -23,7 +23,7 @@ open Entries
 type 'a proof_entry = {
   proof_entry_body   : 'a Entries.const_entry_body;
   (* List of section variables *)
-  proof_entry_secctx : Constr.named_context option;
+  proof_entry_secctx : Id.Set.t option;
   (* State id on which the completion of type checking is reported *)
   proof_entry_feedback : Stateid.t option;
   proof_entry_type        : Constr.types option;
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index a2929e45cd..b723922642 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -36,7 +36,7 @@ type opacity_flag = Opaque | Transparent
 
 type t =
   { endline_tactic : Genarg.glob_generic_argument option
-  ; section_vars : Constr.named_context option
+  ; section_vars : Id.Set.t option
   ; proof : Proof.t
   ; udecl: UState.universe_decl
   (** Initial universe declarations *)
@@ -128,7 +128,7 @@ let set_used_variables ps l =
   if not (Option.is_empty ps.section_vars) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
   (* EJGA: This is always empty thus we should modify the type *)
-  (ctx, []), { ps with section_vars = Some ctx}
+  (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) }
 
 let get_open_goals ps =
   let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index d15e23c2cc..b9d1b37a11 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -17,7 +17,7 @@ type t
 (* Should be moved into a proper view *)
 val get_proof : t -> Proof.t
 val get_proof_name : t -> Names.Id.t
-val get_used_variables : t -> Constr.named_context option
+val get_used_variables : t -> Names.Id.Set.t option
 
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : t -> UState.universe_decl
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42d1a1f3fc..c7a588d2b4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -359,7 +359,7 @@ let save_lemma_admitted ~(lemma : t) : unit =
         let env = Global.env () in
         let ids_typ = Environ.global_vars_set env typ in
         let ids_def = Environ.global_vars_set env pproof in
-        Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
+        Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
       | _ -> None in
   let universes = Proof_global.get_initial_euctx lemma.proof in
   let ctx = UState.check_univ_decl ~poly universes udecl in