Quick improvement of some error messages related to module application

(localization of the error and hopefully improved messages)
[Is there a reason why the restriction is not enforced at the parsing level?
Anyway, treating it at interpretation time allows more appropriate messages]

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

6 files changed, 44 insertions, 31 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index c127590923..a13560c0ff 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -53,11 +53,11 @@ let error_not_a_module_loc loc s =
 let error_not_a_module_nor_modtype_loc loc s =
   Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s))
 
-let error_incorrect_with_in_module () =
-  raise (ModuleInternalizationError IncorrectWithInModule)
+let error_incorrect_with_in_module loc =
+  Compat.Loc.raise loc (ModuleInternalizationError IncorrectWithInModule)
 
-let error_application_to_module_type () =
-  raise (ModuleInternalizationError IncorrectModuleApplication)
+let error_application_to_module_type loc =
+  Compat.Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
 
 
 
@@ -142,24 +142,35 @@ let transl_with_decl env = function
   | CWith_Definition ((_,fqid),c) ->
       With_Definition (fqid,interp_constr Evd.empty env c)
 
+let loc_of_module = function
+  | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
+
+let check_module_argument_is_path me' = function
+  | CMident _ -> ()
+  | (CMapply (loc,_,_) | CMwith (loc,_,_)) ->
+      Compat.Loc.raise loc
+        (Modops.ModuleTypingError (Modops.ApplicationToNotPath me'))
+
 let rec interp_modexpr env = function
   | CMident qid ->
       MSEident (lookup_module qid)
-  | CMapply (me1,me2) ->
-      let me1 = interp_modexpr env me1 in
-      let me2 = interp_modexpr env me2 in
-	MSEapply(me1,me2)
-  | CMwith _ -> error_incorrect_with_in_module ()
+  | CMapply (_,me1,me2) ->
+      let me1' = interp_modexpr env me1 in
+      let me2' = interp_modexpr env me2 in
+      check_module_argument_is_path me2' me2;
+      MSEapply(me1',me2')
+  | CMwith (loc,_,_) -> error_incorrect_with_in_module loc
 
 
 let rec interp_modtype env = function
   | CMident qid ->
       MSEident (lookup_modtype qid)
-  | CMapply (mty1,me) ->
+  | CMapply (_,mty1,me) ->
       let mty' = interp_modtype env mty1 in
       let me' = interp_modexpr env me in
-	MSEapply(mty',me')
-  | CMwith (mty,decl) ->
+      check_module_argument_is_path me' me;
+      MSEapply(mty',me')
+  | CMwith (_,mty,decl) ->
       let mty = interp_modtype env mty in
       let decl = transl_with_decl env decl in
 	MSEwith(mty,decl)
@@ -168,13 +179,14 @@ let rec interp_modexpr_or_modtype env = function
   | CMident qid ->
       let (mp,ismod) = lookup_module_or_modtype qid in
       (MSEident mp, ismod)
-  | CMapply (me1,me2) ->
-      let me1,ismod1 = interp_modexpr_or_modtype env me1 in
-      let me2,ismod2 = interp_modexpr_or_modtype env me2 in
-      if not ismod2 then error_application_to_module_type ();
-      (MSEapply (me1,me2), ismod1)
-  | CMwith (me,decl) ->
+  | CMapply (_,me1,me2) ->
+      let me1',ismod1 = interp_modexpr_or_modtype env me1 in
+      let me2',ismod2 = interp_modexpr_or_modtype env me2 in
+      check_module_argument_is_path me2' me2;
+      if not ismod2 then error_application_to_module_type (loc_of_module me2);
+      (MSEapply (me1',me2'), ismod1)
+  | CMwith (loc,me,decl) ->
       let me,ismod = interp_modexpr_or_modtype env me in
       let decl = transl_with_decl env decl in
-      if ismod then error_incorrect_with_in_module ();
+      if ismod then error_incorrect_with_in_module loc;
       (MSEwith(me,decl), ismod)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5ed7f31b19..73fb3452b4 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1237,8 +1237,8 @@ type with_declaration_ast =
 
 type module_ast =
   | CMident of qualid located
-  | CMapply of module_ast * module_ast
-  | CMwith of module_ast * with_declaration_ast
+  | CMapply of loc * module_ast * module_ast
+  | CMwith of loc * module_ast * with_declaration_ast
 
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
 (* and which are then occupied by proper symbols of the notation (or spaces) *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 95c1af17d9..ecffed6a45 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -262,8 +262,8 @@ type with_declaration_ast =
 
 type module_ast =
   | CMident of qualid located
-  | CMapply of module_ast * module_ast
-  | CMwith of module_ast * with_declaration_ast
+  | CMapply of loc * module_ast * module_ast
+  | CMwith of loc * module_ast * with_declaration_ast
 
 val ntn_loc :
   Util.loc -> constr_notation_substitution -> string -> (int * int) list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 965091683a..e27fcca275 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -485,7 +485,7 @@ GEXTEND Gram
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
-      | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2)
+      | me1 = module_expr; me2 = module_expr_atom -> CMapply (loc,me1,me2)
       ] ]
   ;
   module_expr_atom:
@@ -501,8 +501,9 @@ GEXTEND Gram
   module_type:
     [ [ qid = qualid -> CMident qid
       | "("; mt = module_type; ")" -> mt
-      | mty = module_type; me = module_expr_atom -> CMapply (mty,me)
-      | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl)
+      | mty = module_type; me = module_expr_atom -> CMapply (loc,mty,me)
+      | mty = module_type; "with"; decl = with_declaration ->
+          CMwith (loc,mty,decl)
       ] ]
   ;
 END
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index db6f0e6216..375e071f8b 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -218,13 +218,13 @@ let pr_with_declaration pr_c = function
 
 let rec pr_module_ast pr_c = function
   | CMident qid -> spc () ++ pr_located pr_qualid qid
-  | CMwith (mty,decl) ->
+  | CMwith (_,mty,decl) ->
       let m = pr_module_ast pr_c mty in
       let p = pr_with_declaration pr_c decl in
       m ++ spc() ++ str"with" ++ spc() ++ p
-  | CMapply (me1,(CMident _ as me2)) ->
+  | CMapply (_,me1,(CMident _ as me2)) ->
       pr_module_ast pr_c me1 ++ spc() ++ pr_module_ast pr_c me2
-  | CMapply (me1,me2) ->
+  | CMapply (_,me1,me2) ->
       pr_module_ast pr_c me1 ++ spc() ++
       hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 06fc7e663a..1bd680144b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -579,7 +579,7 @@ let explain_label_already_declared l =
   str ("The label "^string_of_label l^" is already declared.")
 
 let explain_application_to_not_path _ =
-  str "Application to not path."
+  str "Application of modules is restricted to paths."
 
 let explain_not_a_functor mtb =
   str "Application of not a functor."
@@ -668,7 +668,7 @@ let explain_incorrect_with_in_module () =
   str "The syntax \"with\" is not allowed for modules."
 
 let explain_incorrect_module_application () =
-  str "Module application to a module type."
+  str "Illegal application to a module type."
 
 open Modintern