summaryrefslogtreecommitdiff
path: root/library/declaremods.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r--library/declaremods.ml229
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 22:40:33 +0000