Merge pull request #879 from SkySkimmer/stream-comlex-fail

Adapt to rocq-prover/rocq#20964 (less exn driven parser)

Author: SkySkimmer

src/rocq_elpi_arg_syntax.mlg

@@ -35,9 +35,11 @@ let rec strip_square loc s =
   else Rocq_elpi_utils.of_coq_loc loc, s
 
 [%%if coq = "8.20" || coq = "9.0" || coq = "9.1"]
-let streamFail = Gramlib.Stream.Failure
+let streamOk x = x
+let streamFail () = raise Gramlib.Stream.Failure
 [%%else]
-let streamFail = Procq.StreamFail
+let streamOk x = Ok x
+let streamFail () = Error ()
 [%%endif]
 }
 
@@ -78,8 +80,9 @@ let any_qname kwstate strm =
           else
             the_qname := sym
       | _ -> the_qname := sym
-      end
-  | _ -> raise streamFail
+      end;
+      streamOk ()
+  | _ -> streamFail ()
 let any_qname = Pcoq.Entry.(of_parser "any_qname" { parser_fun = any_qname })
 
 }
@@ -205,8 +208,8 @@ let opt2list = function None -> [] | Some l -> l
 
 let any_kwd kwstate strm =
   match LStream.peek kwstate strm with
-  | Some (Tok.KEYWORD sym) when sym <> "." -> LStream.junk kwstate strm; sym
-  | _ -> raise streamFail
+  | Some (Tok.KEYWORD sym) when sym <> "." -> LStream.junk kwstate strm; streamOk sym
+  | _ -> streamFail ()
 let any_kwd = Pcoq.Entry.(of_parser "any_symbols_or_kwd" { parser_fun = any_kwd })
 
 let pr_attributes _ _ _ atts =

src/rocq_elpi_utils.ml

@@ -78,6 +78,12 @@ let patch_loc_source execution_loc error_loc msg =
       (* external file *)
       Pp.(hv 0 (Loc.pr elpiloc ++ spc () ++ msg)), execution_loc
 
+[%%if coq = "8.20" || coq = "9.0" || coq = "9.1"]
+exception ParseError = Gramlib.Grammar.Error
+[%%else]
+exception ParseError = Gramlib.Grammar.ParseError
+[%%endif]
+
 let handle_elpi_compiler_errors ~loc ?error_header f =
   let w_header m =
     match error_header with
@@ -95,7 +101,7 @@ let handle_elpi_compiler_errors ~loc ?error_header f =
     let _,info = Exninfo.capture e in
     let msg, loc = patch_loc_source loc (Some (to_coq_loc oloc)) (Pp.str msg) in
     CErrors.user_err ~info ~loc (w_header msg)
-  | Gramlib.Grammar.Error _ as e ->
+  | ParseError _ as e ->
     let _,info = Exninfo.capture e in
     let cloc = Loc.get_loc info in
     let msg = CErrors.print_no_report e in

src/rocq_elpi_vernacular.ml

@@ -26,6 +26,12 @@ let main_interp_qedc = ET.Constants.declare_global_symbol "main-interp-qed"
 let main_synterpc = ET.Constants.declare_global_symbol "main-synterp"
 let attributesc = ET.Constants.declare_global_symbol "attributes"
 
+[%%if coq = "8.20" || coq = "9.0" || coq = "9.1"]
+exception ParseError = Gramlib.Grammar.Error
+[%%else]
+exception ParseError = Gramlib.Grammar.ParseError
+[%%endif]
+
 let atts2impl ~depth loc phase
  state atts q =
   let open Rocq_elpi_builtins_synterp in
@@ -52,7 +58,7 @@ let atts2impl ~depth loc phase
         match Pcoq.parse_string (Pvernac.main_entry None) (Printf.sprintf "#[%s] Qed." txt) |> Option.map (fun x -> x.CAst.v) with
         | None -> atts
         | Some { Vernacexpr.attrs ; _ } -> List.map (fun {CAst.v=(name,v)} -> convert_att_r ("elpi."^name,v)) attrs @ atts
-        | exception Gramlib.Grammar.Error msg ->
+        | exception ParseError msg ->
             CErrors.user_err Pp.(str"Environment variable COQ_ELPI_ATTRIBUTES contains ill formed value:" ++ spc () ++ str txt ++ cut () ++ str msg) in
   let state, atts, _ = EU.map_acc (Rocq_elpi_builtins_synterp.attribute.API.Conversion.embed ~depth) state atts in
   let atts = ET.mkApp attributesc (EU.list_to_lp_list atts) [] in

src/rocq_elpi_vernacular_syntax.mlg

@@ -91,9 +91,9 @@ let lookahead_lib_colon kwstate strm =
   match Gramlib.LStream.peek_nth kwstate 0 strm with
   | Some (Tok.IDENT "lib") ->
       (match Gramlib.LStream.peek_nth kwstate 1 strm with
-      | Some (Tok.KEYWORD ":") -> ()
-      | _ -> raise streamFail)
-  | _ -> raise streamFail
+      | Some (Tok.KEYWORD ":") -> streamOk ()
+      | _ -> streamFail ())
+  | _ -> streamFail ()
 [%%endif]
 
 [%%if coq = "8.20"]