From ef6c99e0e2e55b9fe316cc14663df161ebf4a21e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sun, 24 Mar 2019 22:06:44 +0100
Subject: Improve coqpp error message for SELF in anonymous entry

Something like "("; [ s = SELF -> { s } ]; ")" in a GRAMMAR EXTEND in
a mlg file was causing an error message such as

OCAMLOPT  f.ml
File "f.mlg", line 179, characters 55-67:  # not in a semantic rule so line doesn't match anything in the mlg file
Error: This expression has type ('a, Extend.mayrec, 'a) Extend.symbol
       but an expression was expected of type
         ('a, Extend.norec, 'b) Extend.symbol
       Type Extend.mayrec is not compatible with type Extend.norec

It is now

COQPP   f.mlg
Error: 'SELF' or 'NEXT' illegal in anonymous entry level
---
 coqpp/coqpp_main.ml | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8657d315f5..baa6c2d64e 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -161,29 +161,33 @@ let is_token s = match string_split s with
 | [s] -> is_uident s
 | _ -> false
 
-let rec parse_tokens = function
+let rec parse_tokens ?(in_anon=false) =
+let err_anon () =
+  if in_anon then
+    fatal (Printf.sprintf "'SELF' or 'NEXT' illegal in anonymous entry level") in
+function
 | [GSymbString s] -> SymbToken ("", Some s)
 | [GSymbQualid ("QUOTATION", None); GSymbString s] ->
     SymbToken ("QUOTATION", Some s)
-| [GSymbQualid ("SELF", None)] -> SymbSelf
-| [GSymbQualid ("NEXT", None)] -> SymbNext
+| [GSymbQualid ("SELF", None)] -> err_anon (); SymbSelf
+| [GSymbQualid ("NEXT", None)] -> err_anon (); SymbNext
 | [GSymbQualid ("LIST0", None); tkn] ->
-  SymbList0 (parse_token tkn, None)
+  SymbList0 (parse_token ~in_anon tkn, None)
 | [GSymbQualid ("LIST1", None); tkn] ->
-  SymbList1 (parse_token tkn, None)
+  SymbList1 (parse_token ~in_anon tkn, None)
 | [GSymbQualid ("LIST0", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
-  SymbList0 (parse_token tkn, Some (parse_token tkn'))
+  SymbList0 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn'))
 | [GSymbQualid ("LIST1", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
-  SymbList1 (parse_token tkn, Some (parse_token tkn'))
+  SymbList1 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn'))
 | [GSymbQualid ("OPT", None); tkn] ->
-  SymbOpt (parse_token tkn)
+  SymbOpt (parse_token ~in_anon tkn)
 | [GSymbQualid (e, None)] when is_token e -> SymbToken (e, None)
 | [GSymbQualid (e, None); GSymbString s] when is_token e -> SymbToken (e, Some s)
 | [GSymbQualid (e, lvl)] when not (is_token e) -> SymbEntry (e, lvl)
-| [GSymbParen tkns] -> parse_tokens tkns
+| [GSymbParen tkns] -> parse_tokens ~in_anon tkns
 | [GSymbProd prds] ->
   let map p =
-    let map (pat, tkns) = (pat, parse_tokens tkns) in
+    let map (pat, tkns) = (pat, parse_tokens ~in_anon:true tkns) in
     (List.map map p.gprod_symbs, p.gprod_body)
   in
   SymbRules (List.map map prds)
@@ -199,7 +203,7 @@ let rec parse_tokens = function
   in
   fatal (Printf.sprintf "Invalid token: %s" (db_tokens t))
 
-and parse_token tkn = parse_tokens [tkn]
+and parse_token ~in_anon tkn = parse_tokens ~in_anon [tkn]
 
 let print_fun fmt (vars, body) =
   let vars = List.rev vars in
-- 
cgit v1.2.3