aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/extraction/extract_env.ml2
-rw-r--r--library/declaremods.ml142
-rw-r--r--library/declaremods.mli33
-rw-r--r--library/library.ml6
-rwxr-xr-xlibrary/nametab.ml5
-rwxr-xr-xlibrary/nametab.mli5
-rw-r--r--parsing/g_vernac.ml43
-rw-r--r--test-suite/output/TranspModtype.out7
-rw-r--r--test-suite/output/TranspModtype.v22
-rw-r--r--toplevel/vernacentries.ml10
-rw-r--r--toplevel/vernacexpr.ml2
11 files changed, 189 insertions, 48 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9e68ec8e4..0e5325a2e 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -259,7 +259,7 @@ let mono_environment kn_set =
let dir_module_of_id m =
try
- Nametab.locate_loaded_library (make_short_qualid m)
+ Nametab.full_name_module (make_short_qualid m)
with Not_found ->
errorlabstrm "module_message"
(str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.")
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 2be5e8a73..5dba4c208 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -77,7 +77,8 @@ let modtab_objects =
(* currently started interactive module (if any) - its arguments (if it
is a functor) and declared output type *)
let openmod_info =
- ref (([],None) : mod_bound_id list * module_type_entry option)
+ ref (([],None,None) : mod_bound_id list * module_type_entry option
+ * module_type_body option)
let _ = Summary.declare_summary "MODULE-INFO"
{ Summary.freeze_function = (fun () ->
@@ -91,7 +92,7 @@ let _ = Summary.declare_summary "MODULE-INFO"
Summary.init_function = (fun () ->
modtab_substobjs := MPmap.empty;
modtab_objects := MPmap.empty;
- openmod_info := ([],None));
+ openmod_info := ([],None,None));
Summary.survive_section = false }
(* auxiliary functions to transform section_path and kernel_name given
@@ -119,6 +120,18 @@ let msid_of_prefix (_,(mp,sec)) =
anomaly ("Non-empty section in module name!" ^
string_of_mp mp ^ "." ^ string_of_dirpath sec)
+
+(* This function checks if the type calculated for the module [mp] is
+ a subtype of [sub_mtb]. Uses only the global environment. *)
+let check_subtypes mp sub_mtb =
+ let env = Global.env () in
+ let mtb = (Environ.lookup_module mp env).mod_type in
+ let _ = Environ.add_constraints
+ (Subtyping.check_subtypes env mtb sub_mtb)
+ in
+ () (* The constraints are checked and forgot immediately! *)
+
+
(* This function registers the visibility of the module and iterates
through its components. It is called by plenty module functions *)
@@ -164,10 +177,20 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
let _ = match entry with
| None ->
anomaly "You must not recache interactive modules!"
- | Some me ->
+ | Some (me,sub_mte_o) ->
+ let sub_mtb_o = match sub_mte_o with
+ None -> None
+ | Some mte -> Some (Mod_typing.translate_modtype (Global.env()) mte)
+ in
+
let mp = Global.add_module (basename sp) me in
if mp <> mp_of_kn kn then
- anomaly "Kernel and Library names do not match"
+ anomaly "Kernel and Library names do not match";
+
+ match sub_mtb_o with
+ None -> ()
+ | Some sub_mtb -> check_subtypes mp sub_mtb
+
in
conv_names_do_module false "cache" load_objects 1 oname substobjs substituted
@@ -431,12 +454,31 @@ let start_module interp_modtype id args res_o =
List.fold_left (intern_args interp_modtype) (env,[]) args
in
let arg_entries = List.concat (List.rev arg_entries_revlist) in
- let res_entry_o = option_app (interp_modtype env) res_o in
+
+ let res_entry_o, sub_body_o = match res_o with
+ None -> None, None
+ | Some (res, true) ->
+ Some (interp_modtype env res), None
+ | Some (res, false) ->
+ (* If the module type is non-restricting, we must translate it
+ here to catch errors as early as possible. If it is
+ estricting, the kernel takes care of it. *)
+ let sub_mte =
+ List.fold_right
+ (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ arg_entries
+ (interp_modtype env res)
+ in
+ let sub_mtb =
+ Mod_typing.translate_modtype (Global.env()) sub_mte
+ in
+ None, Some sub_mtb
+ in
let mp = Global.start_module id arg_entries res_entry_o in
let mbids = List.map fst arg_entries in
- openmod_info:=(mbids,res_entry_o);
+ openmod_info:=(mbids,res_entry_o,sub_body_o);
let prefix = Lib.start_module id mp fs in
Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
Lib.add_frozen_state ()
@@ -446,11 +488,17 @@ let end_module id =
let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
let mp = Global.end_module id in
+ let mbids, res_o, sub_o = !openmod_info in
+
+ begin match sub_o with
+ None -> ()
+ | Some sub_mtb -> check_subtypes mp sub_mtb
+ end;
+
let substitute, keep, special = Lib.classify_segment lib_stack in
let dir = fst oldprefix in
let msid = msid_of_prefix oldprefix in
- let mbids, res_o = !openmod_info in
Summary.unfreeze_other_summaries fs;
@@ -528,7 +576,7 @@ let register_library dir cenv objs digest =
let start_library dir =
let mp = Global.start_library dir in
- openmod_info:=[],None;
+ openmod_info:=[],None,None;
Lib.start_compilation dir mp;
Lib.add_frozen_state ()
@@ -542,6 +590,33 @@ let export_library dir =
+let do_open_export (_,(_,mp)) =
+(* for non-substitutive exports:
+ let mp = Nametab.locate_module (qualid_of_dirpath dir) in *)
+ let prefix,objects = MPmap.find mp !modtab_objects in
+ open_objects 1 prefix objects
+
+let classify_export (_,(export,_ as obj)) =
+ if export then Substitute obj else Dispose
+
+let subst_export (_,subst,(export,mp as obj)) =
+ let mp' = subst_mp subst mp in
+ if mp'==mp then obj else
+ (export,mp')
+
+let (in_export,out_export) =
+ declare_object {(default_object "EXPORT MODULE") with
+ cache_function = do_open_export;
+ open_function = (fun i o -> if i=1 then do_open_export o);
+ subst_function = subst_export;
+ classify_function = classify_export }
+
+let export_module mp =
+(* for non-substitutive exports:
+ let dir = Nametab.dir_of_mp mp in *)
+ Lib.add_anonymous_leaf (in_export (true,mp))
+
+
let import_module mp =
let prefix,objects = MPmap.find mp !modtab_objects in
open_objects 1 prefix objects
@@ -638,21 +713,32 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
List.fold_left (intern_args interp_modtype) (env,[]) args
in
let arg_entries = List.concat (List.rev arg_entries_revlist) in
- let mty_entry_o = option_app (interp_modtype env) mty_o in
- let mexpr_entry_o = option_app (interp_modexpr env) mexpr_o in
+ let mty_entry_o, mty_sub_o = match mty_o with
+ None -> None, None
+ | (Some (mty, true)) ->
+ Some (List.fold_right
+ (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ arg_entries
+ (interp_modtype env mty)),
+ None
+ | (Some (mty, false)) ->
+ None,
+ Some (List.fold_right
+ (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
+ arg_entries
+ (interp_modtype env mty))
+ in
+ let mexpr_entry_o = match mexpr_o with
+ None -> None
+ | Some mexpr ->
+ Some (List.fold_right
+ (fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
+ arg_entries
+ (interp_modexpr env mexpr))
+ in
let entry =
- {mod_entry_type =
- option_app
- (List.fold_right
- (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
- arg_entries)
- mty_entry_o;
- mod_entry_expr =
- option_app
- (List.fold_right
- (fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
- arg_entries)
- mexpr_entry_o }
+ {mod_entry_type = mty_entry_o;
+ mod_entry_expr = mexpr_entry_o }
in
let substobjs =
match entry with
@@ -660,14 +746,14 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
| {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr
| _ -> anomaly "declare_module: No type, no body ..."
in
- Summary.unfreeze_summaries fs;
+ Summary.unfreeze_summaries fs;
- let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
- let substituted = subst_substobjs dir mp substobjs in
+ let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+ let substituted = subst_substobjs dir mp substobjs in
- ignore (add_leaf
- id
- (in_module (Some entry, substobjs, substituted)))
+ ignore (add_leaf
+ id
+ (in_module (Some (entry, mty_sub_o), substobjs, substituted)))
(*s Iterators. *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 9edd051ca..114ea3cf9 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -15,21 +15,36 @@ open Environ
open Libnames
open Libobject
open Lib
-(*i*)
+ (*i*)
-(*s This modules provides official fucntions to declare modules and
- module types *)
+(*s This modules provides official functions to declare modules and
+ module types *)
(*s Modules *)
+(* [declare_module interp_modtype interp_modexpr id fargs typ expr]
+ declares module [id], with type constructed by [interp_modtype]
+ from functor arguments [fargs] and [typ] and with module body
+ constructed by [interp_modtype] from functor arguments [fargs] and
+ by [interp_modexpr] from [expr]. At least one of [typ], [expr] must
+ be non-empty.
+
+ The [bool] in [typ] tells if the module must be abstracted [true]
+ with respect to the module type or merely matched without any
+ restriction [false].
+*)
+
val declare_module :
(env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) ->
identifier ->
- (identifier list * 'modtype) list -> 'modtype option -> 'modexpr option -> unit
-
-val start_module : (env -> 'modtype -> module_type_entry) ->
- identifier -> (identifier list * 'modtype) list -> 'modtype option -> unit
+ (identifier list * 'modtype) list -> ('modtype * bool) option ->
+ 'modexpr option -> unit
+
+val start_module : (env -> 'modtype -> module_type_entry) ->
+ identifier ->
+ (identifier list * 'modtype) list -> ('modtype * bool) option ->
+ unit
val end_module : identifier -> unit
@@ -74,6 +89,10 @@ val export_library :
val import_module : module_path -> unit
+(* [export_module mp] is similar, but is run when the module
+ containing it is imported *)
+
+val export_module : module_path -> unit
(*s [fold_all_segments] and [iter_all_segments] iterate over all
segments, the modules' segments first and then the current
diff --git a/library/library.ml b/library/library.ml
index e7087438b..1f75b4ca0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -389,7 +389,7 @@ let rec_intern_by_filename_only id f =
let locate_qualified_library qid =
(* Look if loaded in current environment *)
try
- let dir = Nametab.locate_loaded_library qid in
+ let dir = Nametab.full_name_module qid in
(LibLoaded, dir, library_full_filename dir)
with Not_found ->
(* Look if in loadpath *)
@@ -511,8 +511,8 @@ let export_library (loc,qid) =
match Nametab.locate_module qid with
MPfile dir ->
add_anonymous_leaf (in_require ([dir],Some true))
- | _ ->
- raise Not_found
+ | mp ->
+ export_module mp
with
Not_found ->
user_err_loc
diff --git a/library/nametab.ml b/library/nametab.ml
index f6418de3e..cbb3b23e9 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -355,7 +355,7 @@ let locate_module qid =
| DirModule (_,(mp,_)) -> mp
| _ -> raise Not_found
-let locate_loaded_library qid =
+let full_name_module qid =
match locate_dir qid with
| DirModule (dir,_) -> dir
| _ -> raise Not_found
@@ -428,6 +428,9 @@ let id_of_global ctx_opt ref =
let sp_of_syntactic_definition kn =
Globrevtab.find (SyntacticDef kn) !the_globrevtab
+let dir_of_mp mp =
+ MPmap.find mp !the_modrevtab
+
(* Shortest qualid functions **********************************************)
diff --git a/library/nametab.mli b/library/nametab.mli
index 1f29a9313..bd1a8b1bd 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -127,7 +127,7 @@ val full_name_modtype : qualid -> section_path
val full_name_cci : qualid -> section_path
(* As above but checks that the path found is indeed a module *)
-val locate_loaded_library : qualid -> dir_path
+val full_name_module : qualid -> dir_path
(*s Reverse lookup -- finding user names corresponding to the given
@@ -145,6 +145,9 @@ val shortest_qualid_of_syndef :
val id_of_global :
Sign.named_context option -> global_reference -> identifier
+val dir_of_mp :
+ module_path -> dir_path
+
(* Printing of global references using names as short as possible *)
val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b4f7abbb0..fdf73d047 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -343,7 +343,8 @@ GEXTEND Gram
[ [ bls = LIST0 module_binders -> List.flatten bls ] ]
;
of_module_type:
- [ [ ":"; mty = Module.module_type -> mty ] ]
+ [ [ ":"; mty = Module.module_type -> (mty, true)
+ | "<:"; mty = Module.module_type -> (mty, false) ] ]
;
is_module_type:
[ [ ":="; mty = Module.module_type -> mty ] ]
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
new file mode 100644
index 000000000..f94ed6423
--- /dev/null
+++ b/test-suite/output/TranspModtype.out
@@ -0,0 +1,7 @@
+TrM.A = M.A
+ : Set
+OpM.A = M.A
+ : Set
+TrM.B = M.B
+ : Set
+*** [ OpM.B : Set ]
diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v
new file mode 100644
index 000000000..27b1fb9f9
--- /dev/null
+++ b/test-suite/output/TranspModtype.v
@@ -0,0 +1,22 @@
+Module Type SIG.
+ Axiom A:Set.
+ Axiom B:Set.
+End SIG.
+
+Module M:SIG.
+ Definition A:=nat.
+ Definition B:=nat.
+End M.
+
+Module N<:SIG:=M.
+
+Module TranspId[X:SIG] <: SIG with Definition A:=X.A := X.
+Module OpaqueId[X:SIG] : SIG with Definition A:=X.A := X.
+
+Module TrM := TranspId M.
+Module OpM := OpaqueId M.
+
+Print TrM.A.
+Print OpM.A.
+Print TrM.B.
+Print OpM.B.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5efbcc5d3..5bba0c630 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -819,16 +819,16 @@ let vernac_print = function
| PrintHintDb -> Auto.print_searchtable ()
| PrintScope s -> pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
-let global_loaded_library r =
+let global_module r =
let (loc,qid) = qualid_of_reference r in
- try Nametab.locate_loaded_library qid
+ try Nametab.full_name_module qid
with Not_found ->
- user_err_loc (loc, "global_loaded_library",
+ user_err_loc (loc, "global_module",
str "Module/section " ++ pr_qualid qid ++ str " not found")
let interp_search_restriction = function
- | SearchOutside l -> (List.map global_loaded_library l, true)
- | SearchInside l -> (List.map global_loaded_library l, false)
+ | SearchOutside l -> (List.map global_module l, true)
+ | SearchInside l -> (List.map global_module l, false)
let vernac_search s r =
let r = interp_search_restriction r in
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 4756755b4..51d080faf 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -196,7 +196,7 @@ type vernac_expr =
(* Modules and Module Types *)
| VernacDeclareModule of identifier *
- module_binder list * module_type_ast option * module_ast option
+ module_binder list * (module_type_ast * bool) option * module_ast option
| VernacDeclareModuleType of identifier *
module_binder list * module_type_ast option
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 16:42:02 +0000