Add `String Notation` vernacular like `Numeral Notation`

Users can now register string notations for custom inductives.

Much of the code and documentation was copied from numeral notations.

I chose to use a 256-constructor inductive for primitive string syntax
because (a) it is easy to convert between character codes and
constructors, and (b) it is more efficient than the existing `ascii`
type.

Some choices about proofs of the new `byte` type were made based on
efficiency.  For example, https://github.com/coq/coq/issues/8517 means
that we cannot simply use `Scheme Equality` for this type, and I have
taken some care to ensure that the proofs of decidable equality and
conversion are fast.  (Unfortunately, the `Init/Byte.v` file is the
slowest one in the prelude (it takes a couple of seconds to build), and
I'm not sure where the slowness is.)

In String.v, some uses of `0` as a `nat` were replaced by `O`, because
the file initially refused to check interactively otherwise (it
complained that `0` could not be interpreted in `string_scope` before
loading `Coq.Strings.String`).

There is unfortunately a decent amount of code duplication between
numeral notations and string notations.

I have not put too much thought into chosing names; most names have been
chosen to be similar to numeral notations, though I chose the name
`byte` from
https://github.com/coq/coq/issues/8483#issuecomment-421671785.

Unfortunately, this feature does not support declaring string syntax for
`list ascii`, unless that type is wrapped in a record or other inductive
type.  This is not a fundamental limitation; it should be relatively
easy for someone who knows the API of the reduction machinery in Coq to
extend both this and numeral notations to support any type whose hnf
starts with an inductive type.  (The reason for needing an inductive
type to bottom out at is that this is how the plugin determines what
constructors are the entry points for printing the given notation.
However, see also https://github.com/coq/coq/issues/8964 for
complications that are more likely to arise if inductive type families
are supported.)

N.B. I generated the long lists of constructors for the `byte` type with
short python scripts.

Closes #8853

9 files changed, 147 insertions, 198 deletions

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
deleted file mode 100644
index 94255bab6c..0000000000
--- a/plugins/syntax/ascii_syntax.ml
+++ /dev/null
@@ -1,100 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "ascii_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-open Pp
-open CErrors
-open Util
-open Names
-open Glob_term
-open Globnames
-open Coqlib
-
-exception Non_closed_ascii
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let ascii_module = ["Coq";"Strings";"Ascii"]
-let ascii_modpath = MPfile (make_dir ascii_module)
-
-let ascii_path = make_path ascii_module "ascii"
-
-let ascii_label = Label.make "ascii"
-let ascii_kn = MutInd.make2 ascii_modpath ascii_label
-let path_of_Ascii = ((ascii_kn,0),1)
-let static_glob_Ascii  = ConstructRef path_of_Ascii
-
-let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii")
-
-open Lazy
-
-let interp_ascii ?loc p =
-  let rec aux n p =
-     if Int.equal n 0 then [] else
-     let mp = p mod 2 in
-     (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None))
-     :: (aux (n-1) (p/2)) in
-  DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
-
-let interp_ascii_string ?loc s =
-  let p =
-    if Int.equal (String.length s) 1 then int_of_char s.[0]
-    else
-      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
-      then int_of_string s
-      else
-	user_err ?loc ~hdr:"interp_ascii_string"
-	 (str "Expects a single character or a three-digits ascii code.") in
-  interp_ascii ?loc p
-
-let uninterp_ascii r =
-  let rec uninterp_bool_list n = function
-    | [] when Int.equal n 0 -> 0
-    | r::l when is_gr r (lib_ref "core.bool.true")  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l)
-    | _ -> raise Non_closed_ascii in
-  try
-    let aux c = match DAst.get c with
-    | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l
-    | _ -> raise Non_closed_ascii in
-    Some (aux r)
-  with
-   Non_closed_ascii -> None
-
-let make_ascii_string n =
-  if n>=32 && n<=126 then String.make 1 (char_of_int n)
-  else Printf.sprintf "%03d" n
-
-let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let _ =
-  let sc = "char_scope" in
-  register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = sc;
-      pt_interp_info = Uid sc;
-      pt_required = (ascii_path,ascii_module);
-      pt_refs = [static_glob_Ascii];
-      pt_in_match = true }
diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack
deleted file mode 100644
index 7b9213a0e2..0000000000
--- a/plugins/syntax/ascii_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Ascii_syntax
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
new file mode 100644
index 0000000000..1e06cd8ddb
--- /dev/null
+++ b/plugins/syntax/g_string.mlg
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+DECLARE PLUGIN "string_notation_plugin"
+
+{
+
+open String_notation
+open Names
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
+  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+      ident(sc) ] ->
+    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+END
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index bfdd480fe9..1ab16c700d 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -6,6 +6,13 @@
  (libraries coq.plugins.ltac))
 
 (library
+ (name string_notation_plugin)
+ (public_name coq.plugins.string_notation)
+ (synopsis "Coq string notation plugin")
+ (modules g_string string_notation)
+ (libraries coq.vernac))
+
+(library
  (name r_syntax_plugin)
  (public_name coq.plugins.r_syntax)
  (synopsis "Coq syntax plugin: reals")
@@ -13,23 +20,8 @@
  (libraries coq.vernac))
 
 (library
- (name ascii_syntax_plugin)
- (public_name coq.plugins.ascii_syntax)
- (synopsis "Coq syntax plugin: ASCII")
- (modules ascii_syntax)
- (libraries coq.vernac))
-
-(library
- (name string_syntax_plugin)
- (public_name coq.plugins.string_syntax)
- (synopsis "Coq syntax plugin: strings")
- (modules string_syntax)
- (libraries coq.plugins.ascii_syntax))
-
-(library
  (name int31_syntax_plugin)
  (public_name coq.plugins.int31_syntax)
  (synopsis "Coq syntax plugin: int31")
  (modules int31_syntax)
  (libraries coq.vernac))
