Support for recognizing string constants tokens in notations.

We follow the same principle as numbers:
- string constants can be used as part of notations
- if parsing articulation points, string constants can be set as keywords

Note that isolated double quotes, as in ``Notation "a "" b" := ...''
are (still) not permitted (they would be considered as the start of an
unterminated string by the lexer).

interp/constrextern.ml

@@ -263,15 +263,18 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
         mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
     | _ ->
         match decompose_notation_key ntn, l with
+        | (InConstrEntry,[Terminal x]), [] ->
+           begin match String.unquote_coq_string x with
+           | Some s -> mkprim (loc, String s)
+           | None ->
+           match NumTok.Unsigned.parse_string x with
+           | Some n -> mkprim (loc, Number (NumTok.SPlus,n))
+           | None -> mknot (loc,ntn,l,bl) end
         | (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
            | Some n -> mkprim (loc, Number (NumTok.SMinus,n))
            | None -> mknot (loc,ntn,l,bl) end
-        | (InConstrEntry,[Terminal x]), [] ->
-           begin match NumTok.Unsigned.parse_string x with
-           | Some n -> mkprim (loc, Number (NumTok.SPlus,n))
-           | None -> mknot (loc,ntn,l,bl) end
-        | _ -> mknot (loc,ntn,l,bl)
+         | _ -> mknot (loc,ntn,l,bl)
 
 let make_notation loc (inscope,ntn) (terms,termlists,binders,binderlists as subst) =
   if not (List.is_empty termlists) || not (List.is_empty binderlists) then

interp/notation.ml

@@ -1412,7 +1412,7 @@ let find_notation ntn sc =
 let notation_of_prim_token = function
   | Constrexpr.Number (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
   | Constrexpr.Number (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
-  | String _ -> raise Not_found
+  | String s -> InConstrEntry, String.quote_coq_string s
 
 let find_prim_token check_allowed ?loc p sc =
   (* Try for a user-defined numerical notation *)
@@ -1979,9 +1979,19 @@ let make_notation_key from symbols =
 
 let decompose_notation_pure_key s =
   let len = String.length s in
+  let rec find_string_end n =
+    let next =
+      try String.index_from s (n+1) '"'
+      with Not_found -> assert false
+    in
+    if next = len - 1 then next+1
+    else if s.[next+1] = '"' then (* skip doubled double quotes: *) find_string_end (n+2)
+    else next+1 in
   let rec decomp_ntn dirs n =
     if n>=len then List.rev dirs else
     let pos =
+      if s.[n] = '"' then find_string_end n
+      else
       try
         String.index_from s n ' '
       with Not_found -> len
@@ -2103,18 +2113,30 @@ let split_notation_string str =
     if i < String.length str then
       if str.[i] == ' ' then
         push_token beg i (loop_on_whitespace (i+1) (i+1))
+      else if beg = i && str.[i] = '"' then
+        loop_on_string i (i+1)
       else
         loop beg (i+1)
     else
       push_token beg i []
   and loop_on_whitespace beg i =
     if i < String.length str then
       if str.[i] != ' ' then
-        push_whitespace beg i (loop i (i+1))
+        push_whitespace beg i (loop i i)
       else
         loop_on_whitespace beg (i+1)
     else
       push_whitespace beg i []
+  and loop_on_string beg i =
+    if i < String.length str then
+      if str.[i] = '"' then
+        if i+1 < String.length str then
+          if str.[i+1] = '"' then loop_on_string beg (i+2)
+          else if str.[i+1] = ' ' then push_token beg (i+1) (loop_on_whitespace (i+2) (i+2))
+          else user_err (Pp.str "End of string not followed by a space in notation.")
+        else push_token beg (i+1) []
+      else loop_on_string beg (i+1)
+    else user_err (Pp.str "Unterminated string in notation.")
   in
   loop 0 0
 

parsing/cLexer.ml

@@ -232,7 +232,7 @@ let unlocated f x =
 
 let check_keyword str =
   let rec loop_symb s = match Stream.peek s with
-    | Some (' ' | '\n' | '\r' | '\t' | '"') ->
+    | Some (' ' | '\n' | '\r' | '\t') ->
         Stream.junk s;
         bad_token str
     | _ ->
@@ -727,7 +727,10 @@ let rec next_token ~diff_mode loc s =
       in
       let ep = Stream.count s in
       comment_stop bp;
-      (STRING (get_buff len), set_loc_pos loc bp ep)
+      let str = get_buff len in
+      begin try find_keyword loc (CString.quote_coq_string str) bp s
+      with Not_found ->
+      (STRING str, set_loc_pos loc bp ep) end
   | Some ('(' as c) ->
       Stream.junk s;
       begin try

parsing/g_constr.mlg

@@ -188,6 +188,7 @@ GRAMMAR EXTEND Gram
       | id = ident; i = univ_annot ->
         { CAst.make ~loc @@ CRef (qualid_of_ident ~loc id, i) }
       | n = NUMBER-> { CAst.make ~loc @@ CPrim (Number (NumTok.SPlus,n)) }
+      | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "("; c = term LEVEL "200"; ")" ->
         { (* Preserve parentheses around numbers so that constrintern does not
              collapse -(3) into the number -3. *)
@@ -274,7 +275,6 @@ GRAMMAR EXTEND Gram
   ;
   atomic_constr:
     [ [ s = sort   -> { CAst.make ~loc @@ CSort s }
-      | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
       | "?"; "["; id = identref; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id.CAst.v, None) }
       | "?"; "["; id = pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroFresh id.CAst.v, None) }

parsing/tok.ml

@@ -144,7 +144,10 @@ let match_pattern (type c) (p : c p) : t -> c =
   let err () = raise Gramlib.Stream.Failure in
   let seq = string_equal in
   match p with
-  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMBER n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ())
+  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s'
+                          | NUMBER n when seq s (NumTok.Unsigned.sprint n) -> s
+                          | STRING s' when seq s (CString.quote_coq_string s') -> s
+                          | _ -> err ())
   | PIDENT None -> (function IDENT s' -> s' | _ -> err ())
   | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ())
   | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ())

