1 files changed, 157 insertions, 44 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6970a11e72..9b4d2e69ac 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -113,8 +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_data Section.t;
     modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
@@ -151,6 +159,7 @@ let empty_environment =
     revstruct = [];
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
+    sections = Section.empty;
     future_cst = [];
     univ = Univ.ContextSet.empty;
     engagement = None;
@@ -317,14 +326,23 @@ 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 =
-  { senv with
-    env = Environ.push_context_set ~strict:(not poly) cst senv.env;
-    univ = Univ.ContextSet.union cst senv.univ }
+  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
+    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
@@ -386,7 +404,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)
+  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 *)
@@ -433,19 +451,30 @@ let safe_push_named d env =
     with Not_found -> () in
   Environ.push_named d env
 
-
 let push_named_def (id,de) senv =
+  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 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 } *)
 
@@ -527,8 +556,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 }
@@ -549,30 +589,9 @@ type exported_private_constant = Constant.t
 
 let add_constant_aux ~in_section senv (kn, cb) =
   let l = Constant.label kn in
-  let delayed_cst = match cb.const_body with
-  | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) ->
-    let fc = Opaqueproof.get_direct_constraints o in
-    begin match Future.peek_val fc with
-    | None -> [Later fc]
-    | Some c -> [Now c]
-    end
-  | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> []
-  in
   (* This is the only place where we hashcons the contents of a constant body *)
   let cb = if in_section then cb else Declareops.hcons_const_body cb in
-  let cb, otab = match cb.const_body with
-    | OpaqueDef lc when not in_section ->
-      (* In coqc, opaque constants outside sections will be stored
-         indirectly in a specific table *)
-      let od, otab =
-        Opaqueproof.turn_indirect
-          (library_dp_of_senv senv) lc (Environ.opaque_tables senv.env) in
-      { cb with const_body = OpaqueDef od }, otab
-    | _ -> cb, (Environ.opaque_tables senv.env)
-  in
-  let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
-  let senv' = add_constraints_list delayed_cst senv' in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
       update_resolver
@@ -703,7 +722,7 @@ let constant_entry_of_side_effect eff =
   if Declareops.is_opaque cb then
   OpaqueEff {
     opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ());
-    opaque_entry_secctx = cb.const_hyps;
+    opaque_entry_secctx = Context.Named.to_vars cb.const_hyps;
     opaque_entry_feedback = None;
     opaque_entry_type = cb.const_type;
     opaque_entry_universes = univs;
@@ -711,7 +730,7 @@ let constant_entry_of_side_effect eff =
   else
   DefinitionEff {
     const_entry_body = p;
-    const_entry_secctx = Some cb.const_hyps;
+    const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps);
     const_entry_feedback = None;
     const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
@@ -775,27 +794,30 @@ let export_side_effects mb env (b_ctx, eff) =
      in
        translate_seff trusted seff [] env
 
+let push_opaque_proof pf senv =
+  let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in
+  let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
+  senv, o
+
 let export_private_constants ~in_section ce senv =
   let exported, ce = export_side_effects senv.revstruct senv.env ce in
-  let map univs p =
-    let local = match univs with
+  let map senv (kn, c) = match c.const_body with
+  | OpaqueDef p ->
+    let local = match c.const_universes with
     | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
     | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
     in
-    Opaqueproof.create (Future.from_val (p, local))
+    let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in
+    senv, (kn, { c with const_body = OpaqueDef o })
+  | Def _ | Undef _ | Primitive _ as body ->
+    senv, (kn, { c with const_body = body })
   in
-  let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
-  let bodies = List.map map exported in
+  let senv, bodies = List.fold_left_map map senv exported in
   let exported = List.map (fun (kn, _) -> kn) exported in
+  (* No delayed constants to declare *)
   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 cb = Term_typing.translate_recipe senv.env kn r in
-  let senv = add_constant_aux ~in_section senv (kn, cb) in
-  kn, 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
     let cb = 
@@ -811,8 +833,29 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
         Term_typing.translate_constant Term_typing.Pure senv.env kn ce
     in
   let senv =
-    let cb = map_constant (fun c -> Opaqueproof.create c) cb in
-    add_constant_aux ~in_section senv (kn, cb) in
+    let senv, cb, delayed_cst = match cb.const_body with
+    | OpaqueDef fc ->
+      let senv, o = push_opaque_proof fc senv in
+      let delayed_cst =
+        if not (Declareops.constant_is_polymorphic cb) then
+          let map (_, u) = match u with
+          | Opaqueproof.PrivateMonomorphic ctx -> ctx
+          | Opaqueproof.PrivatePolymorphic _ -> assert false
+          in
+          let fc = Future.chain fc map in
+          match Future.peek_val fc with
+          | None -> [Later fc]
+          | Some c -> [Now c]
+        else []
+      in
+      senv, { cb with const_body = OpaqueDef o }, delayed_cst
+    | Undef _ | Def _ | Primitive _ as body ->
+      senv, { cb with const_body = body }, []
+    in
+    let senv = add_constant_aux ~in_section senv (kn, cb) in
+    add_constraints_list delayed_cst senv
+  in
+
   let senv =
     match decl with
     | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) ->
@@ -902,6 +945,76 @@ let add_module l me inl senv =
   in
   (mp,mb.mod_delta),senv''
 
+(** {6 Interactive sections *)
+
+let open_section senv =
+  let custom = {
+    rev_env = senv.env;
+    rev_univ = senv.univ;
+    rev_objlabels = senv.objlabels;
+  } in
+  let sections = Section.open_section ~custom senv.sections in
+  { senv with sections }
+
+let close_section senv =
+  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 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. Those that are not forced are not readded
+     by {!add_constant_aux}. *)
+  let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in
+  (* Do not revert the opaque table, the discharged opaque constants are
+     referring to it. *)
+  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 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
+    let cb = Term_typing.translate_recipe senv.env kn r in
+    (* Delayed constants are already in the global environment *)
+    add_constant_aux ~in_section senv (kn, cb)
+  | `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 } *)