Implement section discharging inside kernel.

This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.

4 files changed, 153 insertions, 56 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8d34f3a34f..ddaed6c941 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,9 +113,16 @@ type library_info = DirPath.t * vodigest
 (** Functor and funsig parameters, most recent first *)
 type module_parameters = (MBId.t * module_type_body) list
 
+(** Part of the safe_env at a section opening time to be backtracked *)
+type section_data = {
+  rev_env : Environ.env;
+  rev_univ : Univ.ContextSet.t;
+  rev_objlabels : Label.Set.t;
+}
+
 type safe_environment =
   { env : Environ.env;
-    sections : Section.t;
+    sections : section_data Section.t;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -326,12 +333,18 @@ type constraints_addition =
   | 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
+  if Univ.ContextSet.is_empty cst then senv
+  else if Section.is_polymorphic senv.sections 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 }
+  else
+    let sections =
+      if Section.is_empty senv.sections then senv.sections
+      else Section.push_constraints cst senv.sections
+    in
+    { senv with
+      env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+      univ = Univ.ContextSet.union cst senv.univ;
+      sections }
 
 let add_constraints cst senv =
   match cst with
@@ -819,11 +832,10 @@ let export_private_constants ~in_section ce senv =
   let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
   (ce, exported), senv
 
-let add_recipe ~in_section l r senv =
-  let kn = Constant.make2 senv.modpath l in
+let add_recipe ~in_section kn r senv =
   let cb = Term_typing.translate_recipe senv.env kn r in
   let senv = add_constant_aux ~in_section senv (kn, cb) in
-  kn, senv
+  senv
 
 let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
