From 4838fd47542018ba61cd096c93edf45b7ef68529 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Aug 2019 13:48:57 +0200
Subject: Refine the API to declare section-local universes.

The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.

Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
---
 library/lib.ml  | 39 ++++++++++-----------------------------
 library/lib.mli |  2 +-
 2 files changed, 11 insertions(+), 30 deletions(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 851f086961..1f97424590 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -421,7 +421,7 @@ type secentry =
   | Variable of {
       id:Names.Id.t;
     }
-  | Context of Univ.ContextSet.t
+  | Context of Name.t array * Univ.UContext.t
 
 type section_data = {
   sec_entry : secentry list;
@@ -454,12 +454,12 @@ let add_section_variable ~name ~poly =
        let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in
        sectab := s :: sl
 
-let add_section_context ctx =
+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 ctx :: s.sec_entry } in
+       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 *)
@@ -470,8 +470,8 @@ let is_polymorphic_univ u =
       let vars = s.sec_entry in
         List.iter (function
             | Variable _ -> ()
-            | Context (univs,_) ->
-              if LSet.mem u univs then raise PolyFound
+            | Context (_, univs) ->
+              if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound
           ) vars
       ) !sectab;
     false
@@ -485,11 +485,11 @@ let extract_hyps poly (secs,ohyps) =
     | (Variable _::idl,hyps) ->
         let l, r = aux (idl,hyps) in
           l, r
-    | (Context ctx :: idl, hyps) ->
+    | (Context (nas, ctx) :: idl, hyps) ->
       let () = assert poly in
-       let l, r = aux (idl, hyps) in
-       l, Univ.ContextSet.union r ctx
-    | [], _ -> [],Univ.ContextSet.empty
+       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 =
@@ -502,31 +502,12 @@ let extract_worklist info =
 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
-     name information in the section data structure. *)
-  let map lvl = match Univ.Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        Name (Libnames.qualid_basename qid)
-      with Not_found ->
-        (* Best-effort naming from the string representation of the level.
-           See univNames.ml for a similar hack. *)
-        Name (Id.of_string_soft (Univ.Level.to_string lvl))
-  in
-  Array.map map (Univ.Instance.to_array inst)
-
 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 nas = name_instance (Univ.UContext.instance ctx) 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;
diff --git a/library/lib.mli b/library/lib.mli
index 9ffa69ef93..db6df4395b 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -182,7 +182,7 @@ 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 : Univ.ContextSet.t -> 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
-- 
cgit v1.2.3


From 24eccfc6dfec012da081a0891c397f013cc590e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 May 2019 15:58:05 +0200
Subject: Stub code for handling sections in kernel.

For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
---
 library/global.ml  | 7 +++++++
 library/global.mli | 5 +++++
 library/lib.ml     | 3 ++-
 3 files changed, 14 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 6bb4614aa4..e51c147f6e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -104,6 +104,13 @@ let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
 
+let open_section ~poly = globalize0 (Safe_typing.open_section ~poly)
+let close_section fs =
+  (* TODO: use globalize0_with_summary *)
+  Summary.unfreeze_summaries fs;
+  let env = Safe_typing.close_section (safe_env ()) in
+  GlobalSafeEnv.set_safe_env env
+
 let start_module id = globalize (Safe_typing.start_module (i2l id))
 let start_modtype id = globalize (Safe_typing.start_modtype (i2l id))
 
diff --git a/library/global.mli b/library/global.mli
index d0bd556d70..9ac6b1f53c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -71,6 +71,11 @@ val add_include :
   Entries.module_struct_entry -> bool -> Declarations.inline ->
     Mod_subst.delta_resolver
 
+(** Sections *)
+
+val open_section : poly:bool -> unit
+val close_section : Summary.frozen -> unit
+
 (** Interactive modules and module types *)
 
 val start_module : Id.t -> ModPath.t
diff --git a/library/lib.ml b/library/lib.ml
index 1f97424590..367a84409b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -572,6 +572,7 @@ let is_in_section ref =
 (*************)
 (* Sections. *)
 let open_section ~poly id =
+  let () = Global.open_section ~poly in
   let opp = !lib_state.path_prefix in
   let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in
   let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in
@@ -612,7 +613,7 @@ let close_section () =
   lib_state := { !lib_state with lib_stk = before };
   pop_path_prefix ();
   let newdecls = List.map discharge_item secdecls in
-  Summary.unfreeze_summaries fs;
+  let () = Global.close_section fs in
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
 
 (* State and initialization. *)
-- 
cgit v1.2.3


From 58a9de2acacb05291d87fe2b656728ae05d59df4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Jul 2019 10:48:28 +0200
Subject: 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.
---
 library/global.ml  |   1 +
 library/global.mli |   5 ++
 library/lib.ml     | 147 +++++++----------------------------------------------
 library/lib.mli    |   6 +--
 4 files changed, 26 insertions(+), 133 deletions(-)

(limited to 'library')

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
-- 
cgit v1.2.3