Move the Lib section data into the kernel.

Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.

4 files changed, 26 insertions, 133 deletions

diff --git a/library/global.ml b/library/global.ml
index e51c147f6e..3d28178d7b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -83,6 +83,7 @@ let i2l = Label.of_id
 
 let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
 let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_section_context c = globalize0 (Safe_typing.push_section_context c)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 
diff --git a/library/global.mli b/library/global.mli
index 9ac6b1f53c..b809e9b241 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -44,6 +44,7 @@ val sprop_allowed : unit -> bool
 
 val push_named_assum : (Id.t * Constr.types) -> unit
 val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
+val push_section_context : (Name.t array * Univ.UContext.t) -> unit
 
 val export_private_constants : in_section:bool ->
   Safe_typing.private_constants Entries.proof_output ->
@@ -74,7 +75,11 @@ val add_include :
 (** Sections *)
 
 val open_section : poly:bool -> unit
+(** [poly] is true when the section should be universe polymorphic *)
+
 val close_section : Summary.frozen -> unit
+(** Close the section and reset the global state to the one at the time when
+    the section what opened. *)
 
 (** Interactive modules and module types *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 367a84409b..1c6f82e8a6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -410,87 +410,11 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type abstr_info = {
+type abstr_info = Section.abstr_info = private {
   abstr_ctx : Constr.named_context;
   abstr_subst : Univ.Instance.t;
   abstr_uctx : Univ.AUContext.t;
 }
-type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
-
-type secentry =
-  | Variable of {
-      id:Names.Id.t;
-    }
-  | Context of Name.t array * Univ.UContext.t
-
-type section_data = {
-  sec_entry : secentry list;
-  sec_abstr : abstr_list;
-  sec_poly  : bool;
-}
-
-let empty_section_data ~poly = {
-  sec_entry = [];
-  sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty);
-  sec_poly  = poly;
-}
-
-let sectab =
-  Summary.ref ([] : section_data list) ~name:"section-context"
-
-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.")
-
-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 ~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} :: s.sec_entry } in
-       sectab := s :: sl
-
-let add_section_context (nas, ctx) =
-  match !sectab with
-    | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
-    | s :: sl ->
-       check_same_poly true s;
-       let s = { s with sec_entry = Context (nas, ctx) :: s.sec_entry } in
-       sectab := s :: sl
-
-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 _ -> ()
-            | Context (_, univs) ->
-              if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound
-          ) vars
-      ) !sectab;
-    false
-  with PolyFound -> true
-
-let extract_hyps poly (secs,ohyps) =
-  let rec aux = function
-    | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
-      let l, r = aux (idl,hyps) in 
-      decl :: l, r
-    | (Variable _::idl,hyps) ->
-        let l, r = aux (idl,hyps) in
-          l, r
-    | (Context (nas, ctx) :: idl, hyps) ->
-      let () = assert poly in
-       let l, (snas, sctx) = aux (idl, hyps) in
-       l, (Array.append snas nas, Univ.UContext.union sctx ctx)
-    | [], _ -> [], ([||], Univ.UContext.empty)
-  in aux (secs,ohyps)
 
 let instance_from_variable_context =
   List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
@@ -499,47 +423,21 @@ 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 add_section_replacement g poly hyps =
-  match !sectab with
-  | [] -> ()
-  | s :: sl ->
-    let () = check_same_poly poly s in
-    let sechyps, (nas, ctx) = extract_hyps s.sec_poly (s.sec_entry, hyps) in
-    let subst, ctx = Univ.abstract_universes nas ctx in
-    let info = {
-      abstr_ctx = sechyps;
-      abstr_subst = subst;
-      abstr_uctx = ctx;
-    } in
-    let s = { s with
-      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 poly
-
-let add_section_constant ~poly kn =
-  let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f poly
-
-let replacement_context () = make_worklist (List.hd !sectab).sec_abstr
+let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env ()
+
+let is_polymorphic_univ u =
+  Section.is_polymorphic_univ u (sections ())
+
+let replacement_context () =
+  Section.replacement_context (Global.env ()) (sections ())
 
 let section_segment_of_constant con =
-  Names.Cmap.find con (fst (List.hd !sectab).sec_abstr)
+  Section.segment_of_constant (Global.env ()) con (sections ())
 
 let section_segment_of_mutual_inductive kn =
-  Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr)
+  Section.segment_of_inductive (Global.env ()) kn (sections ())
 
-let empty_segment = {
-  abstr_ctx = [];
-  abstr_subst = Univ.Instance.empty;
-  abstr_uctx = Univ.AUContext.empty;
-}
+let empty_segment = Section.empty_segment
 
 let section_segment_of_reference = let open GlobRef in function
 | ConstRef c -> section_segment_of_constant c
@@ -550,25 +448,20 @@ 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 is_in_section ref =
+  Section.is_in_section (Global.env ()) ref (sections ())
+
 let section_instance = let open GlobRef in function
   | VarRef id ->
-     let eq = function
-       | Variable {id=id'} -> Names.Id.equal id id'
-       | Context _ -> false
-     in
-     if List.exists eq (List.hd !sectab).sec_entry
-     then Univ.Instance.empty, [||]
-     else raise Not_found
+    if is_in_section (VarRef id) then (Univ.Instance.empty, [||])
+    else raise Not_found
   | ConstRef con ->
-    let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in
+    let data = section_segment_of_constant con in
     extract_worklist data
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-    let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in
+    let data = section_segment_of_mutual_inductive kn in
     extract_worklist data
 
-let is_in_section ref =
-  try ignore (section_instance ref); true with Not_found -> false
-
 (*************)
 (* Sections. *)
 let open_section ~poly id =
@@ -582,9 +475,7 @@ let open_section ~poly id =
   add_entry (make_foname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix));
-  lib_state := { !lib_state with path_prefix = prefix };
-  add_section ~poly ()
-
+  lib_state := { !lib_state with path_prefix = prefix }
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
diff --git a/library/lib.mli b/library/lib.mli
index db6df4395b..5ce601f2d3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type abstr_info = private {
+type abstr_info = Section.abstr_info = private {
   abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
   abstr_subst : Univ.Instance.t;
@@ -181,10 +181,6 @@ val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context
 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 -> poly:bool -> unit
-val add_section_context : Name.t array * Univ.UContext.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
 val replacement_context : unit -> Opaqueproof.work_list
 
 val is_polymorphic_univ : Univ.Level.t -> bool