diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 4 | ||||
| -rw-r--r-- | kernel/entries.mli | 4 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 34 | ||||
| -rw-r--r-- | kernel/modops.ml | 5 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 |
5 files changed, 41 insertions, 8 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 504c11fdfb..6ea4bfc591 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 4b4cee03ab..71c756e260 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 1d63486ba1..bb3027aa8b 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 744da223a9..390461d5a0 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 e770edc93e..052bac2430 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 |