Section.t is never empty

This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.

We may instead consider using `type t = section * section list` which
needs some boilerplate to update.

4 files changed, 106 insertions, 148 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 06f5aae047..759feda9ab 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -122,7 +122,7 @@ type section_data = {
 
 type safe_environment =
   { env : Environ.env;
-    sections : section_data Section.t;
+    sections : section_data Section.t option;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -159,7 +159,7 @@ let empty_environment =
     revstruct = [];
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
-    sections = Section.empty;
+    sections = None;
     future_cst = [];
     univ = Univ.ContextSet.empty;
     engagement = None;
@@ -173,7 +173,7 @@ let is_initial senv =
   | [], NONE -> ModPath.equal senv.modpath ModPath.initial
   | _ -> false
 
-let sections_are_opened senv = not (Section.is_empty senv.sections)
+let sections_are_opened senv = not (Option.is_empty senv.sections)
 
 let delta_of_senv senv = senv.modresolver,senv.paramresolver
 
@@ -323,6 +323,10 @@ let env_of_senv = env_of_safe_env
 
 let sections_of_safe_env senv = senv.sections
 
+let get_section = function
+  | None -> CErrors.user_err Pp.(str "No open section.")
+  | Some s -> s
+
 type constraints_addition =
   | Now of Univ.ContextSet.t
   | Later of Univ.ContextSet.t Future.computation
@@ -330,9 +334,7 @@ type constraints_addition =
 let push_context_set poly cst senv =
   if Univ.ContextSet.is_empty cst then senv
   else
-    let sections =
-      if Section.is_empty senv.sections then senv.sections
-      else Section.push_constraints cst senv.sections
+    let sections = Option.map (Section.push_constraints cst) senv.sections
     in
     { senv with
       env = Environ.push_context_set ~strict:(not poly) cst senv.env;
@@ -399,7 +401,7 @@ let check_current_library dir senv = match senv.modvariant with
 (** When operating on modules, we're normally outside sections *)
 
 let check_empty_context senv =
-  assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
+  assert (Environ.empty_context senv.env && Option.is_empty senv.sections)
 
 (** When adding a parameter to the current module/modtype,
     it must have been freshly started *)
@@ -447,22 +449,25 @@ let safe_push_named d env =
   Environ.push_named d env
 
 let push_named_def (id,de) senv =
-  let sections = Section.push_local senv.sections in
+  let sections = get_section senv.sections in
+  let sections = Section.push_local 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 sections; env = env'' }
+  { senv with sections=Some sections; env = env'' }
 
 let push_named_assum (x,t) senv =
-  let sections = Section.push_local senv.sections in
+  let sections = get_section senv.sections in
+  let sections = Section.push_local 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 sections; env = env'' }
+  { senv with sections=Some 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 sections = get_section senv.sections in
+  let sections = Section.push_context (nas, ctx) sections in
+  let senv = { senv with sections=Some 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. *)
@@ -551,15 +556,18 @@ 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
+  let sections = match senv.sections with
+    | None -> None
+    | Some sections ->
+      match sfb, gn with
+      | SFBconst cb, C con ->
+        let poly = Declareops.constant_is_polymorphic cb in
+        Some (Section.push_constant ~poly con sections)
+      | SFBmind mib, I mind ->
+        let poly = Declareops.inductive_is_polymorphic mib in
+        Some (Section.push_inductive ~poly mind sections)
+      | _, (M | MT) -> Some sections
+      | _ -> assert false
   in
   { senv with
     env = env';
@@ -952,11 +960,11 @@ let open_section senv =
     rev_objlabels = senv.objlabels;
   } in
   let sections = Section.open_section ~custom senv.sections in
-  { senv with sections }
+  { senv with sections=Some sections }
 
 let close_section senv =
   let open Section in
-  let sections0 = senv.sections in
+  let sections0 = get_section 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
@@ -990,7 +998,7 @@ let close_section senv =
   let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) 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 senv = push_context_set false cstrs senv in
   let modlist = Section.replacement_context env0 sections0 in
   let cooking_info seg =
     let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ae6993b0e2..0b7ca26e09 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -35,7 +35,7 @@ val is_initial : safe_environment -> bool
 
 val env_of_safe_env : safe_environment -> Environ.env
 
-val sections_of_safe_env : safe_environment -> section_data Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t option
 
 (** The safe_environment state monad *)
 
diff --git a/kernel/section.ml b/kernel/section.ml
index a1242f0faf..603ef5d006 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -20,7 +20,9 @@ type section_entry =
 
 type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
 
-type 'a section = {
+type 'a t = {
+  sec_prev : 'a t option;
+  (** Section surrounding the current one *)
   sec_context : int;
   (** Length of the named context suffix that has been introduced locally *)
   sec_mono_universes : ContextSet.t;
@@ -35,19 +37,9 @@ type 'a section = {
   sec_custom : 'a;
 }
 
-(** Sections can be nested with the proviso that no monomorphic section can be
-    opened inside a polymorphic one. The reverse is allowed. *)
-type 'a t = 'a section list
+let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth prev
 
-let empty = []
-
-let is_empty = List.is_empty
-
-let depth = List.length
-
-let has_poly_univs = function
-  | [] -> false
-  | sec :: _ -> sec.has_poly_univs
+let has_poly_univs sec = sec.has_poly_univs
 
 let find_emap e (cmap, imap) = match e with
 | SecDefinition con -> Cmap.find con cmap
@@ -57,80 +49,59 @@ 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)
 
