Skip to content

[asl reference] use \ChapterOutline to auto-generate chapter outlines from the list of sections #1925

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Roman-Manevich wants to merge 2 commits into
base: master
Choose a base branch
from
+637 −589
Open

[asl reference] use \ChapterOutline to auto-generate chapter outlines from the list of sections #1925

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b23d8a9
[asl reference] use \ChapterOutline to automatically list sections fo…
Roman-Manevich Jul 17, 2026
00f8e71
[asl reference] addressing review comments
Roman-Manevich Aug 4, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 22 additions & 27 deletions asllib/doc/ASLFormal.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,22 +4,9 @@ \chapter{Formal System \label{chap:FormalSystem}}
reference.

\ChapterOutline
\begin{itemize}
\item \secref{Mathematical Definitions and Notations} defines general mathematical concepts and notations;
\item \secref{Inference Rules} defines the concept of \emph{inference rules};
\item \secref{Transition Judgements} explains how \emph{transition judgements} can be used to represent
relations and functions;
\item \secref{Configurations} introduces \emph{\configurationsterm{}} as a way of representing compound data;
\item \secref{FlavoursOfEqualityInRules} explains the kinds of equality notations that are used to
convey intention in inference rules;
\item \secref{ASTNotations} introduces AST-related notations that are used in inference rules;
\item \secref{How to Parse Inference Rules Efficiently} explains how to efficiently parse inference rules,
\item \secref{ShortCircuitRuleMacros} defines rule macros, which compactly represent multiple rules;
\item \secref{ConventionallyUsedJudgments} presents commonly used judgements and notations; and
\item \secref{Rule Naming} explains the naming scheme for inference rules used in this reference.
\end{itemize}

\section{Mathematical Definitions and Notations\label{sec:Mathematical Definitions and Notations}}
\SectionDef[defines general mathematical concepts and notations]
{Mathematical Definitions and Notations}{Mathematical Definitions and Notations}
\hypertarget{def-triangleq}{}
We use $\triangleq$ to define mathematical concepts.

Expand Down Expand Up @@ -514,7 +501,8 @@ \subsection{OCaml-style Notations}
\end{definition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Inference Rules\label{sec:Inference Rules}}
\SectionDef[defines the concept of \emph{inference rules}]
{Inference Rules}{Inference Rules}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hypertarget{def-inferencerule}{}
An \emph{\inferencerule} (rule, for short) is an implication between a list of judgements,
Expand Down Expand Up @@ -654,8 +642,9 @@ \section{Inference Rules\label{sec:Inference Rules}}
(see \secref{Semantics of Diverging Specifications}).
\end{definition}

\section{Transition Judgements\label{sec:Transition Judgements}}

\SectionDef[explains how \emph{transition judgements} can be used to represent
relations and functions;]
{Transition Judgements}{Transition Judgements}
We use rules as a structured way for defining relations (and therefore functions, as a special case).

To define a relation $R \subseteq X \cartimes Y$, we use judgements of the form $\termx \rulearrow \termy$
Expand All @@ -681,8 +670,8 @@ \section{Transition Judgements\label{sec:Transition Judgements}}
for a given transition.

\hypertarget{def-configuration}{}
\section{Configurations\label{sec:Configurations}}

\SectionDef[introduces \emph{\configurationsterm{}} as a way of representing compound data]
{Configurations}{Configurations}
Our relations range over compound values. That is, values that often nest tuples and lists inside other tuples and lists.
We refer to such values as \emph{\configurationsterm}. To make it easier to distinguish between different \configurationsterm{},
we will sometimes attach labels to tuples using the OCaml-style notation discussed earlier.
Expand Down Expand Up @@ -721,7 +710,9 @@ \section{Configurations\label{sec:Configurations}}
Since the rule does not need to refer to the value, we do not name it and use an ignore variable
instead.

