Context Navigation

Reverse Diff

refrat.tex [90c3b1c:cf16f94]

File:

: 1 edited

doc/refrat/refrat.tex (modified) (178 diffs)

Legend:

: Unmodified
: Added
: Removed

doc/refrat/refrat.tex

-              r90c3b1c
+              rcf16f94
 \makeatletter
+\renewcommand{\labelitemi}{{\raisebox{0.25ex}{\footnotesize$\bullet$}}}
+\renewenvironment{itemize}{\begin{list}{\labelitemi}{\topsep=5pt\itemsep=5pt\parsep=0pt}}{\end{list}}
+%  Reduce size of chapter/section titles
+\def\@makechapterhead#1{%
+  \vspace*{50\p@}%
+  {\parindent \z@ \raggedright \normalfont
+    \ifnum \c@secnumdepth >\m@ne
+        \large\bfseries \@chapapp\space \thechapter
+        \par\nobreak
+        \vskip 5\p@
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 50\p@
+  }}
+\def\@makeschapterhead#1{%
+  \vspace*{50\p@}%
+  {\parindent \z@ \raggedright
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 50\p@
+  }}
+\renewcommand\section{\@startsection{section}{1}{\z@}{-3.0ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\large\bfseries}}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}{-2.5ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\normalsize\bfseries}}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}{-2.0ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\normalsize\bfseries}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}{-2.0ex \@plus -1ex \@minus -.2ex}{-1em}{\normalfont\normalsize\bfseries}}
+% index macros
 \newcommand{\italic}[1]{\emph{\hyperpage{#1}}}
 \newcommand{\definition}[1]{\textbf{\hyperpage{#1}}}
 …
 %\newcommand{\impl}[1]{\index{\protect#1@{\lstinline$\protect#1$}|definition}}
 % inline text and lowercase index: \Index{inline and lowercase index text}
 % inline text and as-in index: \Index[as-is index text]{inline text}
 % inline text but index with different as-is text: \Index[index text]{inline text}
+% text inline and lowercase index: \Index{Inline and index text}
+% text inline and as-in index: \Index{Inline and Index text}
+% text inline but index with different as-is text: \Index[index text]{inline text}
 \newcommand{\Index}{\@ifstar\@sIndex\@Index}
 \newcommand{\@Index}[2][\@empty]{\lowercase{\def\temp{#2}}#2\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
 …
 \linenumbers                                    % comment out to turn off line numbering
+\title{\Huge
+\CFA (\CFAA) Reference Manual and Rationale
+}% title
+\author{\huge
+Glen Ditchfield and Peter A. Buhr
+}% author
+\date{
+DRAFT\\\today
+}% date
+\title{\CFA (\CFAA) Reference Manual and Rationale}
+\author{Glen Ditchfield \and Peter A. Buhr}
+\date{DRAFT\\\today}
 \pagenumbering{roman}
 …
 \copyright\,2015 Glen Ditchfield \\ \\
 \noindent
 This work is licensed under the Creative Commons Attribution 4.0 International License.
 To view a copy of this license, visit {\small\url{http://creativecommons.org/licenses/by/4.0}}.
+This work is licensed under the Creative Commons Attribution 4.0 International License. To view a
+copy of this license, visit {\small\url{http://creativecommons.org/licenses/by/4.0}}.
 \vspace*{1in}
 …
 \chapter*{Introduction}\addcontentsline{toc}{chapter}{Introduction}
+This document is a reference manual and rationale for \CFA, a polymorphic extension of the C programming language.
+It makes frequent reference to the {\c11} standard \cite{ANS:C11}, and occasionally compares \CFA to {\CC} \cite{c++}.
+The manual deliberately imitates the ordering of the {\c11} standard (although the section numbering differs).
+Unfortunately, this means the manual contains more ``forward references'' than usual, making it harder to follow if the reader does not have a copy of the {\c11} standard.
+For a simple introduction to \CFA, see the companion document ``An Overview of \CFA''
+This document is a reference manual and rationale for \CFA, a polymorphic extension of the C
+programming language. It makes frequent reference to the {\c11} standard \cite{ANS:C11}, and
+occasionally compares \CFA to {\CC} \cite{c++}.
+The manual deliberately imitates the ordering of the {\c11} standard (although the section numbering
+differs). Unfortunately, this means the manual contains more ``forward references'' than usual,
+making it harder to follow if the reader does not have a copy of the {\c11} standard. For a simple
+introduction to \CFA, see the companion document ``An Overview of \CFA''
 \cite{Ditchfield96:Overview}.
 \begin{rationale}
 Commentary (like this) is quoted with quads.
 Commentary usually deals with subtle points, the rationale behind a rule, and design decisions.
+Commentary (like this) is quoted with quads. Commentary usually deals with subtle points, the
+rationale behind a rule, and design decisions.
 \end{rationale}
 …
 \chapter{Terms, definitions, and symbols}
+Terms from the {\c11} standard used in this document have the same meaning as in the {\c11} standard.
+Terms from the {\c11} standard used in this document have the same meaning as in the {\c11}
+standard.
 % No ``Conformance'' or ``Environment'' chapters yet.
 …
 \section{Notation}
+The syntax notation used in this document is the same as in the {\c11} standard, with one exception: ellipsis in the definition of a nonterminal, as in ``\emph{declaration:} \ldots'', indicates that these rules extend a previous definition, which occurs in this document or in the {\c11} standard.
+The syntax notation used in this document is the same as in the {\c11} standard, with one exception:
+ellipsis in the definition of a nonterminal, as in ``\emph{declaration:} \ldots'', indicates that
+these rules extend a previous definition, which occurs in this document or in the {\c11} standard.
 …
 \subsection{Scopes of identifiers}\index{scopes}
+\CFA's scope rules differ from C's in one major respect: a declaration of an identifier may overload\index{overloading} outer declarations of lexically identical identifiers in the same
+\Index{name space}, instead of hiding them.
+The outer declaration is hidden if the two declarations have \Index{compatible type}, or if one declares an array type and the other declares a pointer type and the element type and pointed-at type are compatible, or if one has function type and the other is a pointer to a compatible function type, or if one declaration is a \lstinline$type$\use{type} or
+\CFA's scope rules differ from C's in one major respect: a declaration of an identifier may
+overload\index{overloading} outer declarations of lexically identical identifiers in the same
+\Index{name space}, instead of hiding them. The outer declaration is hidden if the two declarations
+have \Index{compatible type}, or if one declares an array type and the other declares a pointer type
+and the element type and pointed-at type are compatible, or if one has function type and the other
+is a pointer to a compatible function type, or if one declaration is a \lstinline$type$\use{type} or
 \lstinline$typedef$\use{typedef} declaration and the other is not.  The outer declaration becomes
 \Index{visible} when the scope of the inner declaration terminates.
 \begin{rationale}
 Hence, a \CFA program can declare an \lstinline$int v$ and a \lstinline$float v$ in the same scope;
 a {\CC} program can not.
+Hence, a \CFA program can declare an \lstinline$int v$ and a \lstinline$float v$ in the same
+scope; a {\CC} program can not.
 \end{rationale}
 …
 \index{linkage}
+\CFA's linkage rules differ from C's in only one respect: instances of a particular identifier with external or internal linkage do not necessarily denote the same object or function.
+Instead, in the set of translation units and libraries that constitutes an entire program, any two instances of a particular identifier with \Index{external linkage} denote the same object or function if they have
+\Index{compatible type}s, or if one declares an array type and the other declares a pointer type and the element type and pointed-at type are compatible, or if one has function type and the other is a pointer to a compatible function type.
+Within one translation unit, each instance of an identifier with \Index{internal linkage} denotes the same object or function in the same circumstances.
+\CFA's linkage rules differ from C's in only one respect: instances of a particular identifier with
+external or internal linkage do not necessarily denote the same object or function. Instead, in the
+set of translation units and libraries that constitutes an entire program, any two instances of a
+particular identifier with \Index{external linkage} denote the same object or function if they have
+\Index{compatible type}s, or if one declares an array type and the other declares a pointer type and
+the element type and pointed-at type are compatible, or if one has function type and the other is a
+pointer to a compatible function type. Within one translation unit, each instance of an identifier
+with \Index{internal linkage} denotes the same object or function in the same circumstances.
 Identifiers with \Index{no linkage} always denote unique entities.
 \begin{rationale}
 A \CFA program can declare an \lstinline$extern int v$ and an \lstinline$extern float v$;
 a C program cannot.
+A \CFA program can declare an \lstinline$extern int v$ and an \lstinline$extern float v$; a C
+program cannot.
 \end{rationale}
 …
 \subsubsection{Semantics}
+\CFA provides a capability for generic types;
+using this capability a single "generic type generator" can be written that can represent multiple concrete type instantiations by substitution of the "type parameters" of the generic type for concrete types.
+Syntactically a generic type generator is represented by putting a forall specifier on a struct or union declaration, as defined in \VRef{forall}.
+An instantiation of the generic type is written by specifying the type parameters in parentheses after the name of the generic type generator:
+\CFA provides a capability for generic types; using this capability a single "generic type
+generator" can be written that can represent multiple concrete type instantiations by substitution
+of the "type parameters" of the generic type for concrete types. Syntactically a generic type
+generator is represented by putting a forall specifier on a struct or union declaration, as defined
+in \VRef{forall}. An instantiation of the generic type is written by specifying the type parameters
+in parentheses after the name of the generic type generator:
 \begin{lstlisting}
 forall( type T | sumable( T ) ) struct pair {
 …
 \end{lstlisting}
+The type parameters in an instantiation of a generic type must satisfy any constraints in the forall specifier on the type generator declaration, e.g., \lstinline$sumable$.
+The instantiation then has the semantics that would result if the type parameters were substituted into the type generator declaration by macro substitution.
+Polymorphic functions may have generic types as parameters, and those generic types may use type parameters of the polymorphic function as type parameters of the generic type:
+The type parameters in an instantiation of a generic type must satisfy any constraints in the forall
+specifier on the type generator declaration, e.g., \lstinline$sumable$. The instantiation then has
+the semantics that would result if the type parameters were substituted into the type generator
+declaration by macro substitution.
+Polymorphic functions may have generic types as parameters, and those generic types may use type
+parameters of the polymorphic function as type parameters of the generic type:
 \begin{lstlisting}
 forall( type T ) void swap( pair(T) *p ) {
 …
 \subsubsection{Constraints}
+To avoid unduly constraining implementors, the generic type generator definition must be visible at any point where it is instantiated.  Forward declarations of generic type generators are not forbidden, but the definition must be visible to instantiate the generic type.  Equivalently, instantiations of generic types are not allowed to be incomplete types.
+To avoid unduly constraining implementors, the generic type generator definition must be visible at
+any point where it is instantiated.  Forward declarations of generic type generators are not
+forbidden, but the definition must be visible to instantiate the generic type.  Equivalently,
+instantiations of generic types are not allowed to be incomplete types.
 \examples
 …
 forall( type T ) struct B {
         A(T) *a;                        // legal, but cannot instantiate B(T)
+        A(T) *a;  // legal, but cannot instantiate B(T)
 };
 B(T) x;                                 // illegal, *x.a is of an incomplete generic type
+B(T) x; // illegal, *x.a is of an incomplete generic type
 forall( type T ) struct A {
         B( T ) *b;
 };
+B( T ) y;                               // legal, *x.a is now of a complete generic type
+B( T ) y; // legal, *x.a is now of a complete generic type
 // box.h:
 …
 // main.c:
         box( int ) *b = make_box( 42 ); // illegal, definition of box not visible
         use_box( b );           // illegal
+        box( int ) *b = make_box( 42 ); // illegal, def'n of box not visible
+        use_box( b ); // illegal
 \end{lstlisting}
 …
 \section{Conversions}
 \CFA defines situations where values of one type are automatically converted to another type.
+These conversions are called \define{implicit conversion}s.
+The programmer can request
+These conversions are called \define{implicit conversion}s. The programmer can request
 \define{explicit conversion}s using cast expressions.
 …
 \subsubsection{Safe arithmetic conversions}
+In C, a pattern of conversions known as the \define{usual arithmetic conversion}s is used with most binary arithmetic operators to convert the operands to a common type and determine the type of the operator's result.
+In \CFA, these conversions play a role in overload resolution, and collectively are called the \define{safe arithmetic conversion}s.
+Let \(int_r\) and \(unsigned_r\) be the signed and unsigned integer types with integer conversion rank\index{integer conversion rank}\index{rank|see{integer conversion rank}} $r$.
+Let \(unsigned_{mr}\) be the unsigned integer type with maximal rank.
+In C, a pattern of conversions known as the \define{usual arithmetic conversion}s is used with most
+binary arithmetic operators to convert the operands to a common type and determine the type of the
+operator's result. In \CFA, these conversions play a role in overload resolution, and
+collectively are called the \define{safe arithmetic conversion}s.
+Let \(int_r\) and \(unsigned_r\) be the signed and unsigned integer types with integer conversion
+rank\index{integer conversion rank}\index{rank|see{integer conversion rank}} $r$. Let
+\(unsigned_{mr}\) be the unsigned integer type with maximal rank.
 The following conversions are \emph{direct} safe arithmetic conversions.
 …
 \item
 The \Index{integer promotion}s.
+\item
+For every rank $r$ greater than or equal to the rank of \lstinline$int$, conversion from \(int_r\) to \(unsigned_r\).
+\item
+For every rank $r$ greater than or equal to the rank of \lstinline$int$, where \(int_{r+1}\) exists and can represent all values of \(unsigned_r\), conversion from \(unsigned_r\) to \(int_{r+1}\).
+\item
+For every rank $r$ greater than or equal to the rank of \lstinline$int$, conversion from \(int_r\)
+to \(unsigned_r\).
+\item
+For every rank $r$ greater than or equal to the rank of \lstinline$int$, where \(int_{r+1}\) exists
+and can represent all values of \(unsigned_r\), conversion from \(unsigned_r\) to \(int_{r+1}\).
 \item
 Conversion from \(unsigned_{mr}\) to \lstinline$float$.
 \item
 Conversion from an enumerated type to its compatible integer type.
+\item
+Conversion from \lstinline$float$ to \lstinline$double$, and from \lstinline$double$ to \lstinline$long double$.
+\item
+Conversion from \lstinline$float _Complex$ to \lstinline$double _Complex$, and from \lstinline$double _Complex$ to \lstinline$long double _Complex$.
+\item
+Conversion from \lstinline$float$ to \lstinline$double$, and from \lstinline$double$ to
+\lstinline$long double$.
+\item
+Conversion from \lstinline$float _Complex$ to \lstinline$double _Complex$,
+and from \lstinline$double _Complex$ to \lstinline$long double _Complex$.
 \begin{sloppypar}
 \item
+Conversion from \lstinline$float _Imaginary$ to \lstinline$double _Imaginary$, and from \lstinline$double _Imaginary$ to \lstinline$long double$ \lstinline$_Imaginary$, if the implementation supports imaginary types.
+Conversion from \lstinline$float _Imaginary$ to \lstinline$double _Imaginary$, and from
+\lstinline$double _Imaginary$ to \lstinline$long double$ \lstinline$_Imaginary$, if the
+implementation supports imaginary types.
 \end{sloppypar}
 \end{itemize}
+If type \lstinline$T$ can be converted to type \lstinline$U$ by a safe direct arithmetic conversion and type \lstinline$U$ can be converted to type \lstinline$V$ by a safe arithmetic conversion, then the conversion from \lstinline$T$ to type \lstinline$V$ is an \emph{indirect} safe arithmetic conversion.
+\begin{rationale}
+Note that {\c11} does not include conversion from \Index{real type}s to \Index{complex type}s in the usual arithmetic conversions, and \CFA does not include them as safe conversions.
+If type \lstinline$T$ can be converted to type \lstinline$U$ by a safe direct arithmetic conversion
+and type \lstinline$U$ can be converted to type \lstinline$V$ by a safe arithmetic conversion, then
+the conversion from \lstinline$T$ to type \lstinline$V$ is an \emph{indirect} safe arithmetic
+conversion.
+\begin{rationale}
+Note that {\c11} does not include conversion from \Index{real type}s to \Index{complex type}s in the
+usual arithmetic conversions, and \CFA does not include them as safe conversions.
 \end{rationale}
 …
 If an expression's type is a pointer to a structure or union type that has a member that is an
+\Index{anonymous structure} or an \Index{anonymous union}, it can be implicitly converted\index{implicit conversion} to a pointer to the anonymous structure's or anonymous union's type.
+The result of the conversion is a pointer to the member.
+\Index{anonymous structure} or an \Index{anonymous union}, it can be implicitly
+converted\index{implicit conversion} to a pointer to the anonymous structure's or anonymous union's
+type. The result of the conversion is a pointer to the member.
 \examples
 …
         int x, y;
 };
 void move_by( struct point * p1, struct point * p2 ) {@\impl{move_by}@
+void move_by(struct point * p1, struct point * p2) {@\impl{move_by}@
         p1->x += p2.x;
         p1->y += p2.y;
+}
 struct color_point {
         enum { RED, BLUE, GREEN } color;
         struct point;
 } cp1, cp2;
 move_to( &cp1, &cp2 );
+move_to(&cp1, &cp2);
 \end{lstlisting}
 Thanks to implicit conversion, the two arguments that \lstinline$move_by()$ receives are pointers to
 …
 \subsubsection{Specialization}
 A function or value whose type is polymorphic may be implicitly converted to one whose type is
+\Index{less polymorphic} by binding values to one or more of its \Index{inferred parameter}.
+Any value that is legal for the inferred parameter may be used, including other inferred parameters.
+If, after the inferred parameter binding, an \Index{assertion parameter} has no inferred parameters in its type, then an object or function must be visible at the point of the specialization that has the same identifier as the assertion parameter and has a type that is compatible\index{compatible
+  type} with or can be specialized to the type of the assertion parameter.  The assertion parameter is bound to that object or function.
+The type of the specialization is the type of the original with the bound inferred parameters and the bound assertion parameters replaced by their bound values.
+\Index{less polymorphic} by binding values to one or more of its \Index{inferred parameter}. Any
+value that is legal for the inferred parameter may be used, including other inferred parameters.
+If, after the inferred parameter binding, an \Index{assertion parameter} has no inferred parameters
+in its type, then an object or function must be visible at the point of the specialization that has
+the same identifier as the assertion parameter and has a type that is compatible\index{compatible
+  type} with or can be specialized to the type of the assertion parameter.  The assertion parameter
+is bound to that object or function.
+The type of the specialization is the type of the original with the bound inferred parameters and
+the bound assertion parameters replaced by their bound values.
 \examples
 …
 can be specialized to (among other things)
 \begin{lstlisting}
 forall( type T ) void (*)( T, T );              // U bound to T
 forall( type T ) void (*)( T, real );   // U bound to real
 forall( type U ) void (*)( real, U );   // T bound to real
+forall( type T ) void (*)( T, T );              // U bound to T
+forall( type T ) void (*)( T, real );   // U bound to real
+forall( type U ) void (*)( real, U );   // T bound to real
 void f( real, real );                                   // both bound to real
 \end{lstlisting}
 …
 The type
 \begin{lstlisting}
 forall( type T | T ?+?( T, T ) ) T (*)( T );
+forall( type T | T ?+?( T, T )) T (*)( T );
 \end{lstlisting}
 can be specialized to (among other things)
 \begin{lstlisting}
 int (*)( int );         // T bound to int, and T ?+?(T, T ) bound to int ?+?( int, int )
+int (*)( int );                                         // T bound to int, and T ?+?(T, T ) bound to int ?+?( int, int )
 \end{lstlisting}
 …
 from a pointer to any non-\lstinline$void$ type to a pointer to \lstinline$void$;
 \item
+from a pointer to any type to a pointer to a more qualified version of the type\index{qualified type};
+\item
+from a pointer to a structure or union type to a pointer to the type of a member of the structure or union that is an \Index{anonymous structure} or an \Index{anonymous union};
+\item
+within the scope of an initialized \Index{type declaration}, conversions between a type and its implementation or between a pointer to a type and a pointer to its implementation.
+from a pointer to any type to a pointer to a more qualified version of the type\index{qualified
+type};
+\item
+from a pointer to a structure or union type to a pointer to the type of a member of the structure or
+union that is an \Index{anonymous structure} or an \Index{anonymous union};
+\item
+within the scope of an initialized \Index{type declaration}, conversions between a type and its
+implementation or between a pointer to a type and a pointer to its implementation.
 \end{itemize}
 Conversions that are not safe conversions are \define{unsafe conversion}s.
 \begin{rationale}
+As in C, there is an implicit conversion from \lstinline$void *$ to any pointer type.
+This is clearly dangerous, and {\CC} does not have this implicit conversion.
+\CFA\index{deficiencies!void * conversion} keeps it, in the interest of remaining as pure a superset of C as possible, but discourages it by making it unsafe.
+As in C, there is an implicit conversion from \lstinline$void *$ to any pointer type. This is
+clearly dangerous, and {\CC} does not have this implicit conversion.
+\CFA\index{deficiencies!void * conversion} keeps it, in the interest of remaining as pure a
+superset of C as possible, but discourages it by making it unsafe.
 \end{rationale}
 …
 \subsection{Conversion cost}
+The \define{conversion cost} of a safe\index{safe conversion} conversion\footnote{Unsafe\index{unsafe conversion} conversions do not have defined conversion costs.} is a measure of how desirable or undesirable it is.
+It is defined as follows.
+The \define{conversion cost} of a safe\index{safe conversion}
+conversion\footnote{Unsafe\index{unsafe conversion} conversions do not have defined conversion
+costs.} is a measure of how desirable or undesirable it is. It is defined as follows.
 \begin{itemize}
 \item
 …
 \item
+The cost of an indirect safe arithmetic conversion is the smallest number of direct conversions needed to make up the conversion.
+The cost of an indirect safe arithmetic conversion is the smallest number of direct conversions
+needed to make up the conversion.
 \end{itemize}
 …
 \begin{itemize}
 \item
+The cost of an implicit conversion from \lstinline$int$ to \lstinline$long$ is 1.
+The cost of an implicit conversion from \lstinline$long$ to \lstinline$double$ is 3, because it is defined in terms of conversions from \lstinline$long$ to \lstinline$unsigned long$, then to \lstinline$float$, and then to \lstinline$double$.
+\item
+If \lstinline$int$ can represent all the values of \lstinline$unsigned short$, then the cost of an implicit conversion from \lstinline$unsigned short$ to \lstinline$unsigned$ is 2:
+\lstinline$unsigned short$ to \lstinline$int$ to \lstinline$unsigned$.
+Otherwise,
+The cost of an implicit conversion from \lstinline$int$ to \lstinline$long$ is 1. The cost of an
+implicit conversion from \lstinline$long$ to \lstinline$double$ is 3, because it is defined in terms
+of conversions from \lstinline$long$ to \lstinline$unsigned long$, then to \lstinline$float$, and
+then to \lstinline$double$.
+\item
+If \lstinline$int$ can represent all the values of \lstinline$unsigned short$, then the cost of an
+implicit conversion from \lstinline$unsigned short$ to \lstinline$unsigned$ is 2:
+\lstinline$unsigned short$ to \lstinline$int$ to \lstinline$unsigned$. Otherwise,
 \lstinline$unsigned short$ is converted directly to \lstinline$unsigned$, and the cost is 1.
 \item
+If \lstinline$long$ can represent all the values of \lstinline$unsigned$, then the conversion cost of \lstinline$unsigned$ to \lstinline$long$ is 1.
+Otherwise, the conversion is an unsafe conversion, and its conversion cost is undefined.
+If \lstinline$long$ can represent all the values of \lstinline$unsigned$, then the conversion cost
+of \lstinline$unsigned$ to \lstinline$long$ is 1. Otherwise, the conversion is an unsafe
+conversion, and its conversion cost is undefined.
 \end{itemize}
 …
 \subsection{Identifiers}
+\CFA allows operator \Index{overloading} by associating operators with special function identifiers.
+Furthermore, the constants ``\lstinline$0$'' and ``\lstinline$1$'' have special status for many of C's data types (and for many programmer-defined data types as well), so \CFA treats them as overloadable identifiers.
+Programmers can use these identifiers to declare functions and objects that implement operators and constants for their own types.
+\CFA allows operator \Index{overloading} by associating operators with special function
+identifiers. Furthermore, the constants ``\lstinline$0$'' and ``\lstinline$1$'' have special status
+for many of C's data types (and for many programmer-defined data types as well), so \CFA treats them
+as overloadable identifiers. Programmers can use these identifiers to declare functions and objects
+that implement operators and constants for their own types.
 …
 \end{syntax}
+\index{constant identifiers}\index{identifiers!for constants} The tokens ``\lstinline$0$''\impl{0} and ``\lstinline$1$''\impl{1} are identifiers.
+No other tokens defined by the rules for integer constants are considered to be identifiers.
+\begin{rationale}
+Why ``\lstinline$0$'' and ``\lstinline$1$''? Those integers have special status in C.
+All scalar types can be incremented and decremented, which is defined in terms of adding or subtracting 1.
+The operations ``\lstinline$&&$'', ``\lstinline$||$'', and ``\lstinline$!$'' can be applied to any scalar arguments, and are defined in terms of comparison against 0.
+A \nonterm{constant-expression} that evaluates to 0 is effectively compatible with every pointer type.
+In C, the integer constants 0 and 1 suffice because the integer promotion rules can convert them to any arithmetic type, and the rules for pointer expressions treat constant expressions evaluating to
+as a special case.
+However, user-defined arithmetic types often need the equivalent of a 1 or 0 for their functions or operators, polymorphic functions often need 0 and 1 constants of a type matching their polymorphic parameters, and user-defined pointer-like types may need a null value.
+Defining special constants for a user-defined type is more efficient than defining a conversion to the type from \lstinline$_Bool$.
+Why \emph{just} ``\lstinline$0$'' and ``\lstinline$1$''? Why not other integers? No other integers have special status in C.
+A facility that let programmers declare specific constants---``\lstinline$const Rational 12$'', for instance---would not be much of an improvement.
+Some facility for defining the creation of values of programmer-defined types from arbitrary integer tokens would be needed.
+The complexity of such a feature doesn't seem worth the gain.
+\index{constant identifiers}\index{identifiers!for constants} The tokens ``\lstinline$0$''\impl{0}
+and ``\lstinline$1$''\impl{1} are identifiers. No other tokens defined by the rules for integer
+constants are considered to be identifiers.
+\begin{rationale}
+Why ``\lstinline$0$'' and ``\lstinline$1$''? Those integers have special status in C. All scalar
+types can be incremented and decremented, which is defined in terms of adding or subtracting 1. The
+operations ``\lstinline$&&$'', ``\lstinline$||$'', and ``\lstinline$!$'' can be applied to any
+scalar arguments, and are defined in terms of comparison against 0. A \nonterm{constant-expression}
+that evaluates to 0 is effectively compatible with every pointer type.
+In C, the integer constants 0 and 1 suffice because the integer promotion rules can convert them to
+any arithmetic type, and the rules for pointer expressions treat constant expressions evaluating to
+as a special case. However, user-defined arithmetic types often need the equivalent of a 1 or 0
+for their functions or operators, polymorphic functions often need 0 and 1 constants of a type
+matching their polymorphic parameters, and user-defined pointer-like types may need a null value.
+Defining special constants for a user-defined type is more efficient than defining a conversion to
+the type from \lstinline$_Bool$.
+Why \emph{just} ``\lstinline$0$'' and ``\lstinline$1$''? Why not other integers? No other integers
+have special status in C. A facility that let programmers declare specific
+constants---``\lstinline$const Rational 12$'', for instance---would not be much of an improvement.
+Some facility for defining the creation of values of programmer-defined types from arbitrary integer
+tokens would be needed. The complexity of such a feature doesn't seem worth the gain.
 \end{rationale}
 …
 \subsubsection{Operator identifiers}
+\index{operator identifiers}\index{identifiers!for operators} Table \ref{opids} lists the programmer-definable operator identifiers and the operations they are associated with.
+Functions that are declared with (or pointed at by function pointers that are declared with) these identifiers can be called by expressions that use the operator tokens and syntax, or the operator identifiers and ``function call'' syntax.
+The relationships between operators and function calls are discussed in descriptions of the operators.
+\index{operator identifiers}\index{identifiers!for operators} Table \ref{opids} lists the
+programmer-definable operator identifiers and the operations they are associated with. Functions
+that are declared with (or pointed at by function pointers that are declared with) these identifiers
+can be called by expressions that use the operator tokens and syntax, or the operator identifiers
+and ``function call'' syntax. The relationships between operators and function calls are discussed
+in descriptions of the operators.
 \begin{table}[hbt]
 …
 \begin{rationale}
+Operator identifiers are made up of the characters of the operator token, with question marks added to mark the positions of the arguments of operators.
+The question marks serve as mnemonic devices;
+programmers can not create new operators by arbitrarily mixing question marks and other non-alphabetic characters.
+Note that prefix and postfix versions of the increment and decrement operators are distinguished by the position of the question mark.
+\end{rationale}
+\begin{rationale}
+The use of ``\lstinline$?$'' in identifiers means that some C programs are not \CFA programs.  For instance, the sequence of characters ``\lstinline$(i < 0)?--i:i$'' is legal in a C program, but a
+\CFA compiler detects a syntax error because it treats ``\lstinline$?--$'' as an identifier, not as the two tokens ``\lstinline$?$'' and ``\lstinline$--$''.
+Operator identifiers are made up of the characters of the operator token, with question marks added
+to mark the positions of the arguments of operators. The question marks serve as mnemonic devices;
+programmers can not create new operators by arbitrarily mixing question marks and other
+non-alphabetic characters. Note that prefix and postfix versions of the increment and decrement
+operators are distinguished by the position of the question mark.
+\end{rationale}
+\begin{rationale}
+The use of ``\lstinline$?$'' in identifiers means that some C programs are not \CFA programs.  For
+instance, the sequence of characters ``\lstinline$(i < 0)?--i:i$'' is legal in a C program, but a
+\CFA compiler detects a syntax error because it treats ``\lstinline$?--$'' as an identifier, not
+as the two tokens ``\lstinline$?$'' and ``\lstinline$--$''.
 \end{rationale}
 …
 \item
 The logical operators ``\lstinline$&&$'' and ``\lstinline$||$'', and the conditional operator
+``\lstinline$?:$''.
+These operators do not always evaluate their operands, and hence can not be properly defined by functions unless some mechanism like call-by-name is added to the language.
+Note that the definitions of ``\lstinline$&&$'' and ``\lstinline$||$'' say that they work by checking that their arguments are unequal to 0, so defining ``\lstinline$!=$'' and ``\lstinline$0$'' for user-defined types is enough to allow them to be used in logical expressions.
+\item
+The comma operator\index{comma expression}.
+It is a control-flow operator like those above.
+``\lstinline$?:$''. These operators do not always evaluate their operands, and hence can not be
+properly defined by functions unless some mechanism like call-by-name is added to the language.
+Note that the definitions of ``\lstinline$&&$'' and ``\lstinline$||$'' say that they work by
+checking that their arguments are unequal to 0, so defining ``\lstinline$!=$'' and ``\lstinline$0$''
+for user-defined types is enough to allow them to be used in logical expressions.
+\item
+The comma operator\index{comma expression}. It is a control-flow operator like those above.
 Changing its meaning seems pointless and confusing.
 \item
+The ``address of'' operator.
+It would seem useful to define a unary ``\lstinline$&$'' operator that returns values of some programmer-defined pointer-like type.
+The problem lies with the type of the operator.
+Consider the expression ``\lstinline$p = &x$'', where \lstinline$x$ is of type
+\lstinline$T$ and \lstinline$p$ has the programmer-defined type \lstinline$T_ptr$.
+The expression might be treated as a call to the unary function ``\lstinline$&?$''.
+Now what is the type of the function's parameter? It can not be \lstinline$T$, because then \lstinline$x$ would be passed by value, and there is no way to create a useful pointer-like result from a value.
+Hence the parameter must have type \lstinline$T *$.
+But then the expression must be rewritten as ``\lstinline$p = &?( &x )$''
+The ``address of'' operator. It would seem useful to define a unary ``\lstinline$&$'' operator that
+returns values of some programmer-defined pointer-like type. The problem lies with the type of the
+operator. Consider the expression ``\lstinline$p = &x$'', where \lstinline$x$ is of type
+\lstinline$T$ and \lstinline$p$ has the programmer-defined type \lstinline$T_ptr$. The expression
+might be treated as a call to the unary function ``\lstinline$&?$''. Now what is the type of the
+function's parameter? It can not be \lstinline$T$, because then \lstinline$x$ would be passed by
+value, and there is no way to create a useful pointer-like result from a value. Hence the parameter
+must have type \lstinline$T *$. But then the expression must be rewritten as ``\lstinline$p = &?( &x )$''
 ---which doesn't seem like progress!
+The rule for address-of expressions would have to be something like ``keep applying address-of functions until you get one that takes a pointer argument, then use the built-in operator and stop''.
+It seems simpler to define a conversion function from \lstinline$T *$ to \lstinline$T_ptr$.
+\item
+The \lstinline$sizeof$ operator.
+It is already defined for every object type, and intimately tied into the language's storage allocation model.
+Redefining it seems pointless.
+\item
+The ``member of'' operators ``\lstinline$.$'' and ``\lstinline$->$''.
+These are not really infix operators, since their right ``operand'' is not a value or object.
+\item
+Cast operators\index{cast expression}.
+Anything that can be done with an explicit cast can be done with a function call.
+The difference in syntax is small.
+The rule for address-of expressions would have to be something like ``keep applying address-of
+functions until you get one that takes a pointer argument, then use the built-in operator and
+stop''. It seems simpler to define a conversion function from \lstinline$T *$ to \lstinline$T_ptr$.
+\item
+The \lstinline$sizeof$ operator. It is already defined for every object type, and intimately tied
+into the language's storage allocation model. Redefining it seems pointless.
+\item
+The ``member of'' operators ``\lstinline$.$'' and ``\lstinline$->$''. These are not really infix
+operators, since their right ``operand'' is not a value or object.
+\item
+Cast operators\index{cast expression}. Anything that can be done with an explicit cast can be done
+with a function call. The difference in syntax is small.
 \end{itemize}
 \end{rationale}
 …
 \section{Expressions}
+\CFA allows operators and identifiers to be overloaded.
+Hence, each expression can have a number of \define{interpretation}s, each of which has a different type.
+The interpretations that are potentially executable are called \define{valid interpretation}s.
+The set of interpretations depends on the kind of expression and on the interpretations of the subexpressions that it contains.
+The rules for determining the valid interpretations of an expression are discussed below for each kind of expression.
+Eventually the context of the outermost expression chooses one interpretation of that expression.
+An \define{ambiguous interpretation} is an interpretation which does not specify the exact object or function denoted by every identifier in the expression.
+An expression can have some interpretations that are ambiguous and others that are unambiguous.
+An expression that is chosen to be executed shall not be ambiguous.
+The \define{best valid interpretations} are the valid interpretations that use the fewest unsafe\index{unsafe conversion} conversions.
+Of these, the best are those where the functions and objects involved are the least polymorphic\index{less polymorphic}.
+Of these, the best have the lowest total \Index{conversion cost}, including all implicit conversions in the argument expressions.
+Of these, the best have the highest total conversion cost for the implicit conversions
+(if any) applied to the argument expressions.
+If there is no single best valid interpretation, or if the best valid interpretation is ambiguous, then the resulting interpretation is ambiguous\index{ambiguous interpretation}.
+\begin{rationale}
+\CFA's rules for selecting the best interpretation are designed to allow overload resolution to mimic C's operator semantics.
+In C, the ``usual arithmetic conversions'' are applied to the operands of binary operators if necessary to convert the operands to types with a common real type.
+In \CFA, those conversions are ``safe''.
+The ``fewest unsafe conversions'' rule ensures that the usual conversions are done, if possible.
+The ``lowest total expression cost'' rule chooses the proper common type.
+The odd-looking ``highest argument conversion cost'' rule ensures that, when unary expressions must be converted, conversions of function results are preferred to conversion of function arguments: \lstinline$(double)-i$ will be preferred to \lstinline$-(double)i$.
+The ``least polymorphic'' rule reduces the number of polymorphic function calls, since such functions are presumably more expensive than monomorphic functions and since the more specific function is presumably more appropriate.
+It also gives preference to monomorphic values (such as the
+\CFA allows operators and identifiers to be overloaded. Hence, each expression can have a number
+of \define{interpretation}s, each of which has a different type. The interpretations that are
+potentially executable are called \define{valid interpretation}s. The set of interpretations
+depends on the kind of expression and on the interpretations of the subexpressions that it contains.
+The rules for determining the valid interpretations of an expression are discussed below for each
+kind of expression. Eventually the context of the outermost expression chooses one interpretation
+of that expression.
+An \define{ambiguous interpretation} is an interpretation which does not specify the exact object or
+function denoted by every identifier in the expression. An expression can have some interpretations
+that are ambiguous and others that are unambiguous. An expression that is chosen to be executed
+shall not be ambiguous.
+The \define{best valid interpretations} are the valid interpretations that use the fewest
+unsafe\index{unsafe conversion} conversions. Of these, the best are those where the functions and
+objects involved are the least polymorphic\index{less polymorphic}. Of these, the best have the
+lowest total \Index{conversion cost}, including all implicit conversions in the argument
+expressions. Of these, the best have the highest total conversion cost for the implicit conversions
+(if any) applied to the argument expressions. If there is no single best valid interpretation, or if
+the best valid interpretation is ambiguous, then the resulting interpretation is
+ambiguous\index{ambiguous interpretation}.
+\begin{rationale}
+\CFA's rules for selecting the best interpretation are designed to allow overload resolution to
+mimic C's operator semantics. In C, the ``usual arithmetic conversions'' are applied to the
+operands of binary operators if necessary to convert the operands to types with a common real type.
+In \CFA, those conversions are ``safe''. The ``fewest unsafe conversions'' rule ensures that the
+usual conversions are done, if possible. The ``lowest total expression cost'' rule chooses the
+proper common type. The odd-looking ``highest argument conversion cost'' rule ensures that, when
+unary expressions must be converted, conversions of function results are preferred to conversion of
+function arguments: \lstinline$(double)-i$ will be preferred to \lstinline$-(double)i$.
+The ``least polymorphic'' rule reduces the number of polymorphic function calls, since such
+functions are presumably more expensive than monomorphic functions and since the more specific
+function is presumably more appropriate. It also gives preference to monomorphic values (such as the
 \lstinline$int$ \lstinline$0$) over polymorphic values (such as the \Index{null pointer}
+\lstinline$0$\use{0}).
+However, interpretations that call polymorphic functions are preferred to interpretations that perform unsafe conversions, because those conversions potentially lose accuracy or violate strong typing.
+\lstinline$0$\use{0}). However, interpretations that call polymorphic functions are preferred to
+interpretations that perform unsafe conversions, because those conversions potentially lose accuracy
+or violate strong typing.
 There are two notable differences between \CFA's overload resolution rules and the rules for
+{\CC} defined in \cite{c++}.
+First, the result type of a function plays a role.
+In {\CC}, a function call must be completely resolved based on the arguments to the call in most circumstances.
+In \CFA, a function call may have several interpretations, each with a different result type, and the interpretations of the containing context choose among them.
+Second, safe conversions are used to choose among interpretations of all sorts of functions;
+in {\CC}, the ``usual arithmetic conversions'' are a separate set of rules that apply only to the built-in operators.
+\end{rationale}
+Expressions involving certain operators\index{operator identifiers} are considered to be equivalent to function calls.
+A transformation from ``operator'' syntax to ``function call'' syntax is defined by \define{rewrite rules}.
+Each operator has a set of predefined functions that overload its identifier.
+Overload resolution determines which member of the set is executed in a given expression.
+The functions have \Index{internal linkage} and are implicitly declared with \Index{file scope}.
+The predefined functions and rewrite rules are discussed below for each of these operators.
+\begin{rationale}
+Predefined functions and constants have internal linkage because that simplifies optimization in traditional compile-and-link environments.
+For instance, ``\lstinline$an_int + an_int$'' is equivalent to ``\lstinline$?+?(an_int, an_int)$''.
+If integer addition has not been redefined in the current scope, a compiler can generate code to perform the addition directly.
+If predefined functions had external linkage, this optimization would be difficult.
+\end{rationale}
+\begin{rationale}
+Since each subsection describes the interpretations of an expression in terms of the interpretations of its subexpressions, this chapter can be taken as describing an overload resolution algorithm that uses one bottom-up pass over an expression tree.
+Such an algorithm was first described (for Ada) by Baker~\cite{Bak:overload}.
+It is extended here to handle polymorphic functions and arithmetic conversions.
+The overload resolution rules and the predefined functions have been chosen so that, in programs that do not introduce overloaded declarations, expressions will have the same meaning in C and in \CFA.
+\end{rationale}
+\begin{rationale}
+Expression syntax is quoted from the {\c11} standard.
+The syntax itself defines the precedence and associativity of operators.
+The sections are arranged in decreasing order of precedence, with all operators in a section having the same precedence.
+{\CC} defined in \cite{c++}. First, the result type of a function plays a role. In {\CC}, a
+function call must be completely resolved based on the arguments to the call in most circumstances.
+In \CFA, a function call may have several interpretations, each with a different result type, and
+the interpretations of the containing context choose among them. Second, safe conversions are used
+to choose among interpretations of all sorts of functions; in {\CC}, the ``usual arithmetic
+conversions'' are a separate set of rules that apply only to the built-in operators.
+\end{rationale}
+Expressions involving certain operators\index{operator identifiers} are considered to be equivalent
+to function calls. A transformation from ``operator'' syntax to ``function call'' syntax is defined
+by \define{rewrite rules}. Each operator has a set of predefined functions that overload its
+identifier. Overload resolution determines which member of the set is executed in a given
+expression. The functions have \Index{internal linkage} and are implicitly declared with \Index{file
+scope}. The predefined functions and rewrite rules are discussed below for each of these
+operators.
+\begin{rationale}
+Predefined functions and constants have internal linkage because that simplifies optimization in
+traditional compile-and-link environments. For instance, ``\lstinline$an_int + an_int$'' is
+equivalent to ``\lstinline$?+?(an_int, an_int)$''. If integer addition has not been redefined in
+the current scope, a compiler can generate code to perform the addition directly. If predefined
+functions had external linkage, this optimization would be difficult.
+\end{rationale}
+\begin{rationale}
+Since each subsection describes the interpretations of an expression in terms of the interpretations
+of its subexpressions, this chapter can be taken as describing an overload resolution algorithm that
+uses one bottom-up pass over an expression tree. Such an algorithm was first described (for Ada) by
+Baker~\cite{Bak:overload}. It is extended here to handle polymorphic functions and arithmetic
+conversions. The overload resolution rules and the predefined functions have been chosen so that, in
+programs that do not introduce overloaded declarations, expressions will have the same meaning in C
+and in \CFA.
+\end{rationale}
+\begin{rationale}
+Expression syntax is quoted from the {\c11} standard. The syntax itself defines the precedence and
+associativity of operators. The sections are arranged in decreasing order of precedence, with all
+operators in a section having the same precedence.
 \end{rationale}
 …
 const int 1;@\use{1}@
 const int 0;@\use{0}@
 forall( dtype DT ) DT * const 0;
 forall( ftype FT ) FT * const 0;
+forall( dtype DT ) DT *const 0;
+forall( ftype FT ) FT *const 0;
 \end{lstlisting}
 \semantics
+The \Index{valid interpretation} of an \nonterm{identifier} are given by the visible\index{visible} declarations of the identifier.
+A \nonterm{constant} or \nonterm{string-literal} has one valid interpretation, which has the type and value defined by {\c11}.
+The predefined integer identifiers ``\lstinline$1$'' and ``\lstinline$0$'' have the integer values 1 and 0, respectively.
+The other two predefined ``\lstinline$0$'' identifiers are bound to polymorphic pointer values that, when specialized\index{specialization} with a data type or function type respectively, produce a null pointer of that type.
+The \Index{valid interpretation} of an \nonterm{identifier} are given by the visible\index{visible}
+declarations of the identifier.
+A \nonterm{constant} or \nonterm{string-literal} has one valid interpretation, which has the type
+and value defined by {\c11}. The predefined integer identifiers ``\lstinline$1$'' and
+``\lstinline$0$'' have the integer values 1 and 0, respectively. The other two predefined
+``\lstinline$0$'' identifiers are bound to polymorphic pointer values that, when
+specialized\index{specialization} with a data type or function type respectively, produce a null
+pointer of that type.
 A parenthesised expression has the same interpretations as the contained \nonterm{expression}.
 \examples
+The expression \lstinline$(void *)0$\use{0} specializes the (polymorphic) null pointer to a null pointer to \lstinline$void$. \lstinline$(const void *)0$ does the same, and also uses a safe conversion from \lstinline$void *$ to \lstinline$const void *$.
+In each case, the null pointer conversion is better\index{best valid interpretations} than the unsafe conversion of the integer
+The expression \lstinline$(void *)0$\use{0} specializes the (polymorphic) null pointer to a null
+pointer to \lstinline$void$. \lstinline$(const void *)0$ does the same, and also uses a safe
+conversion from \lstinline$void *$ to \lstinline$const void *$. In each case, the null pointer
+conversion is better\index{best valid interpretations} than the unsafe conversion of the integer
 \lstinline$0$ to a pointer.
 …
 Note that the predefined identifiers have addresses.
+\CFA does not have C's concept of ``null pointer constants'', which are not typed values but special strings of tokens.
+The C token ``\lstinline$0$'' is an expression of type \lstinline$int$ with the value ``zero'', and it \emph{also} is a null pointer constant.
+Similarly,
+``\lstinline$(void *)0$ is an expression of type \lstinline$(void *)$ whose value is a null pointer, and it also is a null pointer constant.
+However, in C, ``\lstinline$(void *)(void *)0$'' is
+\emph{not} a null pointer constant, even though it is null-valued, a pointer, and constant! The semantics of C expressions contain many special cases to deal with subexpressions that are null pointer constants.
+\CFA handles these cases through overload resolution.
+The declaration
+\begin{lstlisting}
+forall( dtype DT ) DT * const 0;
+\end{lstlisting} means that \lstinline$0$ is a polymorphic object, and contains a value that can have \emph{any} pointer-to-object type or pointer-to-incomplete type.
+The only such value is the null pointer.
+Therefore the type \emph{alone} is enough to identify a null pointer.
+Where C defines an operator with a special case for the null pointer constant, \CFA defines predefined functions with a polymorphic object parameter.
+\CFA does not have C's concept of ``null pointer constants'', which are not typed values but
+special strings of tokens. The C token ``\lstinline$0$'' is an expression of type \lstinline$int$
+with the value ``zero'', and it \emph{also} is a null pointer constant. Similarly,
+``\lstinline$(void *)0$ is an expression of type \lstinline$(void *)$ whose value is a null pointer,
+and it also is a null pointer constant. However, in C, ``\lstinline$(void *)(void *)0$'' is
+\emph{not} a null pointer constant, even though it is null-valued, a pointer, and constant! The
+semantics of C expressions contain many special cases to deal with subexpressions that are null
+pointer constants.
+\CFA handles these cases through overload resolution. The declaration
+\begin{lstlisting}
+forall( dtype DT ) DT *const 0;
+\end{lstlisting}
+means that \lstinline$0$ is a polymorphic object, and contains a value that can have \emph{any}
+pointer-to-object type or pointer-to-incomplete type. The only such value is the null pointer.
+Therefore the type \emph{alone} is enough to identify a null pointer. Where C defines an operator
+with a special case for the null pointer constant, \CFA defines predefined functions with a
+polymorphic object parameter.
 \end{rationale}
 …
 \subsubsection{Generic selection}
+\constraints The best interpretation of the controlling expression shall be unambiguous\index{ambiguous interpretation}, and shall have type compatible with at most one of the types named in its generic association list.
+If a generic selection has no \lstinline$default$ generic association, the best interpretation of its controlling expression shall have type compatible with exactly one of the types named in its generic association list.
+\constraints The best interpretation of the controlling expression shall be
+unambiguous\index{ambiguous interpretation}, and shall have type compatible with at most one of the
+types named in its generic association list. If a generic selection has no \lstinline$default$
+generic association, the best interpretation of its controlling expression shall have type
+compatible with exactly one of the types named in its generic association list.
 \semantics
 …
 \rewriterules
 \begin{lstlisting}
 a[b] @\rewrite@ ?[?]( b, a ) // if a has integer type@\use{?[?]}@
+a[b] @\rewrite@ ?[?]( b, a ) // if a has integer type */@\use{?[?]}@
 a[b] @\rewrite@ ?[?]( a, b ) // otherwise
 a( @\emph{arguments}@ ) @\rewrite@ ?()( a, @\emph{arguments}@ )@\use{?()}@
+a( ${\em arguments }$ ) @\rewrite@ ?()( a, ${\em arguments} )$@\use{?()}@
 a++ @\rewrite@ ?++(&( a ))@\use{?++}@
 a-- @\rewrite@ ?--(&( a ))@\use{?--}@
 …
 \end{lstlisting}
 \semantics
+The interpretations of subscript expressions are the interpretations of the corresponding function call expressions.
+The interpretations of subscript expressions are the interpretations of the corresponding function
+call expressions.
 \begin{rationale}
 C defines subscripting as pointer arithmetic in a way that makes \lstinline$a[i]$ and
+\lstinline$i[a]$ equivalent. \CFA provides the equivalence through a rewrite rule to reduce the number of overloadings of \lstinline$?[?]$.
+Subscript expressions are rewritten as function calls that pass the first parameter by value.
+This is somewhat unfortunate, since array-like types tend to be large.
+The alternative is to use the rewrite rule ``\lstinline$a[b]$ \rewrite \lstinline$?[?](&(a), b)$''.
+However, C semantics forbid this approach: the \lstinline$a$ in ``\lstinline$a[b]$'' can be an arbitrary pointer value, which does not have an address.
+\lstinline$i[a]$ equivalent. \CFA provides the equivalence through a rewrite rule to reduce the
+number of overloadings of \lstinline$?[?]$.
+Subscript expressions are rewritten as function calls that pass the first parameter by value. This
+is somewhat unfortunate, since array-like types tend to be large. The alternative is to use the
+rewrite rule ``\lstinline$a[b]$ \rewrite \lstinline$?[?](&(a), b)$''. However, C semantics forbid
+this approach: the \lstinline$a$ in ``\lstinline$a[b]$'' can be an arbitrary pointer value, which
+does not have an address.
 The repetitive form of the predefined identifiers shows up a deficiency\index{deficiencies!pointers
+ to qualified types} of \CFA's type system.
+Type qualifiers are not included in type values, so polymorphic functions that take pointers to arbitrary types often come in one flavor for each possible qualification of the pointed-at type.
+ to qualified types} of \CFA's type system. Type qualifiers are not included in type values, so
+polymorphic functions that take pointers to arbitrary types often come in one flavor for each
+possible qualification of the pointed-at type.
 \end{rationale}
 …
 \semantics
+A \define{function designator} is an interpretation of an expression that has function type.
+The
+\nonterm{postfix-expression} in a function call may have some interpretations that are function designators and some that are not.
+For those interpretations of the \nonterm{postfix-expression} that are not function designators, the expression is rewritten and becomes a call of a function named ``\lstinline$?()$''.
+The valid interpretations of the rewritten expression are determined in the manner described below.
+Each combination of function designators and argument interpretations is considered.
+For those interpretations of the \nonterm{postfix-expression} that are \Index{monomorphic function} designators, the combination has a \Index{valid interpretation} if the function designator accepts the number of arguments given, and each argument interpretation matches the corresponding explicit parameter:
+A \define{function designator} is an interpretation of an expression that has function type. The
+\nonterm{postfix-expression} in a function call may have some interpretations that are function
+designators and some that are not.
+For those interpretations of the \nonterm{postfix-expression} that are not function designators, the
+expression is rewritten and becomes a call of a function named ``\lstinline$?()$''. The valid
+interpretations of the rewritten expression are determined in the manner described below.
+Each combination of function designators and argument interpretations is considered. For those
+interpretations of the \nonterm{postfix-expression} that are \Index{monomorphic function}
+designators, the combination has a \Index{valid interpretation} if the function designator accepts
+the number of arguments given, and each argument interpretation matches the corresponding explicit
+parameter:
 \begin{itemize}
+\item if the argument corresponds to a parameter in the function designator's prototype, the argument interpretation must have the same type as the corresponding parameter, or be implicitly convertible to the parameter's type
+\item if the function designator's type does not include a prototype or if the argument corresponds to
+\item
+if the argument corresponds to a parameter in the function designator's prototype, the argument
+interpretation must have the same type as the corresponding parameter, or be implicitly convertible
+to the parameter's type
+\item
+if the function designator's type does not include a prototype or if the argument corresponds to
 ``\lstinline$...$'' in a prototype, a \Index{default argument promotion} is applied to it.
 \end{itemize}
 …
 For those combinations where the interpretation of the \nonterm{postfix-expression} is a
+\Index{polymorphic function} designator and the function designator accepts the number of arguments given, there shall be at least one set of \define{implicit argument}s for the implicit parameters such that
+\Index{polymorphic function} designator and the function designator accepts the number of arguments
+given, there shall be at least one set of \define{implicit argument}s for the implicit parameters
+such that
 \begin{itemize}
 \item
+If the declaration of the implicit parameter uses \Index{type-class} \lstinline$type$\use{type}, the implicit argument must be an object type;
+if it uses \lstinline$dtype$, the implicit argument must be an object type or an incomplete type;
+and if it uses \lstinline$ftype$, the implicit argument must be a function type.
+\item if an explicit parameter's type uses any implicit parameters, then the corresponding explicit argument must have a type that is (or can be safely converted\index{safe conversion} to) the type produced by substituting the implicit arguments for the implicit parameters in the explicit parameter type.
+\item the remaining explicit arguments must match the remaining explicit parameters, as described for monomorphic function designators.
+\item for each \Index{assertion parameter} in the function designator's type, there must be an object or function with the same identifier that is visible at the call site and whose type is compatible with or can be specialized to the type of the assertion declaration.
+If the declaration of the implicit parameter uses \Index{type-class} \lstinline$type$\use{type}, the
+implicit argument must be an object type; if it uses \lstinline$dtype$, the implicit argument must
+be an object type or an incomplete type; and if it uses \lstinline$ftype$, the implicit argument
+must be a function type.
+\item
+if an explicit parameter's type uses any implicit parameters, then the corresponding explicit
+argument must have a type that is (or can be safely converted\index{safe conversion} to) the type
+produced by substituting the implicit arguments for the implicit parameters in the explicit
+parameter type.
+\item
+the remaining explicit arguments must match the remaining explicit parameters, as described for
+monomorphic function designators.
+\item
+for each \Index{assertion parameter} in the function designator's type, there must be an object or
+function with the same identifier that is visible at the call site and whose type is compatible with
+or can be specialized to the type of the assertion declaration.
 \end{itemize}
+There is a valid interpretation for each such set of implicit parameters.
+The type of each valid interpretation is the return type of the function designator with implicit parameter values substituted for the implicit arguments.
+A valid interpretation is ambiguous\index{ambiguous interpretation} if the function designator or any of the argument interpretations is ambiguous.
+Every valid interpretation whose return type is not compatible with any other valid interpretation's return type is an interpretation of the function call expression.
+Every set of valid interpretations that have mutually compatible\index{compatible type} result types also produces an interpretation of the function call expression.
+The type of the interpretation is the \Index{composite type} of the types of the valid interpretations, and the value of the interpretation is that of the \Index{best valid interpretation}.
+\begin{rationale}
+One desirable property of a polymorphic programming language is \define{generalizability}: the ability to replace an abstraction with a more general but equivalent abstraction without requiring changes in any of the uses of the original\cite{Cormack90}.
+For instance, it should be possible to replace a function ``\lstinline$int f( int );$'' with ``\lstinline$forall( type T ) T f( T );$'' without affecting any calls of \lstinline$f$.
+There is a valid interpretation for each such set of implicit parameters. The type of each valid
+interpretation is the return type of the function designator with implicit parameter values
+substituted for the implicit arguments.
+A valid interpretation is ambiguous\index{ambiguous interpretation} if the function designator or
+any of the argument interpretations is ambiguous.
+Every valid interpretation whose return type is not compatible with any other valid interpretation's
+return type is an interpretation of the function call expression.
+Every set of valid interpretations that have mutually compatible\index{compatible type} result types
+also produces an interpretation of the function call expression. The type of the interpretation is
+the \Index{composite type} of the types of the valid interpretations, and the value of the
+interpretation is that of the \Index{best valid interpretation}.
+\begin{rationale}
+One desirable property of a polymorphic programming language is \define{generalizability}: the
+ability to replace an abstraction with a more general but equivalent abstraction without requiring
+changes in any of the uses of the original\cite{Cormack90}. For instance, it should be possible to
+replace a function ``\lstinline$int f( int );$'' with ``\lstinline$forall( type T ) T f( T );$''
+without affecting any calls of \lstinline$f$.
 \CFA\index{deficiencies!generalizability} does not fully possess this property, because
 …
 float f;
 double d;
+f = g( f, f );          // (1)
+f = g( i, f );          // (2) (safe conversion to float)
+f = g( d, f );          // (3) (unsafe conversion to float)
+\end{lstlisting}
+If \lstinline$g$ was replaced by ``\lstinline$forall( type T ) T g( T, T );$'', the first and second calls would be unaffected, but the third would change: \lstinline$f$ would be converted to
+f = g( f, f );  // (1)
+f = g( i, f );  // (2) (safe conversion to float)
+f = g( d, f );  // (3) (unsafe conversion to float)
+\end{lstlisting}
+If \lstinline$g$ was replaced by ``\lstinline$forall( type T ) T g( T, T );$'', the first and second
+calls would be unaffected, but the third would change: \lstinline$f$ would be converted to
 \lstinline$double$, and the result would be a \lstinline$double$.
 Another example is the function ``\lstinline$void h( int *);$''.
+This function can be passed a
+\lstinline$void *$ argument, but the generalization ``\lstinline$forall( type T ) void h( T *);$'' can not.
+In this case, \lstinline$void$ is not a valid value for \lstinline$T$ because it is not an object type.
 If unsafe conversions were allowed, \lstinline$T$ could be inferred to be \emph{any} object type, which is undesirable.
+Another example is the function ``\lstinline$void h( int *);$''. This function can be passed a
+\lstinline$void *$ argument, but the generalization ``\lstinline$forall( type T ) void h( T *);$''
+can not. In this case, \lstinline$void$ is not a valid value for \lstinline$T$ because it is not an
+object type. If unsafe conversions were allowed, \lstinline$T$ could be inferred to be \emph{any}
+object type, which is undesirable.
 \end{rationale}
 …
 For that interpretation, the function call is treated as ``\lstinline$?()( sin_dx, 12.9 )$''.
 \begin{lstlisting}
 int f( long );          // (1)
 int f( int, int );      // (2)
+int f( long );          // (1)
+int f( int, int );      // (2)
 int f( int *);          // (3)
 int i = f( 5 );         // calls (1)
 \end{lstlisting}
+Function (1) provides a valid interpretation of ``\lstinline$f( 5 )$'', using an implicit \lstinline$int$ to \lstinline$long$ conversion.
+The other functions do not, since the second requires two arguments, and since there is no implicit conversion from \lstinline$int$ to \lstinline$int *$ that could be used with the third function.
+Function (1) provides a valid interpretation of ``\lstinline$f( 5 )$'', using an implicit
+\lstinline$int$ to \lstinline$long$ conversion. The other functions do not, since the second
+requires two arguments, and since there is no implicit conversion from \lstinline$int$ to
+\lstinline$int *$ that could be used with the third function.
 \begin{lstlisting}
 …
 \begin{lstlisting}
 forall( type T, type U ) void g( T, U );        // (4)
 forall( type T ) void g( T, T );                        // (5)
 forall( type T ) void g( T, long );                     // (6)
 void g( long, long );                                           // (7)
+forall( type T, type U ) void g( T, U );        // (4)
+forall( type T ) void g( T, T );                        // (5)
+forall( type T ) void g( T, long );                     // (6)
+void g( long, long );                                           // (7)
 double d;
 int i;
 int *p;
+g( d, d );                      // calls (5)
+g( d, i );                      // calls (6)
+g( i, i );                      // calls (7)
+g( d, d );                      // calls (5)
+g( d, i );                      // calls (6)
+g( i, i );                      // calls (7)
 g( i, p );                      // calls (4)
 \end{lstlisting}
+The first call has valid interpretations for all four versions of \lstinline$g$. (6) and (7) are discarded because they involve unsafe \lstinline$double$-to-\lstinline$long$ conversions. (5) is chosen because it is less polymorphic than (4).
+For the second call, (7) is again discarded.
+Of the remaining interpretations for (4), (5), and (6) (with \lstinline$i$ converted to \lstinline$long$), (6) is chosen because it is the least polymorphic.
+The third call has valid interpretations for all of the functions;
+(7) is chosen since it is not polymorphic at all.
+The fourth call has no interpretation for (5), because its arguments must have compatible type. (4) is chosen because it does not involve unsafe conversions.
+The first call has valid interpretations for all four versions of \lstinline$g$. (6) and (7) are
+discarded because they involve unsafe \lstinline$double$-to-\lstinline$long$ conversions. (5) is
+chosen because it is less polymorphic than (4).
+For the second call, (7) is again discarded. Of the remaining interpretations for (4), (5), and (6)
+(with \lstinline$i$ converted to \lstinline$long$), (6) is chosen because it is the least
+polymorphic.
+The third call has valid interpretations for all of the functions; (7) is chosen since it is not
+polymorphic at all.
+The fourth call has no interpretation for (5), because its arguments must have compatible type. (4)
+is chosen because it does not involve unsafe conversions.
 \begin{lstlisting}
 forall( type T ) T min( T, T );
 …
+}
 forall( type U | min_max( U ) ) void shuffle( U, U );
+shuffle( 9, 10 );
+\end{lstlisting}
+The only possibility for \lstinline$U$ is \lstinline$double$, because that is the type used in the only visible \lstinline$max$ function. 9 and 10 must be converted to \lstinline$double$, and
+shuffle(9, 10);
+\end{lstlisting}
+The only possibility for \lstinline$U$ is \lstinline$double$, because that is the type used in the
+only visible \lstinline$max$ function. 9 and 10 must be converted to \lstinline$double$, and
 \lstinline$min$ must be specialized with \lstinline$T$ bound to \lstinline$double$.
 \begin{lstlisting}
 extern void q( int );           // (8)
 extern void q( void * );        // (9)
+extern void q( int );           // (8)
+extern void q( void * );        // (9)
 extern void r();
 q( 0 );
 r( 0 );
 \end{lstlisting}
+The \lstinline$int 0$ could be passed to (8), or the \lstinline$(void *)$ \Index{specialization} of the null pointer\index{null pointer} \lstinline$0$\use{0} could be passed to (9).
+The former is chosen because the \lstinline$int$ \lstinline$0$ is \Index{less polymorphic}.
+For the same reason, \lstinline$int$ \lstinline$0$ is passed to \lstinline$r()$, even though it has \emph{no} declared parameter types.
+The \lstinline$int 0$ could be passed to (8), or the \lstinline$(void *)$ \Index{specialization} of
+the null pointer\index{null pointer} \lstinline$0$\use{0} could be passed to (9). The former is
+chosen because the \lstinline$int$ \lstinline$0$ is \Index{less polymorphic}. For
+the same reason, \lstinline$int$ \lstinline$0$ is passed to \lstinline$r()$, even though it has
+\emph{no} declared parameter types.
 \subsubsection{Structure and union members}
+\semantics In the member selection expression ``\lstinline$s$.\lstinline$m$'', there shall be at least one interpretation of \lstinline$s$ whose type is a structure type or union type containing a member named \lstinline$m$.
+If two or more interpretations of \lstinline$s$ have members named
+\lstinline$m$ with mutually compatible types, then the expression has an \Index{ambiguous interpretation} whose type is the composite type of the types of the members.
+If an interpretation of \lstinline$s$ has a member \lstinline$m$ whose type is not compatible with any other
+\lstinline$s$'s \lstinline$m$, then the expression has an interpretation with the member's type.
+The expression has no other interpretations.
+\semantics In the member selection expression ``\lstinline$s$.\lstinline$m$'', there shall be at
+least one interpretation of \lstinline$s$ whose type is a structure type or union type containing a
+member named \lstinline$m$. If two or more interpretations of \lstinline$s$ have members named
+\lstinline$m$ with mutually compatible types, then the expression has an \Index{ambiguous
+interpretation} whose type is the composite type of the types of the members. If an interpretation
+of \lstinline$s$ has a member \lstinline$m$ whose type is not compatible with any other
+\lstinline$s$'s \lstinline$m$, then the expression has an interpretation with the member's type. The
+expression has no other interpretations.
 The expression ``\lstinline$p->m$'' has the same interpretations as the expression
 …
 \predefined
 \begin{lstlisting}
+_Bool ?++( volatile _Bool * ), ?++( _Atomic volatile _Bool * );
+char ?++( volatile char * ), ?++( _Atomic volatile char * );
+signed char ?++( volatile signed char * ), ?++( _Atomic volatile signed char * );
+unsigned char ?++( volatile signed char * ), ?++( _Atomic volatile signed char * );
+short int ?++( volatile short int * ), ?++( _Atomic volatile short int * );
+unsigned short int ?++( volatile unsigned short int * ), ?++( _Atomic volatile unsigned short int * );
+int ?++( volatile int * ), ?++( _Atomic volatile int * );
+unsigned int ?++( volatile unsigned int * ), ?++( _Atomic volatile unsigned int * );
+long int ?++( volatile long int * ), ?++( _Atomic volatile long int * );
+long unsigned int ?++( volatile long unsigned int * ), ?++( _Atomic volatile long unsigned int * );
+long long int ?++( volatile long long int * ), ?++( _Atomic volatile long long int * );
+long long unsigned ?++( volatile long long unsigned int * ), ?++( _Atomic volatile long long unsigned int * );
+float ?++( volatile float * ), ?++( _Atomic volatile float * );
+double ?++( volatile double * ), ?++( _Atomic volatile double * );
+long double ?++( volatile long double * ), ?++( _Atomic volatile long double * );
+forall( type T ) T * ?++( T * restrict volatile * ), * ?++( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * ?++( _Atomic T * restrict volatile * ), * ?++( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * ?++( const T * restrict volatile * ), * ?++( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * ?++( volatile T * restrict volatile * ), * ?++( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * ?++( restrict T * restrict volatile * ), * ?++( restrict T * _Atomic restrict volatile * );
+_Bool ?++( volatile _Bool * ),
+        ?++( _Atomic volatile _Bool * );
+char ?++( volatile char * ),
+        ?++( _Atomic volatile char * );
+signed char ?++( volatile signed char * ),
+        ?++( _Atomic volatile signed char * );
+unsigned char ?++( volatile signed char * ),
+        ?++( _Atomic volatile signed char * );
+short int ?++( volatile short int * ),
+        ?++( _Atomic volatile short int * );
+unsigned short int ?++( volatile unsigned short int * ),
+        ?++( _Atomic volatile unsigned short int * );
+int ?++( volatile int * ),
+        ?++( _Atomic volatile int * );
+unsigned int ?++( volatile unsigned int * ),
+        ?++( _Atomic volatile unsigned int * );
+long int ?++( volatile long int * ),
+        ?++( _Atomic volatile long int * );
+long unsigned int ?++( volatile long unsigned int * ),
+        ?++( _Atomic volatile long unsigned int * );
+long long int ?++( volatile long long int * ),
+        ?++( _Atomic volatile long long int * );
+long long unsigned ?++( volatile long long unsigned int * ),
+        ?++( _Atomic volatile long long unsigned int * );
+float ?++( volatile float * ),
+        ?++( _Atomic volatile float * );
+double ?++( volatile double * ),
+        ?++( _Atomic volatile double * );
+long double ?++( volatile long double * ),
+        ?++( _Atomic volatile long double * );
+forall( type T ) T * ?++( T * restrict volatile * ),
+        * ?++( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * ?++( _Atomic T * restrict volatile * ),
+        * ?++( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * ?++( const T * restrict volatile * ),
+        * ?++( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * ?++( volatile T * restrict volatile * ),
+        * ?++( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * ?++( restrict T * restrict volatile * ),
+        * ?++( restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const T * ?++( _Atomic const T * restrict volatile * ),
         * ?++( _Atomic const T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict T * ?++( _Atomic restrict T * restrict volatile * ),
         * ?++( _Atomic restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic volatile T * ?++( _Atomic volatile T * restrict volatile * ),
         * ?++( _Atomic volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict T * ?++( const restrict T * restrict volatile * ),
         * ?++( const restrict T * _Atomic restrict volatile * );
 forall( type T ) const volatile T * ?++( const volatile T * restrict volatile * ),
         * ?++( const volatile T * _Atomic restrict volatile * );
 forall( type T ) restrict volatile T * ?++( restrict volatile T * restrict volatile * ),
         * ?++( restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict T * ?++( _Atomic const restrict T * restrict volatile * ),
         * ?++( _Atomic const restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const volatile T * ?++( _Atomic const volatile T * restrict volatile * ),
         * ?++( _Atomic const volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict volatile T * ?++( _Atomic restrict volatile T * restrict volatile * ),
         * ?++( _Atomic restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict volatile T * ?++( const restrict volatile T * restrict volatile * ),
         * ?++( const restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict volatile T * ?++( _Atomic const restrict volatile T * restrict volatile * ),
         * ?++( _Atomic const restrict volatile T * _Atomic restrict volatile * );
+_Bool ?--( volatile _Bool * ), ?--( _Atomic volatile _Bool * );
+char ?--( volatile char * ), ?--( _Atomic volatile char * );
+signed char ?--( volatile signed char * ), ?--( _Atomic volatile signed char * );
+unsigned char ?--( volatile signed char * ), ?--( _Atomic volatile signed char * );
+short int ?--( volatile short int * ), ?--( _Atomic volatile short int * );
+unsigned short int ?--( volatile unsigned short int * ), ?--( _Atomic volatile unsigned short int * );
+int ?--( volatile int * ), ?--( _Atomic volatile int * );
+unsigned int ?--( volatile unsigned int * ), ?--( _Atomic volatile unsigned int * );
+long int ?--( volatile long int * ), ?--( _Atomic volatile long int * );
+long unsigned int ?--( volatile long unsigned int * ), ?--( _Atomic volatile long unsigned int * );
+long long int ?--( volatile long long int * ), ?--( _Atomic volatile long long int * );
+long long unsigned ?--( volatile long long unsigned int * ), ?--( _Atomic volatile long long unsigned int * );
+float ?--( volatile float * ), ?--( _Atomic volatile float * );
+double ?--( volatile double * ), ?--( _Atomic volatile double * );
+long double ?--( volatile long double * ), ?--( _Atomic volatile long double * );
+forall( type T ) T * ?--( T * restrict volatile * ), * ?--( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * ?--( _Atomic T * restrict volatile * ), * ?--( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * ?--( const T * restrict volatile * ), * ?--( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * ?--( volatile T * restrict volatile * ), * ?--( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * ?--( restrict T * restrict volatile * ), * ?--( restrict T * _Atomic restrict volatile * );
+_Bool ?--( volatile _Bool * ),
+        ?--( _Atomic volatile _Bool * );
+char ?--( volatile char * ),
+        ?--( _Atomic volatile char * );
+signed char ?--( volatile signed char * ),
+        ?--( _Atomic volatile signed char * );
+unsigned char ?--( volatile signed char * ),
+        ?--( _Atomic volatile signed char * );
+short int ?--( volatile short int * ),
+        ?--( _Atomic volatile short int * );
+unsigned short int ?--( volatile unsigned short int * ),
+        ?--( _Atomic volatile unsigned short int * );
+int ?--( volatile int * ),
+        ?--( _Atomic volatile int * );
+unsigned int ?--( volatile unsigned int * ),
+        ?--( _Atomic volatile unsigned int * );
+long int ?--( volatile long int * ),
+        ?--( _Atomic volatile long int * );
+long unsigned int ?--( volatile long unsigned int * ),
+        ?--( _Atomic volatile long unsigned int * );
+long long int ?--( volatile long long int * ),
+        ?--( _Atomic volatile long long int * );
+long long unsigned ?--( volatile long long unsigned int * ),
+        ?--( _Atomic volatile long long unsigned int * );
+float ?--( volatile float * ),
+        ?--( _Atomic volatile float * );
+double ?--( volatile double * ),
+        ?--( _Atomic volatile double * );
+long double ?--( volatile long double * ),
+        ?--( _Atomic volatile long double * );
+forall( type T ) T * ?--( T * restrict volatile * ),
+        * ?--( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * ?--( _Atomic T * restrict volatile * ),
+        * ?--( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * ?--( const T * restrict volatile * ),
+        * ?--( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * ?--( volatile T * restrict volatile * ),
+        * ?--( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * ?--( restrict T * restrict volatile * ),
+        * ?--( restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const T * ?--( _Atomic const T * restrict volatile * ),
         * ?--( _Atomic const T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict T * ?--( _Atomic restrict T * restrict volatile * ),
         * ?--( _Atomic restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic volatile T * ?--( _Atomic volatile T * restrict volatile * ),
         * ?--( _Atomic volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict T * ?--( const restrict T * restrict volatile * ),
         * ?--( const restrict T * _Atomic restrict volatile * );
 forall( type T ) const volatile T * ?--( const volatile T * restrict volatile * ),
         * ?--( const volatile T * _Atomic restrict volatile * );
 forall( type T ) restrict volatile T * ?--( restrict volatile T * restrict volatile * ),
         * ?--( restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict T * ?--( _Atomic const restrict T * restrict volatile * ),
         * ?--( _Atomic const restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const volatile T * ?--( _Atomic const volatile T * restrict volatile * ),
         * ?--( _Atomic const volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict volatile T * ?--( _Atomic restrict volatile T * restrict volatile * ),
         * ?--( _Atomic restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict volatile T * ?--( const restrict volatile T * restrict volatile * ),
         * ?--( const restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict volatile T * ?--( _Atomic const restrict volatile T * restrict volatile * ),
         * ?--( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 …
 \begin{rationale}
+Note that ``\lstinline$++$'' and ``\lstinline$--$'' are rewritten as function calls that are given a pointer to that operand. (This is true of all operators that modify an operand.) As Hamish Macdonald has pointed out, this forces the modified operand of such expressions to be an lvalue.
+This partially enforces the C semantic rule that such operands must be \emph{modifiable} lvalues.
+\end{rationale}
+\begin{rationale}
+In C, a semantic rule requires that pointer operands of increment and decrement be pointers to object types.
+Hence, \lstinline$void *$ objects cannot be incremented.
+In \CFA, the restriction follows from the use of a \lstinline$type$ parameter in the predefined function definitions, as opposed to \lstinline$dtype$, since only object types can be inferred arguments corresponding to the type parameter \lstinline$T$.
+Note that ``\lstinline$++$'' and ``\lstinline$--$'' are rewritten as function calls that are given a
+pointer to that operand. (This is true of all operators that modify an operand.) As Hamish Macdonald
+has pointed out, this forces the modified operand of such expressions to be an lvalue. This
+partially enforces the C semantic rule that such operands must be \emph{modifiable} lvalues.
+\end{rationale}
+\begin{rationale}
+In C, a semantic rule requires that pointer operands of increment and decrement be pointers to
+object types. Hence, \lstinline$void *$ objects cannot be incremented. In \CFA, the restriction
+follows from the use of a \lstinline$type$ parameter in the predefined function definitions, as
+opposed to \lstinline$dtype$, since only object types can be inferred arguments corresponding to the
+type parameter \lstinline$T$.
 \end{rationale}
 \semantics
+First, each interpretation of the operand of an increment or decrement expression is considered separately.
+For each interpretation that is a bit-field or is declared with the
+\lstinline$register$\index{register@{\lstinline$register$}} \index{Itorage-class specifier}, the expression has one valid interpretation, with the type of the operand, and the expression is ambiguous if the operand is.
+For the remaining interpretations, the expression is rewritten, and the interpretations of the expression are the interpretations of the corresponding function call.
+Finally, all interpretations of the expression produced for the different interpretations of the operand are combined to produce the interpretations of the expression as a whole; where interpretations have compatible result types, the best interpretations are selected in the manner described for function call expressions.
+First, each interpretation of the operand of an increment or decrement expression is considered
+separately. For each interpretation that is a bit-field or is declared with the
+\lstinline$register$\index{register@{\lstinline$register$}} \index{Itorage-class specifier}, the
+expression has one valid interpretation, with the type of the operand, and the expression is
+ambiguous if the operand is.
+For the remaining interpretations, the expression is rewritten, and the interpretations of the
+expression are the interpretations of the corresponding function call. Finally, all interpretations
+of the expression produced for the different interpretations of the operand are combined to produce
+the interpretations of the expression as a whole; where interpretations have compatible result
+types, the best interpretations are selected in the manner described for function call expressions.
 \examples
 …
 \lstinline$vs++$ calls the \lstinline$?++$ function with the \lstinline$volatile short *$ parameter.
 \lstinline$s++$ does the same, applying the safe conversion from \lstinline$short int *$ to
+\lstinline$volatile short int *$.
+Note that there is no conversion that adds an \lstinline$_Atomic$ qualifier, so the \lstinline$_Atomic volatile short int$ overloading does not provide a valid interpretation.
+\lstinline$volatile short int *$. Note that there is no conversion that adds an \lstinline$_Atomic$
+qualifier, so the \lstinline$_Atomic volatile short int$ overloading does not provide a valid
+interpretation.
 \end{sloppypar}
+There is no safe conversion from \lstinline$const short int *$ to \lstinline$volatile short int *$, and no \lstinline$?++$ function that accepts a \lstinline$const *$ parameter, so \lstinline$cs++$ has no valid interpretations.
+The best valid interpretation of \lstinline$as++$ calls the \lstinline$short ?++$ function with the \lstinline$_Atomic volatile short int *$ parameter, applying a safe conversion to add the \lstinline$volatile$ qualifier.
+\begin{lstlisting}
+char * const restrict volatile * restrict volatile pqpc;
+pqpc++
+char * * restrict volatile ppc;
+ppc++;
+\end{lstlisting}
+Since \lstinline$&(pqpc)$ has type \lstinline$char * const restrict volatile * restrict volatile *$, the best valid interpretation of \lstinline$pqpc++$ calls the polymorphic \lstinline$?++$ function with the \lstinline$const restrict volatile T * restrict volatile *$ parameter, inferring \lstinline$T$ to be \lstinline$char *$.
+\lstinline$ppc++$ calls the same function, again inferring \lstinline$T$ to be \lstinline$char *$, and using the safe conversions from \lstinline$T$ to \lstinline$T const$ \lstinline$restrict volatile$.
+\begin{rationale}
+Increment and decrement expressions show up a deficiency of \CFA's type system.
+There is no such thing as a pointer to a register object or bit-field\index{deficiencies!pointers to bit-fields}.
+Therefore, there is no way to define a function that alters them, and hence no way to define increment and decrement functions for them.
+As a result, the semantics of increment and decrement expressions must treat them specially.
+This holds true for all of the operators that may modify such objects.
+\end{rationale}
+\begin{rationale}
+The polymorphic overloadings for pointer increment and decrement can be understood by considering increasingly complex types.
+There is no safe conversion from \lstinline$const short int *$ to \lstinline$volatile short int *$,
+and no \lstinline$?++$ function that accepts a \lstinline$const *$ parameter, so \lstinline$cs++$
+has no valid interpretations.
+The best valid interpretation of \lstinline$as++$ calls the \lstinline$short ?++$ function with the
+\lstinline$_Atomic volatile short int *$ parameter, applying a safe conversion to add the
+\lstinline$volatile$ qualifier.
+\begin{lstlisting}
+char * const restrict volatile * restrict volatile pqpc; pqpc++
+char * * restrict volatile ppc; ppc++;
+\end{lstlisting}
+Since \lstinline$&(pqpc)$ has type \lstinline$char * const restrict volatile * restrict volatile *$,
+the best valid interpretation of \lstinline$pqpc++$ calls the polymorphic \lstinline$?++$ function
+with the \lstinline$const restrict volatile T * restrict volatile *$ parameter, inferring
+\lstinline$T$ to be \lstinline$char *$.
+\begin{sloppypar}
+\lstinline$ppc++$ calls the same function, again inferring \lstinline$T$ to be \lstinline$char *$,
+and using the safe conversions from \lstinline$T$ to \lstinline$T const restrict volatile$.
+\end{sloppypar}
+\begin{rationale}
+Increment and decrement expressions show up a deficiency of \CFA's type system. There is no such
+thing as a pointer to a register object or bit-field\index{deficiencies!pointers to bit-fields}.
+Therefore, there is no way to define a function that alters them, and hence no way to define
+increment and decrement functions for them. As a result, the semantics of increment and decrement
+expressions must treat them specially. This holds true for all of the operators that may modify
+such objects.
+\end{rationale}
+\begin{rationale}
+The polymorphic overloadings for pointer increment and decrement can be understood by considering
+increasingly complex types.
 \begin{enumerate}
 \item
 ``\lstinline$char * p; p++;$''.
+The argument to \lstinline$?++$ has type \lstinline$char * *$, and the result has type \lstinline$char *$.
 The expression would be valid if \lstinline$?++$ were declared by
+``\lstinline$char * p; p++;$''. The argument to \lstinline$?++$ has type \lstinline$char * *$, and
+the result has type \lstinline$char *$. The expression would be valid if \lstinline$?++$ were
+declared by
 \begin{lstlisting}
 forall( type T ) T * ?++( T * * );
+\end{lstlisting} with \lstinline$T$ inferred to be \lstinline$char$.
+\item
+``\lstinline$char *restrict volatile qp; qp++$''.
+The result again has type \lstinline$char *$, but the argument now has type \lstinline$char *restrict volatile *$, so it cannot be passed to the hypothetical function declared in point 1.
+Hence the actual predefined function is
+\end{lstlisting}
+with \lstinline$T$ inferred to be \lstinline$char$.
+\item
+``\lstinline$char *restrict volatile qp; qp++$''. The result again has type \lstinline$char *$, but
+the argument now has type \lstinline$char *restrict volatile *$, so it cannot be passed to the
+hypothetical function declared in point 1. Hence the actual predefined function is
 \begin{lstlisting}
 forall( type T ) T * ?++( T * restrict volatile * );
+\end{lstlisting} which also accepts a \lstinline$char * *$ argument, because of the safe conversions that add
+\lstinline$volatile$ and \lstinline$restrict$ qualifiers. (The parameter is not const-qualified, so constant pointers cannot be incremented.)
+\item
+``\lstinline$char *_Atomic ap; ap++$''.
+The result again has type \lstinline$char *$, but no safe conversion adds an \lstinline$_Atomic$ qualifier, so the function in point 2 is not applicable.
+A separate overloading of \lstinline$?++$ is required.
+\item
+``\lstinline$char const volatile * pq; pq++$''.
+Here the result has type
+\end{lstlisting}
+which also accepts a \lstinline$char * *$ argument, because of the safe conversions that add
+\lstinline$volatile$ and \lstinline$restrict$ qualifiers. (The parameter is not const-qualified, so
+constant pointers cannot be incremented.)
+\item
+``\lstinline$char *_Atomic ap; ap++$''. The result again has type \lstinline$char *$, but no safe
+conversion adds an \lstinline$_Atomic$ qualifier, so the function in point 2 is not applicable. A
+separate overloading of \lstinline$?++$ is required.
+\item
+``\lstinline$char const volatile * pq; pq++$''. Here the result has type
 \lstinline$char const volatile *$, so a new overloading is needed:
 \begin{lstlisting}
 forall( type T ) T const volatile * ?++( T const volatile *restrict volatile * );
 \end{lstlisting}
+One overloading is needed for each combination of qualifiers in the pointed-at type\index{deficiencies!pointers to qualified types}.
+One overloading is needed for each combination of qualifiers in the pointed-at
+type\index{deficiencies!pointers to qualified types}.
 \item
 ``\lstinline$float *restrict * prp; prp++$''.
 The \lstinline$restrict$ qualifier is handled just like \lstinline$const$ and \lstinline$volatile$ in the previous case:
+``\lstinline$float *restrict * prp; prp++$''. The \lstinline$restrict$ qualifier is handled just
+like \lstinline$const$ and \lstinline$volatile$ in the previous case:
 \begin{lstlisting}
 forall( type T ) T restrict * ?++( T restrict *restrict volatile * );
+\end{lstlisting} with \lstinline$T$ inferred to be \lstinline$float *$.
+This looks odd, because {\c11} contains a constraint that requires restrict-qualified types to be pointer-to-object types, and \lstinline$T$ is not syntactically a pointer type. \CFA loosens the constraint.
+\end{lstlisting}
+with \lstinline$T$ inferred to be \lstinline$float *$. This looks odd, because {\c11} contains a
+constraint that requires restrict-qualified types to be pointer-to-object types, and \lstinline$T$
+is not syntactically a pointer type. \CFA loosens the constraint.
 \end{enumerate}
 \end{rationale}
 …
 \semantics
+A compound literal has one interpretation, with the type given by the \nonterm{type-name} of the compound literal.
+A compound literal has one interpretation, with the type given by the \nonterm{type-name} of the
+compound literal.
 …
 \rewriterules
 \begin{lstlisting}
 *a      @\rewrite@ *?( a ) @\use{*?}@
 +a      @\rewrite@ +?( a ) @\use{+?}@
 -a      @\rewrite@ -?( a ) @\use{-?}@
 ~a      @\rewrite@ ~?( a ) @\use{~?}@
 !a      @\rewrite@ !?( a ) @\use{"!?}@
 ++a     @\rewrite@ ++?(&( a )) @\use{++?}@
 --a     @\rewrite@ --?(&( a )) @\use{--?}@
+*a      @\rewrite@ *?(a) @\use{*?}@
++a      @\rewrite@ +?(a) @\use{+?}@
+-a      @\rewrite@ -?(a) @\use{-?}@
+~a      @\rewrite@ ~?(a) @\use{~?}@
+!a      @\rewrite@ !?(a) @\use{"!?}@
+++a     @\rewrite@ ++?(&(a)) @\use{++?}@
+--a     @\rewrite@ --?(&(a)) @\use{--?}@
 \end{lstlisting}
 …
 \predefined
 \begin{lstlisting}
+_Bool ++?( volatile _Bool * ), ++?( _Atomic volatile _Bool * );
+char ++?( volatile char * ), ++?( _Atomic volatile char * );
+signed char ++?( volatile signed char * ), ++?( _Atomic volatile signed char * );
+unsigned char ++?( volatile signed char * ), ++?( _Atomic volatile signed char * );
+short int ++?( volatile short int * ), ++?( _Atomic volatile short int * );
+unsigned short int ++?( volatile unsigned short int * ), ++?( _Atomic volatile unsigned short int * );
+int ++?( volatile int * ), ++?( _Atomic volatile int * );
+unsigned int ++?( volatile unsigned int * ), ++?( _Atomic volatile unsigned int * );
+long int ++?( volatile long int * ), ++?( _Atomic volatile long int * );
+long unsigned int ++?( volatile long unsigned int * ), ++?( _Atomic volatile long unsigned int * );
+long long int ++?( volatile long long int * ), ++?( _Atomic volatile long long int * );
+long long unsigned ++?( volatile long long unsigned int * ), ++?( _Atomic volatile long long unsigned int * );
+float ++?( volatile float * ), ++?( _Atomic volatile float * );
+double ++?( volatile double * ), ++?( _Atomic volatile double * );
+long double ++?( volatile long double * ), ++?( _Atomic volatile long double * );
+forall( type T ) T * ++?( T * restrict volatile * ), * ++?( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * ++?( _Atomic T * restrict volatile * ), * ++?( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * ++?( const T * restrict volatile * ), * ++?( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * ++?( volatile T * restrict volatile * ), * ++?( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * ++?( restrict T * restrict volatile * ), * ++?( restrict T * _Atomic restrict volatile * );
+_Bool ++?( volatile _Bool * ),
+        ++?( _Atomic volatile _Bool * );
+char ++?( volatile char * ),
+        ++?( _Atomic volatile char * );
+signed char ++?( volatile signed char * ),
+        ++?( _Atomic volatile signed char * );
+unsigned char ++?( volatile signed char * ),
+        ++?( _Atomic volatile signed char * );
+short int ++?( volatile short int * ),
+        ++?( _Atomic volatile short int * );
+unsigned short int ++?( volatile unsigned short int * ),
+        ++?( _Atomic volatile unsigned short int * );
+int ++?( volatile int * ),
+        ++?( _Atomic volatile int * );
+unsigned int ++?( volatile unsigned int * ),
+        ++?( _Atomic volatile unsigned int * );
+long int ++?( volatile long int * ),
+        ++?( _Atomic volatile long int * );
+long unsigned int ++?( volatile long unsigned int * ),
+        ++?( _Atomic volatile long unsigned int * );
+long long int ++?( volatile long long int * ),
+        ++?( _Atomic volatile long long int * );
+long long unsigned ++?( volatile long long unsigned int * ),
+        ++?( _Atomic volatile long long unsigned int * );
+float ++?( volatile float * ),
+        ++?( _Atomic volatile float * );
+double ++?( volatile double * ),
+        ++?( _Atomic volatile double * );
+long double ++?( volatile long double * ),
+        ++?( _Atomic volatile long double * );
+forall( type T ) T * ++?( T * restrict volatile * ),
+        * ++?( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * ++?( _Atomic T * restrict volatile * ),
+        * ++?( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * ++?( const T * restrict volatile * ),
+        * ++?( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * ++?( volatile T * restrict volatile * ),
+        * ++?( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * ++?( restrict T * restrict volatile * ),
+        * ++?( restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const T * ++?( _Atomic const T * restrict volatile * ),
         * ++?( _Atomic const T * _Atomic restrict volatile * );
 forall( type T ) _Atomic volatile T * ++?( _Atomic volatile T * restrict volatile * ),
         * ++?( _Atomic volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict T * ++?( _Atomic restrict T * restrict volatile * ),
         * ++?( _Atomic restrict T * _Atomic restrict volatile * );
 forall( type T ) const volatile T * ++?( const volatile T * restrict volatile * ),
         * ++?( const volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict T * ++?( const restrict T * restrict volatile * ),
         * ++?( const restrict T * _Atomic restrict volatile * );
 forall( type T ) restrict volatile T * ++?( restrict volatile T * restrict volatile * ),
         * ++?( restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const volatile T * ++?( _Atomic const volatile T * restrict volatile * ),
         * ++?( _Atomic const volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict T * ++?( _Atomic const restrict T * restrict volatile * ),
         * ++?( _Atomic const restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict volatile T * ++?( _Atomic restrict volatile T * restrict volatile * ),
         * ++?( _Atomic restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict volatile T * ++?( const restrict volatile T * restrict volatile * ),
         * ++?( const restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict volatile T * ++?( _Atomic const restrict volatile T * restrict volatile * ),
         * ++?( _Atomic const restrict volatile T * _Atomic restrict volatile * );
+_Bool --?( volatile _Bool * ), --?( _Atomic volatile _Bool * );
+char --?( volatile char * ), --?( _Atomic volatile char * );
+signed char --?( volatile signed char * ), --?( _Atomic volatile signed char * );
+unsigned char --?( volatile signed char * ), --?( _Atomic volatile signed char * );
+short int --?( volatile short int * ), --?( _Atomic volatile short int * );
+unsigned short int --?( volatile unsigned short int * ), --?( _Atomic volatile unsigned short int * );
+int --?( volatile int * ), --?( _Atomic volatile int * );
+unsigned int --?( volatile unsigned int * ), --?( _Atomic volatile unsigned int * );
+long int --?( volatile long int * ), --?( _Atomic volatile long int * );
+long unsigned int --?( volatile long unsigned int * ), --?( _Atomic volatile long unsigned int * );
+long long int --?( volatile long long int * ), --?( _Atomic volatile long long int * );
+long long unsigned --?( volatile long long unsigned int * ), --?( _Atomic volatile long long unsigned int * );
+float --?( volatile float * ), --?( _Atomic volatile float * );
+double --?( volatile double * ), --?( _Atomic volatile double * );
+long double --?( volatile long double * ), --?( _Atomic volatile long double * );
+forall( type T ) T * --?( T * restrict volatile * ), * --?( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * --?( _Atomic T * restrict volatile * ), * --?( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * --?( const T * restrict volatile * ), * --?( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * --?( volatile T * restrict volatile * ), * --?( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * --?( restrict T * restrict volatile * ), * --?( restrict T * _Atomic restrict volatile * );
+_Bool --?( volatile _Bool * ),
+        --?( _Atomic volatile _Bool * );
+char --?( volatile char * ),
+        --?( _Atomic volatile char * );
+signed char --?( volatile signed char * ),
+        --?( _Atomic volatile signed char * );
+unsigned char --?( volatile signed char * ),
+        --?( _Atomic volatile signed char * );
+short int --?( volatile short int * ),
+        --?( _Atomic volatile short int * );
+unsigned short int --?( volatile unsigned short int * ),
+        --?( _Atomic volatile unsigned short int * );
+int --?( volatile int * ),
+        --?( _Atomic volatile int * );
+unsigned int --?( volatile unsigned int * ),
+        --?( _Atomic volatile unsigned int * );
+long int --?( volatile long int * ),
+        --?( _Atomic volatile long int * );
+long unsigned int --?( volatile long unsigned int * ),
+        --?( _Atomic volatile long unsigned int * );
+long long int --?( volatile long long int * ),
+        --?( _Atomic volatile long long int * );
+long long unsigned --?( volatile long long unsigned int * ),
+        --?( _Atomic volatile long long unsigned int * );
+float --?( volatile float * ),
+        --?( _Atomic volatile float * );
+double --?( volatile double * ),
+        --?( _Atomic volatile double * );
+long double --?( volatile long double * ),
+        --?( _Atomic volatile long double * );
+forall( type T ) T * --?( T * restrict volatile * ),
+        * --?( T * _Atomic restrict volatile * );
+forall( type T ) _Atomic T * --?( _Atomic T * restrict volatile * ),
+        * --?( _Atomic T * _Atomic restrict volatile * );
+forall( type T ) const T * --?( const T * restrict volatile * ),
+        * --?( const T * _Atomic restrict volatile * );
+forall( type T ) volatile T * --?( volatile T * restrict volatile * ),
+        * --?( volatile T * _Atomic restrict volatile * );
+forall( type T ) restrict T * --?( restrict T * restrict volatile * ),
+        * --?( restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const T * --?( _Atomic const T * restrict volatile * ),
         * --?( _Atomic const T * _Atomic restrict volatile * );
 forall( type T ) _Atomic volatile T * --?( _Atomic volatile T * restrict volatile * ),
         * --?( _Atomic volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict T * --?( _Atomic restrict T * restrict volatile * ),
         * --?( _Atomic restrict T * _Atomic restrict volatile * );
 forall( type T ) const volatile T * --?( const volatile T * restrict volatile * ),
         * --?( const volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict T * --?( const restrict T * restrict volatile * ),
         * --?( const restrict T * _Atomic restrict volatile * );
 forall( type T ) restrict volatile T * --?( restrict volatile T * restrict volatile * ),
         * --?( restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const volatile T * --?( _Atomic const volatile T * restrict volatile * ),
         * --?( _Atomic const volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict T * --?( _Atomic const restrict T * restrict volatile * ),
         * --?( _Atomic const restrict T * _Atomic restrict volatile * );
 forall( type T ) _Atomic restrict volatile T * --?( _Atomic restrict volatile T * restrict volatile * ),
         * --?( _Atomic restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) const restrict volatile T * --?( const restrict volatile T * restrict volatile * ),
         * --?( const restrict volatile T * _Atomic restrict volatile * );
 forall( type T ) _Atomic const restrict volatile T * --?( _Atomic const restrict volatile T * restrict volatile * ),
         * --?( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 …
 \semantics
+The interpretations of prefix increment and decrement expressions are determined in the same way as the interpretations of postfix increment and decrement expressions.
+The interpretations of prefix increment and decrement expressions are
+determined in the same way as the interpretations of postfix increment and
+decrement expressions.
 …
 forall( type T ) const restrict volatile lvalue T *?( const restrict volatile T * );
 forall( type T ) _Atomic const restrict volatile lvalue T *?( _Atomic const restrict volatile T * );
 forall( ftype FT ) FT *?( FT * );
 \end{lstlisting}
 …
 \lstinline$T$ is the type of the operand.
+The interpretations of an indirection expression are the interpretations of the corresponding function call.
+The interpretations of an indirection expression are the interpretations of the corresponding
+function call.
 …
 \predefined
 \begin{lstlisting}
+int     +?( int ), -?( int ), ~?( int );
+unsigned int +?( unsigned int ), -?( unsigned int ), ~?( unsigned int );
+long int +?( long int ), -?( long int ), ~?( long int );
+long unsigned int +?( long unsigned int ), -?( long unsigned int ), ~?( long unsigned int );
+long long int +?( long long int ), -?( long long int ), ~?( long long int );
+long long unsigned int +?( long long unsigned int ), -?( long long unsigned int ), ~?( long long unsigned int );
+float +?( float ), -?( float );
+double +?( double ), -?( double );
+long double +?( long double ), -?( long double );
+_Complex float +?( _Complex float ), -?( _Complex float );
+_Complex double +?( _Complex double ), -?( _Complex double );
+_Complex long double +?( _Complex long double ), -?( _Complex long double );
+int !?( int ), !?( unsigned int ), !?( long ), !?( long unsigned int ),
+        !?( long long int ), !?( long long unsigned int ),
+        !?( float ), !?( double ), !?( long double ),
+        !?( _Complex float ), !?( _Complex double ), !?( _Complex long double );
+int
+        +?( int ),
+        -?( int ),
+        ~?( int );
+unsigned int
+        +?( unsigned int ),
+        -?( unsigned int ),
+         ~?( unsigned int );
+long int
+        +?( long int ),
+        -?( long int ),
+        ~?( long int );
+long unsigned int
+        +?( long unsigned int ),
+        -?( long unsigned int ),
+        ~?( long unsigned int );
+long long int
+        +?( long long int ),
+        -?( long long int ),
+        ~?( long long int );
+long long unsigned int
+        +?( long long unsigned int ),
+        -?( long long unsigned int ),
+        ~?( long long unsigned int );
+float
+        +?( float ),
+        -?( float );
+double
+        +?( double ),
+        -?( double );
+long double
+        +?( long double ),
+        -?( long double );
+_Complex float
+        +?( _Complex float ),
+        -?( _Complex float );
+_Complex double
+        +?( _Complex double ),
+        -?( _Complex double );
+_Complex long double
+        +?( _Complex long double ),
+        -?( _Complex long double );
+int !?( int ),
+        !?( unsigned int ),
+        !?( long ),
+        !?( long unsigned int ),
+        !?( long long int ),
+        !?( long long unsigned int ),
+        !?( float ),
+        !?( double ),
+        !?( long double ),
+        !?( _Complex float ),
+        !?( _Complex double ),
+        !?( _Complex long double );
 forall( dtype DT ) int !?( const restrict volatile DT * );
 forall( dtype DT ) int !?( _Atomic const restrict volatile DT * );
 forall( ftype FT ) int !?( FT * );
 \end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \semantics
+The interpretations of a unary arithmetic expression are the interpretations of the corresponding function call.
+The interpretations of a unary arithmetic expression are the interpretations of the corresponding
+function call.
 \examples
 …
 long int li;
 void eat_double( double );@\use{eat_double}@
+eat_double(-li ); // @\rewrite@ eat_double( -?( li ) );
+eat_double(-li ); // @\rewrite@ eat_double( -?( li ) );
 \end{lstlisting}
 The valid interpretations of ``\lstinline$-li$'' (assuming no extended integer types exist) are
 \begin{center}
+\begin{tabular}{llc} interpretation & result type & expression conversion cost \\
+\begin{tabular}{llc}
+interpretation & result type & expression conversion cost \\
 \hline
 \lstinline$-?( (int)li )$                                       & \lstinline$int$                                       & (unsafe) \\
 …
 \end{tabular}
 \end{center}
+The valid interpretations of the \lstinline$eat_double$ call, with the cost of the argument conversion and the cost of the entire expression, are
+The valid interpretations of the \lstinline$eat_double$ call, with the cost of the argument
+conversion and the cost of the entire expression, are
 \begin{center}
+\begin{tabular}{lcc} interpretation & argument cost & expression cost \\
+\begin{tabular}{lcc}
+interpretation & argument cost & expression cost \\
 \hline
 \lstinline$eat_double( (double)-?( (int)li) )$                                  & 7                     & (unsafe) \\
 …
 \end{tabular}
 \end{center}
+Each has result type \lstinline$void$, so the best must be selected.
+The interpretations involving unsafe conversions are discarded.
+The remainder have equal expression conversion costs, so the
+Each has result type \lstinline$void$, so the best must be selected. The interpretations involving
+unsafe conversions are discarded. The remainder have equal expression conversion costs, so the
 ``highest argument conversion cost'' rule is invoked, and the chosen interpretation is
 \lstinline$eat_double( (double)-?(li) )$.
 …
 \lstinline$dtype$, or \lstinline$ftype$.
+When the \lstinline$sizeof$\use{sizeof} operator is applied to an expression, the expression shall have exactly one \Index{interpretation}\index{ambiguous interpretation}, which shall be unambiguous. \semantics A \lstinline$sizeof$ or \lstinline$_Alignof$ expression has one interpretation, of type \lstinline$size_t$.
+When the \lstinline$sizeof$\use{sizeof} operator is applied to an expression, the expression shall
+have exactly one \Index{interpretation}\index{ambiguous interpretation}, which shall
+be unambiguous. \semantics A \lstinline$sizeof$ or \lstinline$_Alignof$ expression has one
+interpretation, of type \lstinline$size_t$.
 When \lstinline$sizeof$ is applied to an identifier declared by a \nonterm{type-declaration} or a
+\nonterm{type-parameter}, it yields the size in bytes of the type that implements the operand.
+When the operand is an opaque type or an inferred type parameter\index{inferred parameter}, the expression is not a constant expression.
+\nonterm{type-parameter}, it yields the size in bytes of the type that implements the operand. When
+the operand is an opaque type or an inferred type parameter\index{inferred parameter}, the
+expression is not a constant expression.
 When \lstinline$_Alignof$ is applied to an identifier declared by a \nonterm{type-declaration} or a
+\nonterm{type-parameter}, it yields the alignment requirement of the type that implements the operand.
+When the operand is an opaque type or an inferred type parameter\index{inferred parameter}, the expression is not a constant expression.
+\nonterm{type-parameter}, it yields the alignment requirement of the type that implements the
+operand. When the operand is an opaque type or an inferred type parameter\index{inferred
+parameter}, the expression is not a constant expression.
 \begin{rationale}
 \begin{lstlisting}
 type Pair = struct { int first, second; };
 size_t p_size = sizeof(Pair);           // constant expression
 extern type Rational;@\use{Rational}@
 size_t c_size = sizeof(Rational);       // non-constant expression
 forall(type T) T f(T p1, T p2) {
         size_t t_size = sizeof(T);              // non-constant expression
 …
+}
 \end{lstlisting}
+``\lstinline$sizeof Rational$'', although not statically known, is fixed.
+Within \lstinline$f()$,
+``\lstinline$sizeof Rational$'', although not statically known, is fixed. Within \lstinline$f()$,
 ``\lstinline$sizeof(T)$'' is fixed for each call of \lstinline$f()$, but may vary from call to call.
 \end{rationale}
 …
 In a \Index{cast expression} ``\lstinline$($\nonterm{type-name}\lstinline$)e$'', if
+\nonterm{type-name} is the type of an interpretation of \lstinline$e$, then that interpretation is the only interpretation of the cast expression;
+otherwise, \lstinline$e$ shall have some interpretation that can be converted to \nonterm{type-name}, and the interpretation of the cast expression is the cast of the interpretation that can be converted at the lowest cost.
+The cast expression's interpretation is ambiguous\index{ambiguous interpretation} if more than one interpretation can be converted at the lowest cost or if the selected interpretation is ambiguous.
+\begin{rationale}
+Casts can be used to eliminate ambiguity in expressions by selecting interpretations of subexpressions, and to specialize polymorphic functions and values.
+\nonterm{type-name} is the type of an interpretation of \lstinline$e$, then that interpretation is
+the only interpretation of the cast expression; otherwise, \lstinline$e$ shall have some
+interpretation that can be converted to \nonterm{type-name}, and the interpretation of the cast
+expression is the cast of the interpretation that can be converted at the lowest cost. The cast
+expression's interpretation is ambiguous\index{ambiguous interpretation} if more than one
+interpretation can be converted at the lowest cost or if the selected interpretation is ambiguous.
+\begin{rationale}
+Casts can be used to eliminate ambiguity in expressions by selecting interpretations of
+subexpressions, and to specialize polymorphic functions and values.
 \end{rationale}
 …
 \predefined
 \begin{lstlisting}
+int?*?( int, int ), ?/?( int, int ), ?%?( int, int );
+unsigned int?*?( unsigned int, unsigned int ), ?/?( unsigned int, unsigned int ), ?%?( unsigned int, unsigned int );
+long int?*?( long int, long int ), ?/?( long, long ), ?%?( long, long );
+int?*?( int, int ),
+        ?/?( int, int ),
+        ?%?( int, int );
+unsigned int?*?( unsigned int, unsigned int ),
+        ?/?( unsigned int, unsigned int ),
+        ?%?( unsigned int, unsigned int );
+long int?*?( long int, long int ),
+        ?/?( long, long ),
+        ?%?( long, long );
 long unsigned int?*?( long unsigned int, long unsigned int ),
+        ?/?( long unsigned int, long unsigned int ), ?%?( long unsigned int, long unsigned int );
+long long int?*?( long long int, long long int ), ?/?( long long int, long long int ),
+        ?/?( long unsigned int, long unsigned int ),
+        ?%?( long unsigned int, long unsigned int );
+long long int?*?( long long int, long long int ),
+        ?/?( long long int, long long int ),
         ?%?( long long int, long long int );
 long long unsigned int ?*?( long long unsigned int, long long unsigned int ),
+        ?/?( long long unsigned int, long long unsigned int ), ?%?( long long unsigned int, long long unsigned int );
+float?*?( float, float ), ?/?( float, float );
+double?*?( double, double ), ?/?( double, double );
+long double?*?( long double, long double ), ?/?( long double, long double );
+_Complex float?*?( float, _Complex float ), ?/?( float, _Complex float ),
+        ?*?( _Complex float, float ), ?/?( _Complex float, float ),
+        ?*?( _Complex float, _Complex float ), ?/?( _Complex float, _Complex float );
+_Complex double?*?( double, _Complex double ), ?/?( double, _Complex double ),
+        ?*?( _Complex double, double ), ?/?( _Complex double, double ),
+        ?*?( _Complex double, _Complex double ), ?/?( _Complex double, _Complex double );
+_Complex long double?*?( long double, _Complex long double ), ?/?( long double, _Complex long double ),
+        ?*?( _Complex long double, long double ), ?/?( _Complex long double, long double ),
+        ?*?( _Complex long double, _Complex long double ), ?/?( _Complex long double, _Complex long double );
+\end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+        ?/?( long long unsigned int, long long unsigned int ),
+        ?%?( long long unsigned int, long long unsigned int );
+float?*?( float, float ),
+        ?/?( float, float );
+double?*?( double, double ),
+        ?/?( double, double );
+long double?*?( long double, long double ),
+        ?/?( long double, long double );
+_Complex float?*?( float, _Complex float ),
+        ?/?( float, _Complex float ),
+        ?*?( _Complex float, float ),
+        ?/?( _Complex float, float ),
+        ?*?( _Complex float, _Complex float ),
+        ?/?( _Complex float, _Complex float );
+_Complex double?*?( double, _Complex double ),
+        ?/?( double, _Complex double ),
+        ?*?( _Complex double, double ),
+        ?/?( _Complex double, double ),
+        ?*?( _Complex double, _Complex double ),
+        ?/?( _Complex double, _Complex double );
+_Complex long double?*?( long double, _Complex long double ),
+        ?/?( long double, _Complex long double ),
+        ?*?( _Complex long double, long double ),
+        ?/?( _Complex long double, long double ),
+        ?*?( _Complex long double, _Complex long double ),
+        ?/?( _Complex long double, _Complex long double );
+\end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \begin{rationale}
 {\c11} does not include conversions from the \Index{real type}s to \Index{complex type}s in the
+\Index{usual arithmetic conversion}s.  Instead it specifies conversion of the result of binary operations on arguments from mixed type domains. \CFA's predefined operators match that pattern.
+\Index{usual arithmetic conversion}s.  Instead it specifies conversion of the result of binary
+operations on arguments from mixed type domains. \CFA's predefined operators match that pattern.
 \end{rationale}
 \semantics
+The interpretations of multiplicative expressions are the interpretations of the corresponding function call.
+The interpretations of multiplicative expressions are the interpretations of the corresponding
+function call.
 \examples
 …
 eat_double( li % i );
 \end{lstlisting}
+``\lstinline$li % i$'' is rewritten as ``\lstinline$?%?(li, i )$''.
+The valid interpretations of \lstinline$?%?(li, i )$, the cost\index{conversion cost} of converting their arguments, and the cost of converting the result to \lstinline$double$ (assuming no extended integer types are present ) are
+``\lstinline$li % i$'' is rewritten as ``\lstinline$?%?(li, i )$''. The valid interpretations
+of \lstinline$?%?(li, i )$, the cost\index{conversion cost} of converting their arguments, and
+the cost of converting the result to \lstinline$double$ (assuming no extended integer types are
+present ) are
 \begin{center}
+\begin{tabular}{lcc} interpretation & argument cost & result cost \\
+\begin{tabular}{lcc}
+interpretation & argument cost & result cost \\
 \hline
 \lstinline$ ?%?( (int)li, i )$                                                                          & (unsafe)      & 6     \\
 \lstinline$ ?%?( (unsigned)li,(unsigned)i )$                                            & (unsafe)      & 5     \\
 \lstinline$ ?%?( li, (long)i )$                                                                         & 1                     & 4     \\
+\lstinline$ ?%?(li,(long)i )$                                                                           & 1                     & 4     \\
 \lstinline$ ?%?( (long unsigned)li,(long unsigned)i )$                          & 3                     & 3     \\
 \lstinline$ ?%?( (long long)li,(long long)i )$                                          & 5                     & 2     \\
 …
 \end{center}
 The best interpretation of \lstinline$eat_double( li, i )$ is
+\lstinline$eat_double( (double)?%?(li, (long)i ))$, which has no unsafe conversions and the lowest total cost.
+\begin{rationale}
+{\c11} defines most arithmetic operations to apply an \Index{integer promotion} to any argument that belongs to a type that has an \Index{integer conversion rank} less than that of \lstinline$int$.If
+\lstinline$eat_double( (double)?%?(li, (long)i ))$, which has no unsafe conversions and the
+lowest total cost.
+\begin{rationale}
+{\c11} defines most arithmetic operations to apply an \Index{integer promotion} to any argument that
+belongs to a type that has an \Index{integer conversion rank} less than that of \lstinline$int$.If
 \lstinline$s$ is a \lstinline$short int$, ``\lstinline$s *s$'' does not have type \lstinline$short int$;
+it is treated as ``\lstinline$( (int)s ) * ( (int)s )$'', and has type \lstinline$int$. \CFA matches that pattern;
+it does not predefine ``\lstinline$short ?*?( short, short )$''.
+These ``missing'' operators limit polymorphism.
+Consider
+it is treated as ``\lstinline$( (int)s ) * ( (int)s )$'', and has type \lstinline$int$. \CFA matches
+that pattern; it does not predefine ``\lstinline$short ?*?( short, short )$''.
+These ``missing'' operators limit polymorphism. Consider
 \begin{lstlisting}
 forall( type T | T ?*?( T, T ) ) T square( T );
 …
 Since \CFA does not define a multiplication operator for \lstinline$short int$,
 \lstinline$square( s )$ is treated as \lstinline$square( (int)s )$, and the result has type
+\lstinline$int$.
+This is mildly surprising, but it follows the {\c11} operator pattern.
+\lstinline$int$. This is mildly surprising, but it follows the {\c11} operator pattern.
 A more troubling example is
 …
 \end{lstlisting}
 This has no valid interpretations, because \CFA has no conversion from ``array of
 \lstinline$short int$'' to ``array of \lstinline$int$''.
 The alternatives in such situations include
+\lstinline$short int$'' to ``array of \lstinline$int$''. The alternatives in such situations
+include
 \begin{itemize}
 \item
 …
 \lstinline$product$.
 \item
+Defining \lstinline$product$ to take as an argument a conversion function from the ``small'' type to the operator's argument type.
+Defining \lstinline$product$ to take as an argument a conversion function from the ``small'' type to
+the operator's argument type.
 \end{itemize}
 \end{rationale}
 …
 \predefined
 \begin{lstlisting}
+int?+?( int, int ), ?-?( int, int );
+unsigned int?+?( unsigned int, unsigned int ), ?-?( unsigned int, unsigned int );
+long int?+?( long int, long int ), ?-?( long int, long int );
+long unsigned int?+?( long unsigned int, long unsigned int ), ?-?( long unsigned int, long unsigned int );
+long long int?+?( long long int, long long int ), ?-?( long long int, long long int );
+int?+?( int, int ),
+        ?-?( int, int );
+unsigned int?+?( unsigned int, unsigned int ),
+        ?-?( unsigned int, unsigned int );
+long int?+?( long int, long int ),
+        ?-?( long int, long int );
+long unsigned int?+?( long unsigned int, long unsigned int ),
+        ?-?( long unsigned int, long unsigned int );
+long long int?+?( long long int, long long int ),
+        ?-?( long long int, long long int );
 long long unsigned int ?+?( long long unsigned int, long long unsigned int ),
         ?-?( long long unsigned int, long long unsigned int );
+float?+?( float, float ), ?-?( float, float );
+double?+?( double, double ), ?-?( double, double );
+long double?+?( long double, long double ), ?-?( long double, long double );
+_Complex float?+?( _Complex float, float ), ?-?( _Complex float, float ),
+        ?+?( float, _Complex float ), ?-?( float, _Complex float ),
+        ?+?( _Complex float, _Complex float ), ?-?( _Complex float, _Complex float );
+_Complex double?+?( _Complex double, double ), ?-?( _Complex double, double ),
+        ?+?( double, _Complex double ), ?-?( double, _Complex double ),
+        ?+?( _Complex double, _Complex double ), ?-?( _Complex double, _Complex double );
+_Complex long double?+?( _Complex long double, long double ), ?-?( _Complex long double, long double ),
+        ?+?( long double, _Complex long double ), ?-?( long double, _Complex long double ),
+        ?+?( _Complex long double, _Complex long double ), ?-?( _Complex long double, _Complex long double );
+forall( type T ) T * ?+?( T *, ptrdiff_t ), * ?+?( ptrdiff_t, T * ), * ?-?( T *, ptrdiff_t );
+forall( type T ) _Atomic T * ?+?( _Atomic T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic T * ),
+float?+?( float, float ),
+        ?-?( float, float );
+double?+?( double, double ),
+        ?-?( double, double );
+long double?+?( long double, long double ),
+        ?-?( long double, long double );
+_Complex float?+?( _Complex float, float ),
+        ?-?( _Complex float, float ),
+        ?+?( float, _Complex float ),
+        ?-?( float, _Complex float ),
+        ?+?( _Complex float, _Complex float ),
+        ?-?( _Complex float, _Complex float );
+_Complex double?+?( _Complex double, double ),
+        ?-?( _Complex double, double ),
+        ?+?( double, _Complex double ),
+        ?-?( double, _Complex double ),
+        ?+?( _Complex double, _Complex double ),
+        ?-?( _Complex double, _Complex double );
+_Complex long double?+?( _Complex long double, long double ),
+        ?-?( _Complex long double, long double ),
+        ?+?( long double, _Complex long double ),
+        ?-?( long double, _Complex long double ),
+        ?+?( _Complex long double, _Complex long double ),
+        ?-?( _Complex long double, _Complex long double );
+forall( type T ) T
+        * ?+?( T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, T * ),
+        * ?-?( T *, ptrdiff_t );
+forall( type T ) _Atomic T
+        * ?+?( _Atomic T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, _Atomic T * ),
         * ?-?( _Atomic T *, ptrdiff_t );
+forall( type T ) const T * ?+?( const T *, ptrdiff_t ), * ?+?( ptrdiff_t, const T * ),
+forall( type T ) const T
+        * ?+?( const T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, const T * ),
         * ?-?( const T *, ptrdiff_t );
+forall( type T ) restrict T * ?+?( restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, restrict T * ),
+forall( type T ) restrict T
+        * ?+?( restrict T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, restrict T * ),
         * ?-?( restrict T *, ptrdiff_t );
+forall( type T ) volatile T * ?+?( volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, volatile T * ),
+forall( type T ) volatile T
+        * ?+?( volatile T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, volatile T * ),
         * ?-?( volatile T *, ptrdiff_t );
+forall( type T ) _Atomic const T * ?+?( _Atomic const T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic const T * ),
+forall( type T ) _Atomic const T
+        * ?+?( _Atomic const T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, _Atomic const T * ),
         * ?-?( _Atomic const T *, ptrdiff_t );
+forall( type T ) _Atomic restrict T * ?+?( _Atomic restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic restrict T * ),
+forall( type T ) _Atomic restrict T
+        * ?+?( _Atomic restrict T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, _Atomic restrict T * ),
         * ?-?( _Atomic restrict T *, ptrdiff_t );
+forall( type T ) _Atomic volatile T * ?+?( _Atomic volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic volatile T * ),
+forall( type T ) _Atomic volatile T
+        * ?+?( _Atomic volatile T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, _Atomic volatile T * ),
         * ?-?( _Atomic volatile T *, ptrdiff_t );
+forall( type T ) const restrict T * ?+?( const restrict T *, ptrdiff_t ), * ?+?( ptrdiff_t, const restrict T * ),
+forall( type T ) const restrict T
+        * ?+?( const restrict T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, const restrict T * ),
         * ?-?( const restrict T *, ptrdiff_t );
+forall( type T ) const volatile T * ?+?( const volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, const volatile T * ),
+forall( type T ) const volatile T
+        * ?+?( const volatile T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, const volatile T * ),
         * ?-?( const volatile T *, ptrdiff_t );
+forall( type T ) restrict volatile T * ?+?( restrict volatile T *, ptrdiff_t ), * ?+?( ptrdiff_t, restrict volatile T * ),
+forall( type T ) restrict volatile T
+        * ?+?( restrict volatile T *, ptrdiff_t ),
+        * ?+?( ptrdiff_t, restrict volatile T * ),
         * ?-?( restrict volatile T *, ptrdiff_t );
+forall( type T ) _Atomic const restrict T * ?+?( _Atomic const restrict T *, ptrdiff_t ),
+forall( type T ) _Atomic const restrict T
+        * ?+?( _Atomic const restrict T *, ptrdiff_t ),
         * ?+?( ptrdiff_t, _Atomic const restrict T * ),
         * ?-?( _Atomic const restrict T *, ptrdiff_t );
 forall( type T ) ptrdiff_t
         * ?-?( const restrict volatile T *, const restrict volatile T * ),
         * ?-?( _Atomic const restrict volatile T *, _Atomic const restrict volatile T * );
 \end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \semantics
+The interpretations of additive expressions are the interpretations of the corresponding function calls.
+\begin{rationale}
+\lstinline$ptrdiff_t$ is an implementation-defined identifier defined in \lstinline$<stddef.h>$ that is synonymous with a signed integral type that is large enough to hold the difference between two pointers.
+It seems reasonable to use it for pointer addition as well. (This is technically a difference between \CFA and C, which only specifies that pointer addition uses an \emph{integral} argument.) Hence it is also used for subscripting, which is defined in terms of pointer addition.
+The {\c11} standard uses \lstinline$size_t$ in several cases where a library function takes an argument that is used as a subscript, but \lstinline$size_t$ is unsuitable here because it is an unsigned type.
+The interpretations of additive expressions are the interpretations of the corresponding function
+calls.
+\begin{rationale}
+\lstinline$ptrdiff_t$ is an implementation-defined identifier defined in \lstinline$<stddef.h>$ that
+is synonymous with a signed integral type that is large enough to hold the difference between two
+pointers. It seems reasonable to use it for pointer addition as well. (This is technically a
+difference between \CFA and C, which only specifies that pointer addition uses an \emph{integral}
+argument.) Hence it is also used for subscripting, which is defined in terms of pointer addition.
+The {\c11} standard uses \lstinline$size_t$ in several cases where a library function takes an
+argument that is used as a subscript, but \lstinline$size_t$ is unsuitable here because it is an
+unsigned type.
 \end{rationale}
 …
 \predefined
 \begin{lstlisting}
+int ?<<?( int, int ), ?>>?( int, int );
+unsigned int ?<<?( unsigned int, int ), ?>>?( unsigned int, int );
+long int ?<<?( long int, int ), ?>>?( long int, int );
+long unsigned int ?<<?( long unsigned int, int ), ?>>?( long unsigned int, int );
+long long int ?<<?( long long int, int ), ?>>?( long long int, int );
+long long unsigned int ?<<?( long long unsigned int, int ), ?>>?( long long unsigned int, int);
+\end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+int ?<<?( int, int ),
+         ?>>?( int, int );
+unsigned int ?<<?( unsigned int, int ),
+         ?>>?( unsigned int, int );
+long int ?<<?( long int, int ),
+         ?>>?( long int, int );
+long unsigned int ?<<?( long unsigned int, int ),
+         ?>>?( long unsigned int, int );
+long long int ?<<?( long long int, int ),
+         ?>>?( long long int, int );
+long long unsigned int ?<<?( long long unsigned int, int ),
+         ?>>?( long long unsigned int, int);
+\end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \begin{rationale}
 The bitwise shift operators break the usual pattern: they do not convert both operands to a common type.
 The right operand only undergoes \Index{integer promotion}.
+The bitwise shift operators break the usual pattern: they do not convert both operands to a common
+type. The right operand only undergoes \Index{integer promotion}.
 \end{rationale}
 \semantics
+The interpretations of a bitwise shift expression are the interpretations of the corresponding function calls.
+The interpretations of a bitwise shift expression are the interpretations of the corresponding
+function calls.
 …
 \predefined
 \begin{lstlisting}
+int ?<?( int, int ), ?<=?( int, int ),
+        ?>?( int, int ), ?>=?( int, int );
+int ?<?( unsigned int, unsigned int ), ?<=?( unsigned int, unsigned int ),
+        ?>?( unsigned int, unsigned int ), ?>=?( unsigned int, unsigned int );
+int ?<?( long int, long int ), ?<=?( long int, long int ),
+        ?>?( long int, long int ), ?>=?( long int, long int );
+int ?<?( long unsigned int, long unsigned ), ?<=?( long unsigned int, long unsigned ),
+        ?>?( long unsigned int, long unsigned ), ?>=?( long unsigned int, long unsigned );
+int ?<?( long long int, long long int ), ?<=?( long long int, long long int ),
+        ?>?( long long int, long long int ), ?>=?( long long int, long long int );
+int ?<?( long long unsigned int, long long unsigned ), ?<=?( long long unsigned int, long long unsigned ),
+        ?>?( long long unsigned int, long long unsigned ), ?>=?( long long unsigned int, long long unsigned );
+int ?<?( float, float ), ?<=?( float, float ),
+        ?>?( float, float ), ?>=?( float, float );
+int ?<?( double, double ), ?<=?( double, double ),
+        ?>?( double, double ), ?>=?( double, double );
+int ?<?( long double, long double ), ?<=?( long double, long double ),
+        ?>?( long double, long double ), ?>=?( long double, long double );
+forall( dtype DT ) int ?<?( const restrict volatile DT *, const restrict volatile DT * ),
+int ?<?( int, int ),
+        ?<=?( int, int ),
+        ?>?( int, int ),
+        ?>=?( int, int );
+int ?<?( unsigned int, unsigned int ),
+        ?<=?( unsigned int, unsigned int ),
+        ?>?( unsigned int, unsigned int ),
+        ?>=?( unsigned int, unsigned int );
+int ?<?( long int, long int ),
+        ?<=?( long int, long int ),
+        ?>?( long int, long int ),
+        ?>=?( long int, long int );
+int ?<?( long unsigned int, long unsigned ),
+        ?<=?( long unsigned int, long unsigned ),
+        ?>?( long unsigned int, long unsigned ),
+        ?>=?( long unsigned int, long unsigned );
+int ?<?( long long int, long long int ),
+        ?<=?( long long int, long long int ),
+        ?>?( long long int, long long int ),
+        ?>=?( long long int, long long int );
+int ?<?( long long unsigned int, long long unsigned ),
+        ?<=?( long long unsigned int, long long unsigned ),
+        ?>?( long long unsigned int, long long unsigned ),
+        ?>=?( long long unsigned int, long long unsigned );
+int ?<?( float, float ),
+        ?<=?( float, float ),
+        ?>?( float, float ),
+        ?>=?( float, float );
+int ?<?( double, double ),
+        ?<=?( double, double ),
+        ?>?( double, double ),
+        ?>=?( double, double );
+int ?<?( long double, long double ),
+        ?<=?( long double, long double ),
+        ?>?( long double, long double ),
+        ?>=?( long double, long double );
+forall( dtype DT ) int
+        ?<?( const restrict volatile DT *, const restrict volatile DT * ),
         ?<?( _Atomic const restrict volatile DT *, _Atomic const restrict volatile DT * ),
         ?<=?( const restrict volatile DT *, const restrict volatile DT * ),
 …
         ?>=?( _Atomic const restrict volatile DT *, _Atomic const restrict volatile DT * );
 \end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \semantics
+The interpretations of a relational expression are the interpretations of the corresponding function call.
+The interpretations of a relational expression are the interpretations of the corresponding function
+call.
 …
 \predefined
 \begin{lstlisting}
+int ?==?( int, int ), ?!=?( int, int ),
+        ?==?( unsigned int, unsigned int ), ?!=?( unsigned int, unsigned int ),
+        ?==?( long int, long int ), ?!=?( long int, long int ),
+        ?==?( long unsigned int, long unsigned int ), ?!=?( long unsigned int, long unsigned int ),
+        ?==?( long long int, long long int ), ?!=?( long long int, long long int ),
+        ?==?( long long unsigned int, long long unsigned int ), ?!=?( long long unsigned int, long long unsigned int ),
+        ?==?( float, float ), ?!=?( float, float ),
+        ?==?( _Complex float, float ), ?!=?( _Complex float, float ),
+        ?==?( float, _Complex float ), ?!=?( float, _Complex float ),
+        ?==?( _Complex float, _Complex float ), ?!=?( _Complex float, _Complex float ),
+        ?==?( double, double ), ?!=?( double, double ),
+        ?==?( _Complex double, double ), ?!=?( _Complex double, double ),
+        ?==?( double, _Complex double ), ?!=?( double, _Complex double ),
+        ?==?( _Complex double, _Complex double ), ?!=?( _Complex double, _Complex double ),
+        ?==?( long double, long double ), ?!=?( long double, long double ),
+        ?==?( _Complex long double, long double ), ?!=?( _Complex long double, long double ),
+        ?==?( long double, _Complex long double ), ?!=?( long double, _Complex long double ),
+        ?==?( _Complex long double, _Complex long double ), ?!=?( _Complex long double, _Complex long double );
+int ?==?( int, int ),
+        ?!=?( int, int ),
+        ?==?( unsigned int, unsigned int ),
+        ?!=?( unsigned int, unsigned int ),
+        ?==?( long int, long int ),
+        ?!=?( long int, long int ),
+        ?==?( long unsigned int, long unsigned int ),
+        ?!=?( long unsigned int, long unsigned int ),
+        ?==?( long long int, long long int ),
+        ?!=?( long long int, long long int ),
+        ?==?( long long unsigned int, long long unsigned int ),
+        ?!=?( long long unsigned int, long long unsigned int ),
+        ?==?( float, float ),
+        ?!=?( float, float ),
+        ?==?( _Complex float, float ),
+        ?!=?( _Complex float, float ),
+        ?==?( float, _Complex float ),
+        ?!=?( float, _Complex float ),
+        ?==?( _Complex float, _Complex float ),
+        ?!=?( _Complex float, _Complex float ),
+        ?==?( double, double ),
+        ?!=?( double, double ),
+        ?==?( _Complex double, double ),
+        ?!=?( _Complex double, double ),
+        ?==?( double, _Complex double ),
+        ?!=?( double, _Complex double ),
+        ?==?( _Complex double, _Complex double ),
+        ?!=?( _Complex double, _Complex double ),
+        ?==?( long double, long double ),
+        ?!=?( long double, long double ),
+        ?==?( _Complex long double, long double ),
+        ?!=?( _Complex long double, long double ),
+        ?==?( long double, _Complex long double ),
+        ?!=?( long double, _Complex long double ),
+        ?==?( _Complex long double, _Complex long double ),
+        ?!=?( _Complex long double, _Complex long double );
 forall( dtype DT ) int
         ?==?( const restrict volatile DT *, const restrict volatile DT * ),
 …
         ?==?( forall( dtype DT2) const DT2*, _Atomic const restrict volatile DT * ),
         ?!=?( forall( dtype DT2) const DT2*, _Atomic const restrict volatile DT * );
 forall( ftype FT ) int
+        ?==?( FT *, FT * ), ?!=?( FT *, FT * ),
+        ?==?( FT *, forall( ftype FT2) FT2 * ), ?!=?( FT *, forall( ftype FT2) FT2 * ),
+        ?==?( forall( ftype FT2) FT2*, FT * ), ?!=?( forall( ftype FT2) FT2*, FT * ),
+        ?==?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * ), ?!=?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * );
+\end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+        ?==?( FT *, FT * ),
+        ?!=?( FT *, FT * ),
+        ?==?( FT *, forall( ftype FT2) FT2 * ),
+        ?!=?( FT *, forall( ftype FT2) FT2 * ),
+        ?==?( forall( ftype FT2) FT2*, FT * ),
+        ?!=?( forall( ftype FT2) FT2*, FT * ),
+        ?==?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * ),
+        ?!=?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * );
+\end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \begin{rationale}
+The polymorphic equality operations come in three styles: comparisons between pointers of compatible types, between pointers to \lstinline$void$ and pointers to object types or incomplete types, and between the \Index{null pointer} constant and pointers to any type.
+In the last case, a special constraint rule for null pointer constant operands has been replaced by a consequence of the \CFA type system.
+The polymorphic equality operations come in three styles: comparisons between pointers of compatible
+types, between pointers to \lstinline$void$ and pointers to object types or incomplete types, and
+between the \Index{null pointer} constant and pointers to any type. In the last case, a special
+constraint rule for null pointer constant operands has been replaced by a consequence of the \CFA
+type system.
 \end{rationale}
 \semantics
+The interpretations of an equality expression are the interpretations of the corresponding function call.
+The interpretations of an equality expression are the interpretations of the corresponding function
+call.
 \begin{sloppypar}
+The result of an equality comparison between two pointers to predefined functions or predefined values is implementation-defined.
+The result of an equality comparison between two pointers to predefined functions or predefined
+values is implementation-defined.
 \end{sloppypar}
 \begin{rationale}
+The implementation-defined status of equality comparisons allows implementations to use one library routine to implement many predefined functions.
+These optimization are particularly important when the predefined functions are polymorphic, as is the case for most pointer operations
+The implementation-defined status of equality comparisons allows implementations to use one library
+routine to implement many predefined functions. These optimization are particularly important when
+the predefined functions are polymorphic, as is the case for most pointer operations
 \end{rationale}
 …
 long long unsigned int ?&?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \semantics
+The interpretations of a bitwise AND expression are the interpretations of the corresponding function call.
+The interpretations of a bitwise AND expression are the interpretations of the corresponding
+function call.
 …
 long long unsigned int ?^?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \semantics
+The interpretations of a bitwise exclusive OR expression are the interpretations of the corresponding function call.
+The interpretations of a bitwise exclusive OR expression are the interpretations of the
+corresponding function call.
 …
 long long unsigned int ?|?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the
+rank of \lstinline$int$ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
 …
 \semantics
+The interpretations of a bitwise inclusive OR expression are the interpretations of the corresponding function call.
+The interpretations of a bitwise inclusive OR expression are the interpretations of the
+corresponding function call.
 …
 \semantics The operands of the expression ``\lstinline$a && b$'' are treated as
+``\lstinline$(int)((a)!=0)$'' and ``\lstinline$(int)((b)!=0)$'', which shall both be unambiguous.
+The expression has only one interpretation, which is of type \lstinline$int$.
+\begin{rationale}
+When the operands of a logical expression are values of built-in types, and ``\lstinline$!=$'' has not been redefined for those types, the compiler can optimize away the function calls.
+``\lstinline$(int)((a)!=0)$'' and ``\lstinline$(int)((b)!=0)$'', which shall both be
+unambiguous. The expression has only one interpretation, which is of type \lstinline$int$.
+\begin{rationale}
+When the operands of a logical expression are values of built-in types, and ``\lstinline$!=$'' has
+not been redefined for those types, the compiler can optimize away the function calls.
 A common C idiom omits comparisons to \lstinline$0$ in the controlling expressions of loops and
 \lstinline$if$ statements.
 For instance, the loop below iterates as long as \lstinline$rp$ points at a \lstinline$Rational$ value that is non-zero.
+\lstinline$if$ statements. For instance, the loop below iterates as long as \lstinline$rp$ points
+at a \lstinline$Rational$ value that is non-zero.
 \begin{lstlisting}
 …
 extern int ?!=?( Rational, Rational );
 Rational *rp;
 while ( rp && *rp ) { ... }
 \end{lstlisting}
+The logical expression calls the \lstinline$Rational$ inequality operator, passing it \lstinline$*rp$ and the \lstinline$Rational 0$, and getting a 1 or 0 as a result.
+In contrast, {\CC} would apply a programmer-defined \lstinline$Rational$-to-\lstinline$int$ conversion to \lstinline$*rp$ in the equivalent situation.
+The conversion to \lstinline$int$ would produce a general integer value, which is unfortunate, and possibly dangerous if the conversion was not written with this situation in mind.
+The logical expression calls the \lstinline$Rational$ inequality operator, passing
+it \lstinline$*rp$ and the \lstinline$Rational 0$, and getting a 1 or 0 as a result. In
+contrast, {\CC} would apply a programmer-defined \lstinline$Rational$-to-\lstinline$int$
+conversion to \lstinline$*rp$ in the equivalent situation. The conversion to \lstinline$int$ would
+produce a general integer value, which is unfortunate, and possibly dangerous if the conversion was
+not written with this situation in mind.
 \end{rationale}
 …
 \semantics
+The operands of the expression ``\lstinline$a || b$'' are treated as ``\lstinline$(int)((a)!=0)$'' and ``\lstinline$(int)((b))!=0)$'', which shall both be unambiguous.
+The expression has only one interpretation, which is of type \lstinline$int$.
+The operands of the expression ``\lstinline$a || b$'' are treated as ``\lstinline$(int)((a)!=0)$''
+and ``\lstinline$(int)((b))!=0)$'', which shall both be unambiguous. The expression has only one
+interpretation, which is of type \lstinline$int$.
 …
 \semantics
+In the conditional expression\use{?:} ``\lstinline$a?b:c$'', if the second and third operands both have an interpretation with \lstinline$void$ type, then the expression has an interpretation with type \lstinline$void$, equivalent to
+In the conditional expression\use{?:} ``\lstinline$a?b:c$'', if the second and
+third operands both have an interpretation with \lstinline$void$ type, then the expression has an
+interpretation with type \lstinline$void$, equivalent to
 \begin{lstlisting}
 ( int)(( a)!=0) ? ( void)( b) : ( void)( c)
 \end{lstlisting}
+If the second and third operands both have interpretations with non-\lstinline$void$ types, the expression is treated as if it were the call ``\lstinline$cond((a)!=0, b, c)$'', with \lstinline$cond$ declared as
+If the second and third operands both have interpretations with non-\lstinline$void$ types, the
+expression is treated as if it were the call ``\lstinline$cond((a)!=0, b, c)$'',
+with \lstinline$cond$ declared as
 \begin{lstlisting}
 forall( type T ) T cond( int, T, T );
+forall( dtype D ) void * cond( int, D *, void * ), * cond( int, void *, D * );
+forall( dtype D ) _atomic void * cond(
+        int, _Atomic D *, _Atomic void * ), * cond( int, _Atomic void *, _Atomic D * );
+forall( dtype D ) const void * cond(
+        int, const D *, const void * ), * cond( int, const void *, const D * );
+forall( dtype D ) restrict void * cond(
+        int, restrict D *, restrict void * ), * cond( int, restrict void *, restrict D * );
+forall( dtype D ) volatile void * cond(
+        int, volatile D *, volatile void * ), * cond( int, volatile void *, volatile D * );
+forall( dtype D ) _Atomic const void * cond(
+        int, _Atomic const D *, _Atomic const void * ), * cond( int, _Atomic const void *, _Atomic const D * );
+forall( dtype D ) _Atomic restrict void * cond(
+        int, _Atomic restrict D *, _Atomic restrict void * ), * cond( int, _Atomic restrict void *, _Atomic restrict D * );
+forall( dtype D ) _Atomic volatile void * cond(
+        int, _Atomic volatile D *, _Atomic volatile void * ), * cond( int, _Atomic volatile void *, _Atomic volatile D * );
+forall( dtype D ) const restrict void * cond(
+        int, const restrict D *, const restrict void * ), * cond( int, const restrict void *, const restrict D * );
+forall( dtype D ) const volatile void * cond(
+        int, const volatile D *, const volatile void * ), * cond( int, const volatile void *, const volatile D * );
+forall( dtype D ) restrict volatile void * cond(
+        int, restrict volatile D *, restrict volatile void * ), * cond( int, restrict volatile void *, restrict volatile D * );
+forall( dtype D ) _Atomic const restrict void * cond(
+        int, _Atomic const restrict D *, _Atomic const restrict void * ),
+forall( dtype D ) void
+        * cond( int, D *, void * ),
+        * cond( int, void *, D * );
+forall( dtype D ) _atomic void
+        * cond( int, _Atomic D *, _Atomic void * ),
+        * cond( int, _Atomic void *, _Atomic D * );
+forall( dtype D ) const void
+        * cond( int, const D *, const void * ),
+        * cond( int, const void *, const D * );
+forall( dtype D ) restrict void
+        * cond( int, restrict D *, restrict void * ),
+        * cond( int, restrict void *, restrict D * );
+forall( dtype D ) volatile void
+        * cond( int, volatile D *, volatile void * ),
+        * cond( int, volatile void *, volatile D * );
+forall( dtype D ) _Atomic const void
+        * cond( int, _Atomic const D *, _Atomic const void * ),
+        * cond( int, _Atomic const void *, _Atomic const D * );
+forall( dtype D ) _Atomic restrict void
+        * cond( int, _Atomic restrict D *, _Atomic restrict void * ),
+        * cond( int, _Atomic restrict void *, _Atomic restrict D * );
+forall( dtype D ) _Atomic volatile void
+        * cond( int, _Atomic volatile D *, _Atomic volatile void * ),
+        * cond( int, _Atomic volatile void *, _Atomic volatile D * );
+forall( dtype D ) const restrict void
+        * cond( int, const restrict D *, const restrict void * ),
+        * cond( int, const restrict void *, const restrict D * );
+forall( dtype D ) const volatile void
+        * cond( int, const volatile D *, const volatile void * ),
+        * cond( int, const volatile void *, const volatile D * );
+forall( dtype D ) restrict volatile void
+        * cond( int, restrict volatile D *, restrict volatile void * ),
+        * cond( int, restrict volatile void *, restrict volatile D * );
+forall( dtype D ) _Atomic const restrict void
+        * cond( int, _Atomic const restrict D *, _Atomic const restrict void * ),
         * cond( int, _Atomic const restrict void *, _Atomic const restrict D * );
+forall( dtype D ) _Atomic const volatile void * cond(
+        int, _Atomic const volatile D *, _Atomic const volatile void * ),
+forall( dtype D ) _Atomic const volatile void
+        * cond( int, _Atomic const volatile D *, _Atomic const volatile void * ),
         * cond( int, _Atomic const volatile void *, _Atomic const volatile D * );
+forall( dtype D ) _Atomic restrict volatile void * cond(
+        int, _Atomic restrict volatile D *, _Atomic restrict volatile void * ),
+        * cond( int, _Atomic restrict volatile void *, _Atomic restrict volatile D * );
+forall( dtype D ) const restrict volatile void * cond(
+        int, const restrict volatile D *, const restrict volatile void * ),
+        * cond( int, const restrict volatile void *, const restrict volatile D * );
+forall( dtype D ) _Atomic const restrict volatile void * cond(
+        int, _Atomic const restrict volatile D *, _Atomic const restrict volatile void * ),
+        * cond( int, _Atomic const restrict volatile void *, _Atomic const restrict volatile D * );
+\end{lstlisting}
+\begin{rationale}
+The object of the above is to apply the \Index{usual arithmetic conversion}s when the second and third operands have arithmetic type, and to combine the qualifiers of the second and third operands if they are pointers.
+forall( dtype D ) _Atomic restrict volatile void
+        * cond( int, _Atomic restrict volatile D *,
+         _Atomic restrict volatile void * ),
+        * cond( int, _Atomic restrict volatile void *,
+         _Atomic restrict volatile D * );
+forall( dtype D ) const restrict volatile void
+        * cond( int, const restrict volatile D *,
+         const restrict volatile void * ),
+        * cond( int, const restrict volatile void *,
+         const restrict volatile D * );
+forall( dtype D ) _Atomic const restrict volatile void
+        * cond( int, _Atomic const restrict volatile D *,
+         _Atomic const restrict volatile void * ),
+        * cond( int, _Atomic const restrict volatile void *,
+         _Atomic const restrict volatile D * );
+\end{lstlisting}
+\begin{rationale}
+The object of the above is to apply the \Index{usual arithmetic conversion}s when the second and
+third operands have arithmetic type, and to combine the qualifiers of the second and third operands
+if they are pointers.
 \end{rationale}
 …
 rand() ? cip : vip;
 \end{lstlisting}
+The expression has type \lstinline$const volatile int *$, with safe conversions applied to the second and third operands to add \lstinline$volatile$ and \lstinline$const$ qualifiers, respectively.
+The expression has type \lstinline$const volatile int *$, with safe conversions applied to the second
+and third operands to add \lstinline$volatile$ and \lstinline$const$ qualifiers, respectively.
 \begin{lstlisting}
 …
 \rewriterules
+Let ``\(\leftarrow\)'' be any of the assignment operators.
+Then
+Let ``\(\leftarrow\)'' be any of the assignment operators. Then
 \use{?=?}\use{?*=?}\use{?/=?}\use{?%=?}\use{?+=?}\use{?-=?}
 \use{?>>=?}\use{?&=?}\use{?^=?}\use{?"|=?}%use{?<<=?}
 …
 \semantics
+Each interpretation of the left operand of an assignment expression is considered separately.
+For each interpretation that is a bit-field or is declared with the \lstinline$register$ storage class specifier, the expression has one valid interpretation, with the type of the left operand.
+The right operand is cast to that type, and the assignment expression is ambiguous if either operand is.
+For the remaining interpretations, the expression is rewritten, and the interpretations of the assignment expression are the interpretations of the corresponding function call.
+Finally, all interpretations of the expression produced for the different interpretations of the left operand are combined to produce the interpretations of the expression as a whole;
+where interpretations have compatible result types, the best interpretations are selected in the manner described for function call expressions.
+Each interpretation of the left operand of an assignment expression is considered separately. For
+each interpretation that is a bit-field or is declared with the \lstinline$register$ storage class
+specifier, the expression has one valid interpretation, with the type of the left operand. The
+right operand is cast to that type, and the assignment expression is ambiguous if either operand is.
+For the remaining interpretations, the expression is rewritten, and the interpretations of the
+assignment expression are the interpretations of the corresponding function call. Finally, all
+interpretations of the expression produced for the different interpretations of the left operand are
+combined to produce the interpretations of the expression as a whole; where interpretations have
+compatible result types, the best interpretations are selected in the manner described for function
+call expressions.
 …
         ?=?( volatile _Complex long double *, _Complex long double ),
         ?=?( _Atomic volatile _Complex long double *, _Atomic _Complex long double );
 forall( ftype FT ) FT
         * ?=?( FT * volatile *, FT * ),
         * ?=?( FT * volatile *, forall( ftype F ) F * );
 forall( ftype FT ) FT const
         * ?=?( FT const * volatile *, FT const * ),
         * ?=?( FT const * volatile *, forall( ftype F ) F * );
 forall( ftype FT ) FT volatile
         * ?=?( FT volatile * volatile *, FT * ),
         * ?=?( FT volatile * volatile *, forall( ftype F ) F * );
 forall( ftype FT ) FT const
         * ?=?( FT const volatile * volatile *, FT const * ),
         * ?=?( FT const volatile * volatile *, forall( ftype F ) F * );
 forall( dtype DT ) DT
         * ?=?( DT * restrict volatile *, DT * ),
 …
         * ?=?( DT * _Atomic restrict volatile *, void * ),
         * ?=?( DT * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic
         * ?=?( _Atomic DT * restrict volatile *, DT _Atomic * ),
 …
         * ?=?( _Atomic DT * _Atomic restrict volatile *, void * ),
         * ?=?( _Atomic DT * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT const
         * ?=?( DT const * restrict volatile *, DT const * ),
 …
         * ?=?( DT const * _Atomic restrict volatile *, void const * ),
         * ?=?( DT const * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT restrict
         * ?=?( restrict DT * restrict volatile *, DT restrict * ),
 …
         * ?=?( restrict DT * _Atomic restrict volatile *, void * ),
         * ?=?( restrict DT * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT volatile
         * ?=?( DT volatile * restrict volatile *, DT volatile * ),
 …
         * ?=?( DT volatile * _Atomic restrict volatile *, void volatile * ),
         * ?=?( DT volatile * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic const
         * ?=?( DT _Atomic const * restrict volatile *, DT _Atomic const * ),
 …
         * ?=?( DT _Atomic const * _Atomic restrict volatile *, void const * ),
         * ?=?( DT _Atomic const * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic restrict
         * ?=?( _Atomic restrict DT * restrict volatile *, DT _Atomic restrict * ),
 …
         * ?=?( _Atomic restrict DT * _Atomic restrict volatile *, void * ),
         * ?=?( _Atomic restrict DT * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic volatile
         * ?=?( DT _Atomic volatile * restrict volatile *, DT _Atomic volatile * ),
 …
         * ?=?( DT _Atomic volatile * _Atomic restrict volatile *, void volatile * ),
         * ?=?( DT _Atomic volatile * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT const restrict
         * ?=?( DT const restrict * restrict volatile *, DT const restrict * ),
 …
         * ?=?( DT const restrict * _Atomic restrict volatile *, void const * ),
         * ?=?( DT const restrict * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT const volatile
         * ?=?( DT const volatile * restrict volatile *, DT const volatile * ),
 …
         * ?=?( DT const volatile * _Atomic restrict volatile *, void const volatile * ),
         * ?=?( DT const volatile * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT restrict volatile
         * ?=?( DT restrict volatile * restrict volatile *, DT restrict volatile * ),
 …
         * ?=?( DT restrict volatile * _Atomic restrict volatile *, void volatile * ),
         * ?=?( DT restrict volatile * _Atomic restrict volatile *, forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic const restrict
         * ?=?( DT _Atomic const restrict * restrict volatile *,
 …
         * ?=?( DT _Atomic const restrict * _Atomic restrict volatile *,
          forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic const volatile
         * ?=?( DT _Atomic const volatile * restrict volatile *,
 …
         * ?=?( DT _Atomic const volatile * _Atomic restrict volatile *,
          forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic restrict volatile
         * ?=?( DT _Atomic restrict volatile * restrict volatile *,
 …
         * ?=?( DT _Atomic restrict volatile * _Atomic restrict volatile *,
          forall( dtype D ) D * );
 forall( dtype DT ) DT const restrict volatile
         * ?=?( DT const restrict volatile * restrict volatile *,
 …
         * ?=?( DT const restrict volatile * _Atomic restrict volatile *,
          forall( dtype D ) D * );
 forall( dtype DT ) DT _Atomic const restrict volatile
         * ?=?( DT _Atomic const restrict volatile * restrict volatile *,
 …
         * ?=?( DT _Atomic const restrict volatile * _Atomic restrict volatile *,
          forall( dtype D ) D * );
 forall( dtype DT ) void
         * ?=?( void * restrict volatile *, DT * );
 forall( dtype DT ) void const
         * ?=?( void const * restrict volatile *, DT const * );
 forall( dtype DT ) void volatile
         * ?=?( void volatile * restrict volatile *, DT volatile * );
 forall( dtype DT ) void const volatile
         * ?=?( void const volatile * restrict volatile *, DT const volatile * );
 \end{lstlisting}
 \begin{rationale}
+The pattern of overloadings for simple assignment resembles that of pointer increment and decrement, except that the polymorphic pointer assignment functions declare a \lstinline$dtype$ parameter, instead of a \lstinline$type$ parameter, because the left operand may be a pointer to an incomplete type.
+The pattern of overloadings for simple assignment resembles that of pointer increment and decrement,
+except that the polymorphic pointer assignment functions declare a \lstinline$dtype$ parameter,
+instead of a \lstinline$type$ parameter, because the left operand may be a pointer to an incomplete
+type.
 \end{rationale}
 …
 \semantics
+The structure assignment functions provide member-wise assignment;
+each non-array member and each element of each array member of the right argument is assigned to the corresponding member or element of the left argument using the assignment function defined for its type.
+All other assignment functions have the same effect as the corresponding C assignment expression.
+\begin{rationale}
+Note that, by default, union assignment\index{deficiencies!union assignment} uses C semantics---that is, bitwise copy---even if some of the union members have programmer-defined assignment functions.
+The structure assignment functions provide member-wise assignment; each non-array member and each
+element of each array member of the right argument is assigned to the corresponding member or
+element of the left argument using the assignment function defined for its type. All other
+assignment functions have the same effect as the corresponding C assignment expression.
+\begin{rationale}
+Note that, by default, union assignment\index{deficiencies!union assignment} uses C semantics---that
+is, bitwise copy---even if some of the union members have programmer-defined assignment functions.
 \end{rationale}
 …
         * ?+=?( T * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic
         * ?+=?( T _Atomic * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T const
         * ?+=?( T const * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T const * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T restrict
         * ?+=?( T restrict * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T restrict * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T volatile
         * ?+=?( T volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic const
         * ?+=?( T _Atomic const restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic const _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic const _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic restrict
         * ?+=?( T _Atomic restrict * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic restrict * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic volatile
         * ?+=?( T _Atomic volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T const restrict
         * ?+=?( T const restrict * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T const restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const restrict * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T const volatile
         * ?+=?( T const volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T const volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T restrict volatile
         * ?+=?( T restrict volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic const restrict
         * ?+=?( T _Atomic const restrict * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic const restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic const restrict * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic const volatile
         * ?+=?( T _Atomic const volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic const volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic const volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic restrict volatile
         * ?+=?( T _Atomic restrict volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T _Atomic restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T const restrict volatile
         * ?+=?( T const restrict volatile * restrict volatile *, ptrdiff_t ),
 …
         * ?+=?( T const restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
 forall( type T ) T _Atomic const restrict volatile
         * ?+=?( T _Atomic const restrict volatile * restrict volatile *, ptrdiff_t ),
 …
 \semantics
 In the comma expression ``\lstinline$a, b$'', the first operand is interpreted as
 ``\lstinline$( void )(a)$'', which shall be unambiguous\index{ambiguous interpretation}.
 The interpretations of the expression are the interpretations of the second operand.
+``\lstinline$( void )(a)$'', which shall be unambiguous\index{ambiguous interpretation}. The
+interpretations of the expression are the interpretations of the second operand.
 …
 \constraints
+If an identifier has \Index{no linkage}, there shall be no more than one declaration of the identifier ( in a declarator or type specifier ) with compatible types in the same scope and in the same name space, except that:
+If an identifier has \Index{no linkage}, there shall be no more than one declaration of the
+identifier ( in a declarator or type specifier ) with compatible types in the same scope and in the
+same name space, except that:
 \begin{itemize}
+\item a typedef name may be redefined to denote the same type as it currently does, provided that type is not a variably modified type;
+\item tags may be redeclared as specified in section 6.7.2.3 of the {\c11} standard.
+\item
+a typedef name may be redefined to denote the same type as it currently does, provided that type is
+not a variably modified type;
+\item
+tags may be redeclared as specified in section 6.7.2.3 of the {\c11} standard.
 \end{itemize}
 \begin{rationale}
+This constraint adds the phrase ``with compatible types'' to the {\c11} constraint, to allow overloading.
+\end{rationale}
+An identifier declared by a type declaration shall not be redeclared as a parameter in a function definition whose declarator includes an identifier list.
+\begin{rationale}
+This restriction echos {\c11}'s ban on the redeclaration of typedef names as parameters.
+This avoids an ambiguity between old-style function declarations and new-style function prototypes:
+This constraint adds the phrase ``with compatible types'' to the {\c11} constraint, to allow
+overloading.
+\end{rationale}
+An identifier declared by a type declaration shall not be redeclared as a parameter in a function
+definition whose declarator includes an identifier list.
+\begin{rationale}
+This restriction echos {\c11}'s ban on the redeclaration of typedef names as parameters. This
+avoids an ambiguity between old-style function declarations and new-style function prototypes:
 \begin{lstlisting}
 void f( Complex,        // ... 3000 characters ...
 void g( Complex,        // ... 3000 characters ...
 int Complex;
 { ... }
+\end{lstlisting}
 Without the rule, \lstinline$Complex$ would be a type in the first case, and a parameter name in the second.
+int Complex; { ... }
+\end{lstlisting}
+Without the rule, \lstinline$Complex$ would be a type in the first case, and a parameter name in the
+second.
 \end{rationale}
 …
 \semantics
+\CFA extends the {\c11} definition of \define{anonymous structure} to include structure specifiers with tags, and extends the {\c11} definition of \define{anonymous union} to include union specifiers with tags.
+\CFA extends the {\c11} definition of \define{anonymous structure} to include structure
+specifiers with tags, and extends the {\c11} definition of \define{anonymous union} to include union
+specifiers with tags.
 \begin{rationale}
 This extension imitates an extension in the Plan 9 C compiler \cite{Thompson90new}.
 …
 cp.x = 0;
 cp.color = RED;
 struct literal {@\impl{literal}@
         enum { NUMBER, STRING } tag;
         union {
                 double n;
                 char *s;
+         double n;
+         char *s;
         };
 };
 …
 \begin{comment}
 \constraints
+If the \nonterm{declaration-specifiers} of a declaration that contains a \nonterm{forall-specifier} declares a structure or union tag, the types of the members of the structure or union shall not use any of the type identifiers declared by the \nonterm{type-parameter-list}.
+\begin{rationale}
+This sort of declaration is illegal because the scope of the type identifiers ends at the end of the declaration, but the scope of the structure tag does not.
+\begin{lstlisting}
+forall( type T ) struct Pair { T a, b;
+} mkPair( T, T ); // illegal
+\end{lstlisting}
+If an instance of \lstinline$struct Pair$ was declared later in the current scope, what would the members' type be?
+If the \nonterm{declaration-specifiers} of a declaration that contains a \nonterm{forall-specifier}
+declares a structure or union tag, the types of the members of the structure or union shall not use
+any of the type identifiers declared by the \nonterm{type-parameter-list}.
+\begin{rationale}
+This sort of declaration is illegal because the scope of the type identifiers ends at the end of the
+declaration, but the scope of the structure tag does not.
+\begin{lstlisting}
+forall( type T ) struct Pair { T a, b; } mkPair( T, T ); // illegal
+\end{lstlisting}
+If an instance of \lstinline$struct Pair$ was declared later in the current scope, what would the
+members' type be?
 \end{rationale}
 \end{comment}
 \semantics
+The \nonterm{type-parameter-list}s and assertions of the \nonterm{forall-specifier}s declare type identifiers, function and object identifiers with \Index{no linkage}.
+The \nonterm{type-parameter-list}s and assertions of the \nonterm{forall-specifier}s declare type
+identifiers, function and object identifiers with \Index{no linkage}.
 If, in the declaration ``\lstinline$T D$'', \lstinline$T$ contains \nonterm{forall-specifier}s and
 …
 \begin{lstlisting}
 D( @\normalsize\nonterm{parameter-type-list}@ )
+\end{lstlisting} then a type identifier declared by one of the \nonterm{forall-specifier}s is an \define{inferred parameter} of the function declarator if and only if it is not an inferred parameter of a function declarator in \lstinline$D$, and it is used in the type of a parameter in the following
+\end{lstlisting}
+then a type identifier declared by one of the \nonterm{forall-specifier}s is an \define{inferred
+parameter} of the function declarator if and only if it is not an inferred parameter of a function
+declarator in \lstinline$D$, and it is used in the type of a parameter in the following
 \nonterm{type-parameter-list} or it and an inferred parameter are used as arguments of a
+\Index{specification} in one of the \nonterm{forall-specifier}s.
+The identifiers declared by assertions that use an inferred parameter of a function declarator are \Index{assertion parameter}s of that function declarator.
+\Index{specification} in one of the \nonterm{forall-specifier}s. The identifiers declared by
+assertions that use an inferred parameter of a function declarator are \Index{assertion parameter}s
+of that function declarator.
 \begin{comment}
 \begin{rationale}
+Since every inferred parameter is used by some parameter, inference can be understood as a single bottom-up pass over the expression tree, that only needs to apply local reasoning at each node.
+Since every inferred parameter is used by some parameter, inference can be understood as a single
+bottom-up pass over the expression tree, that only needs to apply local reasoning at each node.
 If this restriction were lifted, it would be possible to write
 \begin{lstlisting}
+forall( type T ) T * alloc( void );@\use{alloc}@ int *p = alloc();
+forall( type T ) T * alloc( void );@\use{alloc}@
+int *p = alloc();
 \end{lstlisting}
 Here \lstinline$alloc()$ would receive \lstinline$int$ as an inferred argument, and return an
+\lstinline$int *$.
+In general, if a call to \lstinline$alloc()$ is a subexpression of an expression involving polymorphic functions and overloaded identifiers, there could be considerable distance between the call and the subexpression that causes \lstinline$T$ to be bound.
+\lstinline$int *$. In general, if a call to \lstinline$alloc()$ is a subexpression of an expression
+involving polymorphic functions and overloaded identifiers, there could be considerable distance
+between the call and the subexpression that causes \lstinline$T$ to be bound.
 With the current restriction, \lstinline$alloc()$ must be given an argument that determines
 …
 \end{comment}
 If a function declarator is part of a function definition, its inferred parameters and assertion parameters have \Index{block scope};
 otherwise, identifiers declared by assertions have a
+If a function declarator is part of a function definition, its inferred parameters and assertion
+parameters have \Index{block scope}; otherwise, identifiers declared by assertions have a
 \define{declaration scope}, which terminates at the end of the \nonterm{declaration}.
 A function type that has at least one inferred parameter is a \define{polymorphic function} type.
+Function types with no inferred parameters are \define{monomorphic function} types.
+One function type is \define{less polymorphic} than another if it has fewer inferred parameters, or if it has the same number of inferred parameters and fewer of its explicit parameters have types that depend on an inferred parameter.
+The names of inferred parameters and the order of identifiers in forall specifiers are not relevant to polymorphic function type compatibility.
+Let $f$ and $g$ be two polymorphic function types with the same number of inferred parameters, and let $f_i$ and $g_i$ be the inferred parameters of $f$ and $g$ in their order of occurance in the function types' \nonterm{parameter-type-list}s.
+Let $f'$ be $f$ with every occurrence of $f_i$ replaced by $g_i$, for all $i$.
+Then $f$ and $g$ are
+\Index{compatible type}s if $f'$'s and $g$'s return types and parameter lists are compatible, and if for every assertion parameter of $f'$ there is an assertion parameter in $g$ with the same identifier and compatible type, and vice versa.
+Function types with no inferred parameters are \define{monomorphic function} types. One function
+type is \define{less polymorphic} than another if it has fewer inferred parameters, or if it has the
+same number of inferred parameters and fewer of its explicit parameters have types that depend on an
+inferred parameter.
+The names of inferred parameters and the order of identifiers in forall specifiers are not relevant
+to polymorphic function type compatibility. Let $f$ and $g$ be two polymorphic function types with
+the same number of inferred parameters, and let $f_i$ and $g_i$ be the inferred parameters of $f$
+and $g$ in their order of occurance in the function types' \nonterm{parameter-type-list}s. Let $f'$
+be $f$ with every occurrence of $f_i$ replaced by $g_i$, for all $i$. Then $f$ and $g$ are
+\Index{compatible type}s if $f'$'s and $g$'s return types and parameter lists are compatible, and if
+for every assertion parameter of $f'$ there is an assertion parameter in $g$ with the same
+identifier and compatible type, and vice versa.
 \examples
 …
 forall( type T ) T (*pfT )( T ) = fT;
 \end{lstlisting}
+\lstinline$pfi$ and \lstinline$pfT$ are pointers to functions. \lstinline$pfT$ is not polymorphic, but the function it points at is.
+\lstinline$pfi$ and \lstinline$pfT$ are pointers to functions. \lstinline$pfT$ is not
+polymorphic, but the function it points at is.
 \begin{lstlisting}
 int (*fvpfi( void ))( int ) {
 …
+}
 \end{lstlisting}
+\lstinline$fvpfi()$ and \lstinline$fvpfT()$ are functions taking no arguments and returning pointers to functions. \lstinline$fvpfT()$ is monomorphic, but the function that its return value points at is polymorphic.
+\lstinline$fvpfi()$ and \lstinline$fvpfT()$ are functions taking no arguments and returning pointers
+to functions. \lstinline$fvpfT()$ is monomorphic, but the function that its return value points
+at is polymorphic.
 \begin{lstlisting}
 forall( type T ) int ( *fTpfi( T ) )( int );
 …
 forall( type T, type U ) U ( *fTpfU( T ) )( U );
 \end{lstlisting}
+\lstinline$fTpfi()$ is a polymorphic function that returns a pointer to a monomorphic function taking an integer and returning an integer.
+It could return \lstinline$pfi$. \lstinline$fTpfT()$ is subtle: it is a polymorphic function returning a \emph{monomorphic} function taking and returning
+\lstinline$T$, where \lstinline$T$ is an inferred parameter of \lstinline$fTpfT()$.
+For instance, in the expression ``\lstinline$fTpfT(17)$'', \lstinline$T$ is inferred to be \lstinline$int$, and the returned value would have type \lstinline$int ( * )( int )$. ``\lstinline$fTpfT(17)(13)$'' and
+\lstinline$fTpfi()$ is a polymorphic function that returns a pointer to a monomorphic function
+taking an integer and returning an integer. It could return \lstinline$pfi$. \lstinline$fTpfT()$
+is subtle: it is a polymorphic function returning a \emph{monomorphic} function taking and returning
+\lstinline$T$, where \lstinline$T$ is an inferred parameter of \lstinline$fTpfT()$. For instance,
+in the expression ``\lstinline$fTpfT(17)$'', \lstinline$T$ is inferred to be \lstinline$int$, and
+the returned value would have type \lstinline$int ( * )( int )$. ``\lstinline$fTpfT(17)(13)$'' and
 ``\lstinline$fTpfT("yes")("no")$'' are legal, but ``\lstinline$fTpfT(17)("no")$'' is illegal.
+\lstinline$fTpfU()$ is polymorphic ( in type \lstinline$T$), and returns a pointer to a function that is polymorphic ( in type \lstinline$U$). ``\lstinline$f5(17)("no")$'' is a legal expression of type
+\lstinline$fTpfU()$ is polymorphic ( in type \lstinline$T$), and returns a pointer to a function that
+is polymorphic ( in type \lstinline$U$). ``\lstinline$f5(17)("no")$'' is a legal expression of type
 \lstinline$char *$.
 \begin{lstlisting}
 …
 forall( type U, type V, type W ) U * g( V *, U, W * const );
 \end{lstlisting}
+The functions \lstinline$f()$ and \lstinline$g()$ have compatible types.
+Let \(f\) and \(g\) be their types;
+then \(f_1\) = \lstinline$T$, \(f_2\) = \lstinline$U$, \(f_3\) = \lstinline$V$, \(g_1\)
+= \lstinline$V$, \(g_2\) = \lstinline$U$, and \(g_3\) = \lstinline$W$.
+Replacing every \(f_i\) by \(g_i\) in \(f\) gives
+The functions \lstinline$f()$ and \lstinline$g()$ have compatible types. Let \(f\) and \(g\) be
+their types; then \(f_1\) = \lstinline$T$, \(f_2\) = \lstinline$U$, \(f_3\) = \lstinline$V$, \(g_1\)
+= \lstinline$V$, \(g_2\) = \lstinline$U$, and \(g_3\) = \lstinline$W$. Replacing every \(f_i\)
+by \(g_i\) in \(f\) gives
 \begin{lstlisting}
 forall( type V, type U, type W ) U * f( V *, U, W * const );
+\end{lstlisting} which has a return type and parameter list that is compatible with \(g\).
+\begin{rationale}
+The word ``\lstinline$type$'' in a forall specifier is redundant at the moment, but I want to leave room for inferred parameters of ordinary types in case parameterized types get added one day.
+\end{lstlisting}
+which has a return type and parameter list that is compatible with \(g\).
+\begin{rationale}
+The word ``\lstinline$type$'' in a forall specifier is redundant at the moment, but I want to leave
+room for inferred parameters of ordinary types in case parameterized types get added one day.
 Even without parameterized types, I might try to allow
 \begin{lstlisting}
 forall( int n ) int sum( int vector[n] );
+\end{lstlisting} but C currently rewrites array parameters as pointer parameters, so the effects of such a change require more thought.
+\end{rationale}
+\begin{rationale}
+A polymorphic declaration must do two things: it must introduce type parameters, and it must apply assertions to those types.
+Adding this to existing C declaration syntax and semantics was delicate, and not entirely successful.
+C depends on declaration-before-use, so a forall specifier must introduce type names before they can be used in the declaration specifiers.
+This could be done by making the forall specifier part of the declaration specifiers, or by making it a new introductory clause of declarations.
+Assertions are also part of polymorphic function types, because it must be clear which functions have access to the assertion parameters declared by the assertions.
+All attempts to put assertions inside an introductory clause produced complex semantics and confusing code.
+Building them into the declaration specifiers could be done by placing them in the function's parameter list, or in a forall specifier that is a declaration specifier.
+Assertions are also used with type parameters of specifications, and by type declarations.
+For consistency's sake it seems best to attach assertions to the type declarations in forall specifiers, which means that forall specifiers must be declaration specifiers.
+\end{lstlisting}
+but C currently rewrites array parameters as pointer parameters, so the effects of such a change
+require more thought.
+\end{rationale}
+\begin{rationale}
+A polymorphic declaration must do two things: it must introduce type parameters, and it must apply
+assertions to those types. Adding this to existing C declaration syntax and semantics was delicate,
+and not entirely successful.
+C depends on declaration-before-use, so a forall specifier must introduce type names before they can
+be used in the declaration specifiers. This could be done by making the forall specifier part of
+the declaration specifiers, or by making it a new introductory clause of declarations.
+Assertions are also part of polymorphic function types, because it must be clear which functions
+have access to the assertion parameters declared by the assertions. All attempts to put assertions
+inside an introductory clause produced complex semantics and confusing code. Building them into the
+declaration specifiers could be done by placing them in the function's parameter list, or in a
+forall specifier that is a declaration specifier. Assertions are also used with type parameters of
+specifications, and by type declarations. For consistency's sake it seems best to attach assertions
+to the type declarations in forall specifiers, which means that forall specifiers must be
+declaration specifiers.
 \end{rationale}
 %HERE
 …
 \constraints
+\lstinline$restrict$\index{register@{\lstinline$restrict$}} Types other than type parameters and pointer types whose referenced type is an object type shall not be restrict-qualified.
+\lstinline$restrict$\index{register@{\lstinline$restrict$}} Types other than type parameters and
+pointer types whose referenced type is an object type shall not be restrict-qualified.
 \semantics
+An object's type may be a restrict-qualified type parameter. \lstinline$restrict$ does not establish any special semantics in that case.
+\begin{rationale}
+\CFA loosens the constraint on the restrict qualifier so that restrict-qualified pointers may be passed to polymorphic functions.
+\end{rationale}
+\lstinline$lvalue$ may be used to qualify the return type of a function type.
+Let \lstinline$T$ be an unqualified version of a type;
+then the result of calling a function with return type
+An object's type may be a restrict-qualified type parameter. \lstinline$restrict$ does not
+establish any special semantics in that case.
+\begin{rationale}
+\CFA loosens the constraint on the restrict qualifier so that restrict-qualified pointers may be
+passed to polymorphic functions.
+\end{rationale}
+\lstinline$lvalue$ may be used to qualify the return type of a function type. Let \lstinline$T$ be
+an unqualified version of a type; then the result of calling a function with return type
 \lstinline$lvalue T$ is a \Index{modifiable lvalue} of type \lstinline$T$.
+\lstinline$const$\use{const} and \lstinline$volatile$\use{volatile} qualifiers may also be added to indicate that the function result is a constant or volatile lvalue.
+\begin{rationale}
+The \lstinline$const$ and \lstinline$volatile$ qualifiers can only be sensibly used to qualify the return type of a function if the \lstinline$lvalue$ qualifier is also used.
+\end{rationale}
+An {lvalue}-qualified type may be used in a \Index{cast expression} if the operand is an lvalue;
+the result of the expression is an lvalue.
+\begin{rationale}
+\lstinline$lvalue$ provides some of the functionality of {\CC}'s ``\lstinline$T&$'' ( reference to object of type \lstinline$T$) type.
+Reference types have four uses in {\CC}.
+\lstinline$const$\use{const} and \lstinline$volatile$\use{volatile} qualifiers may also be added to
+indicate that the function result is a constant or volatile lvalue.
+\begin{rationale}
+The \lstinline$const$ and \lstinline$volatile$ qualifiers can only be sensibly used to qualify the
+return type of a function if the \lstinline$lvalue$ qualifier is also used.
+\end{rationale}
+An {lvalue}-qualified type may be used in a \Index{cast expression} if the operand is an lvalue; the
+result of the expression is an lvalue.
+\begin{rationale}
+\lstinline$lvalue$ provides some of the functionality of {\CC}'s ``\lstinline$T&$'' ( reference to
+object of type \lstinline$T$) type. Reference types have four uses in {\CC}.
 \begin{itemize}
 \item
 …
 \item
+A reference can be used to define an alias for a complicated lvalue expression, as a way of getting some of the functionality of the Pascal \lstinline$with$ statement.
+The following {\CC} code gives an example.
+A reference can be used to define an alias for a complicated lvalue expression, as a way of getting
+some of the functionality of the Pascal \lstinline$with$ statement. The following {\CC} code gives
+an example.
 \begin{lstlisting}
+{
 …
 \item
+A reference parameter can be used to allow a function to modify an argument without forcing the caller to pass the address of the argument.
+This is most useful for user-defined assignment operators.
+In {\CC}, plain assignment is done by a function called ``\lstinline$operator=$'', and the two expressions
+A reference parameter can be used to allow a function to modify an argument without forcing the
+caller to pass the address of the argument. This is most useful for user-defined assignment
+operators. In {\CC}, plain assignment is done by a function called ``\lstinline$operator=$'', and
+the two expressions
 \begin{lstlisting}
 a = b;
 operator=( a, b );
 \end{lstlisting} are equivalent.
+If \lstinline$a$ and \lstinline$b$ are of type \lstinline$T$, then the first parameter of \lstinline$operator=$ must have type ``\lstinline$T&$''.
 It cannot have type
+\end{lstlisting}
+are equivalent. If \lstinline$a$ and \lstinline$b$ are of type \lstinline$T$, then the first
+parameter of \lstinline$operator=$ must have type ``\lstinline$T&$''. It cannot have type
 \lstinline$T$, because then assignment couldn't alter the variable, and it can't have type
 ``\lstinline$T *$'', because the assignment would have to be written ``\lstinline$&a = b;$''.
+In the case of user-defined operators, this could just as well be handled by using pointer types and by changing the rewrite rules so that ``\lstinline$a = b;$'' is equivalent to
+``\lstinline$operator=(&( a), b )$''.
+Reference parameters of ``normal'' functions are Bad Things, because they remove a useful property of C function calls: an argument can only be modified by a function if it is preceded by ``\lstinline$&$''.
+In the case of user-defined operators, this could just as well be handled by using pointer types and
+by changing the rewrite rules so that ``\lstinline$a = b;$'' is equivalent to
+``\lstinline$operator=(&( a), b )$''. Reference parameters of ``normal'' functions are Bad Things,
+because they remove a useful property of C function calls: an argument can only be modified by a
+function if it is preceded by ``\lstinline$&$''.
 \item
 …
 void fiddle( const Thing & );
 \end{lstlisting}
+If the second form is used, then constructors and destructors are not invoked to create a temporary variable at the call site ( and it is bad style for the caller to make any assumptions about such things), and within \lstinline$fiddle$ the parameter is subject to the usual problems caused by aliases.
+The reference form might be chosen for efficiency's sake if \lstinline$Thing$s are too large or their constructors or destructors are too expensive.
+An implementation may switch between them without causing trouble for well-behaved clients.
+This leaves the implementor to define ``too large'' and ``too expensive''.
+If the second form is used, then constructors and destructors are not invoked to create a temporary
+variable at the call site ( and it is bad style for the caller to make any assumptions about such
+things), and within \lstinline$fiddle$ the parameter is subject to the usual problems caused by
+aliases. The reference form might be chosen for efficiency's sake if \lstinline$Thing$s are too
+large or their constructors or destructors are too expensive. An implementation may switch between
+them without causing trouble for well-behaved clients. This leaves the implementor to define ``too
+large'' and ``too expensive''.
 I propose to push this job onto the compiler by allowing it to implement
 \begin{lstlisting}
 void fiddle( const volatile Thing );
+\end{lstlisting} with call-by-reference.
+Since it knows all about the size of \lstinline$Thing$s and the parameter passing mechanism, it should be able to come up with a better definition of ``too large'', and may be able to make a good guess at ``too expensive''.
+\end{lstlisting}
+with call-by-reference. Since it knows all about the size of \lstinline$Thing$s and the parameter
+passing mechanism, it should be able to come up with a better definition of ``too large'', and may
+be able to make a good guess at ``too expensive''.
 \end{itemize}
+In summary, since references are only really necessary for returning lvalues, I'll only provide lvalue functions.
+In summary, since references are only really necessary for returning lvalues, I'll only provide
+lvalue functions.
 \end{rationale}
 …
 \subsection{Initialization}
+An expression that is used as an \nonterm{initializer} is treated as being cast to the type of the object being initialized.
+An expression used in an \nonterm{initializer-list} is treated as being cast to the type of the aggregate member that it initializes.
+In either case the cast must have a single unambiguous \Index{interpretation}.
+An expression that is used as an \nonterm{initializer} is treated as being cast to the type of the
+object being initialized. An expression used in an \nonterm{initializer-list} is treated as being
+cast to the type of the aggregate member that it initializes. In either case the cast must have a
+single unambiguous \Index{interpretation}.
 …
 \end{syntax}
 \begin{rationale}
+The declarations allowed in a specification are much the same as those allowed in a structure, except that bit fields are not allowed, and \Index{incomplete type}s and function types are allowed.
+The declarations allowed in a specification are much the same as those allowed in a structure,
+except that bit fields are not allowed, and \Index{incomplete type}s and function types are allowed.
 \end{rationale}
 \semantics
+A \define{specification definition} defines a name for a \define{specification}: a parameterized collection of object and function declarations.
+A \define{specification definition} defines a name for a \define{specification}: a parameterized
+collection of object and function declarations.
 The declarations in a specification consist of the declarations in the
 \nonterm{spec-declaration-list} and declarations produced by any assertions in the
+\nonterm{spec-parameter-list}.
+If the collection contains two declarations that declare the same identifier and have compatible types, they are combined into one declaration with the composite type constructed from the two types.
+\nonterm{spec-parameter-list}. If the collection contains two declarations that declare the same
+identifier and have compatible types, they are combined into one declaration with the composite type
+constructed from the two types.
 …
 \constraints
+The \nonterm{identifier} in an assertion that is not a \nonterm{spec-declaration} shall be the name of a specification.
+The \nonterm{type-name-list} shall contain one \nonterm{type-name} argument for each \nonterm{type-parameter} in that specification's \nonterm{spec-parameter-list}.
+If the
+\nonterm{type-parameter} uses type-class \lstinline$type$\use{type}, the argument shall be the type name of an \Index{object type};
+if it uses \lstinline$dtype$, the argument shall be the type name of an object type or an \Index{incomplete type};
+and if it uses \lstinline$ftype$, the argument shall be the type name of a \Index{function type}.
+The \nonterm{identifier} in an assertion that is not a \nonterm{spec-declaration} shall be the name
+of a specification. The \nonterm{type-name-list} shall contain one \nonterm{type-name} argument for
+each \nonterm{type-parameter} in that specification's \nonterm{spec-parameter-list}. If the
+\nonterm{type-parameter} uses type-class \lstinline$type$\use{type}, the argument shall be the type
+name of an \Index{object type}; if it uses \lstinline$dtype$, the argument shall be the type name of
+an object type or an \Index{incomplete type}; and if it uses \lstinline$ftype$, the argument shall
+be the type name of a \Index{function type}.
 \semantics
 …
 \define{assertion parameters}.
+The assertion parameters produced by an assertion that applies the name of a specification to type arguments are found by taking the declarations specified in the specification and treating each of the specification's parameters as a synonym for the corresponding \nonterm{type-name} argument.
+The collection of assertion parameters produced by the \nonterm{assertion-list} are found by combining the declarations produced by each assertion.
+If the collection contains two declarations that declare the same identifier and have compatible types, they are combined into one declaration with the \Index{composite type} constructed from the two types.
+The assertion parameters produced by an assertion that applies the name of a specification to type
+arguments are found by taking the declarations specified in the specification and treating each of
+the specification's parameters as a synonym for the corresponding \nonterm{type-name} argument.
+The collection of assertion parameters produced by the \nonterm{assertion-list} are found by
+combining the declarations produced by each assertion. If the collection contains two declarations
+that declare the same identifier and have compatible types, they are combined into one declaration
+with the \Index{composite type} constructed from the two types.
 \examples
 …
         return val + val;
+}
 context summable( type T ) {@\impl{summable}@
         T ?+=?( T *, T );@\use{?+=?}@
 …
 context sum_list( type List, type Element | summable( Element ) | list_of( List, Element ) ) {};
 \end{lstlisting}
+\lstinline$sum_list$ contains seven declarations, which describe a list whose elements can be added up.
+The assertion ``\lstinline$|sum_list( i_list, int )$''\use{sum_list} produces the assertion parameters
+\lstinline$sum_list$ contains seven declarations, which describe a list whose elements can be added
+up. The assertion ``\lstinline$|sum_list( i_list, int )$''\use{sum_list} produces the assertion
+parameters
 \begin{lstlisting}
 int ?+=?( int *, int );
 …
 \constraints
+If a type declaration has block scope, and the declared identifier has external or internal linkage, the declaration shall have no initializer for the identifier.
+If a type declaration has block scope, and the declared identifier has external or internal linkage,
+the declaration shall have no initializer for the identifier.
 \semantics
+A \nonterm{type-parameter} or a \nonterm{type-declarator} declares an identifier to be a \Index{type name} for a type incompatible with all other types.
+An identifier declared by a \nonterm{type-parameter} has \Index{no linkage}.
+Identifiers declared with type-class \lstinline$type$\use{type} are \Index{object type}s;
+those declared with type-class
+\lstinline$dtype$\use{dtype} are \Index{incomplete type}s;
+and those declared with type-class
+\lstinline$ftype$\use{ftype} are \Index{function type}s.
+The identifier has \Index{block scope} that terminates at the end of the \nonterm{spec-declaration-list} or polymorphic function that contains the \nonterm{type-parameter}.
+A \nonterm{type-declarator} with an \Index{initializer} is a \define{type definition}.  The declared identifier is an \Index{incomplete type} within the initializer, and an \Index{object type} after the end of the initializer.
+The type in the initializer is called the \define{implementation
+  type}.
+Within the scope of the declaration, \Index{implicit conversion}s can be performed between the defined type and the implementation type, and between pointers to the defined type and pointers to the implementation type.
+A type declaration without an \Index{initializer} and without a \Index{storage-class specifier} or with storage-class specifier \lstinline$static$\use{static} defines an \Index{incomplete type}.
+If a
+\Index{translation unit} or \Index{block} contains one or more such declarations for an identifier, it must contain exactly one definition of the identifier ( but not in an enclosed block, which would define a new type known only within that block).
+A \nonterm{type-parameter} or a \nonterm{type-declarator} declares an identifier to be a \Index{type
+name} for a type incompatible with all other types.
+An identifier declared by a \nonterm{type-parameter} has \Index{no linkage}. Identifiers declared
+with type-class \lstinline$type$\use{type} are \Index{object type}s; those declared with type-class
+\lstinline$dtype$\use{dtype} are \Index{incomplete type}s; and those declared with type-class
+\lstinline$ftype$\use{ftype} are \Index{function type}s. The identifier has \Index{block scope} that
+terminates at the end of the \nonterm{spec-declaration-list} or polymorphic function that contains
+the \nonterm{type-parameter}.
+A \nonterm{type-declarator} with an \Index{initializer} is a \define{type definition}.  The declared
+identifier is an \Index{incomplete type} within the initializer, and an \Index{object type} after
+the end of the initializer. The type in the initializer is called the \define{implementation
+  type}. Within the scope of the declaration, \Index{implicit conversion}s can be performed between
+the defined type and the implementation type, and between pointers to the defined type and pointers
+to the implementation type.
+A type declaration without an \Index{initializer} and without a \Index{storage-class specifier} or
+with storage-class specifier \lstinline$static$\use{static} defines an \Index{incomplete type}. If a
+\Index{translation unit} or \Index{block} contains one or more such declarations for an identifier,
+it must contain exactly one definition of the identifier ( but not in an enclosed block, which would
+define a new type known only within that block).
 \begin{rationale}
 Incomplete type declarations allow compact mutually-recursive types.
 \begin{lstlisting}
 type t1; // incomplete type declaration
+type t1; // Incomplete type declaration.
 type t2 = struct { t1 * p; ... };
 type t1 = struct { t2 * p; ... };
 \end{lstlisting}
+Without them, mutual recursion could be handled by declaring mutually recursive structures, then initializing the types to those structures.
+Without them, mutual recursion could be handled by declaring mutually recursive structures, then
+initializing the types to those structures.
 \begin{lstlisting}
 struct s1;
 …
 type t1 = struct s1 { struct s2 * p; ... };
 \end{lstlisting}
+This introduces extra names, and may force the programmer to cast between the types and their implementations.
+This introduces extra names, and may force the programmer to cast between the types and their
+implementations.
 \end{rationale}
 A type declaration without an initializer and with \Index{storage-class specifier}
 \lstinline$extern$\use{extern} is an \define{opaque type declaration}.
 Opaque types are
+\Index{object type}s.
+An opaque type is not a \nonterm{constant-expression};
+neither is a structure or union that has a member whose type is not a \nonterm{constant-expression}.  Every other
 \Index{object type} is a \nonterm{constant-expression}.
+Objects with static storage duration shall be declared with a type that is a \nonterm{constant-expression}.
+\begin{rationale}
 Type declarations can declare identifiers with external linkage, whereas typedef declarations declare identifiers that only exist within a translation unit.
+These opaque types can be used in declarations, but the implementation of the type is not visible.
+Static objects can not have opaque types because space for them would have to be allocated at program start-up.
 This is a deficiency\index{deficiencies!static opaque objects}, but I don't want to deal with ``module initialization'' code just now.
 \end{rationale}
 An \Index{incomplete type} which is not a qualified version\index{qualified type} of a type is a value of \Index{type-class} \lstinline$dtype$.
+An object type\index{object types} which is not a qualified version of a type is a value of type-classes \lstinline$type$ and \lstinline$dtype$.
+A
+\lstinline$extern$\use{extern} is an \define{opaque type declaration}. Opaque types are
+\Index{object type}s. An opaque type is not a \nonterm{constant-expression}; neither is a structure
+or union that has a member whose type is not a \nonterm{constant-expression}.  Every other
+\Index{object type} is a \nonterm{constant-expression}. Objects with static storage duration shall
+be declared with a type that is a \nonterm{constant-expression}.
+\begin{rationale}
+Type declarations can declare identifiers with external linkage, whereas typedef declarations
+declare identifiers that only exist within a translation unit. These opaque types can be used in
+declarations, but the implementation of the type is not visible.
+Static objects can not have opaque types because space for them would have to be allocated at
+program start-up. This is a deficiency\index{deficiencies!static opaque objects}, but I don't want
+to deal with ``module initialization'' code just now.
+\end{rationale}
+An \Index{incomplete type} which is not a qualified version\index{qualified type} of a type is a
+value of \Index{type-class} \lstinline$dtype$. An object type\index{object types} which is not a
+qualified version of a type is a value of type-classes \lstinline$type$ and \lstinline$dtype$. A
 \Index{function type} is a value of type-class \lstinline$ftype$.
 \begin{rationale}
+Syntactically, a type value is a \nonterm{type-name}, which is a declaration for an object which omits the identifier being declared.
+Object types are precisely the types that can be instantiated.
+Type qualifiers are not included in type values because the compiler needs the information they provide at compile time to detect illegal statements or to produce efficient machine instructions.
+For instance, the code that a compiler must generate to manipulate an object that has volatile-qualified type may be different from the code to manipulate an ordinary object.
+Type qualifiers are a weak point of C's type system.
+Consider the standard library function
+\lstinline$strchr()$ which, given a string and a character, returns a pointer to the first occurrence of the character in the string.
+Syntactically, a type value is a \nonterm{type-name}, which is a declaration for an object which
+omits the identifier being declared.
+Object types are precisely the types that can be instantiated. Type qualifiers are not included in
+type values because the compiler needs the information they provide at compile time to detect
+illegal statements or to produce efficient machine instructions. For instance, the code that a
+compiler must generate to manipulate an object that has volatile-qualified type may be different
+from the code to manipulate an ordinary object.
+Type qualifiers are a weak point of C's type system. Consider the standard library function
+\lstinline$strchr()$ which, given a string and a character, returns a pointer to the first
+occurrence of the character in the string.
 \begin{lstlisting}
 char *strchr( const char *s, int c ) {@\impl{strchr}@
         char real_c = c; // done because c was declared as int.
         for ( ; *s != real_c; s++ )
                 if ( *s == '\0' ) return NULL;
+         if ( *s == '\0' ) return NULL;
         return ( char * )s;
+}
 \end{lstlisting}
+The parameter \lstinline$s$ must be \lstinline$const char *$, because \lstinline$strchr()$ might be used to search a constant string, but the return type must be \lstinline$char *$, because the result might be used to modify a non-constant string.
+Hence the body must perform a cast, and ( even worse)
+\lstinline$strchr()$ provides a type-safe way to attempt to modify constant strings.
+What is needed is some way to say that \lstinline$s$'s type might contain qualifiers, and the result type has exactly the same qualifiers.
+Polymorphic functions do not provide a fix for this deficiency\index{deficiencies!pointers to qualified types}, because type qualifiers are not part of type values.
+Instead, overloading can be used to define \lstinline$strchr()$ for each combination of qualifiers.
+\end{rationale}
+\begin{rationale}
+Since \Index{incomplete type}s are not type values, they can not be used as the initializer in a type declaration, or as the type of a structure or union member.
+This prevents the declaration of types that contain each other.
+The parameter \lstinline$s$ must be \lstinline$const char *$, because \lstinline$strchr()$ might be
+used to search a constant string, but the return type must be \lstinline$char *$, because the result
+might be used to modify a non-constant string. Hence the body must perform a cast, and ( even worse)
+\lstinline$strchr()$ provides a type-safe way to attempt to modify constant strings. What is needed
+is some way to say that \lstinline$s$'s type might contain qualifiers, and the result type has
+exactly the same qualifiers. Polymorphic functions do not provide a fix for this
+deficiency\index{deficiencies!pointers to qualified types}, because type qualifiers are not part of
+type values. Instead, overloading can be used to define \lstinline$strchr()$ for each combination
+of qualifiers.
+\end{rationale}
+\begin{rationale}
+Since \Index{incomplete type}s are not type values, they can not be used as the initializer in a
+type declaration, or as the type of a structure or union member. This prevents the declaration of
+types that contain each other.
 \begin{lstlisting}
 type t1;
 type t2 = t1; // illegal: incomplete type t1
+type t2 = t1; // illegal: incomplete type t1.
 type t1 = t2;
 \end{lstlisting}
 The initializer in a file-scope declaration must be a constant expression.
 This means type declarations can not build on opaque types, which is a deficiency\index{deficiencies!nesting opaque
+The initializer in a file-scope declaration must be a constant expression. This means type
+declarations can not build on opaque types, which is a deficiency\index{deficiencies!nesting opaque
  types}.
 \begin{lstlisting}
 extern type Huge; // extended-precision integer type
+extern type Huge; // extended-precision integer type.
 type Rational = struct {
         Huge numerator, denominator;    // illegal
 …
 \end{lstlisting}
 Without this restriction, \CFA might require ``module initialization'' code ( since
+\lstinline$Rational$ has external linkage, it must be created before any other translation unit instantiates it), and would force an ordering on the initialization of the translation unit that defines \lstinline$Huge$ and the translation that declares \lstinline$Rational$.
+A benefit of the restriction is that it prevents the declaration in separate translation units of types that contain each other, which would be hard to prevent otherwise.
+\lstinline$Rational$ has external linkage, it must be created before any other translation unit
+instantiates it), and would force an ordering on the initialization of the translation unit that
+defines \lstinline$Huge$ and the translation that declares \lstinline$Rational$.
+A benefit of the restriction is that it prevents the declaration in separate translation units of
+types that contain each other, which would be hard to prevent otherwise.
 \begin{lstlisting}
 //  File a.c:
 …
 \begin{rationale}
 Since a \nonterm{type-declaration} is a \nonterm{declaration} and not a
+\nonterm{struct-declaration}, type declarations can not be structure members.
+The form of
+\nonterm{struct-declaration}, type declarations can not be structure members. The form of
 \nonterm{type-declaration} forbids arrays of, pointers to, and functions returning \lstinline$type$.
+Hence the syntax of \nonterm{type-specifier} does not have to be extended to allow type-valued expressions.
+It also side-steps the problem of type-valued expressions producing different values in different declarations.
+Since a type declaration is not a \nonterm{parameter-declaration}, functions can not have explicit type parameters.
+This may be too restrictive, but it attempts to make compilation simpler.
+Recall that when traditional C scanners read in an identifier, they look it up in the symbol table to determine whether or not it is a typedef name, and return a ``type'' or ``identifier'' token depending on what they find.
+A type parameter would add a type name to the current scope.
+The scope manipulations involved in parsing the declaration of a function that takes function pointer parameters and returns a function pointer may just be too complicated.
+Explicit type parameters don't seem to be very useful, anyway, because their scope would not include the return type of the function.
+Consider the following attempt to define a type-safe memory allocation function.
+Hence the syntax of \nonterm{type-specifier} does not have to be extended to allow type-valued
+expressions. It also side-steps the problem of type-valued expressions producing different values
+in different declarations.
+Since a type declaration is not a \nonterm{parameter-declaration}, functions can not have explicit
+type parameters. This may be too restrictive, but it attempts to make compilation simpler. Recall
+that when traditional C scanners read in an identifier, they look it up in the symbol table to
+determine whether or not it is a typedef name, and return a ``type'' or ``identifier'' token
+depending on what they find. A type parameter would add a type name to the current scope. The
+scope manipulations involved in parsing the declaration of a function that takes function pointer
+parameters and returns a function pointer may just be too complicated.
+Explicit type parameters don't seem to be very useful, anyway, because their scope would not include
+the return type of the function. Consider the following attempt to define a type-safe memory
+allocation function.
 \begin{lstlisting}
 #include <stdlib.h>
 T * new( type T ) { return ( T * )malloc( sizeof( T) ); };
+@\ldots@ int * ip = new( int );
+\end{lstlisting}
+This looks sensible, but \CFA's declaration-before-use rules mean that ``\lstinline$T$'' in the function body refers to the parameter, but the ``\lstinline$T$'' in the return type refers to the meaning of \lstinline$T$ in the scope that contains \lstinline$new$;
+it could be undefined, or a type name, or a function or variable name.
+Nothing good can result from such a situation.
+@\ldots@
+int * ip = new( int );
+\end{lstlisting}
+This looks sensible, but \CFA's declaration-before-use rules mean that ``\lstinline$T$'' in the
+function body refers to the parameter, but the ``\lstinline$T$'' in the return type refers to the
+meaning of \lstinline$T$ in the scope that contains \lstinline$new$; it could be undefined, or a
+type name, or a function or variable name. Nothing good can result from such a situation.
 \end{rationale}
 …
 f2( v2 );
 \end{lstlisting}
+\lstinline$V1$ is passed by value, so \lstinline$f1()$'s assignment to \lstinline$a[0]$ does not modify v1.  \lstinline$V2$ is converted to a pointer, so \lstinline$f2()$ modifies \lstinline$v2[0]$.
+\lstinline$V1$ is passed by value, so \lstinline$f1()$'s assignment to \lstinline$a[0]$ does not
+modify v1.  \lstinline$V2$ is converted to a pointer, so \lstinline$f2()$ modifies
+\lstinline$v2[0]$.
 A translation unit containing the declarations
 \begin{lstlisting}
 extern type Complex;@\use{Complex}@ // opaque type declaration
+extern type Complex;@\use{Complex}@ // opaque type declaration.
 extern float abs( Complex );@\use{abs}@
+\end{lstlisting} can contain declarations of complex numbers, which can be passed to \lstinline$abs$.
+Some other translation unit must implement \lstinline$Complex$ and \lstinline$abs$.
+That unit might contain the declarations
+\end{lstlisting}
+can contain declarations of complex numbers, which can be passed to \lstinline$abs$. Some other
+translation unit must implement \lstinline$Complex$ and \lstinline$abs$. That unit might contain
+the declarations
 \begin{lstlisting}
 type Complex = struct { float re, im; };@\impl{Complex}@
 …
+}
 \end{lstlisting}
+Note that \lstinline$c$ is implicitly converted to a \lstinline$struct$ so that its components can be retrieved.
+Note that \lstinline$c$ is implicitly converted to a \lstinline$struct$ so that its components can
+be retrieved.
 \begin{lstlisting}
 …
 \begin{rationale}
+Within the scope of a type definition, an instance of the type can be viewed as having that type or as having the implementation type.
+In the \lstinline$Time_of_day$ example, the difference is important.
+Different languages have treated the distinction between the abstraction and the implementation in different ways.
+Within the scope of a type definition, an instance of the type can be viewed as having that type or
+as having the implementation type. In the \lstinline$Time_of_day$ example, the difference is
+important. Different languages have treated the distinction between the abstraction and the
+implementation in different ways.
 \begin{itemize}
 \item
+Inside a Clu cluster \cite{clu}, the declaration of an instance states which view applies.
+Two primitives called \lstinline$up$ and \lstinline$down$ can be used to convert between the views.
+\item
+The Simula class \cite{Simula87} is essentially a record type.
+Since the only operations on a record are member selection and assignment, which can not be overloaded, there is never any ambiguity as to whether the abstraction or the implementation view is being used.
+In {\CC}
+\cite{c++}, operations on class instances include assignment and ``\lstinline$&$'', which can be overloaded.
+A ``scope resolution'' operator can be used inside the class to specify whether the abstract or implementation version of the operation should be used.
+\item
+An Ada derived type definition \cite{ada} creates a new type from an old type, and also implicitly declares derived subprograms that correspond to the existing subprograms that use the old type as a parameter type or result type.
+The derived subprograms are clones of the existing subprograms with the old type replaced by the derived type.
+Literals and aggregates of the old type are also cloned.
+Inside a Clu cluster \cite{clu}, the declaration of an instance states which view applies. Two
+primitives called \lstinline$up$ and \lstinline$down$ can be used to convert between the views.
+\item
+The Simula class \cite{Simula87} is essentially a record type. Since the only operations on a
+record are member selection and assignment, which can not be overloaded, there is never any
+ambiguity as to whether the abstraction or the implementation view is being used. In {\CC}
+\cite{c++}, operations on class instances include assignment and ``\lstinline$&$'', which can be
+overloaded. A ``scope resolution'' operator can be used inside the class to specify whether the
+abstract or implementation version of the operation should be used.
+\item
+An Ada derived type definition \cite{ada} creates a new type from an old type, and also implicitly
+declares derived subprograms that correspond to the existing subprograms that use the old type as a
+parameter type or result type. The derived subprograms are clones of the existing subprograms with
+the old type replaced by the derived type. Literals and aggregates of the old type are also cloned.
 In other words, the abstract view provides exactly the same operations as the implementation view.
 This allows the abstract view to be used in all cases.
 The derived subprograms can be replaced by programmer-specified subprograms.
+This is an exception to the normal scope rules, which forbid duplicate definitions of a subprogram in a scope.
 In this case, explicit conversions between the derived type and the old type can be used.
+The derived subprograms can be replaced by programmer-specified subprograms. This is an exception
+to the normal scope rules, which forbid duplicate definitions of a subprogram in a scope. In this
+case, explicit conversions between the derived type and the old type can be used.
 \end{itemize}
+\CFA's rules are like Clu's, except that implicit conversions and conversion costs allow it to do away with most uses of \lstinline$up$ and \lstinline$down$.
+\CFA's rules are like Clu's, except that implicit conversions and
+conversion costs allow it to do away with most uses of \lstinline$up$ and \lstinline$down$.
 \end{rationale}
 …
 A declaration\index{type declaration} of a type identifier \lstinline$T$ with type-class
 \lstinline$type$ implicitly declares a \define{default assignment} function
+\lstinline$T ?=?( T *, T )$\use{?=?}, with the same \Index{scope} and \Index{linkage} as the identifier \lstinline$T$.
+\begin{rationale}
+Assignment is central to C's imperative programming style, and every existing C object type has assignment defined for it ( except for array types, which are treated as pointer types for purposes of assignment).
+Without this rule, nearly every inferred type parameter would need an accompanying assignment assertion parameter.
+If a type parameter should not have an assignment operation,
+\lstinline$dtype$ should be used.
+If a type should not have assignment defined, the user can define an assignment function that causes a run-time error, or provide an external declaration but no definition and thus cause a link-time error.
+\end{rationale}
+A definition\index{type definition} of a type identifier \lstinline$T$ with \Index{implementation type} \lstinline$I$ and type-class \lstinline$type$ implicitly defines a default assignment function.
+A definition\index{type definition} of a type identifier \lstinline$T$ with implementation type \lstinline$I$ and an assertion list implicitly defines \define{default function}s and
+\define{default object}s as declared by the assertion declarations.
+The default objects and functions have the same \Index{scope} and \Index{linkage} as the identifier \lstinline$T$.
+Their values are determined as follows:
+\lstinline$T ?=?( T *, T )$\use{?=?}, with the same \Index{scope} and \Index{linkage} as the
+identifier \lstinline$T$.
+\begin{rationale}
+Assignment is central to C's imperative programming style, and every existing C object type has
+assignment defined for it ( except for array types, which are treated as pointer types for purposes
+of assignment). Without this rule, nearly every inferred type parameter would need an accompanying
+assignment assertion parameter. If a type parameter should not have an assignment operation,
+\lstinline$dtype$ should be used. If a type should not have assignment defined, the user can define
+an assignment function that causes a run-time error, or provide an external declaration but no
+definition and thus cause a link-time error.
+\end{rationale}
+A definition\index{type definition} of a type identifier \lstinline$T$ with \Index{implementation
+type} \lstinline$I$ and type-class \lstinline$type$ implicitly defines a default assignment
+function. A definition\index{type definition} of a type identifier \lstinline$T$ with implementation
+type \lstinline$I$ and an assertion list implicitly defines \define{default function}s and
+\define{default object}s as declared by the assertion declarations. The default objects and
+functions have the same \Index{scope} and \Index{linkage} as the identifier \lstinline$T$. Their
+values are determined as follows:
 \begin{itemize}
 \item
+If at the definition of \lstinline$T$ there is visible a declaration of an object with the same name as the default object, and if the type of that object with all occurrence of \lstinline$I$ replaced by \lstinline$T$ is compatible with the type of the default object, then the default object is initialized with that object.
+Otherwise the scope of the declaration of \lstinline$T$ must contain a definition of the default object.
+If at the definition of \lstinline$T$ there is visible a declaration of an object with the same name
+as the default object, and if the type of that object with all occurrence of \lstinline$I$ replaced
+by \lstinline$T$ is compatible with the type of the default object, then the default object is
+initialized with that object. Otherwise the scope of the declaration of \lstinline$T$ must contain
+a definition of the default object.
 \item
+If at the definition of \lstinline$T$ there is visible a declaration of a function with the same name as the default function, and if the type of that function with all occurrence of \lstinline$I$ replaced by \lstinline$T$ is compatible with the type of the default function, then the default function calls that function after converting its arguments and returns the converted result.
+Otherwise, if \lstinline$I$ contains exactly one anonymous member\index{anonymous member} such that at the definition of \lstinline$T$ there is visible a declaration of a function with the same name as the default function, and the type of that function with all occurrences of the anonymous member's type in its parameter list replaced by \lstinline$T$ is compatible with the type of the default function, then the default function calls that function after converting its arguments and returns the result.
+Otherwise the scope of the declaration of \lstinline$T$ must contain a definition of the default function.
+If at the definition of \lstinline$T$ there is visible a declaration of a function with the same
+name as the default function, and if the type of that function with all occurrence of \lstinline$I$
+replaced by \lstinline$T$ is compatible with the type of the default function, then the default
+function calls that function after converting its arguments and returns the converted result.
+Otherwise, if \lstinline$I$ contains exactly one anonymous member\index{anonymous member} such that
+at the definition of \lstinline$T$ there is visible a declaration of a function with the same name
+as the default function, and the type of that function with all occurrences of the anonymous
+member's type in its parameter list replaced by \lstinline$T$ is compatible with the type of the
+default function, then the default function calls that function after converting its arguments and
+returns the result.
+Otherwise the scope of the declaration of \lstinline$T$ must contain a definition of the default
+function.
 \end{itemize}
 \begin{rationale}
+Note that a pointer to a default function will not compare as equal to a pointer to the inherited function.
+\end{rationale}
+A function or object with the same type and name as a default function or object that is declared within the scope of the definition of \lstinline$T$ replaces the default function or object.
+Note that a pointer to a default function will not compare as equal to a pointer to the inherited
+function.
+\end{rationale}
+A function or object with the same type and name as a default function or object that is declared
+within the scope of the definition of \lstinline$T$ replaces the default function or object.
 \examples
 …
 context s( type T ) {
         T a, b;
+} struct impl { int left, right; } a = { 0, 0 };
+}
+struct impl { int left, right; } a = { 0, 0 };
 type Pair | s( Pair ) = struct impl;
 Pair b = { 1, 1 };
 \end{lstlisting}
 The definition of \lstinline$Pair$ implicitly defines two objects \lstinline$a$ and \lstinline$b$.
 \lstinline$Pair a$ inherits its value from the \lstinline$struct impl a$.
+The definition of
 \lstinline$Pair b$ is compulsory because there is no \lstinline$struct impl b$ to construct a value from.
+\lstinline$Pair a$ inherits its value from the \lstinline$struct impl a$. The definition of
+\lstinline$Pair b$ is compulsory because there is no \lstinline$struct impl b$ to construct a value
+from.
 \begin{lstlisting}
 context ss( type T ) {
 …
 void munge( Doodad * );
 \end{lstlisting}
+The assignment function inherits \lstinline$struct doodad$'s assignment function because the types match when \lstinline$struct doodad$ is replaced by \lstinline$Doodad$ throughout.
+The assignment function inherits \lstinline$struct doodad$'s assignment function because the types
+match when \lstinline$struct doodad$ is replaced by \lstinline$Doodad$ throughout.
 \lstinline$munge()$ inherits \lstinline$Whatsit$'s \lstinline$munge()$ because the types match when
+\lstinline$Whatsit$ is replaced by \lstinline$Doodad$ in the parameter list. \lstinline$clone()$ does \emph{not} inherit \lstinline$Whatsit$'s \lstinline$clone()$: replacement in the parameter list yields ``\lstinline$Whatsit clone( Doodad )$'', which is not compatible with
+\lstinline$Doodad$'s \lstinline$clone()$'s type.
+Hence the definition of
+\lstinline$Whatsit$ is replaced by \lstinline$Doodad$ in the parameter list. \lstinline$clone()$
+does \emph{not} inherit \lstinline$Whatsit$'s \lstinline$clone()$: replacement in the parameter
+list yields ``\lstinline$Whatsit clone( Doodad )$'', which is not compatible with
+\lstinline$Doodad$'s \lstinline$clone()$'s type. Hence the definition of
 ``\lstinline$Doodad clone( Doodad )$'' is necessary.
 …
 \begin{rationale}
 The \emph{class} construct of object-oriented programming languages performs three independent functions.
+It \emph{encapsulates} a data structure;
 it defines a \emph{subtype} relationship, whereby instances of one class may be used in contexts that require instances of another;
 and it allows one class to \emph{inherit} the implementation of another.
 In \CFA, encapsulation is provided by opaque types and the scope rules, and subtyping is provided by specifications and assertions.
 Inheritance is provided by default functions and objects.
+The \emph{class} construct of object-oriented programming languages performs three independent
+functions. It \emph{encapsulates} a data structure; it defines a \emph{subtype} relationship, whereby
+instances of one class may be used in contexts that require instances of another; and it allows one
+class to \emph{inherit} the implementation of another.
+In \CFA, encapsulation is provided by opaque types and the scope rules, and subtyping is provided
+by specifications and assertions. Inheritance is provided by default functions and objects.
 \end{rationale}
 …
 \end{syntax}
 Many statements contain expressions, which may have more than one interpretation.
+The following sections describe how the \CFA translator selects an interpretation.
 In all cases the result of the selection shall be a single unambiguous \Index{interpretation}.
+Many statements contain expressions, which may have more than one interpretation. The following
+sections describe how the \CFA translator selects an interpretation. In all cases the result of the
+selection shall be a single unambiguous \Index{interpretation}.
 …
 switch ( E ) ...
 choose ( E ) ...
+\end{lstlisting} may have more than one interpretation, but it shall have only one interpretation with an integral type.
+\end{lstlisting}
+may have more than one interpretation, but it shall have only one interpretation with an integral type.
 An \Index{integer promotion} is performed on the expression if necessary.
 The constant expressions in \lstinline$case$ statements with the switch are converted to the promoted type.
 …
 while ( E ) ...
 do ... while ( E );
+\end{lstlisting} is treated as ``\lstinline$( int )((E)!=0)$''.
+\end{lstlisting}
+is treated as ``\lstinline$( int )((E)!=0)$''.
 The statement
 \begin{lstlisting}
 for ( a; b; c ) @\ldots@
+\end{lstlisting} is treated as
+\end{lstlisting}
+is treated as
 \begin{lstlisting}
 for ( ( void )( a ); ( int )(( b )!=0); ( void )( c ) ) ...
 …
 The implementation shall define the macro names \lstinline$__LINE__$, \lstinline$__FILE__$,
+\lstinline$__DATE__$, and \lstinline$__TIME__$, as in the {\c11} standard.
+It shall not define the macro name \lstinline$__STDC__$.
+In addition, the implementation shall define the macro name \lstinline$__CFORALL__$ to be the decimal constant 1.
+\lstinline$__DATE__$, and \lstinline$__TIME__$, as in the {\c11} standard. It shall not define the
+macro name \lstinline$__STDC__$.
+In addition, the implementation shall define the macro name \lstinline$__CFORALL__$ to be the
+decimal constant 1.
 …
 \section{C types}
+This section gives example specifications for some groups of types that are important in the C language, in terms of the predefined operations that can be applied to those types.
+This section gives example specifications for some groups of types that are important in the C
+language, in terms of the predefined operations that can be applied to those types.
 \subsection{Scalar, arithmetic, and integral types}
 The pointer, integral, and floating-point types are all \define{scalar types}.
+All of these types can be logically negated and compared.
 The assertion ``\lstinline$scalar( Complex )$'' should be read as ``type \lstinline$Complex$ is scalar''.
+The pointer, integral, and floating-point types are all \define{scalar types}. All of these types
+can be logically negated and compared. The assertion ``\lstinline$scalar( Complex )$'' should be read
+as ``type \lstinline$Complex$ is scalar''.
 \begin{lstlisting}
 context scalar( type T ) {@\impl{scalar}@
 …
 \end{lstlisting}
+The integral and floating-point types are \define{arithmetic types}, which support the basic arithmetic operators.
+The use of an assertion in the \nonterm{spec-parameter-list} declares that, in order to be arithmetic, a type must also be scalar ( and hence that scalar operations are available ).
+This is equivalent to inheritance of specifications.
+The integral and floating-point types are \define{arithmetic types}, which support the basic
+arithmetic operators. The use of an assertion in the \nonterm{spec-parameter-list} declares that,
+in order to be arithmetic, a type must also be scalar ( and hence that scalar operations are
+available ). This is equivalent to inheritance of specifications.
 \begin{lstlisting}
 context arithmetic( type T | scalar( T ) ) {@\impl{arithmetic}@@\use{scalar}@
 …
 Modifiable scalar lvalues are scalars and are modifiable lvalues, and assertions in the
+\nonterm{spec-parameter-list} reflect those relationships.
+This is equivalent to multiple inheritance of specifications.
+Scalars can also be incremented and decremented.
+\nonterm{spec-parameter-list} reflect those relationships. This is equivalent to multiple
+inheritance of specifications. Scalars can also be incremented and decremented.
 \begin{lstlisting}
 context m_l_scalar( type T | scalar( T ) | m_lvalue( T ) ) {@\impl{m_l_scalar}@
 …
 \end{lstlisting}
 Modifiable arithmetic lvalues are both modifiable scalar lvalues and arithmetic.
 Note that this results in the ``inheritance'' of \lstinline$scalar$ along both paths.
+Modifiable arithmetic lvalues are both modifiable scalar lvalues and arithmetic. Note that this
+results in the ``inheritance'' of \lstinline$scalar$ along both paths.
 \begin{lstlisting}
 context m_l_arithmetic( type T | m_l_scalar( T ) | arithmetic( T ) ) {@\impl{m_l_arithmetic}@
 …
         T ?+=?( T *, T ), ?-=?( T *, T );
 };
 context m_l_integral( type T | m_l_arithmetic( T ) | integral( T ) ) {@\impl{m_l_integral}@
         T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );@\use{m_l_arithmetic}@
 …
 \subsection{Pointer and array types}
+Array types can barely be said to exist in {\c11}, since in most cases an array name is treated as a constant pointer to the first element of the array, and the subscript expression
+Array types can barely be said to exist in {\c11}, since in most cases an array name is treated as a
+constant pointer to the first element of the array, and the subscript expression
 ``\lstinline$a[i]$'' is equivalent to the dereferencing expression ``\lstinline$(*( a+( i )))$''.
 Technically, pointer arithmetic and pointer comparisons other than ``\lstinline$==$'' and
 ``\lstinline$!=$'' are only defined for pointers to array elements, but the type system does not enforce those restrictions.
+Consequently, there is no need for a separate ``array type'' specification.
+Pointer types are scalar types.
 Like other scalar types, they have ``\lstinline$+$'' and
+``\lstinline$!=$'' are only defined for pointers to array elements, but the type system does not
+enforce those restrictions. Consequently, there is no need for a separate ``array type''
+specification.
+Pointer types are scalar types. Like other scalar types, they have ``\lstinline$+$'' and
 ``\lstinline$-$'' operators, but the types do not match the types of the operations in
 \lstinline$arithmetic$, so these operators cannot be consolidated in \lstinline$scalar$.
 …
         ptrdiff_t ?-?( P, P );
 };
 context m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {@\impl{m_l_pointer}@
         P ?+=?( P *, long int ), ?-=?( P *, long int );
 …
 \end{lstlisting}
+Specifications that define the dereference operator ( or subscript operator ) require two parameters, one for the pointer type and one for the pointed-at ( or element ) type.
+Different specifications are needed for each set of \Index{type qualifier}s, because qualifiers are not included in types.
+The assertion ``\lstinline$|ptr_to( Safe_pointer, int )$'' should be read as
+Specifications that define the dereference operator ( or subscript operator ) require two
+parameters, one for the pointer type and one for the pointed-at ( or element ) type. Different
+specifications are needed for each set of \Index{type qualifier}s, because qualifiers are not
+included in types. The assertion ``\lstinline$|ptr_to( Safe_pointer, int )$'' should be read as
 ``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''.
 \begin{lstlisting}
 context ptr_to( type P | pointer( P ), type T ) {@\impl{ptr_to}@@\use{pointer}@
+        lvalue T *?( P );
+        lvalue T ?[?]( P, long int );
+        lvalue T *?( P ); lvalue T ?[?]( P, long int );
 };
 context ptr_to_const( type P | pointer( P ), type T ) {@\impl{ptr_to_const}@
+        const lvalue T *?( P );
+        const lvalue T ?[?]( P, long int );@\use{pointer}@
+        const lvalue T *?( P ); const lvalue T ?[?]( P, long int );@\use{pointer}@
 };
 context ptr_to_volatile( type P | pointer( P ), type T ) }@\impl{ptr_to_volatile}@
+        volatile lvalue T *?( P );
+        volatile lvalue T ?[?]( P, long int );@\use{pointer}@
+        volatile lvalue T *?( P ); volatile lvalue T ?[?]( P, long int );@\use{pointer}@
 };
+\end{lstlisting}
+\begin{lstlisting}
 context ptr_to_const_volatile( type P | pointer( P ), type T ) }@\impl{ptr_to_const_volatile}@
         const volatile lvalue T *?( P );@\use{pointer}@
 …
 \end{lstlisting}
+Assignment to pointers is more complicated than is the case with other types, because the target's type can have extra type qualifiers in the pointed-at type: a ``\lstinline$T *$'' can be assigned to a ``\lstinline$const T *$'', a ``\lstinline$volatile T *$'', and a ``\lstinline$const volatile T *$''.
+Assignment to pointers is more complicated than is the case with other types, because the target's
+type can have extra type qualifiers in the pointed-at type: a ``\lstinline$T *$'' can be assigned to
+a ``\lstinline$const T *$'', a ``\lstinline$volatile T *$'', and a ``\lstinline$const volatile T *$''.
 Again, the pointed-at type is passed in, so that assertions can connect these specifications to the
 ``\lstinline$ptr_to$'' specifications.
 …
         T * ?=?( T **, P );
 };
 context m_l_ptr_to_const( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ type T | ptr_to_const( P, T )@\use{ptr_to_const}@) {
         P ?=?( P *, const T * );
         const T * ?=?( const T **, P );
 };
 context m_l_ptr_to_volatile( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ type T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@
         P ?=?( P *, volatile T * );
         volatile T * ?=?( volatile T **, P );
 };
 context m_l_ptr_to_const_volatile( type P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@
                 type T | m_l_ptr_to_volatile( P, T ) | m_l_ptr_to_const( P )) {@\use{m_l_ptr_to_const}@@\use{m_l_ptr_to_volatile}@
 …
 \end{lstlisting}
+Note the regular manner in which type qualifiers appear in those specifications.
+An alternative specification can make use of the fact that qualification of the pointed-at type is part of a pointer type to capture that regularity.
+Note the regular manner in which type qualifiers appear in those specifications. An alternative
+specification can make use of the fact that qualification of the pointed-at type is part of a
+pointer type to capture that regularity.
 \begin{lstlisting}
 context m_l_ptr_like( type MyP | m_l_pointer( MyP ),@\use{m_l_pointer}@@\impl{m_l_ptr_like}@ type CP | m_l_pointer( CP ) ) {
 …
 \end{lstlisting}
 The assertion ``\lstinline$| m_l_ptr_like( Safe_ptr, const int * )$'' should be read as
 ``\lstinline$Safe_ptr$ is a pointer type like \lstinline$const int *$''.
 This specification has two defects, compared to the original four: there is no automatic assertion that dereferencing a
+``\lstinline$Safe_ptr$ is a pointer type like \lstinline$const int *$''. This specification has two
+defects, compared to the original four: there is no automatic assertion that dereferencing a
 \lstinline$MyP$ produces an lvalue of the type that \lstinline$CP$ points at, and the
+``\lstinline$|m_l_pointer( CP )$'' assertion provides only a weak assurance that the argument passed to \lstinline$CP$ really is a pointer type.
+``\lstinline$|m_l_pointer( CP )$'' assertion provides only a weak assurance that the argument passed
+to \lstinline$CP$ really is a pointer type.
 \section{Relationships between operations}
+Different operators often have related meanings;
+for instance, in C, ``\lstinline$+$'',
+Different operators often have related meanings; for instance, in C, ``\lstinline$+$'',
 ``\lstinline$+=$'', and the two versions of ``\lstinline$++$'' perform variations of addition.
+Languages like {\CC} and Ada allow programmers to define operators for new types, but do not require that these relationships be preserved, or even that all of the operators be implemented.
+Completeness and consistency is left to the good taste and discretion of the programmer.
+It is possible to encourage these attributes by providing generic operator functions, or member functions of abstract classes, that are defined in terms of other, related operators.
+In \CFA, polymorphic functions provide the equivalent of these generic operators, and specifications explicitly define the minimal implementation that a programmer should provide.
+This section shows a few examples.
+Languages like {\CC} and Ada allow programmers to define operators for new types, but do not
+require that these relationships be preserved, or even that all of the operators be implemented.
+Completeness and consistency is left to the good taste and discretion of the programmer. It is
+possible to encourage these attributes by providing generic operator functions, or member functions
+of abstract classes, that are defined in terms of other, related operators.
+In \CFA, polymorphic functions provide the equivalent of these generic operators, and
+specifications explicitly define the minimal implementation that a programmer should provide. This
+section shows a few examples.
 \subsection{Relational and equality operators}
+The different comparison operators have obvious relationships, but there is no obvious subset of the operations to use in the implementation of the others.
+However, it is usually convenient to implement a single comparison function that returns a negative integer, 0, or a positive integer if its first argument is respectively less than, equal to, or greater than its second argument;
+the library function \lstinline$strcmp$ is an example.
+C and \CFA have an extra, non-obvious comparison operator: ``\lstinline$!$'', logical negation, returns 1 if its operand compares equal to 0, and 0 otherwise.
+The different comparison operators have obvious relationships, but there is no obvious subset of the
+operations to use in the implementation of the others. However, it is usually convenient to
+implement a single comparison function that returns a negative integer, 0, or a positive integer if
+its first argument is respectively less than, equal to, or greater than its second argument; the
+library function \lstinline$strcmp$ is an example.
+C and \CFA have an extra, non-obvious comparison operator: ``\lstinline$!$'', logical negation,
+returns 1 if its operand compares equal to 0, and 0 otherwise.
 \begin{lstlisting}
 context comparable( type T ) {
 …
         int compare( T, T );
+}
 forall( type T | comparable( T ) ) int ?<?( T l, T r ) {
         return compare( l, r ) < 0;
+}
 // ... similarly for <=, ==, >=, >, and !=.
 forall( type T | comparable( T ) ) int !?( T operand ) {
         return !compare( operand, 0 );
 …
 \subsection{Arithmetic and integer operations}
+A complete arithmetic type would provide the arithmetic operators and the corresponding assignment operators.
+Of these, the assignment operators are more likely to be implemented directly, because it is usually more efficient to alter the contents of an existing object than to create and return a new one.
+Similarly, a complete integral type would provide integral operations based on integral assignment operations.
+A complete arithmetic type would provide the arithmetic operators and the corresponding assignment
+operators. Of these, the assignment operators are more likely to be implemented directly, because
+it is usually more efficient to alter the contents of an existing object than to create and return a
+new one. Similarly, a complete integral type would provide integral operations based on integral
+assignment operations.
 \begin{lstlisting}
 context arith_base( type T ) {
 …
         T ?+=?( T *, T ), ?-=?( T *, T ), ?*=?( T *, T ), ?/=?( T *, T );
+}
 forall( type T | arith_base( T ) ) T ?+?( T l, T r ) {
         return l += r;
+}
 forall( type T | arith_base( T ) ) T ?++( T * operand ) {
         T temporary = *operand;
 …
         return temporary;
+}
 forall( type T | arith_base( T ) ) T ++?( T * operand ) {
         return *operand += 1;
+}
 // ... similarly for -, --, *, and /.
 context int_base( type T ) {
         T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );
         T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );
+}
 forall( type T | int_base( T ) ) T ?&?( T l, T r ) {
         return l &= r;
 …
 \end{lstlisting}
+Note that, although an arithmetic type would certainly provide comparison functions, and an integral type would provide arithmetic operations, there does not have to be any relationship among
+\lstinline$int_base$, \lstinline$arith_base$ and \lstinline$comparable$.
+Note also that these declarations provide guidance and assistance, but they do not define an absolutely minimal set of requirements.
+A truly minimal implementation of an arithmetic type might only provide
+Note that, although an arithmetic type would certainly provide comparison functions, and an integral
+type would provide arithmetic operations, there does not have to be any relationship among
+\lstinline$int_base$, \lstinline$arith_base$ and \lstinline$comparable$. Note also that these
+declarations provide guidance and assistance, but they do not define an absolutely minimal set of
+requirements. A truly minimal implementation of an arithmetic type might only provide
 \lstinline$0$, \lstinline$1$, and \lstinline$?-=?$, which would be used by polymorphic
 \lstinline$?+=?$, \lstinline$?*=?$, and \lstinline$?/=?$ functions.
 …
 Review index entries.
+Restrict allowed to qualify anything, or type/dtype parameters, but only affects pointers.
+This gets into \lstinline$noalias$ territory.
+Qualifying anything (``\lstinline$short restrict rs$'') means pointer parameters of \lstinline$?++$, etc, would need restrict qualifiers.
+Enumerated types.
+Constants are not ints.
+Overloading.
+Definition should be ``representable as an integer type'', not ``as an int''.
+C11 usual conversions freely convert to and from ordinary integer types via assignment, which works between any integer types.
+Does enum Color ?*?( enum
+Restrict allowed to qualify anything, or type/dtype parameters, but only affects pointers. This gets
+into \lstinline$noalias$ territory. Qualifying anything (``\lstinline$short restrict rs$'') means
+pointer parameters of \lstinline$?++$, etc, would need restrict qualifiers.
+Enumerated types. Constants are not ints. Overloading. Definition should be ``representable as an
+integer type'', not ``as an int''. C11 usual conversions freely convert to and from ordinary
+integer types via assignment, which works between any integer types. Does enum Color ?*?( enum
 Color, enum Color ) really make sense? ?++ does, but it adds (int)1.
+Operators on {,signed,unsigned} char and other small types. ?<? harmless;
+?*? questionable for chars.
+Generic selections make these choices visible.
+Safe conversion operators? Predefined
+Operators on {,signed,unsigned} char and other small types. ?<? harmless; ?*? questionable for
+chars. Generic selections make these choices visible. Safe conversion operators? Predefined
 ``promotion'' function?
+\lstinline$register$ assignment might be handled as assignment to a temporary with copying back and forth, but copying must not be done by assignment.
+\lstinline$register$ assignment might be handled as assignment to a temporary with copying back and
+forth, but copying must not be done by assignment.
 Don't use ptrdiff\_t by name in the predefineds.
+Polymorphic objects.
+Polymorphic typedefs and type declarations.
+Polymorphic objects. Polymorphic typedefs and type declarations.
 …
 \addcontentsline{toc}{chapter}{\indexname} % add index name to table of contents
 \begin{theindex}
+Italic page numbers give the location of the main entry for the referenced term.
+Plain page numbers denote uses of the indexed term.
+Entries for grammar non-terminals are italicized.
+A typewriter font is used for grammar terminals and program identifiers.
+Italic page numbers give the location of the main entry for the referenced term. Plain page numbers
+denote uses of the indexed term. Entries for grammar non-terminals are italicized. A typewriter
+font is used for grammar terminals and program identifiers.
 \indexspace
 \input{refrat.ind}

Note: See TracChangeset for help on using the changeset viewer.

Context Navigation

Changes in doc/refrat/refrat.tex [90c3b1c:cf16f94]

Legend:

doc/refrat/refrat.tex

Download in other formats: