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 --- vernac/explainErr.ml | 4 +++- vernac/himsg.ml | 6 +++--- vernac/himsg.mli | 2 +- 3 files changed, 7 insertions(+), 5 deletions(-) (limited to 'vernac') diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index befb4d7ccf..b238c96913 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -65,7 +65,9 @@ let process_vernac_interp_error exn = match fst exn with | PretypeError(ctx,sigma,te) -> wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) | Notation.NumeralNotationError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te) + wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "numeral" ctx sigma te) + | Notation.StringNotationError(ctx,sigma,te) -> + wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "string" ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 6c7117b513..bf3bd70f09 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1326,12 +1326,12 @@ let explain_reduction_tactic_error = function spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' (Evd.from_env env') e -let explain_numeral_notation_error env sigma = function +let explain_numeral_or_string_notation_error numeral_or_string env sigma = function | Notation.UnexpectedTerm c -> (strbrk "Unexpected term " ++ pr_constr_env env sigma c ++ - strbrk " while parsing a numeral notation.") + strbrk (" while parsing a "^numeral_or_string^" notation.")) | Notation.UnexpectedNonOptionTerm c -> (strbrk "Unexpected non-option term " ++ pr_constr_env env sigma c ++ - strbrk " while parsing a numeral notation.") + strbrk (" while parsing a "^numeral_or_string^" notation.")) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index db05aaa125..ecb69bef1e 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -47,4 +47,4 @@ val explain_module_internalization_error : val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error -val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t +val explain_numeral_or_string_notation_error : string -> env -> Evd.evar_map -> Notation.numeral_or_string_notation_error -> Pp.t -- 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 --- vernac/explainErr.ml | 6 ++---- vernac/himsg.ml | 6 +++--- vernac/himsg.mli | 2 +- 3 files changed, 6 insertions(+), 8 deletions(-) (limited to 'vernac') diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index b238c96913..e1496e58d7 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -64,10 +64,8 @@ let process_vernac_interp_error exn = match fst exn with wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) - | Notation.NumeralNotationError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "numeral" ctx sigma te) - | Notation.StringNotationError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_numeral_or_string_notation_error "string" ctx sigma te) + | Notation.PrimTokenNotationError(kind,ctx,sigma,te) -> + wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index bf3bd70f09..436f7dce37 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1326,12 +1326,12 @@ let explain_reduction_tactic_error = function spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' (Evd.from_env env') e -let explain_numeral_or_string_notation_error numeral_or_string env sigma = function +let explain_prim_token_notation_error kind env sigma = function | Notation.UnexpectedTerm c -> (strbrk "Unexpected term " ++ pr_constr_env env sigma c ++ - strbrk (" while parsing a "^numeral_or_string^" notation.")) + strbrk (" while parsing a "^kind^" notation.")) | Notation.UnexpectedNonOptionTerm c -> (strbrk "Unexpected non-option term " ++ pr_constr_env env sigma c ++ - strbrk (" while parsing a "^numeral_or_string^" notation.")) + strbrk (" while parsing a "^kind^" notation.")) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index ecb69bef1e..bab66b2af4 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -47,4 +47,4 @@ val explain_module_internalization_error : val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error -val explain_numeral_or_string_notation_error : string -> env -> Evd.evar_map -> Notation.numeral_or_string_notation_error -> Pp.t +val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t -- cgit v1.2.3