-let on_last_section f sections = match sections with
-| [] -> CErrors.user_err (Pp.str "No opened section")
-| sec :: rem -> f sec :: rem
-
-let with_last_section f sections = match sections with
-| [] -> f None
-| sec :: _ -> f (Some 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 sec =
-      if UContext.is_empty ctx then sec
-      else
-        let (snas, sctx) = sec.sec_poly_universes in
-        let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
-        { sec with sec_poly_universes; has_poly_univs = true }
-    in
-    on_last_section on_sec s
-
-let is_polymorphic_univ u s =
-  let check sec =
-    let (_, uctx) = sec.sec_poly_universes in
-    Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx))
-  in
-  List.exists check s
-
-let push_constraints uctx s =
-  let on_sec sec =
-    if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx)
-    then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
-    let uctx' = sec.sec_mono_universes in
-    let sec_mono_universes =  (ContextSet.union uctx uctx') in
-    { sec with sec_mono_universes }
-  in
-  on_last_section on_sec s
-
-let open_section ~custom sections =
-  let sec = {
+let push_local sec =
+  { sec with sec_context = sec.sec_context + 1 }
+
+let push_context (nas, ctx) sec =
+  if UContext.is_empty ctx then sec
+  else
+    let (snas, sctx) = sec.sec_poly_universes in
+    let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
+    { sec with sec_poly_universes; has_poly_univs = true }
+
+let rec is_polymorphic_univ u sec =
+  let (_, uctx) = sec.sec_poly_universes in
+  let here = Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) in
+  here || Option.cata (is_polymorphic_univ u) false sec.sec_prev
+
+let push_constraints uctx sec =
+  if sec.has_poly_univs &&
+     Constraint.exists
+       (fun (l,_,r) -> is_polymorphic_univ l sec || is_polymorphic_univ r sec)
+       (snd uctx)
+  then CErrors.user_err
+      Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
+  let uctx' = sec.sec_mono_universes in
+  let sec_mono_universes =  (ContextSet.union uctx uctx') in
+  { sec with sec_mono_universes }
+
+let open_section ~custom sec_prev =
+  {
+    sec_prev;
     sec_context = 0;
     sec_mono_universes = ContextSet.empty;
     sec_poly_universes = ([||], UContext.empty);
-    has_poly_univs = has_poly_univs sections;
+    has_poly_univs = Option.cata has_poly_univs false sec_prev;
     sec_entries = [];
     sec_data = (Cmap.empty, Mindmap.empty);
     sec_custom = custom;
-  } in
-  sec :: sections
+  }
 
-let close_section sections =
-  match sections with
-  | sec :: sections ->
-    sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
-  | [] ->
-    CErrors.user_err (Pp.str "No opened section.")
+let close_section sec =
+  sec.sec_prev, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
 
 let make_decl_univs (nas,uctx) = abstract_universes nas uctx
 
-let push_global ~poly e s =
-  if is_empty s then s
-  else if has_poly_univs s && not poly
+let push_global ~poly e sec =
+  if has_poly_univs sec && not poly
   then CErrors.user_err
       Pp.(str "Cannot add a universe monomorphic declaration when \
                section polymorphic universes are present.")
   else
-    let on_sec sec =
-      { sec with
-        sec_entries = e :: sec.sec_entries;
-        sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
-      }
-    in
-    on_last_section on_sec s
+    { sec with
+      sec_entries = e :: sec.sec_entries;
+      sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
+    }
 
 let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
 
@@ -154,22 +125,16 @@ let extract_hyps sec vars used =
   (* Only keep the part that is used by the declaration *)
   List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
 
-let section_segment_of_entry vars e hyps sections =
+let section_segment_of_entry vars e hyps sec =
   (* [vars] are the named hypotheses, [hyps] the subset that is declared by the
-    global *)
-  let with_sec s = match s with
-  | None ->
-    CErrors.user_err (Pp.str "No opened section.")
-  | Some sec ->
-    let hyps = extract_hyps sec vars hyps in
-    let inst, auctx = find_emap e sec.sec_data in
-    {
-      abstr_ctx = hyps;
-      abstr_subst = inst;
-      abstr_uctx = auctx;
-    }
-  in
-  with_last_section with_sec sections
+     global *)
+  let hyps = extract_hyps sec vars hyps in
+  let inst, auctx = find_emap e sec.sec_data in
+  {
+    abstr_ctx = hyps;
+    abstr_subst = inst;
+    abstr_uctx = auctx;
+  }
 
 let segment_of_constant env con s =
   let body = Environ.lookup_constant con env in
@@ -190,29 +155,19 @@ 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 replacement_context env sec =
+  let cmap, imap = sec.sec_data in
+  let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con sec) cmap in
+  let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind sec) imap in
+  (cmap, imap)
+
+let is_in_section env gr 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)
diff --git a/kernel/section.mli b/kernel/section.mli
index ec863b3b90..fbd3d8254e 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -16,13 +16,8 @@ open Univ
 type 'a t
 (** Type of sections with additional data ['a] *)
 
-val empty : 'a t
-
-val is_empty : 'a t -> bool
-(** Checks whether there is no opened section *)
-
 val depth : 'a t -> int
-(** Number of nested sections (0 if no sections are open) *)
+(** Number of nested sections. *)
 
 (** {6 Manipulating sections} *)
 
@@ -30,13 +25,13 @@ type section_entry =
 | SecDefinition of Constant.t
 | SecInductive of MutInd.t
 
-val open_section : custom:'a -> 'a t -> 'a t
+val open_section : custom:'a -> 'a t option -> '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. A custom data can be attached to this section,
     that will be returned by {!close_section}. *)
 
-val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a
+val close_section : 'a t -> 'a t option * 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. *)