Merge PR #10604: Simplify Lib section handling

Reviewed-by: ejgallego
Reviewed-by: herbelin

7 files changed, 54 insertions, 51 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 0466efa991..3f2a1b075c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -487,11 +487,13 @@ let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  let map (decl, impl) = match impl with
-  | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
-  | _ -> None
+  let map decl =
+    let id = NamedDecl.get_id decl in
+    match Lib.variable_section_kind id with
+    | Implicit -> Some (id, Manual, (true, true))
+    | _ -> None
   in
-  List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx)
+  List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
diff --git a/interp/notation.ml b/interp/notation.ml
index d88182241b..a78bc60e83 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1533,7 +1533,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
     let n =
       try
         let vars = Lib.variable_section_segment_of_reference r in
-        vars |> List.map fst |> List.filter is_local_assum |> List.length
+        vars |> List.filter is_local_assum |> List.length
       with
         Not_found (* Not a ref defined in this section *) -> 0 in
     Some (req,r,n,l,[])
diff --git a/library/lib.ml b/library/lib.ml
index 59b55cc16b..6b01eb07e9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -413,11 +413,8 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
-
-type variable_context = variable_info list
 type abstr_info = {
-  abstr_ctx : variable_context;
+  abstr_ctx : Constr.named_context;
   abstr_subst : Univ.Instance.t;
   abstr_uctx : Univ.AUContext.t;
 }
@@ -426,21 +423,17 @@ type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 type secentry =
   | Variable of {
       id:Names.Id.t;
-      kind:Decl_kinds.binding_kind;
-      univs:Univ.ContextSet.t;
     }
   | Context of Univ.ContextSet.t
 
 type section_data = {
   sec_entry : secentry list;
-  sec_workl : Opaqueproof.work_list;
   sec_abstr : abstr_list;
   sec_poly  : bool;
 }
 
 let empty_section_data ~poly = {
   sec_entry = [];
-  sec_workl = (Names.Cmap.empty,Names.Mindmap.empty);
   sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
   sec_poly  = poly;
 }