test-suite/output/NotationSyntax.out

@@ -11,10 +11,32 @@ File "./output/NotationSyntax.v", line 5, characters 33-43:
 Warning: The format modifier is irrelevant for only-parsing rules.
 [irrelevant-format-only-parsing,parsing]
 File "./output/NotationSyntax.v", line 8, characters 20-30:
-Warning: Notations for numbers are primitive; skipping this modifier.
+Warning:
+Notations for numbers or strings are primitive; skipping this modifier.
 [primitive-token-modifier,parsing]
 1%nat
      : nat
 File "./output/NotationSyntax.v", line 10, characters 23-26:
 The command has indeed failed with message:
-Notations for numbers are primitive and need not be reserved.
+Notations for numbers or strings are primitive and need not be reserved.
+File "./output/NotationSyntax.v", line 12, characters 25-35:
+Warning:
+Notations for numbers or strings are primitive; skipping this modifier.
+[primitive-token-modifier,parsing]
+"tt"
+     : unit
+"tt"%string
+     : string
+File "./output/NotationSyntax.v", line 16, characters 23-31:
+The command has indeed failed with message:
+Notations for numbers or strings are primitive and need not be reserved.
+"t""t"
+     : unit
+"|" true
+     : option bool
+"|"%string
+     : string
+2 "|" 4
+     : nat * nat
+"I'm true"
+     : bool

test-suite/output/NotationSyntax.v

@@ -8,3 +8,33 @@ Notation "#" := 0 (only parsing, format "#").
 Notation "1" := tt (at level 3).
 Check 1%nat.
 Fail Reserved Notation "1".
+
+Notation """tt""" := tt (at level 2).
+Check "tt".
+Require Import String.
+Check "tt"%string.
+Fail Reserved Notation """tt""".
+
+(* Test string literals themselves with double quotes *)
+Notation """t""""t""" := tt.
+Check "t""t".
+
+Module A.
+
+(* Not forced to be a keyword *)
+Notation "# ""|"" a" := (Some a) (at level 0).
+Check # "|" true.
+Check "|"%string.
+
+(* Now forced to be a keyword *)
+Notation "a ""|"" b" := (a, b) (at level 50).
+Check 2 "|" 4.
+
+End A.
+
+Module B.
+
+Notation " ""I'm true"" " := true.
+Check "I'm true".
+
+End B.

vernac/egramcoq.ml

@@ -335,6 +335,9 @@ let make_pattern (keyword,s) =
    if keyword then TPattern (Tok.PKEYWORD s) else
      match NumTok.Unsigned.parse_string s with
      | Some n -> TPattern (Tok.PNUMBER (Some n))
+     | None ->
+     match String.unquote_coq_string s with
+     | Some s -> TPattern (Tok.PSTRING (Some s))
      | None -> TPattern (Tok.PIDENT (Some s))
 
 let make_sep_rules tkl =

vernac/metasyntax.ml

@@ -244,12 +244,13 @@ let quote_notation_token x =
   if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
   else x
 
-let is_numeral_in_constr entry symbs =
+let is_prim_token_constant_in_constr entry symbs =
   match entry, List.filter (function Break _ -> false | _ -> true) symbs with
-  | InConstrEntry, ([Terminal "-"; Terminal x] | [Terminal x]) ->
-      NumTok.Unsigned.parse_string x <> None
-  | _ ->
-      false
+  (* Is this a numeral? *)
+  | InConstrEntry, ([Terminal "-"; Terminal x] | [Terminal x]) when NumTok.Unsigned.parse_string x <> None -> true
+  (* Is this a string constant? *)
+  | InConstrEntry, [Terminal x] when let n = String.length x in n > 1 && x.[0] = '"' && x.[n-1] = '"' -> true
+  | _ -> false
 
 let analyze_notation_tokens ~onlyprinting ~infix entry df =
   let df = if infix then quote_notation_token df else df in
