Merge PR #9815: Multiple payload types in tokens

Reviewed-by: ppedrot
Ack-by: proux01

1 files changed, 34 insertions, 18 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index f4c819eeb6..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
@@ -214,9 +218,20 @@ let print_fun fmt (vars, body) =
 
 (** Meta-program instead of calling Tok.of_pattern here because otherwise
     violates value restriction *)
-let print_tok fmt (k,o) =
-  let print_pat fmt = print_opt fmt print_string in
-  fprintf fmt "(%a,%a)" print_string k print_pat o
+let print_tok fmt =
+let print_pat fmt = print_opt fmt print_string in
+function
+| "", Some s -> fprintf fmt "Tok.PKEYWORD (%a)" print_string s
+| "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
+| "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s
+| "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
+| "INT", s -> fprintf fmt "Tok.PINT (%a)" print_pat s
+| "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
+| "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
+| "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
+| "QUOTATION", Some s -> fprintf fmt "Tok.PQUOTATION %a" print_string s
+| "EOI", None -> fprintf fmt "Tok.PEOI"
+| _ -> failwith "Tok.of_pattern: not a constructor"
 
 let rec print_prod fmt p =
   let (vars, tkns) = List.split p.gprod_symbs in
@@ -225,12 +240,13 @@ let rec print_prod fmt p =
 
 and print_extrule fmt (tkn, vars, body) =
   let tkn = List.rev tkn in
-  fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun (vars, body)
+  fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
 
-and print_symbols fmt = function
+and print_symbols ~norec fmt = function
 | [] -> fprintf fmt "Extend.Stop"
 | tkn :: tkns ->
-  fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn
+  let c = if norec then "Extend.NextNoRec" else "Extend.Next" in
+  fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn
 
 and print_symbol fmt tkn = match tkn with
 | SymbToken (t, s) ->
@@ -257,7 +273,7 @@ and print_symbol fmt tkn = match tkn with
   let pr fmt (r, body) =
     let (vars, tkn) = List.split r in
     let tkn = List.rev tkn in
-    fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body)
+    fprintf fmt "Extend.Rules @[(%a,@ (%a))@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
   in
   let pr fmt rules = print_list fmt pr rules in
   fprintf fmt "(Extend.Arules %a)" pr (List.rev rules)