Merge PR #17136: [gramlib] Move syntax errors to Grammar.

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

dev/ci/user-overlays/17136-ppedrot-stream_error_to_gramlib.sh

@@ -0,0 +1,2 @@
+overlay elpi https://github.com/ppedrot/coq-elpi stream_error_to_gramlib 17136
+overlay vscoq https://github.com/ppedrot/vscoq stream_error_to_gramlib 17136

gramlib/grammar.ml

@@ -6,6 +6,10 @@ open Gramext
 open Format
 open Util
 
+exception Error of string
+(** Raised by parsers when the first component of a stream pattern is
+   accepted, but one of the following components is rejected. *)
+
 (* Functorial interface *)
 
 type norec
@@ -1155,7 +1159,7 @@ let token_ematch tok =
   fun tok -> tematch tok
 
 let empty_entry ename levn strm =
-  raise (Stream.Error ("entry [" ^ ename ^ "] is empty"))
+  raise (Error ("entry [" ^ ename ^ "] is empty"))
 
 let start_parser_of_entry gstate entry levn (strm:_ LStream.t) =
   (get_entry gstate.estate entry).estart gstate levn strm
@@ -1202,7 +1206,7 @@ let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_
              let act =
                try p1 gstate bp a strm__ with
                  Stream.Failure ->
-                   raise (Stream.Error (tree_failed entry a s son))
+                   raise (Error (tree_failed entry a s son))
              in
              act a)
   | Node (_, {node = s; son = son; brother = bro}) ->
@@ -1218,7 +1222,7 @@ let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_
                    (try Some (p1 gstate bp a strm) with Stream.Failure -> None)
                  with
                    Some act -> act a
-                 | None -> raise (Stream.Error (tree_failed entry a s son))
+                 | None -> raise (Error (tree_failed entry a s son))
                  end
              | None -> p2 gstate strm)
 and parser_cont : type s tr tr' a r.
@@ -1260,7 +1264,7 @@ and parser_cont : type s tr tr' a r.
         let a = continue_parser_of_entry gstate (entry_of_symb entry s) 0 bp a strm__ in
         let act =
           try p1 gstate strm__ with
-            Stream.Failure -> raise (Stream.Error (tree_failed entry a s son))
+            Stream.Failure -> raise (Error (tree_failed entry a s son))
         in
         fun _ -> act a
 
@@ -1318,8 +1322,12 @@ and parser_of_token_list : type s tr lt r.
     match LStream.peek gstate.kwstate strm with
     | Some tok' ->
       let a = tematch tok' in
-      begin try let act = ps gstate a strm in act a
-      with TokenListFailed (entry, a, tok, tree) -> raise (Stream.Error (tree_failed entry a tok tree)) end
+      begin
+        try let act = ps gstate a strm in act a
+        with
+        | TokenListFailed (entry, a, tok, tree) ->
+          raise (Error (tree_failed entry a tok tree))
+      end
     | None -> raise Stream.Failure
 and parser_of_symbol : type s tr a.
   s ty_entry -> int -> (s, tr, a) ty_symbol -> GState.t -> a parser_t =
@@ -1343,7 +1351,7 @@ and parser_of_symbol : type s tr a.
             let al =
               try ps gstate strm__ :: al with
                 Stream.Failure ->
-                  raise (Stream.Error (symb_failed entry v sep symb))
+                  raise (Error (symb_failed entry v sep symb))
             in
             kont gstate al strm__
         | _ -> al
@@ -1392,7 +1400,7 @@ and parser_of_symbol : type s tr a.
                   let a =
                     try parse_top_symb entry symb gstate strm__ with
                       Stream.Failure ->
-                        raise (Stream.Error (symb_failed entry v sep symb))
+                        raise (Error (symb_failed entry v sep symb))
                   in
                   a :: al
             in
@@ -1656,9 +1664,9 @@ module Parsable = struct
       let exn, info = Exninfo.capture exn in
       let loc = get_parsing_loc () in
       let info = Loc.add_loc info loc in
-      let exn = Stream.Error ("illegal begin of " ^ entry.ename) in
+      let exn = Error ("illegal begin of " ^ entry.ename) in
       Exninfo.iraise (exn, info)
-    | Stream.Error _ as exn ->
+    | Error _ as exn ->
       let exn, info = Exninfo.capture exn in
       let loc = get_parsing_loc () in
       let info = Loc.add_loc info loc in

gramlib/grammar.mli

@@ -8,6 +8,10 @@
     Grammars entries can be extended using the [EXTEND] statement,
     added by loading the Camlp5 [pa_extend.cmo] file. *)
 
+exception Error of string
+(** Raised by parsers when the first component of a stream pattern is
+   accepted, but one of the following components is rejected. *)
+
 (** {6 Functorial interface} *)
 
    (** Alternative for grammars use. Grammars are no more Ocaml values:

gramlib/stream.ml

@@ -24,7 +24,6 @@ and buffio =
   { ic : in_channel; buff : bytes; mutable len : int; mutable ind : int }
 
 exception Failure
-exception Error of string
 
 let count { count } = count
 

gramlib/stream.mli

@@ -20,13 +20,7 @@ type ('e,'a) t
     Producing a new value needs an environment ['e]. *)
 
 exception Failure
-(** Raised by parsers when none of the first components of the stream
-   patterns is accepted. *)
-
-exception Error of string
-(** Raised by parsers when the first component of a stream pattern is
-   accepted, but one of the following components is rejected. *)
-
+(** Raised by streams when trying to access beyond their end. *)
 
 (** {1 Stream builders} *)
 

interp/constrexpr_ops.ml

@@ -585,7 +585,7 @@ let split_at_annot bl na =
         else
           aux (x :: acc) rest
       | CLocalPattern _ :: rest ->
-        Loc.raise ?loc (Gramlib.Stream.Error "pattern with quote not allowed after fix")
+        Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed after fix")
       | [] ->
         CErrors.user_err ?loc
           (str "No parameter named " ++ Id.print id ++ str".")

interp/constrintern.ml

@@ -581,7 +581,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
       let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous) in
       (na,Explicit,Some c,t)
   | GLocalPattern (_,_,_,_) ->
-      Loc.raise ?loc (Gramlib.Stream.Error "pattern with quote not allowed here")
+      Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
   )
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")

