Moving printing of module typing errors upwards to himsg.ml so as to

be able to call term printers.

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

7 files changed, 103 insertions, 132 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index bbcabd72a2..335c2a94ee 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -132,12 +132,12 @@ and check_with_aux_def env sign with_decl mp equiv =
 						    mod_type_alg = None}) in
 			  SEBstruct(before@((l,new_spec)::after)),cb,cst
                     | Some msb ->
-			error_a_generative_module_expected l
+			error_generative_module_expected l
 		end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+      | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
 and check_with_aux_mod env sign with_decl mp equiv = 
   let sig_b = match sign with 
@@ -175,12 +175,12 @@ and check_with_aux_mod env sign with_decl mp equiv =
 			  (check_subtypes env' mtb_mp1 
 			     (module_type_of_module env' None old))
 			  old.mod_constraints
-			with Failure _ -> error_with_incorrect (label_of_id id)
+			with Failure _ -> error_incorrect_with_constraint (label_of_id id)
 		      end
 		  | Some (SEBident(mp')) ->
 		      check_modpath_equiv env' mp1 mp';
 		      old.mod_constraints
-		  | _ ->  error_a_generative_module_expected l
+		  | _ ->  error_generative_module_expected l
 	      in
 	      let new_mb = strengthen_and_subst_mb mb_mp1
 		(MPdot(mp,l)) env false in
@@ -220,12 +220,12 @@ and check_with_aux_mod env sign with_decl mp equiv =
 			  SEBstruct(before@(l,spec)::after)
 			    ,equiv,empty_constraint
 		  | _ ->
-		      error_a_generative_module_expected l
+		      error_generative_module_expected l
               end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+      | Reduction.NotConvertible -> error_incorrect_with_constraint l
 
 and translate_module env mp inl me =
   match me.mod_entry_expr, me.mod_entry_type with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 302d251949..6d4ebb989b 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -25,19 +25,6 @@ open Environ
 open Entries
 open Mod_subst
 
-let error_existing_label l = 
-  error ("The label "^string_of_label l^" is already declared.")
-
-let error_declaration_not_path _ = error "Declaration is not a path."
-
-let error_application_to_not_path _ = error "Application to not path."
-
-let error_not_a_functor _ = error "Application of not a functor."
-
-let error_incompatible_modtypes _ _ = error "Incompatible module types."
-
-let error_not_equal _ _ = error "Non equal modules."
-
 type signature_mismatch_error =
   | InductiveFieldExpected of mutual_inductive_body
   | DefinitionFieldExpected
@@ -57,104 +44,83 @@ type signature_mismatch_error =
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
 
-let explain_not_match_error = function
-  | InductiveFieldExpected _ ->
-    strbrk "an inductive definition is expected"
-  | DefinitionFieldExpected ->
-    strbrk "a definition is expected"
-  | ModuleFieldExpected ->
-    strbrk "a module is expected"
-  | ModuleTypeFieldExpected ->
-    strbrk "a module type is expected"
-  | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
-    str "types given to " ++ str (string_of_id id) ++ str " differ"
-  | NotConvertibleBodyField ->
-    str "the body of definitions differs"
-  | NotConvertibleTypeField ->
-    str "types differ"
-  | NotSameConstructorNamesField ->
-    str "constructor names differ"
-  | NotSameInductiveNameInBlockField ->
-    str "inductive types names differ"
-  | FiniteInductiveFieldExpected isfinite ->
-    str "type is expected to be " ++
-    str (if isfinite then "coinductive" else "inductive")
-  | InductiveNumbersFieldExpected n ->
-    str "number of inductive types differs"
-  | InductiveParamsNumberField n ->
-    str "inductive type has not the right number of parameters"
-  | RecordFieldExpected isrecord ->
-    str "type is expected " ++ str (if isrecord then "" else "not ") ++
-    str "to be a record"
-  | RecordProjectionsExpected nal ->
-    (if List.length nal >= 2 then str "expected projection names are "
-     else str "expected projection name is ") ++
-    pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal
-  | NotEqualInductiveAliases ->
-    str "Aliases to inductive types do not match"
-  | NoTypeConstraintExpected ->
-    strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained"
-
-let error_not_match l _ why =
-  errorlabstrm ""
-    (str "Signature components for label " ++ str (string_of_label l) ++
-     str " do not match:" ++ spc () ++ explain_not_match_error why ++ str ".")
-
-let error_no_such_label l = error ("No such label "^string_of_label l^".")
-
-let error_incompatible_labels l l' = 
-  error ("Opening and closing labels are not the same: "
-	 ^string_of_label l^" <> "^string_of_label l'^" !")
-
-let error_result_must_be_signature () = 
-  error "The result module type must be a signature."
+type module_typing_error =
+  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of label
+  | ApplicationToNotPath of module_struct_entry
+  | NotAFunctor of struct_expr_body
+  | IncompatibleModuleTypes of module_type_body * module_type_body
+  | NotEqualModulePaths of module_path * module_path
+  | NoSuchLabel of label
+  | IncompatibleLabels of label * label
+  | SignatureExpected of struct_expr_body
+  | NoModuleToEnd
+  | NoModuleTypeToEnd
+  | NotAModule of string
+  | NotAModuleType of string
+  | NotAConstant of label
+  | IncorrectWithConstraint of label
+  | GenerativeModuleExpected of label
+  | NonEmptyLocalContect of label option
+  | LabelMissing of label * string
 
-let error_signature_expected mtb =
-  error "Signature expected."
+exception ModuleTypingError of module_typing_error
 
-let error_no_module_to_end _ = 
-  error "No open module to end."
+let error_existing_label l =
+  raise (ModuleTypingError (LabelAlreadyDeclared l))
 
-let error_no_modtype_to_end _ =
-  error "No open module type to end."
+let error_application_to_not_path mexpr =
+  raise (ModuleTypingError (ApplicationToNotPath mexpr))
 
-let error_not_a_modtype_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module type."))
+let error_not_a_functor mtb =
+  raise (ModuleTypingError (NotAFunctor mtb))
 
-let error_not_a_module_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
+let error_incompatible_modtypes mexpr1 mexpr2 =
+  raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2)))
 
-let error_not_a_module_or_modtype_loc loc s =
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type."))
+let error_not_equal_modpaths mp1 mp2 =
+  raise (ModuleTypingError (NotEqualModulePaths (mp1,mp2)))
 
-let error_not_a_module s = error_not_a_module_loc dummy_loc s
+let error_signature_mismatch l spec why =
+  raise (ModuleTypingError (SignatureMismatch (l,spec,why)))
 
-let error_not_a_constant l = 
-  error ("\""^(string_of_label l)^"\" is not a constant.")
+let error_no_such_label l =
+  raise (ModuleTypingError (NoSuchLabel l))
 
-let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(string_of_label l)^"\".")
+let error_incompatible_labels l l' =
+  raise (ModuleTypingError (IncompatibleLabels (l,l')))
 
-let error_a_generative_module_expected l =
-  error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
-         "components of generative modules can be changed using the \"with\" " ^
-         "construct.")
+let error_signature_expected mtb =
+  raise (ModuleTypingError (SignatureExpected mtb))
 
-let error_local_context lo = 
-  match lo with
-      None -> 
-	error ("The local context is not empty.")
-    | (Some l) ->
-	error ("The local context of the component "^
-	       (string_of_label l)^" is not empty.")
+let error_no_module_to_end _ =
+  raise (ModuleTypingError NoModuleToEnd)
 
+let error_no_modtype_to_end _ =
+  raise (ModuleTypingError NoModuleTypeToEnd)
 
-let error_no_such_label_sub l l1 =
-  error ("The field "^(string_of_label l)^" is missing in "^l1^".")
+let error_not_a_modtype s =
+  raise (ModuleTypingError (NotAModuleType s))
+
+let error_not_a_module s =
+  raise (ModuleTypingError (NotAModule s))
+
+let error_not_a_constant l =
+  raise (ModuleTypingError (NotAConstant l))
 
-let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules."
+let error_incorrect_with_constraint l =
+  raise (ModuleTypingError (IncorrectWithConstraint l))
+
+let error_generative_module_expected l =
+  raise (ModuleTypingError (GenerativeModuleExpected l))
+
+let error_non_empty_local_context lo =
+  raise (ModuleTypingError (NonEmptyLocalContect lo))
+
+let error_no_such_label_sub l l1 =
+  raise (ModuleTypingError (LabelMissing (l,l1)))
 
-let error_application_to_module_type _ = error "Module application to a module type."
+(************************)
 
 let destr_functor env mtb =
   match mtb with
@@ -181,7 +147,7 @@ let check_modpath_equiv env mp1 mp2 =
     let mb2=lookup_module mp2 env in
       if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
       then ()
-      else error_not_equal mp1 mp2
+      else error_not_equal_modpaths mp1 mp2
 	
 let rec subst_with_body sub = function
   | With_module_body(id,mp) ->
diff --git a/kernel/modops.mli b/kernel/modops.mli
index cf8d62043f..35be04665b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -72,53 +72,56 @@ type signature_mismatch_error =
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
 
-val error_existing_label : label -> 'a
+type module_typing_error =
+  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of label
+  | ApplicationToNotPath of module_struct_entry
+  | NotAFunctor of struct_expr_body
+  | IncompatibleModuleTypes of module_type_body * module_type_body
+  | NotEqualModulePaths of module_path * module_path
+  | NoSuchLabel of label
+  | IncompatibleLabels of label * label
+  | SignatureExpected of struct_expr_body
+  | NoModuleToEnd
+  | NoModuleTypeToEnd
+  | NotAModule of string
+  | NotAModuleType of string
+  | NotAConstant of label
+  | IncorrectWithConstraint of label
+  | GenerativeModuleExpected of label
+  | NonEmptyLocalContect of label option
+  | LabelMissing of label * string
+
+exception ModuleTypingError of module_typing_error
 
-val error_declaration_not_path : module_struct_entry -> 'a
+val error_existing_label : label -> 'a
 
 val error_application_to_not_path : module_struct_entry -> 'a
 
-val error_not_a_functor :  module_struct_entry -> 'a
-
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
-val error_not_equal : module_path -> module_path -> 'a
-
-val error_not_match :
+val error_signature_mismatch :
   label -> structure_field_body -> signature_mismatch_error -> 'a
 
 val error_incompatible_labels : label -> label -> 'a
 
 val error_no_such_label : label -> 'a
 
-val error_result_must_be_signature : unit -> 'a
-
 val error_signature_expected : struct_expr_body -> 'a
 
 val error_no_module_to_end : unit -> 'a
 
 val error_no_modtype_to_end : unit -> 'a
 
-val error_not_a_modtype_loc : loc -> string -> 'a
-
-val error_not_a_module_loc : loc -> string -> 'a
-
-val error_not_a_module_or_modtype_loc : loc -> string -> 'a
-
 val error_not_a_module : string -> 'a
 
 val error_not_a_constant : label -> 'a
 
-val error_with_incorrect : label -> 'a
+val error_incorrect_with_constraint : label -> 'a
 
-val error_a_generative_module_expected : label -> 'a
+val error_generative_module_expected : label -> 'a
 
-val error_local_context : label option -> 'a
+val error_non_empty_local_context : label option -> 'a
 
 val error_no_such_label_sub : label->string->'a
-
-val error_with_in_module : unit -> 'a
-
-val error_application_to_module_type : unit -> 'a
-
diff --git a/kernel/names.ml b/kernel/names.ml
index 6e39b35bb3..4466f558f9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -107,6 +107,7 @@ let label_of_mbid (_,s,_) = s
 
 let mk_label l = l
 let string_of_label = string_of_id
+let pr_label l = str (string_of_label l)
 
 let id_of_label l = l
 let label_of_id id = id
diff --git a/kernel/names.mli b/kernel/names.mli
index 2d112b32ac..acc764028f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -47,6 +47,7 @@ type label
 
 val mk_label : string -> label
 val string_of_label : label -> string
+val pr_label : label -> Pp.std_ppcmds
 
 val label_of_id : identifier -> label
 val id_of_label : label -> identifier
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 66c731a9de..8f4ec76f84 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -367,7 +367,7 @@ let end_module l restype senv =
       | STRUCT params -> params, (List.length params > 0)
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
-  if not (empty_context senv.env) then error_local_context None;
+  if not (empty_context senv.env) then error_non_empty_local_context None;
   let functorize_struct tb =
     List.fold_left
       (fun mtb (arg_id,arg_b) ->
@@ -574,7 +574,7 @@ let end_modtype l senv =
       | SIG params -> params
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
-  if not (empty_context senv.env) then error_local_context None;
+  if not (empty_context senv.env) then error_non_empty_local_context None;
   let auto_tb =
      SEBstruct (List.rev senv.revstruct)
   in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8085575217..0c72995080 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -78,7 +78,7 @@ let check_conv_error error why cst f env a1 a2 =
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
   let kn1 = make_mind mp1 empty_dirpath l in
   let kn2 = make_mind mp2 empty_dirpath l in
-  let error why = error_not_match l spec2 why in
+  let error why = error_signature_mismatch l spec2 why in
   let check_conv why cst f = check_conv_error error why cst f in
   let mib1 =
     match info1 with
@@ -201,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 
     
 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
-  let error why = error_not_match l spec2 why in
+  let error why = error_signature_mismatch l spec2 why in
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
@@ -353,13 +353,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      match info1 with
 		| Module msb -> check_modules cst env msb msb2 
 		    subst1 subst2
-		| _ -> error_not_match l spec2 ModuleFieldExpected
+		| _ -> error_signature_mismatch l spec2 ModuleFieldExpected
 	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 =
 	      match info1 with
 		| Modtype mtb -> mtb
-		| _ -> error_not_match l spec2 ModuleTypeFieldExpected
+		| _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
 	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
 	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in