-
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
new file mode 100644
index 0000000000..fff8e928c3
--- /dev/null
+++ b/plugins/syntax/string_notation.ml
@@ -0,0 +1,97 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Globnames
+open Constrexpr
+open Constrexpr_ops
+open Notation
+
+(** * String notation *)
+
+let get_constructors ind =
+  let mib,oib = Global.lookup_inductive ind in
+  let mc = oib.Declarations.mind_consnames in
+  Array.to_list
+    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_option () = qualid_of_ref "core.option.type"
+let q_list () = qualid_of_ref "core.list.type"
+let q_byte () = qualid_of_ref "core.byte.type"
+
+let has_type f ty =
+  let (sigma, env) = Pfedit.get_current_context () in
+  let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
+  try let _ = Constrintern.interp_constr env sigma c in true
+  with Pretype_errors.PretypeError _ -> false
+
+let type_error_to f ty =
+  CErrors.user_err
+    (pr_qualid f ++ str " should go from Byte.byte or (list Byte.byte) to " ++
+     pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ").")
+
+let type_error_of g ty =
+  CErrors.user_err
+    (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
+     str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
+
+let vernac_string_notation local ty f g scope =
+  let app x y = mkAppC (x,[y]) in
+  let cref q = mkRefC q in
+  let cbyte = cref (q_byte ()) in
+  let clist = cref (q_list ()) in
+  let coption = cref (q_option ()) in
+  let opt r = app coption r in
+  let clist_byte = app clist cbyte in
+  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let to_ty = Smartlocate.global_with_alias f in
+  let of_ty = Smartlocate.global_with_alias g in
+  let cty = cref ty in
+  let arrow x y =
+    mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+  in
+  let constructors = get_constructors tyc in
+  (* Check the type of f *)
+  let to_kind =
+    if has_type f (arrow clist_byte cty) then ListByte, Direct
+    else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option
+    else if has_type f (arrow cbyte cty) then Byte, Direct
+    else if has_type f (arrow cbyte (opt cty)) then Byte, Option
+    else type_error_to f ty
+  in
+  (* Check the type of g *)
+  let of_kind =
+    if has_type g (arrow cty clist_byte) then ListByte, Direct
+    else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option
+    else if has_type g (arrow cty cbyte) then Byte, Direct
+    else if has_type g (arrow cty (opt cbyte)) then Byte, Option
+    else type_error_of g ty
+  in
+  let o = { sto_kind = to_kind;
+            sto_ty = to_ty;
+            sof_kind = of_kind;
+            sof_ty = of_ty;
+            string_ty = ty }
+  in
+  let i =
+       { pt_local = local;
+         pt_scope = scope;
+         pt_interp_info = StringNotation o;
+         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_refs = constructors;
+         pt_in_match = true }
+  in
+  enable_prim_token_interpretation i
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
new file mode 100644
index 0000000000..9a0174abf2
--- /dev/null
+++ b/plugins/syntax/string_notation.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Libnames
+open Vernacexpr
+
+(** * String notation *)
+
+val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit
diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack
new file mode 100644
index 0000000000..6aa081dab4
--- /dev/null
+++ b/plugins/syntax/string_notation_plugin.mlpack
@@ -0,0 +1,2 @@
+String_notation
+G_string
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
deleted file mode 100644
index 59e65a0672..0000000000
--- a/plugins/syntax/string_syntax.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-open Globnames
-open Ascii_syntax_plugin.Ascii_syntax
-open Glob_term
-open Coqlib
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "string_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_string
-
-(* make a string term from the string s *)
-
-let string_module = ["Coq";"Strings";"String"]
-
-let string_modpath = MPfile (make_dir string_module)
-let string_path = make_path string_module "string"
-
-let string_kn = MutInd.make2 string_modpath @@ Label.make "string"
-let static_glob_EmptyString  = ConstructRef ((string_kn,0),1)
-let static_glob_String  = ConstructRef ((string_kn,0),2)
-
-let glob_String = lazy (lib_ref "plugins.syntax.String")
-let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString")
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-open Lazy
-
-let interp_string ?loc s =
-  let le = String.length s in
-  let rec aux n =
-     if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else
-     DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None),
-       [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
-  in aux 0
-
-let uninterp_string (AnyGlobConstr r) =
-  try
-    let b = Buffer.create 16 in
-    let rec aux c = match DAst.get c with
-    | GApp (k,[a;s]) when is_gr k (force glob_String) ->
-	(match uninterp_ascii a with
-	  | Some c -> Buffer.add_char b (Char.chr c); aux s
-	  | _ -> raise Non_closed_string)
-    | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) ->
-	Some (Buffer.contents b)
-    | _ ->
-	raise Non_closed_string
-    in aux r
-  with
-   Non_closed_string -> None
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let _ =
-  let sc = "string_scope" in
-  register_string_interpretation sc (interp_string,uninterp_string);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = sc;
-      pt_interp_info = Uid sc;
-      pt_required = (string_path,["Coq";"Strings";"String"]);
-      pt_refs = [static_glob_String; static_glob_EmptyString];
-      pt_in_match = true }
diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack
deleted file mode 100644
index 45d6e0fa23..0000000000
--- a/plugins/syntax/string_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-String_syntax