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, 97 insertions, 0 deletions

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