@@ -448,6 +441,9 @@ let empty_section_data ~poly = {
 let sectab =
   Summary.ref ([] : section_data list) ~name:"section-context"
 
+let sec_implicits =
+  Summary.ref Id.Map.empty ~name:"section-implicits"
+
 let check_same_poly p sec =
   if p != sec.sec_poly then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
@@ -456,13 +452,14 @@ let add_section ~poly () =
   List.iter (fun tab -> check_same_poly poly tab) !sectab;
   sectab := empty_section_data ~poly :: !sectab
 
-let add_section_variable ~name ~kind ~poly univs =
+let add_section_variable ~name ~kind ~poly =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | s :: sl ->
        List.iter (fun tab -> check_same_poly poly tab) !sectab;
-       let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in
-       sectab := s :: sl
+       let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
+       sectab := s :: sl;
+       sec_implicits := Id.Map.add name kind !sec_implicits
 
 let add_section_context ctx =
   match !sectab with
@@ -472,38 +469,45 @@ let add_section_context ctx =
        let s = { s with sec_entry = Context ctx :: s.sec_entry } in
        sectab := s :: sl
 
-exception PolyFound of bool (* make this a let exception once possible *)
+exception PolyFound (* make this a let exception once possible *)
 let is_polymorphic_univ u =
   try
     let open Univ in
     List.iter (fun s ->
       let vars = s.sec_entry in
         List.iter (function
-            | Variable {univs=(univs,_)} ->
-              if LSet.mem u univs then raise (PolyFound s.sec_poly)
+            | Variable _ -> ()
             | Context (univs,_) ->
-              if LSet.mem u univs then raise (PolyFound true)
+              if LSet.mem u univs then raise PolyFound
           ) vars
       ) !sectab;
     false
-  with PolyFound b -> b
+  with PolyFound -> true
 
 let extract_hyps poly (secs,ohyps) =
   let rec aux = function
-    | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
-      (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
-    | (Variable {univs}::idl,hyps) ->
+      decl :: l, r
+    | (Variable _::idl,hyps) ->
         let l, r = aux (idl,hyps) in
-          l, if poly then Univ.ContextSet.union r univs else r
+          l, r
     | (Context ctx :: idl, hyps) ->
+      let () = assert poly in
        let l, r = aux (idl, hyps) in
        l, Univ.ContextSet.union r ctx
     | [], _ -> [],Univ.ContextSet.empty
   in aux (secs,ohyps)
 
 let instance_from_variable_context =
-  List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+  List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
+
+let extract_worklist info =
+  let args = instance_from_variable_context info.abstr_ctx in
+  info.abstr_subst, args
+
+let make_worklist (cmap, mmap) =
+  Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap
 
 let name_instance inst =
   (* FIXME: this should probably be done at an upper level, by storing the
@@ -522,37 +526,34 @@ let name_instance inst =
   in
   Array.map map (Univ.Instance.to_array inst)
 
-let add_section_replacement f g poly hyps =
+let add_section_replacement g poly hyps =
   match !sectab with
   | [] -> ()
   | s :: sl ->
     let () = check_same_poly poly s in
     let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
-    let inst = Univ.UContext.instance ctx in
-    let nas = name_instance inst in
+    let nas = name_instance (Univ.UContext.instance ctx) in
     let subst, ctx = Univ.abstract_universes nas ctx in
-    let args = instance_from_variable_context (List.rev sechyps) in
     let info = {
       abstr_ctx = sechyps;
       abstr_subst = subst;
       abstr_uctx = ctx;
     } in
     let s = { s with
-      sec_workl = f (inst, args) s.sec_workl;
       sec_abstr = g info s.sec_abstr;
     } in
     sectab := s :: sl
 
 let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f f poly
+    add_section_replacement f poly
 
 let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f f poly
+    add_section_replacement f poly
 
-let replacement_context () = (List.hd !sectab).sec_workl
+let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
 
 let section_segment_of_constant con =
   Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
@@ -575,6 +576,8 @@ let section_segment_of_reference = let open GlobRef in function
 let variable_section_segment_of_reference gr =
   (section_segment_of_reference gr).abstr_ctx
 
+let variable_section_kind id = Id.Map.get id !sec_implicits
+
 let section_instance = let open GlobRef in function
   | VarRef id ->
      let eq = function
@@ -585,9 +588,11 @@ let section_instance = let open GlobRef in function
      then Univ.Instance.empty, [||]
      else raise Not_found
   | ConstRef con ->
-      Names.Cmap.find con (fst (List.hd !sectab).sec_workl)
+    let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+    extract_worklist data
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl)
+    let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+    extract_worklist data
 
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
diff --git a/library/lib.mli b/library/lib.mli
index fe6bf69ec4..7dc8b52282 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,10 +163,8 @@ val drop_objects : frozen -> frozen
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
-type variable_context = variable_info list 
 type abstr_info = private {
-  abstr_ctx : variable_context;
+  abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
   abstr_subst : Univ.Instance.t;
   (** Actual names of the abstracted variables *)
@@ -174,18 +172,17 @@ type abstr_info = private {
   (** Universe quantification, same length as the substitution *)
 }
 
-val instance_from_variable_context : variable_context -> Id.t array
-
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
 val section_segment_of_reference : GlobRef.t -> abstr_info
 
-val variable_section_segment_of_reference : GlobRef.t -> variable_context
+val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
+val variable_section_kind : Id.t -> Decl_kinds.binding_kind
 
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit
+val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
 val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 534c0ca20b..a86d237164 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -47,7 +47,7 @@ let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) when not (isVarRef c && Lib.is_in_section c) ->
      (try 
        let vars = Lib.variable_section_segment_of_reference c in
-       let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
+       let var_names = List.map (NamedDecl.get_id %> Name.mk_name) vars in
        let names' = var_names @ names in
        Some (ReqGlobal (c, names), (c, names'))
      with Not_found -> Some req)
diff --git a/tactics/declare.ml b/tactics/declare.ml
index b8ba62a5e5..61f9c3b1c5 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -71,8 +71,7 @@ let load_constant i ((sp,kn), obj) =
 
 let cooking_info segment =
   let modlist = replacement_context () in
-  let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in
-  let named_ctx = List.map fst hyps in
+  let { abstr_ctx = named_ctx; abstr_subst = subst; abstr_uctx = uctx } = segment in
   let abstract = (named_ctx, subst, uctx) in
   { Opaqueproof.modlist; abstract }
 
@@ -308,12 +307,12 @@ let declare_variable ~name ~kind d =
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-  let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
+  let impl,opaque,poly = match d with (* Fails if not well-typed *)
     | SectionLocalAssum {typ;univs;poly;impl} ->
       let () = declare_universe_context ~poly univs in
       let () = Global.push_named_assum (name,typ) in
       let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in
-      impl, true, poly, univs
+      impl, true, poly
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -338,10 +337,10 @@ let declare_variable ~name ~kind d =
       } in
       let () = Global.push_named_def (name, se) in
       Decl_kinds.Explicit, de.proof_entry_opaque,
-      poly, univs
+      poly
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
-  add_section_variable ~name ~kind:impl ~poly univs;
+  add_section_variable ~name ~kind:impl ~poly;
   Decls.(add_variable_data name {opaque;kind});
   add_anonymous_leaf (inVariable ());
   Impargs.declare_var_implicits name;
diff --git a/vernac/classes.ml b/vernac/classes.ml
index efe452d5f1..075d89d0df 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -179,7 +179,7 @@ let discharge_class (_,cl) =
   let open CVars in
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
-    ( fun (decl,_) (ctx', subst) ->
+    ( fun decl (ctx', subst) ->
         let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
         (decl' :: ctx', NamedDecl.get_id decl :: subst)
     ) ctx ([], []) in