modifications des messages d'erreurs renvoyés lors de la comparaison

de deux signatures de modules.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 85f007b7-540e-0410-9357-904b9bb8a0f7

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 ->