@@ -261,8 +262,8 @@ let analyze_notation_tokens ~onlyprinting ~infix entry df =
         user_err
           (str "Variable " ++ Id.print id ++ str " occurs more than once.")
     | _ -> ());
-  let isnumeral = is_numeral_in_constr entry symbols in
-  res, isnumeral
+  let is_prim_token = is_prim_token_constant_in_constr entry symbols in
+  res, is_prim_token
 
 let adjust_symbols vars notation_symbols =
   let x = Namegen.next_ident_away (Id.of_string "x") vars in
@@ -289,7 +290,7 @@ let adjust_infix_notation df notation_symbols c =
 
 let warn_unexpected_primitive_token_modifier =
   CWarnings.create ~name:"primitive-token-modifier" ~category:"parsing"
-         (fun () -> str "Notations for numbers are primitive; skipping this modifier.")
+         (fun () -> str "Notations for numbers or strings are primitive; skipping this modifier.")
 
 let check_no_syntax_modifiers_for_numeral = function
   | [] -> ()
@@ -709,6 +710,12 @@ let keyword_needed need s =
     if need then
       Flags.if_verbose Feedback.msg_info (str "Number '" ++ NumTok.Unsigned.print n ++ str "' now a keyword");
     need
+  | None ->
+  match String.unquote_coq_string s with
+  | Some _ ->
+    if need then
+      Flags.if_verbose Feedback.msg_info (str "String '" ++ str s ++ str "' now a keyword");
+    need
   | _ -> true
 
 let make_production (_,lev,_) etyps symbols =
@@ -1720,10 +1727,10 @@ let add_reserved_notation ~local ~infix ({CAst.loc;v=df},mods) =
   let open SynData in
   let (main_data,mods) = interp_non_syntax_modifiers ~reserved:true ~infix ~abbrev:false None mods in
   let mods = interp_modifiers main_data.entry mods in
-  let notation_symbols, isnumeral = analyze_notation_tokens ~onlyprinting:main_data.onlyprinting ~infix main_data.entry df in
+  let notation_symbols, is_prim_token = analyze_notation_tokens ~onlyprinting:main_data.onlyprinting ~infix main_data.entry df in
   let notation_symbols = if infix then adjust_reserved_infix_notation notation_symbols else notation_symbols in
   let ntn = make_notation_key main_data.entry notation_symbols.symbols in
-  if isnumeral then user_err ?loc (str "Notations for numbers are primitive and need not be reserved.");
+  if is_prim_token then user_err ?loc (str "Notations for numbers or strings are primitive and need not be reserved.");
   let sd = compute_syntax_data ~local main_data notation_symbols ntn mods in
   let synext = make_syntax_rules true main_data ntn sd in
   List.iter (fun f -> f ()) sd.msgs;
@@ -1745,10 +1752,10 @@ let prepare_where_notation ntn_decl =
   match mods with
   | _::_ -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here.")
   | [] ->
-    let notation_symbols, isnumeral = analyze_notation_tokens ~onlyprinting:main_data.onlyprinting ~infix:false main_data.entry df in
+    let notation_symbols, is_prim_token = analyze_notation_tokens ~onlyprinting:main_data.onlyprinting ~infix:false main_data.entry df in
     let ntn = make_notation_key main_data.entry notation_symbols.symbols in
     let syntax_rules =
-      if isnumeral then PrimTokenSyntax else
+      if is_prim_token then PrimTokenSyntax else
       try SpecificSyntax (recover_notation_syntax ntn)
       with NoSyntaxRule ->
         user_err Pp.(str "Parsing rule for this notation has to be previously declared.") in
@@ -1772,12 +1779,12 @@ let build_notation_syntax ~local ~infix deprecation ntn_decl =
   (* Extract the modifiers not affecting the parsing rule *)
   let (main_data,syntax_modifiers) = interp_non_syntax_modifiers ~reserved:false ~infix ~abbrev:false deprecation modifiers in
   (* Extract the modifiers not affecting the parsing rule *)
-  let notation_symbols, isnumeral = analyze_notation_tokens ~onlyprinting:main_data.onlyprinting ~infix main_data.entry df in
+  let notation_symbols, is_prim_token = analyze_notation_tokens ~onlyprinting:main_data.onlyprinting ~infix main_data.entry df in
   (* Add variables on both sides if an infix notation *)
   let df, notation_symbols, c = if infix then adjust_infix_notation df notation_symbols c else df, notation_symbols, c in
   (* Build the canonical identifier of the syntactic part of the notation *)
   let ntn = make_notation_key main_data.entry notation_symbols.symbols in
-  let syntax_rules = if isnumeral then (check_no_syntax_modifiers_for_numeral syntax_modifiers; PrimTokenSyntax) else
+  let syntax_rules = if is_prim_token then (check_no_syntax_modifiers_for_numeral syntax_modifiers; PrimTokenSyntax) else
   match syntax_modifiers with
   | [] ->
     (* No syntax data: try to rely on a previously declared rule *)