\section{Flavours of Equality In Rules\label{sec:FlavoursOfEqualityInRules}}
\SectionDef[explains the kinds of equality notations that are used to
convey intention in inference rules;]
{FlavoursOfEqualityInRules}{Flavours of Equality In Rules}
This section explains the equality notations used in rules, two of which are used in \SemanticsRuleRef{ECond},
shown here:
\begin{mathpar}
Expand Down Expand Up @@ -794,8 +785,8 @@ \section{Flavours of Equality In Rules\label{sec:FlavoursOfEqualityInRules}}
\end{mathpar}
\end{description}

\section{AST-related Notations\label{sec:ASTNotations}}

\SectionDef[introduces AST-related notations that are used in inference rules]
{ASTNotations}{AST-related Notations}
When deconstructing AST record nodes such as $\{f_1:t_1,\ldots,f_k:t_k\}$,
we sometimes only care about a subset of the fields $\{f_{i_1},\ldots,f_{i_m}\} \subset \{f_{1..k}\}$.
In such cases, we write $\{f_{i_1}:t_{i_1},\ldots,f_{i_m}:t_{i_m},\ldots\}$,
Expand All @@ -813,7 +804,8 @@ \section{AST-related Notations\label{sec:ASTNotations}}
The partial function $\astlabel$ returns the label $\vl\in\ASTLabels$ of an AST node, when it exists.
For example, $\astlabel(\TBool) = \TBool$ and $\astlabel(\TNamed(\vx)) = \TNamed$.

