From e2c4d3ad72b85f1fb1ea1a7c42aff0831eff3c30 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 25 Sep 2018 12:54:16 +0200 Subject: Documentation of the rules for printing notations depending on scopes. Mostly courtesy of Jason Gross. --- doc/sphinx/user-extensions/syntax-extensions.rst | 40 ++++++++++++++++++++++++ 1 file changed, 40 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 1c53f5981d..66fa3af052 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1040,6 +1040,8 @@ interpreted in the scope stack extended with the scope bound tokey. To remove a delimiting key of a scope, use the command :n:`Undelimit Scope @scope` +.. _ArgumentScopes: + Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1307,6 +1309,44 @@ Displaying information about scopes It also displays the delimiting key if any and the class to which the scope is bound, if any. +Impact of scopes on printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When several notations are available for printing the same expression, +Coq will use the following rules for printing priorities: + +- If two notations are available in different scopes which are open, + the notation in the more recently opened scope takes precedence. + +- If two notations are available in the same scope, the more recently + defined (or imported) notation takes precedence. + +- Abbreviations and lonely notations, both of which have no scope, + take precedence over a notation in an open scope if and only if the + abbreviation or lonely notation was defined (or imported) more + recently than when the corresponding scope was open. They take + precedence over any notation not in an open scope, whether this scope + has a delimiter or not. + +- A scope is *active* for printing a term either because it was opened + with :cmd:`Open Scope`, or the term is the immediate argument of a + constant which temporarily opens a scope for this argument (see + :ref:`Arguments `) in which case this temporary + scope is the most recent open one. + +- In case no abbreviation, nor lonely notation, nor notation in an + explicitly open scope, nor notation in a temporarily open scope of + arguments, has been found, notations in those closed scopes which + have a delimiter are considered. A notation is chosen and the + corresponding delimiter is inserted, making the corresponding scope + the most recent explicitly open scope for all subterms of the + current term. + +- A scope can be closed by using :cmd:`Close Scope` and its delimiter + removed by using :cmd:`Undelimit Scope`. To remove automatic + temporary opening of scopes for arguments of a constant, use + :ref:`Arguments `. + .. _Abbreviations: Abbreviations -- cgit v1.2.3 From 8f7c82b8a67a3c94073e55289996f02285c04914 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 15 Oct 2018 15:50:28 +0200 Subject: Printing priority to most recent notation in case of non-open scopes with delim. This modifies the strategy in previous commits so that priorities are as before in case of non-open scopes with delimiters. Additionally, we document the rare situation of overlapping applicative notations (maybe this is too rare and ad hoc to be worth being documented though). --- doc/sphinx/user-extensions/syntax-extensions.rst | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 66fa3af052..ce79e2915e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1337,10 +1337,22 @@ Coq will use the following rules for printing priorities: - In case no abbreviation, nor lonely notation, nor notation in an explicitly open scope, nor notation in a temporarily open scope of arguments, has been found, notations in those closed scopes which - have a delimiter are considered. A notation is chosen and the - corresponding delimiter is inserted, making the corresponding scope - the most recent explicitly open scope for all subterms of the - current term. + have a delimiter are considered, giving priority to the most + recently defined (or imported) ones. The corresponding delimiter is + inserted, making the corresponding scope the most recent explicitly + open scope for all subterms of the current term. + +- As a refinement of the previous rule, in the case of applied global + references, notations in a non-opened scope with delimiter + specifically defined for this applied global reference take priority + over notations in a non-opened scope with delimiter for generic + applications. For instance, in the presence of ``Notation "f ( x + )" := (f x) (at level 10, format "f ( x )") : app_scope`` and + ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") : + mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being + bound to a delimiter *and* both not opened, the latter, more + specific notation will always take precedence over the first, more + generic one. - A scope can be closed by using :cmd:`Close Scope` and its delimiter removed by using :cmd:`Undelimit Scope`. To remove automatic -- cgit v1.2.3 From 0336e86ea5ef63a587aae695adeeb4607346c337 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 31 Oct 2018 20:32:11 +0100 Subject: Giving to type_scope a softer role in printing. Namely, it does not explicitly open a scope, but we remember that we don't need the %type delimiter when in type position. --- doc/sphinx/user-extensions/syntax-extensions.rst | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ce79e2915e..a5869055fa 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1340,7 +1340,16 @@ Coq will use the following rules for printing priorities: have a delimiter are considered, giving priority to the most recently defined (or imported) ones. The corresponding delimiter is inserted, making the corresponding scope the most recent explicitly - open scope for all subterms of the current term. + open scope for all subterms of the current term. As an exception to + the insertion of the corresponding delimiter, when an expression is + statically known to be in a position expecting a type and the + notation is from scope ``type_scope``, and the latter is closed, the + delimiter is not inserted. This is because expressions statically + known to be in a position expecting a type are by default + interpreted with `type_scope` temporarily activated. Expressions + statically known to be in a position expecting a type typically + include being on the right-hand side of `:`, `<:`, `<<:` and after + the comma in a `forall` expression. - As a refinement of the previous rule, in the case of applied global references, notations in a non-opened scope with delimiter -- cgit v1.2.3