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

1 files changed, 0 insertions, 81 deletions

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 }