diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/modops.ml | 20 | ||||
| -rw-r--r-- | kernel/modops.mli | 6 | ||||
| -rw-r--r-- | kernel/names.ml | 15 | ||||
| -rw-r--r-- | kernel/names.mli | 8 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 10 |
6 files changed, 49 insertions, 25 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 785778235f..824d2e4eb5 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -120,10 +120,10 @@ and merge_with env mtb with_decl = we check that there is no msid bound in mtb *) begin try - let _ = subst_modtype (map_msid msid (MPself msid)) mtb in + let _ = subst_modtype (map_msid msid (MPself msid)) mtb in () with - Failure _ -> error_circular_with_module id + Circularity _ -> error_circular_with_module id end; let cst = try check_subtypes env' mtb old.msb_modtype @@ -247,9 +247,7 @@ and translate_module env is_definition me = | None -> mtb1, None, Constraint.empty | Some mte -> let mtb2 = translate_modtype env mte in - let cst = - try check_subtypes env mtb1 mtb2 - with Failure _ -> error "not subtype" in + let cst = check_subtypes env mtb1 mtb2 in mtb2, Some mtb2, cst in { mod_type = mtb; @@ -274,10 +272,7 @@ and translate_mexpr env mexpr = match mexpr with let ftb = scrape_modtype env ftb in let farg_id, farg_b, fbody_b = destr_functor ftb in let meb,mtb = translate_mexpr env mexpr in - let cst = - try check_subtypes env mtb farg_b - with Failure _ -> - error "" in + let cst = check_subtypes env mtb farg_b in let mp = try path_of_mexpr mexpr @@ -290,7 +285,7 @@ and translate_mexpr env mexpr = match mexpr with (* This is the place where the functor formal parameter is substituted by the given argument to compute the type of the functor application. *) - subst_modtype + subst_modtype (map_mbid farg_id mp (Some resolve)) fbody_b | MEstruct (msid,structure) -> let structure,signature = translate_entry_list env msid true structure in diff --git a/kernel/modops.ml b/kernel/modops.ml index 0108229ca0..ad7b7d9ad4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -20,6 +20,8 @@ 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") @@ -83,6 +85,12 @@ let error_local_context lo = 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^".") + let rec scrape_modtype env = function | MTBident kn -> scrape_modtype env (lookup_modtype kn env) | mtb -> mtb @@ -134,16 +142,16 @@ 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 failwith "capture"; + if occur_mbid arg_id sub then raise (Circularity (debug_string_of_mbid arg_id)); MTBfunsig (arg_id, - subst_modtype sub arg_b, - subst_modtype sub body_b) + subst_modtype sub arg_b, + subst_modtype sub body_b) | MTBsig (sid1, msb) -> - if occur_msid sid1 sub then failwith "capture"; + if occur_msid sid1 sub then raise (Circularity (debug_string_of_msid sid1)); MTBsig (sid1, subst_signature sub msb) and subst_signature sub sign = - let subst_body = function + let subst_body = function SPBconst cb -> SPBconst (subst_const_body sub cb) | SPBmind mib -> @@ -155,7 +163,7 @@ and subst_signature sub sign = in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub mb = +and subst_module sub mb = let mtb' = subst_modtype sub mb.msb_modtype in (* This is similar to the previous case. In this case we have a module M in a signature that is knows to be equivalent to a module M' diff --git a/kernel/modops.mli b/kernel/modops.mli index b8f1f66a3c..803bdc8398 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 *) @@ -98,5 +98,9 @@ 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 : mod_bound_id -> module_type_body -> module_path -> env -> resolver diff --git a/kernel/names.ml b/kernel/names.ml index d73af7fa1d..5dcd8a68f6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -73,26 +73,33 @@ let string_of_dirpath = function let u_number = ref 0 type uniq_ident = int * string * dir_path let make_uid dir s = incr u_number;(!u_number,String.copy s,dir) + let debug_string_of_uid (i,s,p) = + "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" let string_of_uid (i,s,p) = - "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" + string_of_dirpath p ^"."^s module Umap = Map.Make(struct type t = uniq_ident let compare = Pervasives.compare end) +type label = string type mod_self_id = uniq_ident let make_msid = make_uid -let debug_string_of_msid = string_of_uid +let debug_string_of_msid = debug_string_of_uid +let string_of_msid = string_of_uid let id_of_msid (_,s,_) = s +let label_of_msid (_,s,_) = s type mod_bound_id = uniq_ident let make_mbid = make_uid -let debug_string_of_mbid = string_of_uid +let debug_string_of_mbid = debug_string_of_uid +let string_of_mbid = string_of_uid let id_of_mbid (_,s,_) = s +let label_of_mbid (_,s,_) = s + -type label = string let mk_label l = l let string_of_label l = l diff --git a/kernel/names.mli b/kernel/names.mli index 4c51269d08..051087f5d4 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -42,24 +42,28 @@ 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 mod_self_id (* The first argument is a file name - to prevent conflict between different files *) 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 debug_string_of_msid : mod_self_id -> string +val string_of_msid : mod_self_id -> string (*s Unique names for bound modules *) type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id val id_of_mbid : mod_bound_id -> identifier +val label_of_mbid : mod_bound_id -> label val debug_string_of_mbid : mod_bound_id -> string +val string_of_mbid : mod_bound_id -> string (*s Names of structure elements *) -type label + val mk_label : string -> label val string_of_label : label -> string diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 537c20aef2..98ec21eaaa 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -22,6 +22,8 @@ open Mod_subst open Entries (*i*) + + (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in inductive types *) @@ -304,14 +306,18 @@ 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 = subst_signature_msid msid2 mp1 sig2' in + let sig2 = try + subst_signature_msid msid2 mp1 sig2' + with + | Circularity l -> + error_circularity_in_subtyping l (debug_string_of_msid msid1) (debug_string_of_msid msid2) in let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = try Labmap.find l map1 with - Not_found -> error_no_such_label l + Not_found -> error_no_such_label_sub l (debug_string_of_msid msid1) (debug_string_of_msid msid2) in match spec2 with | SPBconst cb2 -> |