[asl][reference] added a lexical rule for double underscores

asllib/doc/ASLmacros.tex

@@ -158,8 +158,6 @@
 \newcommand\AllApplyCase[1]{All of the following apply (\textsc{#1}):}
 \newcommand\OneApplies[0]{One of the following applies:}
 \newcommand\Proseeqdef[2]{define #1 as #2}
-\newcommand\RequirementDef[1]{\paragraph{R\_#1\label{Requirement.#1}}}
-\newcommand\RequirementRef[1]{\nameref{Requirement.#1}}
 
 \usepackage{enumitem}
 \renewlist{itemize}{itemize}{20}
@@ -227,19 +225,25 @@
 % Typesetting macros
 \newtheorem{definition}{Definition}
 \newtheorem{example}{Example}
+\newcommand\ConventionDef[1]{\paragraph{Convention.#1:\label{sec:Convention.#1}}}
+\newcommand\RequirementDef[1]{\paragraph{Requirement.#1\label{Requirement.#1}}}
+\newcommand\LexicalRuleDef[1]{\subsubsection{LexicalRule.#1\label{sec:LexicalRule.#1}}}
+\newcommand\ASTRuleDef[1]{\subsubsection{ASTRule.#1\label{sec:ASTRule.#1}}}
 \newcommand\TypingRuleDef[1]{\subsubsection{TypingRule.#1\label{sec:TypingRule.#1}}}
 \newcommand\SemanticsRuleDef[1]{\subsubsection{SemanticsRule.#1\label{sec:SemanticsRule.#1}}}
-\newcommand\ASTRuleDef[1]{\subsubsection{ASTRule.#1\label{sec:ASTRule.#1}}}
 \newcommand\listingref[1]{Listing~\ref{listing:#1}}
 \newcommand\taref[1]{Table.~\ref{ta:#1}}
 \newcommand\defref[1]{Definition~\ref{def:#1}}
 \newcommand\secref[1]{Section~\ref{sec:#1}}
 \newcommand\chapref[1]{Chapter~\ref{chap:#1}}
 \newcommand\partref[1]{Part~\ref{part:#1}}
 \newcommand\appendixref[1]{Appendix~\ref{appendix:#1}}
-\newcommand\SemanticsRuleRef[1]{\nameref{sec:SemanticsRule.#1}}
-\newcommand\TypingRuleRef[1]{\nameref{sec:TypingRule.#1}}
 \newcommand\ASTRuleRef[1]{\nameref{sec:ASTRule.#1}}
+\newcommand\ConventionRef[1]{\nameref{sec:Convention.#1}}
+\newcommand\RequirementRef[1]{\nameref{Requirement.#1}}
+\newcommand\LexicalRuleRef[1]{\nameref{sec:LexicalRule.#1}}
+\newcommand\TypingRuleRef[1]{\nameref{sec:TypingRule.#1}}
+\newcommand\SemanticsRuleRef[1]{\nameref{sec:SemanticsRule.#1}}
 \newcommand\secreflink[1]{\small\nameref{sec:#1}}
 \newcommand\prosesection[0]{\subsubsection{Prose}}
 \newcommand\ie{i.\,e.}

asllib/doc/LexicalStructure.tex

@@ -189,12 +189,7 @@ \section{String Literals}
 
 \section{Identifiers}
 Identifiers start with a letter or underscore and continue with zero or more letters, underscores or digits.
-Identifiers are case sensitive. To improve readability, it is recommended to avoid the use of identifiers that differ
-only by the case of some characters.
-
-By convention, identifiers that begin with double-underscore are reserved for use in the implementation and should
-not be used in specifications.
-
+Identifiers are case sensitive.
 \hypertarget{def-reletter}{}
 \hypertarget{def-reidentifier}{}
 \begin{center}
@@ -204,7 +199,19 @@ \section{Identifiers}
 \end{tabular}
 \end{center}
 
-% An enumeration literal is also classed as a literal constant, but is syntactically an identifier.
+\RequirementDef{ReservedIdentifiers}
+Identifiers that begin with double-underscore are reserved for use in the implementation and should
+not be used in specifications (see \LexicalRuleRef{ReservedIdentifiers}).
+
+\ConventionDef{IdentifiersDifferingByCase}
+To improve readability, it is recommended to avoid the use of identifiers that differ
+only by the case of some characters.
+
+\ConventionDef{SingleUnderscore}
+Any identifier with a single underscore followed by an alphanumeric character
+is treated as a normal identifier. We recommend that these are only
+for use by platform-specific code, which should not clash with the rest of a
+portable ASL specification.
 
 Tuple element selectors are classed as identifiers. That is, in cases like \texttt{(1, 2).item0},
 the selector \texttt{item0} is classed as an identifier.
@@ -418,8 +425,6 @@ \subsection{Scanning Regular Tokens}
 \item The function $\tokenid(s)$ returns $\Tlexeme(s)$.
 \hypertarget{def-lexicalerror}{}
 \item The function $\lexicalerror$ returns $\Terror$.
-\hypertarget{def-toidentifier}{}
-\item The function $\toidentifier(s)$ returns $\Tidentifier(s)$.
 \hypertarget{def-eoftoken}{}
 \item The lexeme action
 \[
@@ -431,6 +436,26 @@ \subsection{Scanning Regular Tokens}
 checks whether $\eof$ is not followed by more characters and returns a lexical error otherwise.
 \end{itemize}
 
+\LexicalRuleDef{ReservedIdentifiers}
+\hypertarget{def-toidentifier}{}
+The function $\toidentifier(s)$ checks whether $s$ is a legal identifier
+and if so returns $\Tidentifier(s)$. Otherwise, the result is a lexical error.
+
+\ProseParagraph
+Given a string $s$, $\toidentifier(s)$ checks whether $s$ starts with a double
+underscore. If so, the result is a lexical error. Otherwise the result is
+$\Tidentifier(s)$.
+
+\FormallyParagraph
+\[
+  \toidentifier(s) = \begin{cases}
+    \LexicalError & \text{if }s = \underbracket{\texttt{ \_ } }\ \underbracket{\texttt{ \_ } } s'\\
+    \Tidentifier(s) & \text{else}
+  \end{cases}
+\]
+
+\subsection{Regular Tokens Tables}
+
 \hypertarget{def-spectoken}{}
 The lexical specification  $\spectoken$ is given by the following four tables.
 Splitting the lexical specification into four tables is done for presentation purposes ---