[declaremods] Remove abstraction layer over module interpretation.

Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.

Improvement suggested by Gaëtan Gilbert.

5 files changed, 72 insertions, 99 deletions

diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh
new file mode 100644
index 0000000000..a5f6551474
--- /dev/null
+++ b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then
+
+    elpi_CI_REF=library+to_vernac_step2
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 9f2e30b7a6..58a7dff5fd 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -17,7 +17,6 @@ open Entries
 open Libnames
 open Libobject
 open Mod_subst
-open Modintern
 
 (** {6 Inlining levels} *)
 
@@ -546,11 +545,11 @@ let process_module_binding mbid me =
     Objects in these parameters are also loaded.
     Output is accumulated on top of [acc] (in reverse order). *)
 
-let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) =
+let intern_arg (acc, cst) (idl,(typ,ann)) =
   let inl = inl2intopt ann in
   let lib_dir = Lib.library_dp() in
   let env = Global.env() in
-  let (mty, _, cst') = interp_modast env ModType typ in
+  let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in
   let () = Global.push_context_set true cst' in
   let env = Global.env () in
   let sobjs = get_module_sobjs false env inl mty in
@@ -578,8 +577,8 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) =
     be more efficient and independent of [List.map] eval order.
 *)
 
-let intern_args interp_modast params =
-  List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params
+let intern_args params =
+  List.fold_left intern_arg ([], Univ.ContextSet.empty) params
 
 
 (** {6 Auxiliary functions concerning subtyping checks} *)
@@ -630,11 +629,11 @@ let mk_funct_type env args seb0 =
 
 (** Prepare the module type list for check of subtypes *)
 
