aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--contrib/interface/ascent.mli4
-rw-r--r--contrib/interface/vtp.ml4
-rw-r--r--contrib/interface/xlate.ml9
-rw-r--r--interp/modintern.ml8
-rw-r--r--interp/topconstr.ml4
-rw-r--r--interp/topconstr.mli4
-rw-r--r--kernel/entries.ml4
-rw-r--r--kernel/entries.mli4
-rw-r--r--kernel/mod_typing.ml34
-rw-r--r--kernel/modops.ml5
-rw-r--r--kernel/modops.mli2
-rw-r--r--library/declaremods.ml24
-rw-r--r--parsing/g_module.ml48
-rw-r--r--parsing/g_prim.ml43
-rw-r--r--parsing/g_primnew.ml47
-rw-r--r--parsing/g_vernacnew.ml48
-rw-r--r--parsing/pcoq.ml41
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--translate/ppvernacnew.ml16
20 files changed, 107 insertions, 45 deletions
diff --git a/CHANGES b/CHANGES
index 098ab23ff..9610e84f8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,8 @@ Modules
- Added syntactic sugar "Module M(Export/Import X Y: T)" and
"Module Type M(Export/Import X Y: T)"
(only for interactive definitions) (doc TODO)
+- Construct "with" generalized to module paths:
+ T with (Definition|Module) M1.M2....Mn.l := l'. (doc TODO)
Notations
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index dfe64d227..09980413a 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -467,8 +467,8 @@ and ct_MODULE_EXPR =
| CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR
and ct_MODULE_TYPE =
CT_coerce_ID_to_MODULE_TYPE of ct_ID
- | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID * ct_FORMULA
- | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * ct_ID
+ | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID_LIST * ct_FORMULA
+ | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID
and ct_MODULE_TYPE_CHECK =
CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
| CT_only_check of ct_MODULE_TYPE
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index ebad14080..ff67c1485 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1157,12 +1157,12 @@ and fMODULE_TYPE = function
| CT_coerce_ID_to_MODULE_TYPE x -> fID x
| CT_module_type_with_def(x1, x2, x3) ->
fMODULE_TYPE x1;
- fID x2;
+ fID_LIST x2;
fFORMULA x3;
fNODE "module_type_with_def" 3
| CT_module_type_with_mod(x1, x2, x3) ->
fMODULE_TYPE x1;
- fID x2;
+ fID_LIST x2;
fID x3;
fNODE "module_type_with_mod" 3
and fMODULE_TYPE_CHECK = function
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ea1484d00..3b4af8c7e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1507,12 +1507,13 @@ let rec xlate_module_type = function
| CMTEwith(mty, decl) ->
let mty1 = xlate_module_type mty in
(match decl with
- CWith_Definition((_, id), c) ->
+ CWith_Definition((_, idl), c) ->
CT_module_type_with_def(xlate_module_type mty,
- xlate_ident id, xlate_formula c)
- | CWith_Module((_, id), (_, qid)) ->
+ CT_id_list (List.map xlate_ident idl),
+ xlate_formula c)
+ | CWith_Module((_, idl), (_, qid)) ->
CT_module_type_with_mod(xlate_module_type mty,
- xlate_ident id,
+ CT_id_list (List.map xlate_ident idl),
CT_ident (xlate_qualid qid)));;
let xlate_module_binder_list (l:module_binder list) =
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 56fc8cb5e..f077bea93 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -79,10 +79,10 @@ let lookup_modtype (loc,qid) =
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
let transl_with_decl env = function
- | CWith_Module ((_,id),qid) ->
- With_Module (id,lookup_module qid)
- | CWith_Definition ((_,id),c) ->
- With_Definition (id,interp_constr Evd.empty env c)
+ | CWith_Module ((_,fqid),qid) ->
+ With_Module (fqid,lookup_module qid)
+ | CWith_Definition ((_,fqid),c) ->
+ With_Definition (fqid,interp_constr Evd.empty env c)
let rec interp_modtype env = function
| CMTEident qid ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f18be16cc..9c155f854 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -720,8 +720,8 @@ let rec replace_vars_constr_expr l = function
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
- | CWith_Module of identifier located * qualid located
- | CWith_Definition of identifier located * constr_expr
+ | CWith_Module of identifier list located * qualid located
+ | CWith_Definition of identifier list located * constr_expr
type module_type_ast =
| CMTEident of qualid located
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 9b9dd80dc..4cfa0a0da 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -159,8 +159,8 @@ val map_constr_expr_with_binders :
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
- | CWith_Module of identifier located * qualid located
- | CWith_Definition of identifier located * constr_expr
+ | CWith_Module of identifier list located * qualid located
+ | CWith_Definition of identifier list located * constr_expr
type module_type_ast =
| CMTEident of qualid located
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 504c11fdf..6ea4bfc59 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -85,8 +85,8 @@ and module_type_entry =
and module_signature_entry = (label * specification_entry) list
and with_declaration =
- With_Module of identifier * module_path
- | With_Definition of identifier * constr
+ With_Module of identifier list * module_path
+ | With_Definition of identifier list * constr
and module_expr =
MEident of module_path
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 4b4cee03a..71c756e26 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -85,8 +85,8 @@ and module_type_entry =
and module_signature_entry = (label * specification_entry) list
and with_declaration =
- With_Module of identifier * module_path
- | With_Definition of identifier * constr
+ With_Module of identifier list * module_path
+ | With_Definition of identifier list * constr
and module_expr =
MEident of module_path
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 1d63486ba..bb3027aa8 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -66,8 +66,9 @@ and merge_with env mtb with_decl =
| MTBsig(msid,sig_b) -> msid,sig_b
| _ -> error_signature_expected mtb
in
- let id = match with_decl with
- | With_Definition (id,_) | With_Module (id,_) -> id
+ let id,idl = match with_decl with
+ | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
+ | With_Definition ([],_) | With_Module ([],_) -> assert false
in
let l = label_of_id id in
try
@@ -75,7 +76,9 @@ and merge_with env mtb with_decl =
let before = List.rev rev_before in
let env' = Modops.add_signature (MPself msid) before env in
let new_spec = match with_decl with
- | With_Definition (id,c) ->
+ | With_Definition ([],_)
+ | With_Module ([],_) -> assert false
+ | With_Definition ([id],c) ->
let cb = match spec with
SPBconst cb -> cb
| _ -> error_not_a_constant l
@@ -107,7 +110,7 @@ and merge_with env mtb with_decl =
const_constraints = cst}
end
(* and what about msid's ????? Don't they clash ? *)
- | With_Module (id, mp) ->
+ | With_Module ([id], mp) ->
let old = match spec with
SPBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
@@ -138,6 +141,29 @@ and merge_with env mtb with_decl =
msb_constraints = Constraint.union old.msb_constraints cst }
in
SPBmodule msb
+ | With_Definition (_::_,_)
+ | With_Module (_::_,_) ->
+ let old = match spec with
+ SPBmodule msb -> msb
+ | _ -> error_not_a_module (string_of_label l)
+ in
+ begin
+ match old.msb_equiv with
+ None ->
+ let new_with_decl = match with_decl with
+ With_Definition (_,c) -> With_Definition (idl,c)
+ | With_Module (_,c) -> With_Module (idl,c) in
+ let modtype =
+ merge_with env' old.msb_modtype new_with_decl in
+ let msb =
+ {msb_modtype = modtype;
+ msb_equiv = None;
+ msb_constraints = old.msb_constraints }
+ in
+ SPBmodule msb
+ | Some mp ->
+ error_a_generative_module_expected l
+ end
in
MTBsig(msid, before@(l,new_spec)::after)
with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 744da223a..390461d5a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,6 +67,11 @@ let error_not_a_constant l =
let error_with_incorrect l =
error ("Incorrect constraint for label \""^(string_of_label l)^"\"")
+let error_a_generative_module_expected l =
+ error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
+ "component of generative modules can be changed using the \"with\" " ^
+ "construct.")
+
let error_local_context lo =
match lo with
None ->
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e770edc93..052bac243 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -92,6 +92,8 @@ val error_not_a_constant : label -> 'a
val error_with_incorrect : label -> 'a
+val error_a_generative_module_expected : label -> 'a
+
val error_local_context : label option -> 'a
val error_circular_with_module : identifier -> 'a
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 57be3dbdf..1ac7eb823 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -373,19 +373,25 @@ let (in_modtype,out_modtype) =
-let replace_module_object id (subst, mbids, msid, lib_stack) modobjs =
+let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs =
if mbids<>[] then
error "Unexpected functor objects"
else
- let rec replace_id = function
- | [] -> []
- | (id',obj)::tail when id = id' ->
+ let rec replace_idl = function
+ | _,[] -> []
+ | id::idl,(id',obj)::tail when id = id' ->
if object_tag obj = "MODULE" then
- (id, in_module (None,modobjs,None))::tail
+ (match idl with
+ [] -> (id, in_module (None,modobjs,None))::tail
+ | _ ->
+ let (_,substobjs,_) = out_module obj in
+ let substobjs' = replace_module_object idl substobjs modobjs in
+ (id, in_module (None,substobjs',None))::tail
+ )
else error "MODULE expected!"
- | lobj::tail -> lobj::replace_id tail
+ | idl,lobj::tail -> lobj::replace_idl (idl,tail)
in
- (subst, mbids, msid, replace_id lib_stack)
+ (subst, mbids, msid, replace_idl (idl,lib_stack))
let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
(subst, mbids1@mbids2, msid, lib_stack)
@@ -397,10 +403,10 @@ let rec get_modtype_substobjs = function
let (subst, mbids, msid, objs) = get_modtype_substobjs mte in
(subst, mbid::mbids, msid, objs)
| MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty
- | MTEwith (mty, With_Module (id,mp)) ->
+ | MTEwith (mty, With_Module (idl,mp)) ->
let substobjs = get_modtype_substobjs mty in
let modobjs = MPmap.find mp !modtab_substobjs in
- replace_module_object id substobjs modobjs
+ replace_module_object idl substobjs modobjs
| MTEsig (msid,_) ->
todo "Anonymous module types"; (empty_subst, [], msid, [])
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4
index e0173d632..e1937b5f9 100644
--- a/parsing/g_module.ml4
+++ b/parsing/g_module.ml4
@@ -31,10 +31,10 @@ GEXTEND Gram
;
with_declaration:
- [ [ "Definition"; id = identref; ":="; c = Constr.constr ->
- CWith_Definition (id,c)
- | IDENT "Module"; id = identref; ":="; qid = qualid ->
- CWith_Module (id,qid)
+ [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.constr ->
+ CWith_Definition (fqid,c)
+ | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
+ CWith_Module (fqid,qid)
] ]
;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 10ffbecaf..2bb5b0630 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -34,7 +34,8 @@ let local_append l id = l@[id]
GEXTEND Gram
GLOBAL: bigint ident natural integer string preident ast
- astlist qualid reference dirpath identref name base_ident var hyp;
+ astlist qualid reference dirpath identref name base_ident var
+ hyp;
(* Compatibility: Prim.var is a synonym of Prim.ident *)
var:
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index 14fb119e4..667b5654e 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -49,7 +49,7 @@ let local_append l id = l@[id]
if not !Options.v7 then
GEXTEND Gram
- GLOBAL: bigint qualid reference ne_string;
+ GLOBAL: bigint fullyqualid qualid reference ne_string;
field:
[ [ s = FIELD -> local_id_of_string s ] ]
;
@@ -58,6 +58,11 @@ GEXTEND Gram
| id = field -> ([],id)
] ]
;
+ fullyqualid:
+ [ [ id = base_ident; (l,id')=fields -> loc,id::List.rev (id'::l)
+ | id = base_ident -> loc,[id]
+ ] ]
+ ;
basequalid:
[ [ id = base_ident; (l,id')=fields ->
local_make_qualid (local_append l id) id'
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index acc691082..05f177512 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -372,10 +372,10 @@ GEXTEND Gram
] ]
;
with_declaration:
- [ [ "Definition"; id = identref; ":="; c = Constr.lconstr ->
- CWith_Definition (id,c)
- | IDENT "Module"; id = identref; ":="; qid = qualid ->
- CWith_Module (id,qid)
+ [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
+ CWith_Definition (fqid,c)
+ | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
+ CWith_Module (fqid,qid)
] ]
;
module_type:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 73e0b4cc8..cc7bb3dad 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -323,6 +323,7 @@ module Prim =
let base_ident = Gram.Entry.create "Prim.base_ident"
let qualid = Gram.Entry.create "Prim.qualid"
+ let fullyqualid = Gram.Entry.create "Prim.fullyqualid"
let dirpath = Gram.Entry.create "Prim.dirpath"
let ne_string = Gram.Entry.create "Prim.ne_string"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9963bad73..2fdb91254 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -117,6 +117,7 @@ module Prim :
val integer : int Gram.Entry.e
val string : string Gram.Entry.e
val qualid : qualid located Gram.Entry.e
+ val fullyqualid : identifier list located Gram.Entry.e
val reference : reference Gram.Entry.e
val dirpath : dir_path Gram.Entry.e
val ne_string : string Gram.Entry.e
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 4b47b8d0a..f052310b7 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -36,6 +36,18 @@ let pr_lident (b,_ as loc,id) =
pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
else pr_id id
+let string_of_fqid fqid =
+ String.concat "." (List.map string_of_id fqid)
+
+let pr_fqid fqid = str (string_of_fqid fqid)
+
+let pr_lfqid (_,_ as loc,fqid) =
+ if loc <> dummy_loc then
+ let (b,_) = unloc loc in
+ pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
+ else
+ pr_fqid fqid
+
let pr_lname = function
(loc,Name id) -> pr_lident (loc,id)
| lna -> pr_located pr_name lna
@@ -229,9 +241,9 @@ let pr_hints local db h pr_c pr_pat =
let pr_with_declaration pr_c = function
| CWith_Definition (id,c) ->
let p = pr_c c in
- str"Definition" ++ spc() ++ pr_lident id ++ str" := " ++ p
+ str"Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p
| CWith_Module (id,qid) ->
- str"Module" ++ spc() ++ pr_lident id ++ str" := " ++
+ str"Module" ++ spc() ++ pr_lfqid id ++ str" := " ++
pr_located pr_qualid qid
let rec pr_module_type pr_c = function
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 00:21:21 +0000