From 912eaf40d4efd29b7e3489d51c55b8b79206df79 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 Mar 2019 11:42:17 +0100
Subject: [parsing] Split Tok.t into Tok.t and Tok.pattern

Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals

Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t

Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")
---
 coqpp/coqpp_main.ml | 15 +++------------
 1 file changed, 3 insertions(+), 12 deletions(-)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 90158c3aa3..c8a87e6cb6 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -212,17 +212,9 @@ let print_fun fmt (vars, body) =
 
 (** Meta-program instead of calling Tok.of_pattern here because otherwise
     violates value restriction *)
-let print_tok fmt = function
-| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s
-| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s
-| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s
-| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s
-| "INT", s -> fprintf fmt "Tok.INT %a" print_string s
-| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s
-| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK"
-| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s
-| "EOI", _ -> fprintf fmt "Tok.EOI"
-| _ -> failwith "Tok.of_pattern: not a constructor"
+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 rec print_prod fmt p =
   let (vars, tkns) = List.split p.gprod_symbs in
@@ -240,7 +232,6 @@ and print_symbols fmt = function
 
 and print_symbol fmt tkn = match tkn with
 | SymbToken (t, s) ->
-  let s = match s with None -> "" | Some s -> s in
   fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s)
 | SymbEntry (e, None) ->
   fprintf fmt "(Extend.Aentry %s)" e
-- 
cgit v1.2.3


From 46b9e086093d66ff7a916e0475549a9cfb0b056d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 8 Mar 2019 16:16:34 +0100
Subject: [parsing] add keyword-protected generic quotation

One can now register a quotation using a grammar rule with
QUOTATION("name:"). "name:" becomes a keyword and the token is
generated for name: followed by a an identifier or a parenthesized
text. Eg

  constr:x
  string:[....]
  ltac:(....)
  ltac:{....}

The delimiter is made of 1 or more occurrences of the same parenthesis,
eg ((.....)) or [[[[....]]]]. The idea being that if the text happens to
contain the closing delimiter, one can make the delimiter longer and avoid
confusion (no escaping). Eg

  string:[[ .. ']' .. ]]


Nesting the delimiter is allowed, eg ((..((...))..)) is OK.

The text inside the quotation is returned as a string (including the
parentheses), so that a third party parser can take care of it.

Keywords don't need to end in ':'.
---
 coqpp/coqpp_main.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index c8a87e6cb6..f4c819eeb6 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -163,6 +163,8 @@ let is_token s = match string_split s with
 
 let rec parse_tokens = function
 | [GSymbString s] -> SymbToken ("", Some s)
+| [GSymbQualid ("QUOTATION", None); GSymbString s] ->
+    SymbToken ("QUOTATION", Some s)
 | [GSymbQualid ("SELF", None)] -> SymbSelf
 | [GSymbQualid ("NEXT", None)] -> SymbNext
 | [GSymbQualid ("LIST0", None); tkn] ->
-- 
cgit v1.2.3