-let build_subtypes interp_modast env mp args mtys =
+let build_subtypes env mp args mtys =
   let (cst, ans) = List.fold_left_map
     (fun cst (m,ann) ->
        let inl = inl2intopt ann in
-       let mte, _, cst' = interp_modast env ModType m in
+       let mte, _, cst' = Modintern.interp_module_ast env Modintern.ModType m in
        let env = Environ.push_context_set ~strict:true cst' env in
        let cst = Univ.ContextSet.union cst cst' in
        let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in
@@ -672,22 +671,22 @@ let openmodtype_info =
 
 module RawModOps = struct
 
-let start_module interp_modast export id args res fs =
+let start_module export id args res fs =
   let mp = Global.start_module id in
-  let arg_entries_r, cst = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args args in
   let () = Global.push_context_set true cst in
   let env = Global.env () in
   let res_entry_o, subtyps, cst = match res with
     | Enforce (res,ann) ->
         let inl = inl2intopt ann in
-        let (mte, _, cst) = interp_modast env ModType res in
+        let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType res in
         let env = Environ.push_context_set ~strict:true cst env in
         (* We check immediately that mte is well-formed *)
         let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in
         let cst = Univ.ContextSet.union cst cst' in
         Some (mte, inl), [], cst
     | Check resl ->
-      let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in
+      let typs, cst = build_subtypes env mp arg_entries_r resl in
       None, typs, cst
   in
   let () = Global.push_context_set true cst in
@@ -734,25 +733,25 @@ let end_module () =
 
   mp
 
-let declare_module interp_modast id args res mexpr_o fs =
+let declare_module id args res mexpr_o fs =
   (* We simulate the beginning of an interactive module,
      then we adds the module parameters to the global env. *)
   let mp = Global.start_module id in
-  let arg_entries_r, cst = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args args in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
   let env = Environ.push_context_set ~strict:true cst env in
   let mty_entry_o, subs, inl_res, cst' = match res with
     | Enforce (mty,ann) ->
         let inl = inl2intopt ann in
-        let (mte, _, cst) = interp_modast env ModType mty in
+        let (mte, _, cst) = Modintern.interp_module_ast env Modintern.ModType mty in
         let env = Environ.push_context_set ~strict:true cst env in
         (* We check immediately that mte is well-formed *)
         let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in
         let cst = Univ.ContextSet.union cst cst' in
         Some mte, [], inl, cst
     | Check mtys ->
-      let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in
+      let typs, cst = build_subtypes env mp arg_entries_r mtys in
       None, typs, default_inline (), cst
   in
   let env = Environ.push_context_set ~strict:true cst' env in
@@ -760,7 +759,7 @@ let declare_module interp_modast id args res mexpr_o fs =
   let mexpr_entry_o, inl_expr, cst' = match mexpr_o with
     | None -> None, default_inline (), Univ.ContextSet.empty
     | Some (mexpr,ann) ->
-      let (mte, _, cst) = interp_modast env Module mexpr in
+      let (mte, _, cst) = Modintern.interp_module_ast env Modintern.Module mexpr in
       Some mte, inl2intopt ann, cst
   in
   let env = Environ.push_context_set ~strict:true cst' env in
@@ -802,12 +801,12 @@ end
 
 module RawModTypeOps = struct
 
-let start_modtype interp_modast id args mtys fs =
+let start_modtype id args mtys fs =
   let mp = Global.start_modtype id in
-  let arg_entries_r, cst = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args args in
   let () = Global.push_context_set true cst in
   let env = Global.env () in
-  let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in
+  let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
   let () = Global.push_context_set true cst in
   openmodtype_info := sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
@@ -830,16 +829,16 @@ let end_modtype () =
 
   mp
 
-let declare_modtype interp_modast id args mtys (mty,ann) fs =
+let declare_modtype id args mtys (mty,ann) fs =
   let inl = inl2intopt ann in
   (* We simulate the beginning of an interactive module,
      then we adds the module parameters to the global env. *)
   let mp = Global.start_modtype id in
-  let arg_entries_r, cst = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args args in
   let () = Global.push_context_set true cst in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let mte, _, cst = interp_modast env ModType mty in
+  let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in
   let () = Global.push_context_set true cst in
   let env = Global.env () in
   (* We check immediately that mte is well-formed *)
@@ -847,7 +846,7 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   let () = Global.push_context_set true cst in
   let env = Global.env () in
   let entry = params, mte in
-  let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in
+  let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
   let () = Global.push_context_set true cst in
   let env = Global.env () in
   let sobjs = get_functor_sobjs false env inl entry in
@@ -901,12 +900,12 @@ let type_of_incl env is_mod = function
     decompose_functor mp_l (type_of_mod mp0 env is_mod)
   |MEwith _ -> raise NoIncludeSelf
 
-let declare_one_include interp_modast (me_ast,annot) =
+let declare_one_include (me_ast,annot) =
   let env = Global.env() in
-  let me, kind, cst = interp_modast env ModAny me_ast in
+  let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in
   let () = Global.push_context_set true cst in
   let env = Global.env () in
-  let is_mod = (kind == Module) in
+  let is_mod = (kind == Modintern.Module) in
   let cur_mp = Lib.current_mp () in
   let inl = inl2intopt annot in
   let mbids,aobjs = get_module_sobjs is_mod env inl me in
@@ -924,8 +923,7 @@ let declare_one_include interp_modast (me_ast,annot) =
   let aobjs = subst_aobjs subst aobjs in
   ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs))
 
-let declare_include interp me_asts =
-  List.iter (declare_one_include interp) me_asts
+let declare_include me_asts = List.iter declare_one_include me_asts
 
 end
 
@@ -941,40 +939,40 @@ let protect_summaries f =
     let () = Summary.unfreeze_summaries fs in
     iraise reraise
 
-let start_module interp export id args res =
-  protect_summaries (RawModOps.start_module interp export id args res)
+let start_module export id args res =
+  protect_summaries (RawModOps.start_module export id args res)
 
 let end_module = RawModOps.end_module
 
-let declare_module interp id args mtys me_l =
+let declare_module id args mtys me_l =
   let declare_me fs = match me_l with
-    | [] -> RawModOps.declare_module interp id args mtys None fs
-    | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs
+    | [] -> RawModOps.declare_module id args mtys None fs
+    | [me] -> RawModOps.declare_module id args mtys (Some me) fs
     | me_l ->