parsing/cLexer.ml

@@ -418,7 +418,7 @@ let rec comment loc bp s =
               Stream.junk () s;
               push_string "(*"; comment loc bp s
           | _ -> push_string "("; loc
-        with Stream.Failure -> raise (Stream.Error "")
+        with Stream.Failure -> raise (Gramlib.Grammar.Error "")
       in
       comment loc bp s
   | Some '*' ->
@@ -427,7 +427,7 @@ let rec comment loc bp s =
         match Stream.peek () s with
           Some ')' -> Stream.junk () s; push_string "*)"; loc
         | _ -> real_push_char '*'; comment loc bp s
-      with Stream.Failure -> raise (Stream.Error "")
+      with Stream.Failure -> raise (Gramlib.Grammar.Error "")
       end
   | Some '"' ->
       Stream.junk () s;
@@ -521,7 +521,7 @@ let parse_quotation loc bp s =
       let c = Stream.next () s in
       let len =
         try ident_tail loc (store 0 c) s with
-          Stream.Failure -> raise (Stream.Error "")
+          Stream.Failure -> raise (Gramlib.Grammar.Error "")
       in
       get_buff len, set_loc_pos loc bp (Stream.count s)
   | Delimited (lenmarker, bmarker, emarker) ->
@@ -651,7 +651,7 @@ let rec next_token ~diff_mode ttree loc s =
       Stream.junk () s;
       let t, newloc =
         try parse_after_dot ~diff_mode ttree loc c bp s with
-          Stream.Failure -> raise (Stream.Error "")
+          Stream.Failure -> raise (Gramlib.Grammar.Error "")
       in
       comment_stop bp;
       (* We enforce that "." should either be part of a larger keyword,
@@ -682,7 +682,7 @@ let rec next_token ~diff_mode ttree loc s =
       Stream.junk () s;
       let len =
         try ident_tail loc (store 0 c) s with
-          Stream.Failure -> raise (Stream.Error "")
+          Stream.Failure -> raise (Gramlib.Grammar.Error "")
       in
       let id = get_buff len in
       comment_stop bp;
@@ -701,7 +701,7 @@ let rec next_token ~diff_mode ttree loc s =
       Stream.junk () s;
       let (loc, len) =
         try string loc ~comm_level:None bp 0 s with
-          Stream.Failure -> raise (Stream.Error "")
+          Stream.Failure -> raise (Gramlib.Grammar.Error "")
       in
       let ep = Stream.count s in
       comment_stop bp;
@@ -723,7 +723,7 @@ let rec next_token ~diff_mode ttree loc s =
             push_string "(*";
             let loc = comment loc bp s in next_token ~diff_mode ttree loc s
         | _ -> let t = process_chars ~diff_mode ttree loc bp [c] s in comment_stop bp; t
-      with Stream.Failure -> raise (Stream.Error "")
+      with Stream.Failure -> raise (Gramlib.Grammar.Error "")
       end
   | Some ('{' | '}' as c) ->
       Stream.junk () s;

vernac/comInductive.ml

@@ -445,7 +445,7 @@ let check_param = function
 | CLocalAssum (nas, Default _, _) -> List.iter check_named nas
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern {CAst.loc} ->
-    Loc.raise ?loc (Gramlib.Stream.Error "pattern with quote not allowed here")
+  Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
 
 let restrict_inductive_universes sigma ctx_params arities constructors =
   let merge_universes_of_constr c =
@@ -723,7 +723,7 @@ let rec count_binder_expr = function
   | CLocalAssum(l,_,_) :: rest -> List.length l + count_binder_expr rest
   | CLocalDef _ :: rest -> 1 + count_binder_expr rest
   | CLocalPattern {CAst.loc} :: _ ->
-    Loc.raise ?loc (Gramlib.Stream.Error "pattern with quote not allowed here")
+    Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed here")
 
 let interp_mutual_inductive ~env ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
   let indlocs = List.map (fun ((n,_,_,_),_) -> n.CAst.loc) indl in

vernac/himsg.ml

@@ -1556,7 +1556,7 @@ let wrap_unhandled f e =
 
 let explain_exn_default = function
   (* Basic interaction exceptions *)
-  | Gramlib.Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
+  | Gramlib.Grammar.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
   | Sys_error msg -> hov 0 (str "System error: " ++ quote (str msg))
   | Out_of_memory -> hov 0 (str "Out of memory.")

vernac/record.ml

@@ -100,7 +100,7 @@ let check_parameters_must_be_named = function
   | CLocalAssum (ls, bk, _ce) ->
     List.iter (error_parameters_must_be_named bk) ls
   | CLocalPattern {CAst.loc} ->
-    Loc.raise ?loc (Gramlib.Stream.Error "pattern with quote not allowed in record parameters")
+    Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed in record parameters")
 
 (** [DataI.t] contains the information used in record interpretation,
    it is a strict subset of [Ast.t] thus this should be