From 5285b3a829222b66cc6f5c282927158d875e9493 Mon Sep 17 00:00:00 2001 From: Roman-Manevich Date: Fri, 24 Jan 2025 17:46:54 +0000 Subject: [PATCH] [asl][reference] added a lexical rule for double underscores --- asllib/doc/ASLmacros.tex | 14 +++++++---- asllib/doc/LexicalStructure.tex | 43 ++++++++++++++++++++++++++------- 2 files changed, 43 insertions(+), 14 deletions(-) diff --git a/asllib/doc/ASLmacros.tex b/asllib/doc/ASLmacros.tex index 78d716693..97bae9537 100644 --- a/asllib/doc/ASLmacros.tex +++ b/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,9 +225,12 @@ % 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}} @@ -237,9 +238,12 @@ \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.} diff --git a/asllib/doc/LexicalStructure.tex b/asllib/doc/LexicalStructure.tex index ee9eeff45..071888589 100644 --- a/asllib/doc/LexicalStructure.tex +++ b/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 ---