-        ignore (RawModOps.start_module interp None id args mtys fs);
-        RawIncludeOps.declare_include interp me_l;
+        ignore (RawModOps.start_module None id args mtys fs);
+        RawIncludeOps.declare_include me_l;
         RawModOps.end_module ()
   in
   protect_summaries declare_me
 
-let start_modtype interp id args mtys =
-  protect_summaries (RawModTypeOps.start_modtype interp id args mtys)
+let start_modtype id args mtys =
+  protect_summaries (RawModTypeOps.start_modtype id args mtys)
 
 let end_modtype = RawModTypeOps.end_modtype
 
-let declare_modtype interp id args mtys mty_l =
+let declare_modtype id args mtys mty_l =
   let declare_mt fs = match mty_l with
     | [] -> assert false
-    | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs
+    | [mty] -> RawModTypeOps.declare_modtype id args mtys mty fs
     | mty_l ->
-        ignore (RawModTypeOps.start_modtype interp id args mtys fs);
-        RawIncludeOps.declare_include interp mty_l;
+        ignore (RawModTypeOps.start_modtype id args mtys fs);
+        RawIncludeOps.declare_include mty_l;
         RawModTypeOps.end_modtype ()
   in
   protect_summaries declare_mt
 
-let declare_include interp me_asts =
-  protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts)
+let declare_include me_asts =
+  protect_summaries (fun _ -> RawIncludeOps.declare_include me_asts)
 
 
 (** {6 Libraries} *)
@@ -1054,12 +1052,7 @@ let iter_all_segments f =
 
 (** {6 Some types used to shorten declaremods.mli} *)
 
