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.

5 files changed, 380 insertions, 51 deletions

diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 66bac15e9a..20e742d7f8 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -49,4 +49,5 @@ Term_typing
 Subtyping
 Mod_typing
 Nativelibrary
+Section
 Safe_typing
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 783ce63b8c..8d34f3a34f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,16 +113,9 @@ type library_info = DirPath.t * vodigest
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
 
-(** Sections can be nested with the proviso that no monomorphic section can be
-    opened inside a polymorphic one. The reverse is allowed. *)
-type sections = {
-  sec_poly : int;
-  sec_mono : int;
-}
-
 type safe_environment =
   { env : Environ.env;
-    sections : sections;
+    sections : Section.t;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -150,11 +143,6 @@ let rec library_dp_of_senv senv =
   | SIG(_,senv) -> library_dp_of_senv senv
   | STRUCT(_,senv) -> library_dp_of_senv senv
 
-let empty_sections = {
-  sec_poly = 0;
-  sec_mono = 0;
-}
-
 let empty_environment =
   { env = Environ.empty_env;
     modpath = ModPath.initial;
@@ -164,7 +152,7 @@ let empty_environment =
     revstruct = [];
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
-    sections = empty_sections;
+    sections = Section.empty;
     future_cst = [];
     univ = Univ.ContextSet.empty;
     engagement = None;
@@ -331,11 +319,16 @@ let universes_of_private eff =
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
+let sections_of_safe_env senv = senv.sections
+
 type constraints_addition =
   | Now of Univ.ContextSet.t
   | Later of Univ.ContextSet.t Future.computation
 
 let push_context_set poly cst senv =
+  let () = if Section.is_polymorphic senv.sections && not (Univ.ContextSet.is_empty cst) then
+    CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.")
+  in
   { senv with
     env = Environ.push_context_set ~strict:(not poly) cst senv.env;
     univ = Univ.ContextSet.union cst senv.univ }
@@ -399,11 +392,8 @@ let check_current_library dir senv = match senv.modvariant with
 
 (** When operating on modules, we're normally outside sections *)
 
-let is_empty_sections s =
-  Int.equal s.sec_poly 0 && Int.equal s.sec_mono 0
-
 let check_empty_context senv =
-  assert (Environ.empty_context senv.env && is_empty_sections senv.sections)
+  assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
 
 (** When adding a parameter to the current module/modtype,
     it must have been freshly started *)
@@ -450,21 +440,30 @@ let safe_push_named d env =
     with Not_found -> () in
   Environ.push_named d env
 
-
 let push_named_def (id,de) senv =
-  let () = assert (not @@ is_empty_sections senv.sections) in
+  let sections = Section.push_local senv.sections in
   let c, r, typ = Term_typing.translate_local_def senv.env id de in
   let x = Context.make_annot id r in
   let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
-  { senv with env = env'' }
+  { senv with sections; env = env'' }
 
 let push_named_assum (x,t) senv =
-  let () = assert (not @@ is_empty_sections senv.sections) in
+  let sections = Section.push_local senv.sections in
   let t, r = Term_typing.translate_local_assum senv.env t in
   let x = Context.make_annot x r in
   let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
-    {senv with env=env''}
-
+  { senv with sections; env = env'' }
+
+let push_section_context (nas, ctx) senv =
+  let sections = Section.push_context (nas, ctx) senv.sections in
+  let senv = { senv with sections } in
+  let ctx = Univ.ContextSet.of_context ctx in
+  (* We check that the universes are fresh. FIXME: This should be done
+     implicitly, but we have to work around the API. *)
+  let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in
+  { senv with
+    env = Environ.push_context_set ~strict:false ctx senv.env;
+    univ = Univ.ContextSet.union ctx senv.univ }
 
 (** {6 Insertion of new declarations to current environment } *)
 
@@ -546,8 +545,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
     | SFBmodule mb, M -> Modops.add_module mb senv.env
     | _ -> assert false
   in
+  let sections = match sfb, gn with
+  | SFBconst cb, C con ->
+    let poly = Declareops.constant_is_polymorphic cb in
+    Section.push_constant ~poly con senv.sections
+  | SFBmind mib, I mind ->
+    let poly = Declareops.inductive_is_polymorphic mib in
+    Section.push_inductive ~poly mind senv.sections
+  | _, (M | MT) -> senv.sections
+  | _ -> assert false
+  in
   { senv with
     env = env';
+    sections;
     revstruct = field :: senv.revstruct;
     modlabels = Label.Set.union mlabs senv.modlabels;
     objlabels = Label.Set.union olabs senv.objlabels }
@@ -924,26 +934,13 @@ let add_module l me inl senv =
 (** {6 Interactive sections *)
 
 let open_section ~poly senv =
-  let sections = senv.sections in
-  if poly then
-    let sections = { sections with sec_poly = sections.sec_poly + 1 } in
-    { senv with sections }
-  else if Int.equal sections.sec_poly 0 then
-    let sections = { sections with sec_mono = sections.sec_mono + 1 } in
-    { senv with sections }
-  else
-    CErrors.anomaly (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+  let sections = Section.open_section ~poly senv.sections in
+  { senv with sections }
 
 let close_section senv =
-  let sections = senv.sections in
-  if not (Int.equal sections.sec_poly 0) then
-    let sections = { sections with sec_poly = sections.sec_poly - 1 } in
-    { senv with sections }
-  else if not (Int.equal sections.sec_mono 0) then
-    let sections = { sections with sec_mono = sections.sec_mono - 1 } in
-    { senv with sections }
-  else
-    CErrors.anomaly (Pp.str "No open section")
+  (* TODO: implement me when discharging in kernel *)
+  let sections = Section.close_section senv.sections in
+  { senv with sections }
 
 (** {6 Starting / ending interactive modules and module types } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 4eef43b193..10fedc2faf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -33,6 +33,8 @@ val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
+val sections_of_safe_env : safe_environment -> Section.t
+
 (** The safe_environment state monad *)
 
 type safe_transformer0 = safe_environment -> safe_environment
@@ -67,15 +69,6 @@ val join_safe_environment :
 val is_joined_environment : safe_environment -> bool
 (** {6 Enriching a safe environment } *)
 
-(** Insertion of local declarations (Local or Variables) *)
-
-val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
-
-(** Returns the full universe context necessary to typecheck the definition
-  (futures are forced) *)
-val push_named_def :
-  Id.t * Entries.section_def_entry -> safe_transformer0
-
 (** Insertion of global axioms or definitions *)
 
 type 'a effect_entry =
@@ -146,6 +139,16 @@ val open_section : poly:bool -> safe_transformer0
 
 val close_section : safe_transformer0
 
+(** Insertion of local declarations (Local or Variables) *)
+
+val push_named_assum : (Id.t * Constr.types) -> safe_transformer0
+
+val push_named_def :
+  Id.t * Entries.section_def_entry -> safe_transformer0
+
+(** Add local universes to a polymorphic section *)
+val push_section_context : (Name.t array * Univ.UContext.t) -> safe_transformer0
+
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> ModPath.t safe_transformer
diff --git a/kernel/section.ml b/kernel/section.ml
new file mode 100644
index 0000000000..12e9c2fd60
--- /dev/null
+++ b/kernel/section.ml
@@ -0,0 +1,250 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+open Univ
+
+module NamedDecl = Context.Named.Declaration
+
+type _ section_kind =
+| SecMono : [ `mono ] section_kind
+| SecPoly : [ `poly ] section_kind
+
+type _ section_universes =
+| SecMonoUniv : [ `mono ] section_universes
+| SecPolyUniv : Name.t array * UContext.t -> [ `poly ] section_universes
+
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
+
+type 'a section = {
+  sec_context : int;
+  (** Length of the named context suffix that has been introduced locally *)
+  sec_universes : 'a section_universes;
+  (** Universes local to the section *)
+  sec_entries : section_entry list;
+  (** Definitions introduced in the section *)
+  sec_data : 'a section_universes entry_map;
+}
+
+(** Sections can be nested with the proviso that no monomorphic section can be
+    opened inside a polymorphic one. The reverse is allowed. *)
+type t = {
+  sec_poly : [ `poly ] section list;
+  sec_mono : [ `mono ] section list;
+}
+
+let empty = {
+  sec_poly = [];
+  sec_mono = [];
+}
+
+let is_empty s =
+  List.is_empty s.sec_poly && List.is_empty s.sec_mono
+
+let is_polymorphic s =
+  not (List.is_empty s.sec_poly)
+
+let find_emap e (cmap, imap) = match e with
+| SecDefinition con -> Cmap.find con cmap
+| SecInductive ind -> Mindmap.find ind imap
+
+let add_emap e v (cmap, imap) = match e with
+| SecDefinition con -> (Cmap.add con v cmap, imap)
+| SecInductive ind -> (cmap, Mindmap.add ind v imap)
+
+type on_sec = { on_sec : 'a. 'a section_kind -> 'a section -> 'a section }
+
+let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> CErrors.user_err (Pp.str "No opened section")
+| sec :: rem, _ ->
+  let sec_poly = f.on_sec SecPoly sec :: rem in
+  { sec_mono; sec_poly }
+| [], sec :: rem ->
+  let sec_mono = f.on_sec SecMono sec :: rem in
+  { sec_mono; sec_poly }
+
+type 'r with_sec = { with_sec : 'a. ('a section_kind * 'a section) option -> 'r }
+
+let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
+| [], [] -> f.with_sec None
+| sec :: _, _ -> f.with_sec (Some (SecPoly, sec))
+| [], sec :: _ -> f.with_sec (Some (SecMono, sec))
+
+let push_local s =
+  let on_sec _ sec = { sec with sec_context = sec.sec_context + 1 } in
+  on_last_section { on_sec } s
+
+let push_context (nas, ctx) s =
+  let on_sec (type a) (kind : a section_kind) (sec : a section) : a section = match kind with
+  | SecMono ->
+    CErrors.anomaly (Pp.str "Adding polymorphic constraints to monomorphic section")
+  | SecPoly ->
+    let SecPolyUniv (snas, sctx) = sec.sec_universes in
+    let sec_universes = SecPolyUniv (Array.append snas nas, UContext.union sctx ctx) in
+    { sec with sec_universes }
+  in
+  on_last_section { on_sec } s
+
+let open_section ~poly sections =
+  if poly then
+    let sec = {
+      sec_context = 0;
+      sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
+      sec_entries = [];
+      sec_data = (Cmap.empty, Mindmap.empty);
+    } in
+    { sections with sec_poly = sec :: sections.sec_poly }
+  else if List.is_empty sections.sec_poly then
+    let sec = {
+      sec_context = 0;
+      sec_universes = SecMonoUniv;
+      sec_entries = [];
+      sec_data = (Cmap.empty, Mindmap.empty);
+    } in
+    { sections with sec_mono = sec :: sections.sec_mono }
+  else
+    CErrors.user_err (Pp.str "Cannot open a monomorphic section inside a polymorphic one")
+
+let close_section sections =
+  (* TODO: implement me correctly when discharging in kernel *)
+  match sections.sec_poly, sections.sec_mono with
+  | _sec :: psecs, _ ->
+    let sections = { sections with sec_poly = psecs } in
+    sections
+  | [], _sec :: msecs ->
+    let sections = { sections with sec_mono = msecs } in
+    sections
+  | [], [] ->
+    CErrors.user_err (Pp.str "No opened section.")
+
+let same_poly (type a) ~poly (knd : a section_kind) = match knd with
+| SecPoly -> poly
+| SecMono -> not poly
+
+let push_global ~poly e s =
+  if is_empty s then s
+  else
+    let on_sec knd sec =
+      if same_poly ~poly knd then { sec with
+        sec_entries = e :: sec.sec_entries;
+        sec_data = add_emap e sec.sec_universes sec.sec_data;
+      } else
+        CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
+          monomorphic declarations in sections.")
+    in
+    on_last_section { on_sec } s
+
+let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
+
+let push_inductive ~poly ind s = push_global ~poly (SecInductive ind) s
+
+type abstr_info = {
+  abstr_ctx : Constr.named_context;
+  abstr_subst : Univ.Instance.t;
+  abstr_uctx : Univ.AUContext.t;
+}
+
+let empty_segment = {
+  abstr_ctx = [];
+  abstr_subst = Instance.empty;
+  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 section_segment_of_entry vars e hyps sections =
+  (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
+    global *)
+  let with_sec (type a) (s : (a section_kind * a section) option) = match s with
+  | None ->
+    CErrors.user_err (Pp.str "No opened section.")
+  | Some (knd, sec) ->
+    let hyps = extract_hyps sec vars hyps in
+    let inst, auctx = match knd, find_emap e sec.sec_data with
+    | SecMono, SecMonoUniv ->
+      Instance.empty, AUContext.empty
+    | SecPoly, SecPolyUniv (nas, ctx) ->
+      Univ.abstract_universes nas ctx
+    in
+    {
+      abstr_ctx = hyps;
+      abstr_subst = inst;
+      abstr_uctx = auctx;
+    }
+  in
+  with_last_section { with_sec } 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 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 instance_from_variable_context =
+  List.rev %> List.filter NamedDecl.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 replacement_context env s =
+  let with_sec sec = match sec with
+  | None -> CErrors.user_err (Pp.str "No opened section.")
+  | Some (_, sec) ->
+    let cmap, imap = sec.sec_data in
+    let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
+    let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
+    (cmap, imap)
+  in
+  with_last_section { with_sec } s
+
+let is_in_section env gr s =
+  let with_sec sec = match sec with
+  | None -> false
+  | Some (_, sec) ->
+    let open GlobRef in
+    match gr with
+    | VarRef id ->
+      let vars = List.firstn sec.sec_context (Environ.named_context env) in
+      List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
+    | ConstRef con ->
+      Cmap.mem con (fst sec.sec_data)
+    | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
+      Mindmap.mem ind (snd sec.sec_data)
+  in
+  with_last_section { with_sec } s
+
+let is_polymorphic_univ u s =
+  let check sec =
+    let SecPolyUniv (_, uctx) = sec.sec_universes in
+    Array.mem u (Instance.to_array (UContext.instance uctx))
+  in
+  List.exists check s.sec_poly
diff --git a/kernel/section.mli b/kernel/section.mli
new file mode 100644
index 0000000000..4b23115ca2
--- /dev/null
+++ b/kernel/section.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Univ
+
+(** Kernel implementation of sections. *)
+
+type t
+(** Type of sections *)
+
+val empty : t
+
+val is_empty : t -> bool
+(** Checks whether there is no opened section *)
+
+val is_polymorphic : t -> bool
+(** Checks whether last opened section is polymorphic *)
+
+(** {6 Manipulating sections} *)
+
+val open_section : poly:bool -> t -> t
+(** Open a new section with the provided universe polymorphic status. Sections
+    can be nested, with the proviso that polymorphic sections cannot appear
+    inside a monomorphic one. *)
+
+val close_section : t -> t
+
+(** {6 Extending sections} *)
+
+val push_local : t -> t
+(** Extend the current section with a local definition (cf. push_named). *)
+
+val push_context : Name.t array * UContext.t -> t -> t
+(** Extend the current section with a local universe context. Assumes that the
+    last opened section is polymorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> t -> t
+(** Make the constant as having been defined in this section. *)
+
+val push_inductive : poly:bool -> MutInd.t -> t -> t
+(** Make the inductive block as having been defined in this section. *)
+
+(** {6 Retrieving section data} *)
+
+type abstr_info = private {
+  abstr_ctx : Constr.named_context;
+  (** Section variables of this prefix *)
+  abstr_subst : Univ.Instance.t;
+  (** Actual names of the abstracted variables *)
+  abstr_uctx : Univ.AUContext.t;
+  (** Universe quantification, same length as the substitution *)
+}
+(** Data needed to abstract over the section variable and universe hypotheses *)
+
+
+val empty_segment : abstr_info
+(** Nothing to abstract *)
+
+val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+(** Section segment at the time of the constant declaration *)
+
+val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+(** Section segment at the time of the inductive declaration *)
+
+val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+(** Section segments of all declarations from this section. *)
+
+val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+
+val is_polymorphic_univ : Level.t -> t -> bool