diff options
| -rw-r--r-- | kernel/mod_typing.ml | 12 | ||||
| -rw-r--r-- | kernel/modops.ml | 8 | ||||
| -rw-r--r-- | kernel/modops.mli | 6 | ||||
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 6 | ||||
| -rw-r--r-- | test-suite/failure/circular_subtyping1.v | 2 | ||||
| -rw-r--r-- | test-suite/failure/circular_subtyping2.v | 16 |
8 files changed, 10 insertions, 44 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 824d2e4eb..e9bca9065 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -63,7 +63,8 @@ let rec translate_modtype env mte = and merge_with env mtb with_decl = let msid,sig_b = match (Modops.scrape_modtype env mtb) with - | MTBsig(msid,sig_b) -> msid,sig_b + | MTBsig(msid,sig_b) -> let msid'=(refresh_msid msid) in + msid',(subst_signature_msid msid (MPself(msid')) sig_b) | _ -> error_signature_expected mtb in let id,idl = match with_decl with @@ -116,15 +117,6 @@ and merge_with env mtb with_decl = | _ -> error_not_a_module (string_of_label l) in let mtb = type_modpath env' mp in - (* here, using assertions in substitutions, - we check that there is no msid bound in mtb *) - begin - try - let _ = subst_modtype (map_msid msid (MPself msid)) mtb in - () - with - Circularity _ -> error_circular_with_module id - end; let cst = try check_subtypes env' mtb old.msb_modtype with Failure _ -> error_with_incorrect (label_of_id id) in diff --git a/kernel/modops.ml b/kernel/modops.ml index bd1151544..e9e1d67eb 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -20,7 +20,6 @@ open Entries open Mod_subst (*i*) -exception Circularity of string let error_existing_label l = error ("The label "^string_of_label l^" is already declared") @@ -82,11 +81,6 @@ let error_local_context lo = error ("The local context of the component "^ (string_of_label l)^" is not empty") -let error_circular_with_module l = - error ("The construction \"with Module "^(string_of_id l)^":=...\" is about to create\na circular module type. Their resolution is not implemented yet.\nIf you really need that feature, please report.") - -let error_circularity_in_subtyping l l1 l2 = - error ("An occurrence of "^l^" creates a circularity\n during the subtyping verification between "^l1^" and "^l2^".") let error_no_such_label_sub l l1 l2 = error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".") @@ -142,12 +136,10 @@ let rec subst_modtype sub = function M to M' I must substitute M' for X in "Module N := X". *) | MTBident ln -> MTBident (subst_kn sub ln) | MTBfunsig (arg_id, arg_b, body_b) -> - if occur_mbid arg_id sub then raise (Circularity (string_of_mbid arg_id)); MTBfunsig (arg_id, subst_modtype sub arg_b, subst_modtype sub body_b) | MTBsig (sid1, msb) -> - if occur_msid sid1 sub then raise (Circularity (string_of_msid sid1)); MTBsig (sid1, subst_signature sub msb) and subst_signature sub sign = diff --git a/kernel/modops.mli b/kernel/modops.mli index 803bdc839..c209eac1a 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -17,7 +17,7 @@ open Declarations open Entries open Mod_subst (*i*) -exception Circularity of string + (* Various operations on modules and module types *) (* recursively unfold MTBdent module types *) @@ -96,10 +96,6 @@ val error_a_generative_module_expected : label -> 'a val error_local_context : label option -> 'a -val error_circular_with_module : identifier -> 'a - -val error_circularity_in_subtyping : string->string->string-> 'a - val error_no_such_label_sub : label->string->string->'a val resolver_of_environment : diff --git a/kernel/names.ml b/kernel/names.ml index 5dcd8a68f..09c98eafc 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -88,6 +88,7 @@ type label = string type mod_self_id = uniq_ident let make_msid = make_uid let debug_string_of_msid = debug_string_of_uid +let refresh_msid (_,s,dir) = make_uid dir s let string_of_msid = string_of_uid let id_of_msid (_,s,_) = s let label_of_msid (_,s,_) = s diff --git a/kernel/names.mli b/kernel/names.mli index 051087f5d..64edf1702 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -42,7 +42,7 @@ val string_of_dirpath : dir_path -> string (*s Unique identifier to be used as "self" in structures and signatures - invisible for users *) - type label +type label type mod_self_id (* The first argument is a file name - to prevent conflict between @@ -50,6 +50,7 @@ type mod_self_id val make_msid : dir_path -> string -> mod_self_id val id_of_msid : mod_self_id -> identifier val label_of_msid : mod_self_id -> label +val refresh_msid : mod_self_id -> mod_self_id val debug_string_of_msid : mod_self_id -> string val string_of_msid : mod_self_id -> string diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 3f153ac24..a9403a5e3 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -306,11 +306,7 @@ let rec check_modules cst env msid1 l msb1 msb2 = and check_signatures cst env (msid1,sig1) (msid2,sig2') = let mp1 = MPself msid1 in let env = add_signature mp1 sig1 env in - let sig2 = try - subst_signature_msid msid2 mp1 sig2' - with - | Circularity l -> - error_circularity_in_subtyping l (string_of_msid msid1) (string_of_msid msid2) in + let sig2 = subst_signature_msid msid2 mp1 sig2' in let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v index cfd91a2eb..0b3a8688e 100644 --- a/test-suite/failure/circular_subtyping1.v +++ b/test-suite/failure/circular_subtyping1.v @@ -1,4 +1,4 @@ -(* Circular substitution check in subtyping verification *) +(* subtyping verification in presence of pseudo-circularity*) Module Type S. End S. Module Type T. Declare Module M:S. End T. diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v index 75b27bce9..3bacdc655 100644 --- a/test-suite/failure/circular_subtyping2.v +++ b/test-suite/failure/circular_subtyping2.v @@ -1,20 +1,8 @@ -(* Circular substitution check at functor application *) +(*subtyping verification in presence of pseudo-circularity at functor application *) Module Type S. End S. Module Type T. Declare Module M:S. End T. Module N:S. End N. Module F (X:S) (Y:T with Module M:=X). End F. -Module A := F N N. -(* Circular substitution check at with definition *) -(* Should it be implemented?? *) -(* - -Module NN:T. Module M:=N. End NN. -Module Type U := T with Module M:=NN. -(* -User error: The construction "with Module M:=..." is about to create -a circular module type. Their resolution is not implemented yet. -If you really need that feature, please report. -*) -*) +Module G := F N N.
\ No newline at end of file |