-type 'modast module_interpretor =
-  Environ.env -> module_kind -> 'modast ->
-    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
-
-type 'modast module_params =
-  (lident list * ('modast * inline)) list
+type module_params = (lident list * (Constrexpr.module_ast * inline)) list
 
 (** {6 Debug} *)
 
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli
index 5c2c992825..ae84704656 100644
--- a/vernac/declaremods.mli
+++ b/vernac/declaremods.mli
@@ -29,32 +29,24 @@ type inline =
 
 (** Kinds of modules *)
 
-type 'modast module_interpretor =
-  Environ.env -> Modintern.module_kind -> 'modast ->
-    Entries.module_struct_entry * Modintern.module_kind * Univ.ContextSet.t
+type module_params = (lident list * (Constrexpr.module_ast * inline)) list
 
-type 'modast module_params =
-  (lident list * ('modast * inline)) list
-
-(** [declare_module interp_modast id fargs typ exprs]
-   declares module [id], with structure constructed by [interp_modast]
-   from functor arguments [fargs], with final type [typ].
-   [exprs] is usually of length 1 (Module definition with a concrete
-   body), but it could also be empty ("Declare Module", with non-empty [typ]),
-   or multiple (body of the shape M <+ N <+ ...). *)
+(** [declare_module id fargs typ exprs] declares module [id], from
+   functor arguments [fargs], with final type [typ].  [exprs] is
+   usually of length 1 (Module definition with a concrete body), but
+   it could also be empty ("Declare Module", with non-empty [typ]), or
+   multiple (body of the shape M <+ N <+ ...). *)
 
 val declare_module :
-  'modast module_interpretor ->
   Id.t ->
-  'modast module_params ->
-  ('modast * inline) module_signature ->
-  ('modast * inline) list -> ModPath.t
+  module_params ->
+  (Constrexpr.module_ast * inline) module_signature ->
+  (Constrexpr.module_ast * inline) list -> ModPath.t
 
 val start_module :
-  'modast module_interpretor ->
   bool option -> Id.t ->
-  'modast module_params ->
-  ('modast * inline) module_signature -> ModPath.t
+  module_params ->
+  (Constrexpr.module_ast * inline) module_signature -> ModPath.t
 
 val end_module : unit -> ModPath.t
 
@@ -66,18 +58,16 @@ val end_module : unit -> ModPath.t
     Similar to [declare_module], except that the types could be multiple *)
 
 val declare_modtype :
-  'modast module_interpretor ->
   Id.t ->
-  'modast module_params ->
-  ('modast * inline) list ->
-  ('modast * inline) list ->
+  module_params ->
+  (Constrexpr.module_ast * inline) list ->
+  (Constrexpr.module_ast * inline) list ->
   ModPath.t
 
 val start_modtype :
-  'modast module_interpretor ->
   Id.t ->
-  'modast module_params ->
-  ('modast * inline) list -> ModPath.t
+  module_params ->
+  (Constrexpr.module_ast * inline) list -> ModPath.t
 
 val end_modtype : unit -> ModPath.t
 
@@ -115,8 +105,7 @@ val import_modules : export:bool -> ModPath.t list -> unit
 
 (** Include  *)
 
-val declare_include :
-  'modast module_interpretor -> ('modast * inline) list -> unit
+val declare_include : (Constrexpr.module_ast * inline) list -> unit
 
 (** {6 ... } *)
 (** [iter_all_segments] iterate over all segments, the modules'
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index ea34b601e8..c335d3ad55 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1079,9 +1079,7 @@ let explain_incorrect_with_in_module () =
 let explain_incorrect_module_application () =
   str "Illegal application to a module type."
 
-open Modintern
-
-let explain_module_internalization_error = function
+let explain_module_internalization_error = let open Modintern in function
   | NotAModuleNorModtype s -> explain_not_module_nor_modtype s
   | IncorrectWithInModule -> explain_incorrect_with_in_module ()
   | IncorrectModuleApplication -> explain_incorrect_module_application ()
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 85ba464a2d..ca29a6afb9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -872,10 +872,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
      if not (Option.is_empty export) then
       user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
      else (idl,ty)) binders_ast in
-  let mp =
-    Declaremods.declare_module Modintern.interp_module_ast
-      id binders_ast (Declaremods.Enforce mty_ast) []
-  in
+  let mp = Declaremods.declare_module id binders_ast (Declaremods.Enforce mty_ast) [] in
   Dumpglob.dump_moddef ?loc mp "mod";
   Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared");
   Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export
@@ -892,10 +889,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
          (fun (export,idl,ty) (args,argsexport) ->
            (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
              ([],[]) in
-       let mp =
-         Declaremods.start_module Modintern.interp_module_ast
-           export id binders_ast mty_ast_o
-       in
+       let mp = Declaremods.start_module export id binders_ast mty_ast_o in
        Dumpglob.dump_moddef ?loc mp "mod";
        Flags.if_verbose Feedback.msg_info
          (str "Interactive Module " ++ Id.print id ++ str " started");
@@ -911,7 +905,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt
            user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
           else (idl,ty)) binders_ast in
        let mp =
-         Declaremods.declare_module Modintern.interp_module_ast
+         Declaremods.declare_module
 	   id binders_ast mty_ast_o mexpr_ast_l
        in
        Dumpglob.dump_moddef ?loc mp "mod";
@@ -938,10 +932,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
            (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast
              ([],[]) in
 
-       let mp =
-         Declaremods.start_modtype Modintern.interp_module_ast
-           id binders_ast mty_sign
-       in
+       let mp = Declaremods.start_modtype id binders_ast mty_sign in
        Dumpglob.dump_moddef ?loc mp "modtype";
        Flags.if_verbose Feedback.msg_info
 	 (str "Interactive Module Type " ++ Id.print id ++ str " started");
@@ -957,10 +948,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l =
             if not (Option.is_empty export) then
               user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
-	let mp =
-          Declaremods.declare_modtype Modintern.interp_module_ast
-	    id binders_ast mty_sign mty_ast_l
-        in
+        let mp = Declaremods.declare_modtype id binders_ast mty_sign mty_ast_l in
         Dumpglob.dump_moddef ?loc mp "modtype";
 	Flags.if_verbose Feedback.msg_info
 	  (str "Module Type " ++ Id.print id ++ str " is defined")
@@ -970,8 +958,7 @@ let vernac_end_modtype {loc;v=id} =
   Dumpglob.dump_modref ?loc mp "modtype";
   Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined")
 
-let vernac_include l =
-  Declaremods.declare_include Modintern.interp_module_ast l
+let vernac_include l = Declaremods.declare_include l
 
 (**********************)
 (* Gallina extensions *)