improve some error messages (#776)

* improve error message when require/open unqualified identifier
* add KO test for require without root_path prefix
* improve error message when a pattern is applied to an explicit term
* improve error message in case of invalid character

Author: fblanqui

src/common/error.ml

@@ -3,6 +3,10 @@
 open Lplib
 open Base
 
+(** Exception raised by the parser when an unqualified identifier is given
+   instead of a qualified one. *)
+exception NotQualified
+
 (** [err_fmt] warning/error output formatter. *)
 let err_fmt = Stdlib.ref Format.err_formatter
 

src/parsing/lpLexer.ml

@@ -21,7 +21,7 @@ let fail : Sedlexing.lexbuf -> string -> 'a = fun lb msg ->
   raise (SyntaxError (make_pos (lexing_positions lb) msg))
 
 let invalid_character : Sedlexing.lexbuf -> 'a = fun lb ->
-  fail lb ("Invalid character: \"" ^ Utf8.lexeme lb ^ "\".")
+  fail lb "Invalid character"
 
 (** Tokens. *)
 type token =

src/parsing/lpParser.mly

@@ -141,7 +141,9 @@ qid:
   | s=UID { make_pos $sloc ([], s) }
   | p=QID { qid_of_path $sloc p }
 
-path: p=QID { make_pos $sloc (List.rev p) }
+path:
+  | UID { raise Error.NotQualified }
+  | p=QID { make_pos $sloc (List.rev p) }
 
 qid_expl:
   | s=UID_EXPL { make_pos $sloc ([], s) }
@@ -279,8 +281,8 @@ command:
     { make_pos $sloc (P_require(true,l)) }
   | REQUIRE l=list(path) SEMICOLON
     { make_pos $sloc (P_require(false,l)) }
-  | REQUIRE i=path AS a=uid SEMICOLON
-    { make_pos $sloc (P_require_as(i,a)) }
+  | REQUIRE p=path AS i=uid SEMICOLON
+    { make_pos $sloc (P_require_as(p,i)) }
   | OPEN l=list(path) SEMICOLON
     { make_pos $sloc (P_open l) }
   | ms=modifier* SYMBOL s=uid al=param_list* COLON a=term

src/parsing/parser.ml

@@ -60,9 +60,14 @@ module Lp : PARSER = struct
         | End_of_file -> Option.iter close_in inchan; None
         | LpLexer.SyntaxError {pos=None; _} -> assert false
         | LpLexer.SyntaxError {pos=Some pos; elt} -> parser_fatal pos "%s" elt
+        | Error.NotQualified ->
+          let pos = Pos.locate (Sedlexing.lexing_positions lb) in
+          parser_fatal pos
+            "Unqualified identifier (the root_path is missing)."
         | LpParser.Error ->
             let pos = Pos.locate (Sedlexing.lexing_positions lb) in
-            parser_fatal pos "Unexpected token: %s" (Sedlexing.Utf8.lexeme lb)
+            parser_fatal pos "Unexpected token: \"%s\"."
+              (Sedlexing.Utf8.lexeme lb)
       in
       Stream.from generator
 
@@ -105,7 +110,7 @@ module Dk : PARSER = struct
         | End_of_file -> Option.iter close_in inchan; None
         | DkParser.Error ->
             let pos = Pos.locate (Lexing.(lb.lex_start_p, lb.lex_curr_p)) in
-            parser_fatal pos "Unexpected token [%s]." (Lexing.lexeme lb)
+            parser_fatal pos "Unexpected token \"%s\"." (Lexing.lexeme lb)
       in
       Stream.from generator
 

src/parsing/scope.ml

@@ -200,7 +200,12 @@ and scope_parsed : int -> mode -> sig_state -> env -> p_term -> tbox =
   begin
     match p_head.elt, md with
     | P_Patt _, M_LHS _ when args <> [] ->
-      fatal t.pos "Pattern variables cannot be applied."
+      begin match args with
+        | [{elt=P_Expl _;_}] ->
+          fatal t.pos "Explicit terms are forbidden in rule LHS. \
+                       You perhaps forgot to write a dot before?"
+        | _ -> fatal t.pos "Pattern variables cannot be applied."
+      end
     | _ -> ()
   end;
   (* Scope the head and obtain the implicitness of arguments. *)
@@ -305,7 +310,7 @@ and scope_binder : ?warn:bool -> int -> mode -> sig_state ->
           cons a (Bindlib.bind_var v t)
       | Some {elt=id;pos}::idopts ->
           if is_invalid_bindlib_id id then
-            fatal pos "%s: Escaped identifiers or regular identifiers \
+            fatal pos "\"%s\": Escaped identifiers or regular identifiers \
                        having an integer suffix with leading zeros \
                        are not allowed for bound variable names." id;
           let v = new_tvar id in

tests/KO/req_without_root_path.lp

@@ -0,0 +1 @@
+require bool;