\section{How to Parse Inference Rules Efficiently\label{sec:How to Parse Inference Rules Efficiently}}
\SectionDef[explains how to efficiently parse inference rules,]
{How to Parse Inference Rules Efficiently}{How to Parse Inference Rules Efficiently}
Consider the following examples, which is a simplified version of \SemanticsRuleRef{Binop}
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
Expand Down Expand Up @@ -858,7 +850,8 @@ \section{How to Parse Inference Rules Efficiently\label{sec:How to Parse Inferen
which are components of the previously assigned variables $\vmone$ and $\vmtwo$.

\hypertarget{def-shortcircuitrulemacro}{}
\section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
\SectionDef[defines rule macros, which compactly represent multiple rules]
{ShortCircuitRuleMacros}{Short-circuit Rule Macros}
\emph{\Shortcircuitrulemacros}, or \emph{rule macros}, for short, allow us to succinctly define sets of rules.
Specifically, they allow us to capture situations where
transitions have two alternative output \configurationsterm{}.
Expand Down Expand Up @@ -1066,7 +1059,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}

All these cases are succinctly encoded in a single rule with the alternative output \configurationsterm{}.

\section{Conventionally-used Judgements and Notations\label{sec:ConventionallyUsedJudgments}}
\SectionDef[presents commonly used judgements and notations; and]
{ConventionallyUsedJudgments}{Conventionally-used Judgements and Notations}
We now present functions used conventionally in this reference.

\subsection{Checked Transitions\label{sec:Checked Transitions}}
Expand Down Expand Up @@ -1157,7 +1151,8 @@ \subsection{Conventional Notations}
\hypertarget{def-wrapline}{}
The notation $\wrappedline$ denotes that a line that is longer than the page width continues on the next line.

\section{Rule Naming\label{sec:Rule Naming}}
\SectionDef[explains the naming scheme for inference rules used in this reference.]
{Rule Naming}{Rule Naming}
To name a rule, we place it in a section with its name.
However, some relations are defined by a group of rules.
In such cases, we refer to the individual rules in a group as \emph{case rules},
Expand Down
151 changes: 143 additions & 8 deletions asllib/doc/ASLmacros.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,16 +169,13 @@
% Not imported here means, it is not yet considered for auto-generation.
\newcommand\NotImportedToASLSpecYet[1]{#1}

\newcommand\ChapterOutline[0]{\paragraph{Outline} The rest of this chapter is organized as follows:}
\newcommand\FormalRelationsDef[1]{\section{Formal Relations for #1\label{sec:Formal Relations for #1}}}
\newcommand\FormalRelationsRef[1]{\secref{Formal Relations for #1}}
\newcommand\SyntaxDef[1]{\section{Syntax of #1\label{sec:Syntax of #1}}}
\newcommand\FormalRelationsDef[2][]{\SectionDef[#1]{Formal Relations for #2}{Formal Relations for #2}}
\newcommand\SyntaxDef[2][]{\SectionDef[#1]{Syntax of #2}{Syntax of #2}}
\newcommand\SyntaxRef[1]{\secref{Syntax of #1}}
\newcommand\AbstractSyntaxDef[1]{\section{Abstract Syntax of #1\label{sec:Abstract Syntax of #1}}}
\newcommand\AbstractSyntaxDef[2][]{\SectionDef[#1]{Abstract Syntax of #2}{Abstract Syntax of #2}}
\newcommand\AbstractSyntaxRef[1]{\secref{Abstract Syntax of #1}}
\newcommand\TypeRulesDef[1]{\section{Type Rules for #1\label{sec:Type Rules for #1}}}
\newcommand\TypeRulesRef[1]{\secref{Type Rules for #1}}
\newcommand\SemanticsRulesDef[1]{\section{Dynamic Semantics Rules for #1\label{sec:Dynamic Semantics Rules for #1}}}
\newcommand\TypeRulesDef[2][]{\SectionDef[#1]{Type Rules for #2}{Type Rules for #2}}
\newcommand\SemanticsRulesDef[2][]{\SectionDef[#1]{Dynamic Semantics Rules for #2}{Dynamic Semantics Rules for #2}}
\newcommand\SemanticsRulesRef[1]{\secref{Dynamic Semantics Rules for #1}}
\newcommand\textfunc[1]{\textit{#1}}
\newcommand\textastlabel[1]{\textsc{#1}}
Expand Down Expand Up @@ -296,6 +293,144 @@
}%
\fi
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Chapter outline generation macros
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Use \ChapterOutline once in a chapter, after its introductory text and before
% its first section. It prints an itemized list of every \SectionDef in that
% chapter. Chapter membership is independent of file boundaries, so a chapter
% and its sections may span multiple input files.
%
% Define an outlined section as follows:
%
% \SectionDef[defines the relevant concepts]{StableLabel}{Displayed Title}
%
% The optional first argument is the text printed after the section reference
% in the outline. It should include its final punctuation. The second
% argument is a stable label key: the section receives the label
% `sec:StableLabel' and can be referenced with \secref{StableLabel}. The third
% argument is the displayed section title. Keep the label stable when changing
% either the title or its outline description.
%
% \FormalRelationsDef, \SyntaxDef, \AbstractSyntaxDef, \TypeRulesDef, and
% \SemanticsRulesDef are convenience forms of \SectionDef. They accept the
% same optional outline description before their existing required argument.
%
% Most subsections should continue to use \subsection and do not appear in the
% chapter outline. To include a selected subsection, use:
%
% \OutlineSubsectionDef[defines a special case]{StableLabel}{Displayed Title}
%
% It is nested under the most recent \SectionDef in the same chapter, so it must
% follow its intended parent section.
%
% Outlines are read from the previous LaTeX run, like the table of contents, so
% run LaTeX twice after changing their structure or descriptions. Their
% auxiliary data and state are separate from the rule-list macros.
\let\ASLCurrentOutlineSection\@empty
\let\ASLCurrentOutlineSectionChapter\@empty

\newcommand\ASLChapterOutlineSection[3]{%
\item \secref{#2}%
\def\ASLChapterOutlineDescription{#3}%
\ifx\ASLChapterOutlineDescription\@empty
\else
\space #3;%
\fi
\@ifundefined{ASLChapterOutlineSubsections@#1@#2}{}{%
\begin{itemize}%
\csname ASLChapterOutlineSubsections@#1@#2\endcsname
\end{itemize}%
}%
}

\newcommand\ASLChapterOutlineEntry[3]{%
\@ifundefined{ASLChapterOutlineSeen@#1@#2}{%
\expandafter\gdef\csname ASLChapterOutlineSeen@#1@#2\endcsname{}%
\@ifundefined{ASLChapterOutline@#1}{%
\expandafter\gdef\csname ASLChapterOutline@#1\endcsname{}%
}{}%
\expandafter\g@addto@macro\csname ASLChapterOutline@#1\endcsname{%
\ASLChapterOutlineSection{#1}{#2}{#3}%
}%
}{}%
}

\newcommand\ASLChapterOutlineSubentry[4]{%
\@ifundefined{ASLChapterOutlineSubsectionSeen@#1@#2@#3}{%
\expandafter\gdef\csname ASLChapterOutlineSubsectionSeen@#1@#2@#3\endcsname{}%
\@ifundefined{ASLChapterOutlineSubsections@#1@#2}{%
\expandafter\gdef\csname ASLChapterOutlineSubsections@#1@#2\endcsname{}%
}{}%
\expandafter\g@addto@macro\csname ASLChapterOutlineSubsections@#1@#2\endcsname{%
\item \secref{#3}%
\def\ASLChapterOutlineDescription{#4}%
\ifx\ASLChapterOutlineDescription\@empty
\else
\space #4;%
\fi
}%
}{}%
}

\newcommand\ASLPrintChapterOutline{%
\begin{itemize}%
\@ifundefined{ASLChapterOutline@\number\c@chapter}{%
\item \emph{Run LaTeX again to generate this chapter outline.}%
}{%
\csname ASLChapterOutline@\number\c@chapter\endcsname
}%
\end{itemize}%
}

\newcommand\ChapterOutline[0]{%
\@ifundefined{ASLChapterOutlinePrinted@\number\c@chapter}{%
\expandafter\gdef\csname ASLChapterOutlinePrinted@\number\c@chapter\endcsname{}%
}{%
\PackageError{ASLReference}{Multiple chapter outlines in chapter \number\c@chapter}{}%
}%
\global\let\ASLCurrentOutlineSection\@empty
\global\let\ASLCurrentOutlineSectionChapter\@empty
\paragraph{Outline} The rest of this chapter is organized as follows:
\ASLPrintChapterOutline
}

\newcommand\SectionDef[3][]{%
\section{#3\label{sec:#2}}%
\@ifundefined{ASLChapterOutlineWritten@\number\c@chapter @#2}{%
\expandafter\gdef\csname ASLChapterOutlineWritten@\number\c@chapter @#2\endcsname{}%
}{%
\PackageError{ASLReference}{Duplicate outline section `#2' in chapter \number\c@chapter}{}%
}%
\xdef\ASLCurrentOutlineSectionChapter{\number\c@chapter}%
\gdef\ASLCurrentOutlineSection{#2}%
\immediate\write\@auxout{%
\string\ASLChapterOutlineEntry{\number\c@chapter}{\unexpanded{#2}}{\unexpanded{#1}}%
}%
}

\newcommand\OutlineSubsectionDef[3][]{%
\subsection{#3\label{sec:#2}}%
\@ifundefined{ASLChapterOutlineSubsectionWritten@\number\c@chapter @#2}{%
\expandafter\gdef\csname ASLChapterOutlineSubsectionWritten@\number\c@chapter @#2\endcsname{}%
}{%
\PackageError{ASLReference}{Duplicate outline subsection `#2' in chapter \number\c@chapter}{}%
}%
\edef\ASLCurrentChapter{\number\c@chapter}%
\ifx\ASLCurrentOutlineSection\@empty
\PackageError{ASLReference}{Outline subsection `#2' has no preceding outline section}{}%
\else
\ifx\ASLCurrentChapter\ASLCurrentOutlineSectionChapter
\immediate\write\@auxout{%
\string\ASLChapterOutlineSubentry{\number\c@chapter}{\expandafter\unexpanded\expandafter{\ASLCurrentOutlineSection}}{\unexpanded{#2}}{\unexpanded{#1}}%
}%
\else
\PackageError{ASLReference}{Outline subsection `#2' has no preceding outline section in this chapter}{}%
\fi
\fi
}
\makeatother

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Expand Down
Loading
Loading