From e30e864d61431a0145853fcf90b5f16b781f4a46 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 7 Nov 2018 21:19:05 -0500 Subject: 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 --- interp/notation.mli | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 734198bbf6..6880b9a2cd 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -104,11 +104,12 @@ val register_string_interpretation : (** * Numeral notation *) -type numeral_notation_error = +type numeral_or_string_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error +exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error type numnot_option = | Nop @@ -128,8 +129,13 @@ type target_kind = | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) +type string_target_kind = + | ListByte + | Byte + type option_kind = Option | Direct type conversion_kind = target_kind * option_kind +type string_conversion_kind = string_target_kind * option_kind type numeral_notation_obj = { to_kind : conversion_kind; @@ -139,9 +145,17 @@ type numeral_notation_obj = num_ty : Libnames.qualid; (* for warnings / error messages *) warning : numnot_option } +type string_notation_obj = + { sto_kind : string_conversion_kind; + sto_ty : GlobRef.t; + sof_kind : string_conversion_kind; + sof_ty : GlobRef.t; + string_ty : Libnames.qualid (* for warnings / error messages *) } + type prim_token_interp_info = Uid of prim_token_uid | NumeralNotation of numeral_notation_obj + | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) -- cgit v1.2.3 From f7992de2dc4ce0091197b9476779fc120a2fd9ec Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 27 Nov 2018 21:03:57 -0500 Subject: Factor out common code in numeral/string notations As per https://github.com/coq/coq/pull/8965#issuecomment-441440779 --- interp/notation.mli | 28 +++++++++++----------------- 1 file changed, 11 insertions(+), 17 deletions(-) (limited to 'interp/notation.mli') diff --git a/interp/notation.mli b/interp/notation.mli index 6880b9a2cd..c0ff1a1ac3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -104,12 +104,11 @@ val register_string_interpretation : (** * Numeral notation *) -type numeral_or_string_notation_error = +type prim_token_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error -exception StringNotationError of Environ.env * Evd.evar_map * numeral_or_string_notation_error +exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error type numnot_option = | Nop @@ -134,23 +133,18 @@ type string_target_kind = | Byte type option_kind = Option | Direct -type conversion_kind = target_kind * option_kind -type string_conversion_kind = string_target_kind * option_kind +type 'target conversion_kind = 'target * option_kind -type numeral_notation_obj = - { to_kind : conversion_kind; +type ('target, 'warning) prim_token_notation_obj = + { to_kind : 'target conversion_kind; to_ty : GlobRef.t; - of_kind : conversion_kind; + of_kind : 'target conversion_kind; of_ty : GlobRef.t; - num_ty : Libnames.qualid; (* for warnings / error messages *) - warning : numnot_option } - -type string_notation_obj = - { sto_kind : string_conversion_kind; - sto_ty : GlobRef.t; - sof_kind : string_conversion_kind; - sof_ty : GlobRef.t; - string_ty : Libnames.qualid (* for warnings / error messages *) } + ty_name : Libnames.qualid; (* for warnings / error messages *) + warning : 'warning } + +type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj +type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj type prim_token_interp_info = Uid of prim_token_uid -- cgit v1.2.3