@@ -934,13 +946,68 @@ let add_module l me inl senv =
 (** {6 Interactive sections *)
 
 let open_section ~poly senv =
-  let sections = Section.open_section ~poly senv.sections in
+  let custom = {
+    rev_env = senv.env;
+    rev_univ = senv.univ;
+    rev_objlabels = senv.objlabels;
+  } in
+  let sections = Section.open_section ~poly ~custom senv.sections in
   { senv with sections }
 
 let close_section senv =
-  (* TODO: implement me when discharging in kernel *)
-  let sections = Section.close_section senv.sections in
-  { senv with sections }
+  let open Section in
+  let sections0 = senv.sections in
+  let env0 = senv.env in
+  (* First phase: revert the declarations added in the section *)
+  let sections, entries, cstrs, revert = Section.close_section sections0 in
+  let () = assert (not (Section.is_polymorphic sections0) || Univ.ContextSet.is_empty cstrs) in
+  let rec pop_revstruct accu entries revstruct = match entries, revstruct with
+  | [], revstruct -> accu, revstruct
+  | _ :: _, [] ->
+    CErrors.anomaly (Pp.str "Unmatched section data")
+  | entry :: entries, (lbl, leaf) :: revstruct ->
+    let data = match entry, leaf with
+    | SecDefinition kn, SFBconst cb ->
+      let () = assert (Label.equal lbl (Constant.label kn)) in
+      `Definition (kn, cb)
+    | SecInductive ind, SFBmind mib ->
+      let () = assert (Label.equal lbl (MutInd.label ind)) in
+      `Inductive (ind, mib)
+    | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) ->
+      CErrors.anomaly (Pp.str "Section content mismatch")
+    | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) ->
+      CErrors.anomaly (Pp.str "Module inside a section")
+    in
+    pop_revstruct (data :: accu) entries revstruct
+  in
+  let redo, revstruct = pop_revstruct [] entries senv.revstruct in
+  (* Don't revert the delayed constraints. If some delayed constraints were
+     forced inside the section, they have been turned into global monomorphic
+     that are going to be replayed. FIXME: the other ones are added twice. *)
+  let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in
+  let senv = { senv with env; revstruct; sections; univ; objlabels; } in
+  (* Second phase: replay the discharged section contents *)
+  let senv = add_constraints (Now cstrs) senv in
+  let modlist = Section.replacement_context env0 sections0 in
+  let cooking_info seg =
+    let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
+    let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in
+    { Opaqueproof.modlist; abstract }
+  in
+  let fold senv = function
+  | `Definition (kn, cb) ->
+    let in_section = not (Section.is_empty senv.sections) in
+    let info = cooking_info (Section.segment_of_constant env0 kn sections0) in
+    let r = { Cooking.from = cb; info } in
+    add_recipe ~in_section kn r senv
+  | `Inductive (ind, mib) ->
+    let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
+    let mie = Cooking.cook_inductive info mib in
+    let mie = InferCumulativity.infer_inductive senv.env mie in
+    let _, senv = add_mind (MutInd.label ind) mie senv in
+    senv
+  in
+  List.fold_left fold senv redo
 
 (** {6 Starting / ending interactive modules and module types } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 10fedc2faf..d3ca642a89 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -27,13 +27,15 @@ val digest_match : actual:vodigest -> required:vodigest -> bool
 
 type safe_environment
 
+type section_data
+
 val empty_environment : safe_environment
 
 val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
-val sections_of_safe_env : safe_environment -> Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t
 
 (** The safe_environment state monad *)
 
@@ -89,9 +91,6 @@ val add_constant :
   side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration ->
     (Constant.t * 'a) safe_transformer
 
-val add_recipe :
-  in_section:bool -> Label.t -> Cooking.recipe -> Constant.t safe_transformer
-
 (** Adding an inductive type *)
 
 val add_mind :
diff --git a/kernel/section.ml b/kernel/section.ml
index 12e9c2fd60..188249e77e 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -18,9 +18,9 @@ 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 (_, 'a) section_universes =
+| SecMonoUniv : 'a -> ([ `mono ], 'a) section_universes
+| SecPolyUniv : Name.t array * UContext.t -> ([ `poly ], 'a) section_universes
 
 type section_entry =
 | SecDefinition of Constant.t
@@ -28,21 +28,23 @@ type section_entry =
 
 type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
 
-type 'a section = {
+type ('a, 'b) section = {
   sec_context : int;
   (** Length of the named context suffix that has been introduced locally *)
-  sec_universes : 'a section_universes;
+  sec_universes : ('a, ContextSet.t) section_universes;
   (** Universes local to the section *)
   sec_entries : section_entry list;
   (** Definitions introduced in the section *)
-  sec_data : 'a section_universes entry_map;
+  sec_data : ('a, unit) section_universes entry_map;
+  (** Additional data synchronized with the section *)
+  sec_custom : 'b;
 }
 
 (** 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;
+type 'a t = {
+  sec_poly : ([ `poly ], 'a) section list;
+  sec_mono : ([ `mono ], 'a) section list;
 }
 
 let empty = {
@@ -64,7 +66,7 @@ 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 }
+type 'b on_sec = { on_sec : 'a. 'a section_kind -> ('a, 'b) section -> ('a, 'b) section }
 
 let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
 | [], [] -> CErrors.user_err (Pp.str "No opened section")
@@ -75,7 +77,7 @@ let on_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
   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 }
+type ('r, 'b) with_sec = { with_sec : 'a. ('a section_kind * ('a, 'b) section) option -> 'r }
 
 let with_last_section f { sec_poly; sec_mono } = match sec_poly, sec_mono with
 | [], [] -> f.with_sec None
@@ -87,7 +89,7 @@ let push_local s =
   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
+  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 ->
@@ -97,35 +99,48 @@ let push_context (nas, ctx) s =
   in
   on_last_section { on_sec } s
 
-let open_section ~poly sections =
+let push_constraints uctx s =
+  let on_sec (type a) (kind : a section_kind) (sec : (a, _) section) : (a, _) section = match kind with
+  | SecMono ->
+    let SecMonoUniv uctx' = sec.sec_universes in
+    let sec_universes = SecMonoUniv (ContextSet.union uctx uctx') in
+    { sec with sec_universes }
+  | SecPoly ->
+    CErrors.anomaly (Pp.str "Adding monomorphic constraints to polymorphic section")
+  in
+  on_last_section { on_sec } s
+
+let open_section ~poly ~custom sections =
   if poly then
     let sec = {
       sec_context = 0;
       sec_universes = SecPolyUniv ([||], Univ.UContext.empty);
       sec_entries = [];
       sec_data = (Cmap.empty, Mindmap.empty);
+      sec_custom = custom;
     } 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_universes = SecMonoUniv Univ.ContextSet.empty;
       sec_entries = [];
       sec_data = (Cmap.empty, Mindmap.empty);
+      sec_custom = custom;
     } 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, _ ->
+  | sec :: psecs, _ ->
     let sections = { sections with sec_poly = psecs } in
-    sections
-  | [], _sec :: msecs ->
+    sections, sec.sec_entries, Univ.ContextSet.empty, sec.sec_custom
+  | [], sec :: msecs ->
     let sections = { sections with sec_mono = msecs } in
-    sections
+    let SecMonoUniv cstrs = sec.sec_universes in
+    sections, sec.sec_entries, cstrs, sec.sec_custom
   | [], [] ->
     CErrors.user_err (Pp.str "No opened section.")
 
@@ -133,13 +148,17 @@ let same_poly (type a) ~poly (knd : a section_kind) = match knd with
 | SecPoly -> poly
 | SecMono -> not poly
 
+let drop_global (type a) : (a, _) section_universes -> (a, unit) section_universes = function
+| SecMonoUniv _ -> SecMonoUniv ()
+| SecPolyUniv _ as u -> u
+
 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;
+        sec_data = add_emap e (drop_global sec.sec_universes) sec.sec_data;
       } else
         CErrors.user_err (Pp.str "Cannot mix universe polymorphic and \
           monomorphic declarations in sections.")
@@ -179,13 +198,13 @@ let extract_hyps sec vars 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
+  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 ->
+    | SecMono, SecMonoUniv () ->
       Instance.empty, AUContext.empty
     | SecPoly, SecPolyUniv (nas, ctx) ->
       Univ.abstract_universes nas ctx
diff --git a/kernel/section.mli b/kernel/section.mli
index 4b23115ca2..c1026a2980 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -13,39 +13,51 @@ open Univ
 
 (** Kernel implementation of sections. *)
 
-type t
-(** Type of sections *)
+type 'a t
+(** Type of sections with additional data ['a] *)
 
-val empty : t
+val empty : 'a t
 
-val is_empty : t -> bool
+val is_empty : 'a t -> bool
 (** Checks whether there is no opened section *)
 
-val is_polymorphic : t -> bool
+val is_polymorphic : 'a t -> bool
 (** Checks whether last opened section is polymorphic *)
 
 (** {6 Manipulating sections} *)
 
-val open_section : poly:bool -> t -> t
+type section_entry =
+| SecDefinition of Constant.t
+| SecInductive of MutInd.t
+
+val open_section : poly:bool -> custom:'a -> 'a t -> 'a 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. *)
+    inside a monomorphic one. A custom data can be attached to this section,
+    that will be returned by {!close_section}. *)
 
-val close_section : t -> t
+val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a
+(** Close the current section and returns the entries defined inside, the set
+    of global monomorphic constraints added in this section, and the custom data
+    provided at the opening of the section. *)
 
 (** {6 Extending sections} *)
 
-val push_local : t -> t
+val push_local : 'a t -> 'a t
 (** Extend the current section with a local definition (cf. push_named). *)
 
-val push_context : Name.t array * UContext.t -> t -> t
+val push_context : Name.t array * UContext.t -> 'a t -> 'a 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
+val push_constraints : ContextSet.t -> 'a t -> 'a t
+(** Extend the current section with a global universe context.
+    Assumes that the last opened section is monomorphic. *)
+
+val push_constant : poly:bool -> Constant.t -> 'a t -> 'a t
 (** Make the constant as having been defined in this section. *)
 
-val push_inductive : poly:bool -> MutInd.t -> t -> t
+val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
 (** Make the inductive block as having been defined in this section. *)
 
 (** {6 Retrieving section data} *)
@@ -64,15 +76,15 @@ type abstr_info = private {
 val empty_segment : abstr_info
 (** Nothing to abstract *)
 
-val segment_of_constant : Environ.env -> Constant.t -> t -> abstr_info
+val segment_of_constant : Environ.env -> Constant.t -> 'a t -> abstr_info
 (** Section segment at the time of the constant declaration *)
 
-val segment_of_inductive : Environ.env -> MutInd.t -> t -> abstr_info
+val segment_of_inductive : Environ.env -> MutInd.t -> 'a t -> abstr_info
 (** Section segment at the time of the inductive declaration *)
 
-val replacement_context : Environ.env -> t -> Opaqueproof.work_list
+val replacement_context : Environ.env -> 'a t -> Opaqueproof.work_list
 (** Section segments of all declarations from this section. *)
 
-val is_in_section : Environ.env -> GlobRef.t -> t -> bool
+val is_in_section : Environ.env -> GlobRef.t -> 'a t -> bool
 
-val is_polymorphic_univ : Level.t -> t -> bool
+val is_polymorphic_univ : Level.t -> 'a t -> bool