Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 120 insertions, 109 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index b2806a1a..762efc5e 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <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        *)
+(*    //   *    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 Pp
@@ -39,7 +41,7 @@ let inl2intopt = function
 
 type algebraic_objects =
   | Objs of Lib.lib_objects
-  | Ref of module_path * substitution
+  | Ref of ModPath.t * substitution
 
 type substitutive_objects = MBId.t list * algebraic_objects
 
@@ -62,9 +64,9 @@ type substitutive_objects = MBId.t list * algebraic_objects
 
 module ModSubstObjs :
  sig
-   val set : module_path -> substitutive_objects -> unit
-   val get : module_path -> substitutive_objects
-   val set_missing_handler : (module_path -> substitutive_objects) -> unit
+   val set : ModPath.t -> substitutive_objects -> unit
+   val get : ModPath.t -> substitutive_objects
+   val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit
  end =
  struct
    let table =
@@ -126,8 +128,8 @@ type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects
 
 module ModObjs :
  sig
-   val set : module_path -> module_objects -> unit
-   val get : module_path -> module_objects (* may raise Not_found *)
+   val set : ModPath.t -> module_objects -> unit
+   val get : ModPath.t -> module_objects (* may raise Not_found *)
    val all : unit -> module_objects MPmap.t
  end =
  struct
@@ -143,11 +145,11 @@ module ModObjs :
 (** {6 Name management}
 
     Auxiliary functions to transform full_path and kernel_name given
-    by Lib into module_path and DirPath.t needed for modules
+    by Lib into ModPath.t and DirPath.t needed for modules
 *)
 
 let mp_of_kn kn =
-  let mp,sec,l = repr_kn kn in
+  let mp,sec,l = KerName.repr kn in
   assert (DirPath.is_empty sec);
   MPdot (mp,l)
 
@@ -166,30 +168,30 @@ let consistency_checks exists dir dirinfo =
     let globref =
       try Nametab.locate_dir (qualid_of_dirpath dir)
       with Not_found ->
-        errorlabstrm "consistency_checks"
-          (pr_dirpath dir ++ str " should already exist!")
+        user_err ~hdr:"consistency_checks"
+          (DirPath.print dir ++ str " should already exist!")
     in
     assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      errorlabstrm "consistency_checks"
-        (pr_dirpath dir ++ str " already exists")
+      user_err ~hdr:"consistency_checks"
+        (DirPath.print dir ++ str " already exists")
 
 let compute_visibility exists i =
   if exists then Nametab.Exactly i else Nametab.Until i
 
 (** Iterate some function [iter_objects] on all components of a module *)
 
-let do_module exists iter_objects i dir mp sobjs kobjs =
-  let prefix = (dir,(mp,DirPath.empty)) in
+let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs =
+  let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
   let dirinfo = DirModule prefix in
-  consistency_checks exists dir dirinfo;
-  Nametab.push_dir (compute_visibility exists i) dir dirinfo;
-  ModSubstObjs.set mp sobjs;
+  consistency_checks exists obj_dir dirinfo;
+  Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo;
+  ModSubstObjs.set obj_mp sobjs;
   (* If we're not a functor, let's iter on the internal components *)
   if sobjs_no_functor sobjs then begin
     let objs = expand_sobjs sobjs in
-    ModObjs.set mp (prefix,objs,kobjs);
+    ModObjs.set obj_mp (prefix,objs,kobjs);
     iter_objects (i+1) prefix objs;
     iter_objects (i+1) prefix kobjs
   end
@@ -222,20 +224,20 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
 
 let load_keep i ((sp,kn),kobjs) =
   (* Invariant : seg isn't empty *)
-  let dir = dir_of_sp sp and mp = mp_of_kn kn in
-  let prefix = (dir,(mp,DirPath.empty)) in
+  let obj_dir = dir_of_sp sp and obj_mp  = mp_of_kn kn in
+  let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in
   let prefix',sobjs,kobjs0 =
-    try ModObjs.get mp
+    try ModObjs.get obj_mp
     with Not_found -> assert false (* a substobjs should already be loaded *)
   in
   assert (eq_op prefix' prefix);
   assert (List.is_empty kobjs0);
-  ModObjs.set mp (prefix,sobjs,kobjs);
+  ModObjs.set obj_mp (prefix,sobjs,kobjs);
   Lib.load_objects i prefix kobjs
 
 let open_keep i ((sp,kn),kobjs) =
-  let dir = dir_of_sp sp and mp = mp_of_kn kn in
-  let prefix = (dir,(mp,DirPath.empty)) in
+  let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in
+  let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
   Lib.open_objects i prefix kobjs
 
 let in_modkeep : Lib.lib_objects -> obj =
@@ -252,7 +254,7 @@ let in_modkeep : Lib.lib_objects -> obj =
 
 let do_modtype i sp mp sobjs =
   if Nametab.exists_modtype sp then
-    anomaly (pr_path sp ++ str " already exists");
+    anomaly (pr_path sp ++ str " already exists.");
   Nametab.push_modtype (Nametab.Until i) sp mp;
   ModSubstObjs.set mp sobjs
 
@@ -284,9 +286,9 @@ let (in_modtype : substitutive_objects -> obj),
 (** {6 Declaration of substitutive objects for Include} *)
 
 let do_include do_load do_open i ((sp,kn),aobjs) =
-  let dir = Libnames.dirpath sp in
-  let mp = KerName.modpath kn in
-  let prefix = (dir,(mp,DirPath.empty)) in
+  let obj_dir = Libnames.dirpath sp in
+  let obj_mp = KerName.modpath kn in
+  let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in
   let o = expand_aobjs aobjs in
   if do_load then Lib.load_objects i prefix o;
   if do_open then Lib.open_objects i prefix o
@@ -336,8 +338,8 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs
 
 (** {6 From module expression to substitutive objects} *)
 
-(** Turn a chain of [MSEapply] into the head module_path and the
-    list of module_path parameters (deepest param coming first).
+(** Turn a chain of [MSEapply] into the head ModPath.t and the
+    list of ModPath.t parameters (deepest param coming first).
     The left part of a [MSEapply] must be either [MSEident] or
     another [MSEapply]. *)
 
@@ -345,7 +347,7 @@ let get_applications mexpr =
   let rec get params = function
     | MEident mp -> mp, params
     | MEapply (fexpr, mp) -> get (mp::params) fexpr
-    | MEwith _ -> error "Non-atomic functor application."
+    | MEwith _ -> user_err Pp.(str "Non-atomic functor application.")
   in get [] mexpr
 
 (** Create the substitution corresponding to some functor applications *)
@@ -353,7 +355,7 @@ let get_applications mexpr =
 let rec compute_subst env mbids sign mp_l inl =
   match mbids,mp_l with
     | _,[] -> mbids,empty_subst
-    | [],r -> error "Application of a functor with too few arguments."
+    | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
     | mbid::mbids,mp::mp_l ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
 	let mb = Environ.lookup_module mp env in
@@ -442,23 +444,26 @@ 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 (idl,(typ,ann)) =
+let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) =
   let inl = inl2intopt ann in
   let lib_dir = Lib.library_dp() in
   let env = Global.env() in
-  let mty,_ = interp_modast env ModType typ in
+  let (mty, _, cst') = interp_modast env 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
   let mp0 = get_module_path mty in
-  List.fold_left
-    (fun acc (_,id) ->
-      let dir = DirPath.make [id] in
-      let mbid = MBId.make lib_dir id in
-      let mp = MPbound mbid in
-      let resolver = Global.add_module_parameter mbid mty inl in
-      let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
-      do_module false Lib.load_objects 1 dir mp sobjs [];
-      (mbid,mty,inl)::acc)
-    acc idl
+  let fold acc {CAst.v=id} =
+    let dir = DirPath.make [id] in
+    let mbid = MBId.make lib_dir id in
+    let mp = MPbound mbid in
+    let resolver = Global.add_module_parameter mbid mty inl in
+    let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
+    do_module false Lib.load_objects 1 dir mp sobjs [];
+    (mbid,mty,inl)::acc
+  in
+  let acc = List.fold_left fold acc idl in
+  (acc, Univ.ContextSet.union cst cst')
 
 (** Process a list of declarations of functor parameters
     (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk)
@@ -472,7 +477,7 @@ let intern_arg interp_modast acc (idl,(typ,ann)) =
 *)
 
 let intern_args interp_modast params =
-  List.fold_left (intern_arg interp_modast) [] params
+  List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params
 
 
 (** {6 Auxiliary functions concerning subtyping checks} *)
@@ -524,13 +529,17 @@ 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 =
-  List.map
-    (fun (m,ann) ->
+  let (cst, ans) = List.fold_left_map
+    (fun cst (m,ann) ->
        let inl = inl2intopt ann in
-       let mte,_ = interp_modast env ModType m in
+       let mte, _, cst' = interp_modast env 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
-       { mtb with mod_type = mk_funct_type env args mtb.mod_type })
-    mtys
+       cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type })
+    Univ.ContextSet.empty mtys
+  in
+  (ans, cst)
 
 
 (** {6 Current module information}
@@ -557,40 +566,32 @@ let openmodtype_info =
   Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO"
 
 
-(** XML output hooks *)
-
-let (f_xml_declare_module, xml_declare_module) = Hook.make ~default:ignore ()
-let (f_xml_start_module, xml_start_module) = Hook.make ~default:ignore ()
-let (f_xml_end_module, xml_end_module) = Hook.make ~default:ignore ()
-let (f_xml_declare_module_type, xml_declare_module_type) = Hook.make ~default:ignore ()
-let (f_xml_start_module_type, xml_start_module_type) = Hook.make ~default:ignore ()
-let (f_xml_end_module_type, xml_end_module_type) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
 (** {6 Modules : start, end, declare} *)
 
 module RawModOps = struct
 
 let start_module interp_modast export id args res fs =
   let mp = Global.start_module id in
-  let arg_entries_r = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args interp_modast args in
+  let () = Global.push_context_set true cst in
   let env = Global.env () in
-  let res_entry_o, subtyps = match res with
+  let res_entry_o, subtyps, cst = match res with
     | Enforce (res,ann) ->
         let inl = inl2intopt ann in
-	let mte,_ = interp_modast env ModType res in
+        let (mte, _, cst) = interp_modast env ModType res in
+        let env = Environ.push_context_set ~strict:true cst env in
         (* We check immediately that mte is well-formed *)
-	let _ = Mod_typing.translate_mse env None inl mte in
-	Some (mte,inl), []
+        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 ->
-	None, build_subtypes interp_modast env mp arg_entries_r resl
+      let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in
+      None, typs, cst
   in
+  let () = Global.push_context_set true cst in
   openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
   let prefix = Lib.start_module export id mp fs in
-  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
-  Lib.add_frozen_state ();
-  if_xml (Hook.get f_xml_start_module) mp;
+  Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix);
   mp
 
 let end_module () =
@@ -629,33 +630,39 @@ let end_module () =
   assert (eq_full_path (fst newoname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd newoname)) mp);
 
-  Lib.add_frozen_state () (* to prevent recaching *);
-  if_xml (Hook.get f_xml_end_module) mp;
   mp
 
 let declare_module interp_modast 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 = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args interp_modast args in
   let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let mty_entry_o, subs, inl_res = match res with
+  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, _ = interp_modast env ModType mty in
+        let (mte, _, cst) = interp_modast env ModType mty in
+        let env = Environ.push_context_set ~strict:true cst env in
         (* We check immediately that mte is well-formed *)
-        let _ = Mod_typing.translate_mse env None inl mte in
-        Some mte, [], inl
+        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 ->
-	None, build_subtypes interp_modast env mp arg_entries_r mtys,
-        default_inline ()
+      let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in
+      None, typs, default_inline (), cst
   in
-  let mexpr_entry_o, inl_expr = match mexpr_o with
-    | None -> None, default_inline ()
+  let env = Environ.push_context_set ~strict:true cst' env in
+  let cst = Univ.ContextSet.union cst cst' in
+  let mexpr_entry_o, inl_expr, cst' = match mexpr_o with
+    | None -> None, default_inline (), Univ.ContextSet.empty
     | Some (mexpr,ann) ->
-      Some (fst (interp_modast env Module mexpr)), inl2intopt ann
+      let (mte, _, cst) = interp_modast env Module mexpr in
+      Some mte, inl2intopt ann, cst
   in
+  let env = Environ.push_context_set ~strict:true cst' env in
+  let cst = Univ.ContextSet.union cst cst' in
   let entry = match mexpr_entry_o, mty_entry_o with
     | None, None -> assert false (* No body, no type ... *)
     | None, Some typ -> MType (params, typ)
@@ -674,6 +681,7 @@ let declare_module interp_modast id args res mexpr_o fs =
   | None -> None
   | _ -> inl_res
   in
+  let () = Global.push_context_set true cst in
   let mp_env,resolver = Global.add_module id entry inl in
 
   (* Name consistency check : kernel vs. library *)
@@ -684,7 +692,6 @@ let declare_module interp_modast id args res mexpr_o fs =
 
   let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
   ignore (Lib.add_leaf id (in_module sobjs));
-  if_xml (Hook.get f_xml_declare_module) mp;
   mp
 
 end
@@ -695,14 +702,14 @@ module RawModTypeOps = struct
 
 let start_modtype interp_modast id args mtys fs =
   let mp = Global.start_modtype id in
-  let arg_entries_r = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args interp_modast args in
+  let () = Global.push_context_set true cst in
   let env = Global.env () in
-  let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
+  let sub_mty_l, cst = build_subtypes interp_modast 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
-  Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
-  Lib.add_frozen_state ();
-  if_xml (Hook.get f_xml_start_module_type) mp;
+  Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix);
   mp
 
 let end_modtype () =
@@ -719,8 +726,6 @@ let end_modtype () =
   assert (eq_full_path (fst oname) (fst oldoname));
   assert (ModPath.equal (mp_of_kn (snd oname)) mp);
 
-  Lib.add_frozen_state ()(* to prevent recaching *);
-  if_xml (Hook.get f_xml_end_module_type) mp;
   mp
 
 let declare_modtype interp_modast id args mtys (mty,ann) fs =
@@ -728,14 +733,21 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   (* 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 = intern_args interp_modast args in
+  let arg_entries_r, cst = intern_args interp_modast 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, _ = interp_modast env ModType mty in
+  let mte, _, cst = interp_modast env ModType mty in
+  let () = Global.push_context_set true cst in
+  let env = Global.env () in
   (* We check immediately that mte is well-formed *)
-  let _ = Mod_typing.translate_mse env None inl mte in
+  let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
+  let () = Global.push_context_set true cst in
+  let env = Global.env () in
   let entry = params, mte in
-  let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
+  let sub_mty_l, cst = build_subtypes interp_modast 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
   let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
   let sobjs = subst_sobjs subst sobjs in
@@ -754,7 +766,6 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   check_subtypes_mt mp sub_mty_l;
 
   ignore (Lib.add_leaf id (in_modtype sobjs));
-  if_xml (Hook.get f_xml_declare_module_type) mp;
   mp
 
 end
@@ -777,7 +788,7 @@ let rec decompose_functor mpl typ =
   match mpl, typ with
   | [], _ -> typ
   | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
-  | _ -> error "Application of a functor with too much arguments."
+  | _ -> user_err Pp.(str "Application of a functor with too much arguments.")
 
 exception NoIncludeSelf
 
@@ -790,7 +801,9 @@ let type_of_incl env is_mod = function
 
 let declare_one_include interp_modast (me_ast,annot) =
   let env = Global.env() in
-  let me,kind = interp_modast env ModAny me_ast in
+  let me, kind, cst = interp_modast env ModAny me_ast in
+  let () = Global.push_context_set true cst in
+  let env = Global.env () in
   let is_mod = (kind == Module) in
   let cur_mp = Lib.current_mp () in
   let inl = inl2intopt annot in
@@ -883,7 +896,7 @@ let register_library dir cenv (objs:library_objects) digest univ =
       (* If not, let's do it now ... *)
       let mp' = Global.import cenv univ digest in
       if not (ModPath.equal mp mp') then
-        anomaly (Pp.str "Unexpected disk module name");
+        anomaly (Pp.str "Unexpected disk module name.");
   in
   let sobjs,keepobjs = objs in
   do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
@@ -894,8 +907,7 @@ let get_library_native_symbols dir =
 let start_library dir =
   let mp = Global.start_library dir in
   openmod_info := default_module_info;
-  Lib.start_compilation dir mp;
-  Lib.add_frozen_state ()
+  Lib.start_compilation dir mp
 
 let end_library_hook = ref ignore
 let append_end_library_hook f =
@@ -933,7 +945,7 @@ let subst_import (subst,(export,mp as obj)) =
   let mp' = subst_mp subst mp in
   if mp'==mp then obj else (export,mp')
 
-let in_import : bool * module_path -> obj =
+let in_import : bool * ModPath.t -> obj =
   declare_object {(default_object "IMPORT MODULE") with
     cache_function = cache_import;
     open_function = open_import;
@@ -969,11 +981,10 @@ let iter_all_segments f =
 
 type 'modast module_interpretor =
   Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind
+    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
-  (Id.t Loc.located list * ('modast * inline)) list
-
+  (lident list * ('modast * inline)) list
 
 (** {6 Debug} *)
 
@@ -983,7 +994,7 @@ let debug_print_modtab _ =
     | l -> str "[." ++ int (List.length l) ++ str ".]"
   in
   let pr_modinfo mp (prefix,substobjs,keepobjs) s =
-    s ++ str (string_of_mp mp) ++ (spc ())
+    s ++ str (ModPath.to_string mp) ++ (spc ())
     ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs)))
   in
   let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in