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

File:

• doc/refrat/refrat.tex (modified) (76 diffs)

doc/refrat/refrat.tex

@@ -17 +17 @@
 \usepackage[dvips,plainpages=false,pdfpagelabels,pdfpagemode=UseNone,colorlinks=true,pagebackref=true,linkcolor=blue,citecolor=blue,urlcolor=blue,pagebackref=true,breaklinks=true]{hyperref}
 \usepackage{breakurl}
-\renewcommand{\UrlFont}{\small\sf}
+\urlstyle{sf}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -23 +23 @@
 % Names used in the document.
 
-\newcommand{\CFA}{C$\forall$\xspace}    % set language symbolic name
-\newcommand{\CFL}{Cforall\xspace}               % set language text name
+\newcommand{\CFA}{Cforall\xspace}               % set language text name
+\newcommand{\CFAA}{C$\forall$\xspace}   % set language symbolic name
 \newcommand{\CC}{C\kern-.1em\hbox{+\kern-.25em+}\xspace} % CC symbolic name
 \def\c11{ISO/IEC C} % C11 name (cannot have numbers in latex command name)
@@ -33 +33 @@
 
 \makeatletter
-% allow escape sequence in lstinline
-%\usepackage{etoolbox}
-%\patchcmd{\lsthk@TextStyle}{\let\lst@DefEsc\@empty}{}{}{\errmessage{failed to patch}}
-
-\renewcommand\small{%
-   \@setfontsize\small{8.5}{11}%
-   \abovedisplayskip 8.5pt \@plus 3pt \@minus 4pt
-   \abovedisplayshortskip \z@ \@plus 2pt
-   \belowdisplayshortskip 4pt \@plus 2pt \@minus 2pt
-   \def\@listi{\leftmargin\leftmargini
-               \topsep 4pt \@plus 2pt \@minus 2pt
-               \parsep 2pt \@pluspt \@minuspt
-               \itemsep \parsep}%
-   \belowdisplayskip \abovedisplayskip
-}
-\usepackage{relsize}            % must be after change to small
-
 \renewcommand{\labelitemi}{{\raisebox{0.25ex}{\footnotesize$\bullet$}}}
 \renewenvironment{itemize}{\begin{list}{\labelitemi}{\topsep=5pt\itemsep=5pt\parsep=0pt}}{\end{list}}
@@ -76 +59 @@
 \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.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}}}
@@ -115 +97 @@
 
 % blocks and titles
+\newcommand{\define}[1]{\emph{#1\/}\index{#1}}
 \newenvironment{rationale}{%
   \begin{quotation}\noindent$\Box$\enspace
@@ -120 +103 @@
   \hfill\enspace$\Box$\end{quotation}
 }%
-\newcommand{\define}[1]{\emph{#1\/}\index{#1}}
 \newcommand{\rewrite}{\(\Rightarrow\)}
 \newcommand{\rewriterules}{\paragraph{Rewrite Rules}~\par\noindent}
@@ -149 +131 @@
 \newcommand{\VPageref}[2][page]{\ifx#1\@empty\else{#1}\nobreakspace\fi\pageref{#2}}
 
-% CFA based on ANSI C
+% adjust listings macros
 \lstdefinelanguage{CFA}[ANSI]{C}%
-{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,trait,disable,dtype,enable,
-        fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,otype,restrict,_Static_assert,
-        _Thread_local,throw,throwResume,try,},
+{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,context,disable,dtype,enable,
+        fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,restrict,_Static_assert,
+        _Thread_local,throw,throwResume,try,type,},
 }%
 
@@ -159 +141 @@
 language=CFA,
 columns=flexible,
-basicstyle=\sf\relsize{-1},
+basicstyle=\sf\small,
 tabsize=4,
 xleftmargin=\parindent,
 escapechar=@,
 keepspaces=true,
-showstringspaces=false,
-showlines=true,
+%showtabs=true,
+%tab=\rightarrowfill,
 }%
 
@@ -192 +174 @@
 
 \title{\Huge
-\CFA (\CFL) Reference Manual and Rationale
+\CFA (\CFAA) Reference Manual and Rationale
 }% title
 \author{\huge
@@ -298 +280 @@
 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( otype T | sumable( T ) ) struct pair {
+forall( type T | sumable( T ) ) struct pair {
         T x;
         T y;
@@ -310 +292 @@
 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( otype T ) void swap( pair(T) *p ) {
+forall( type T ) void swap( pair(T) *p ) {
         T z = p->x;
         p->x = p->y;
@@ -320 +302 @@
 \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
 \begin{lstlisting}
-forall( otype T ) struct A;
-
-forall( otype T ) struct B {
+forall( type T ) struct A;
+
+forall( type T ) struct B {
         A(T) *a;                        // legal, but cannot instantiate B(T)
 };
@@ -333 +314 @@
 B(T) x;                                 // illegal, *x.a is of an incomplete generic type
  
-forall( otype T ) struct A {
+forall( type T ) struct A {
         B( T ) *b;
 };
@@ -340 +321 @@
 
 // box.h:
-        forall( otype T ) struct box;
-        forall( otype T ) box( T ) *make_box( T );
-        forall( otype T ) void use_box( box( T ) *b );
+        forall( type T ) struct box;
+        forall( type T ) box( T ) *make_box( T );
+        forall( type T ) void use_box( box( T ) *b );
         
 // main.c:
@@ -429 +410 @@
 
 \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}.
+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.
+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.
@@ -440 +422 @@
 The type
 \begin{lstlisting}
-forall( otype T, otype U ) void (*)( T, U );
+forall( type T, type U ) void (*)( T, U );
 \end{lstlisting}
 can be specialized to (among other things)
 \begin{lstlisting}
-forall( otype T ) void (*)( T, T );             // U bound to T
-forall( otype T ) void (*)( T, real );  // U bound to real
-forall( otype 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}
@@ -452 +434 @@
 The type
 \begin{lstlisting}
-forall( otype T | T ?+?( T, T ) ) T (*)( T );
+forall( type T | T ?+?( T, T ) ) T (*)( T );
 \end{lstlisting}
 can be specialized to (among other things)
@@ -512 +494 @@
 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.
+Otherwise,
+\lstinline$unsigned short$ is converted directly to \lstinline$unsigned$, and the cost is 1.
 
 \item
@@ -525 +508 @@
         \rhs \lstinline$forall$
         \rhs \lstinline$lvalue$
-        \rhs \lstinline$trait$
+        \rhs \lstinline$context$
         \rhs \lstinline$dtype$
         \rhs \lstinline$ftype$
@@ -556 +539 @@
 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 0 as a special case.
+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
+0 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$.
@@ -852 +836 @@
 \predefined
 \begin{lstlisting}
-forall( otype T ) lvalue T ?[?]( T *, ptrdiff_t );@\use{ptrdiff_t}@
-forall( otype T ) lvalue _Atomic T ?[?]( _Atomic T *, ptrdiff_t );
-forall( otype T ) lvalue const T ?[?]( const T *, ptrdiff_t );
-forall( otype T ) lvalue restrict T ?[?]( restrict T *, ptrdiff_t );
-forall( otype T ) lvalue volatile T ?[?]( volatile T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic const T ?[?]( _Atomic const T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic restrict T ?[?]( _Atomic restrict T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic volatile T ?[?]( _Atomic volatile T *, ptrdiff_t );
-forall( otype T ) lvalue const restrict T ?[?]( const restrict T *, ptrdiff_t );
-forall( otype T ) lvalue const volatile T ?[?]( const volatile T *, ptrdiff_t );
-forall( otype T ) lvalue restrict volatile T ?[?]( restrict volatile T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic const restrict T ?[?]( _Atomic const restrict T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic const volatile T ?[?]( _Atomic const volatile T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic restrict volatile T ?[?]( _Atomic restrict volatile T *, ptrdiff_t );
-forall( otype T ) lvalue const restrict volatile T ?[?]( const restrict volatile T *, ptrdiff_t );
-forall( otype T ) lvalue _Atomic const restrict volatile T ?[?]( _Atomic const restrict volatile T *, ptrdiff_t );
+forall( type T ) lvalue T ?[?]( T *, ptrdiff_t );@\use{ptrdiff_t}@
+forall( type T ) lvalue _Atomic T ?[?]( _Atomic T *, ptrdiff_t );
+forall( type T ) lvalue const T ?[?]( const T *, ptrdiff_t );
+forall( type T ) lvalue restrict T ?[?]( restrict T *, ptrdiff_t );
+forall( type T ) lvalue volatile T ?[?]( volatile T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic const T ?[?]( _Atomic const T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic restrict T ?[?]( _Atomic restrict T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic volatile T ?[?]( _Atomic volatile T *, ptrdiff_t );
+forall( type T ) lvalue const restrict T ?[?]( const restrict T *, ptrdiff_t );
+forall( type T ) lvalue const volatile T ?[?]( const volatile T *, ptrdiff_t );
+forall( type T ) lvalue restrict volatile T ?[?]( restrict volatile T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic const restrict T ?[?]( _Atomic const restrict T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic const volatile T ?[?]( _Atomic const volatile T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic restrict volatile T ?[?]( _Atomic restrict volatile T *, ptrdiff_t );
+forall( type T ) lvalue const restrict volatile T ?[?]( const restrict volatile T *, ptrdiff_t );
+forall( type T ) lvalue _Atomic const restrict volatile T ?[?]( _Atomic const restrict volatile T *, ptrdiff_t );
 \end{lstlisting}
 \semantics
@@ -930 +914 @@
 \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( otype T ) T f( T );$'' without affecting any calls of \lstinline$f$.
+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
@@ -944 +928 @@
 f = g( d, f );          // (3) (unsafe conversion to float) 
 \end{lstlisting}
-If \lstinline$g$ was replaced by ``\lstinline$forall( otype T ) T g( T, T );$'', the first and second calls would be unaffected, but the third would change: \lstinline$f$ would be converted to
+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( otype T ) void h( T *);$'' can not.
+\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.
@@ -957 +941 @@
 A function called ``\lstinline$?()$'' might be part of a numerical differentiation package.
 \begin{lstlisting}
-extern otype Derivative;
+extern type Derivative;
 extern double ?()( Derivative, double );
 extern Derivative derivative_of( double (*f)( double ) );
@@ -978 +962 @@
 
 \begin{lstlisting}
-forall( otype T ) T h( T );
+forall( type T ) T h( T );
 double d = h( 1.5 );
 \end{lstlisting}
@@ -985 +969 @@
 
 \begin{lstlisting}
-forall( otype T, otype U ) void g( T, U );      // (4)
-forall( otype T ) void g( T, T );                       // (5)
-forall( otype T ) void g( T, long );                    // (6)
+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;
@@ -1007 +991 @@
 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( otype T ) T min( T, T );
+forall( type T ) T min( T, T );
 double max( double, double );
-trait min_max( T ) {@\impl{min_max}@
+context min_max( T ) {@\impl{min_max}@
         T min( T, T );
         T max( T, T );
 }
-forall( otype U | min_max( U ) ) void shuffle( U, U );
+forall( type U | min_max( U ) ) void shuffle( U, U );
 shuffle( 9, 10 );
 \end{lstlisting}
@@ -1063 +1047 @@
 long double ?++( volatile long double * ), ?++( _Atomic volatile long double * );
 
-forall( otype T ) T * ?++( T * restrict volatile * ), * ?++( T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic T * ?++( _Atomic T * restrict volatile * ), * ?++( _Atomic T * _Atomic restrict volatile * );
-forall( otype T ) const T * ?++( const T * restrict volatile * ), * ?++( const T * _Atomic restrict volatile * );
-forall( otype T ) volatile T * ?++( volatile T * restrict volatile * ), * ?++( volatile T * _Atomic restrict volatile * );
-forall( otype T ) restrict T * ?++( restrict T * restrict volatile * ), * ?++( restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const T * ?++( _Atomic const T * restrict volatile * ),
+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( otype T ) _Atomic restrict T * ?++( _Atomic restrict T * restrict volatile * ),
+forall( type T ) _Atomic restrict T * ?++( _Atomic restrict T * restrict volatile * ),
         * ?++( _Atomic restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic volatile T * ?++( _Atomic volatile T * restrict volatile * ),
+forall( type T ) _Atomic volatile T * ?++( _Atomic volatile T * restrict volatile * ),
         * ?++( _Atomic volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict T * ?++( const restrict T * restrict volatile * ),
+forall( type T ) const restrict T * ?++( const restrict T * restrict volatile * ),
         * ?++( const restrict T * _Atomic restrict volatile * );
-forall( otype T ) const volatile T * ?++( const volatile T * restrict volatile * ),
+forall( type T ) const volatile T * ?++( const volatile T * restrict volatile * ),
         * ?++( const volatile T * _Atomic restrict volatile * );
-forall( otype T ) restrict volatile T * ?++( restrict volatile T * restrict volatile * ),
+forall( type T ) restrict volatile T * ?++( restrict volatile T * restrict volatile * ),
         * ?++( restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict T * ?++( _Atomic const restrict T * restrict volatile * ),
+forall( type T ) _Atomic const restrict T * ?++( _Atomic const restrict T * restrict volatile * ),
         * ?++( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const volatile T * ?++( _Atomic const volatile T * restrict volatile * ),
+forall( type T ) _Atomic const volatile T * ?++( _Atomic const volatile T * restrict volatile * ),
         * ?++( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic restrict volatile T * ?++( _Atomic restrict volatile T * restrict volatile * ),
+forall( type T ) _Atomic restrict volatile T * ?++( _Atomic restrict volatile T * restrict volatile * ),
         * ?++( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict volatile T * ?++( const restrict volatile T * restrict volatile * ),
+forall( type T ) const restrict volatile T * ?++( const restrict volatile T * restrict volatile * ),
         * ?++( const restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict volatile T * ?++( _Atomic const restrict volatile T * 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 * );
 
@@ -1107 +1091 @@
 long double ?--( volatile long double * ), ?--( _Atomic volatile long double * );
 
-forall( otype T ) T * ?--( T * restrict volatile * ), * ?--( T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic T * ?--( _Atomic T * restrict volatile * ), * ?--( _Atomic T * _Atomic restrict volatile * );
-forall( otype T ) const T * ?--( const T * restrict volatile * ), * ?--( const T * _Atomic restrict volatile * );
-forall( otype T ) volatile T * ?--( volatile T * restrict volatile * ), * ?--( volatile T * _Atomic restrict volatile * );
-forall( otype T ) restrict T * ?--( restrict T * restrict volatile * ), * ?--( restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const T * ?--( _Atomic const T * restrict volatile * ),
+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( otype T ) _Atomic restrict T * ?--( _Atomic restrict T * restrict volatile * ),
+forall( type T ) _Atomic restrict T * ?--( _Atomic restrict T * restrict volatile * ),
         * ?--( _Atomic restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic volatile T * ?--( _Atomic volatile T * restrict volatile * ),
+forall( type T ) _Atomic volatile T * ?--( _Atomic volatile T * restrict volatile * ),
         * ?--( _Atomic volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict T * ?--( const restrict T * restrict volatile * ),
+forall( type T ) const restrict T * ?--( const restrict T * restrict volatile * ),
         * ?--( const restrict T * _Atomic restrict volatile * );
-forall( otype T ) const volatile T * ?--( const volatile T * restrict volatile * ),
+forall( type T ) const volatile T * ?--( const volatile T * restrict volatile * ),
         * ?--( const volatile T * _Atomic restrict volatile * );
-forall( otype T ) restrict volatile T * ?--( restrict volatile T * restrict volatile * ),
+forall( type T ) restrict volatile T * ?--( restrict volatile T * restrict volatile * ),
         * ?--( restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict T * ?--( _Atomic const restrict T * restrict volatile * ),
+forall( type T ) _Atomic const restrict T * ?--( _Atomic const restrict T * restrict volatile * ),
         * ?--( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const volatile T * ?--( _Atomic const volatile T * restrict volatile * ),
+forall( type T ) _Atomic const volatile T * ?--( _Atomic const volatile T * restrict volatile * ),
         * ?--( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic restrict volatile T * ?--( _Atomic restrict volatile T * restrict volatile * ),
+forall( type T ) _Atomic restrict volatile T * ?--( _Atomic restrict volatile T * restrict volatile * ),
         * ?--( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict volatile T * ?--( const restrict volatile T * restrict volatile * ),
+forall( type T ) const restrict volatile T * ?--( const restrict volatile T * restrict volatile * ),
         * ?--( const restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict volatile T * ?--( _Atomic const restrict volatile T * 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 * );
 \end{lstlisting}
@@ -1211 +1195 @@
 The expression would be valid if \lstinline$?++$ were declared by
 \begin{lstlisting}
-forall( otype T ) T * ?++( T * * );
+forall( type T ) T * ?++( T * * );
 \end{lstlisting} with \lstinline$T$ inferred to be \lstinline$char$.
 
@@ -1219 +1203 @@
 Hence the actual predefined function is
 \begin{lstlisting}
-forall( otype T ) T * ?++( T * restrict volatile * );
+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.)
@@ -1233 +1217 @@
 \lstinline$char const volatile *$, so a new overloading is needed:
 \begin{lstlisting}
-forall( otype T ) T const volatile * ?++( T const volatile *restrict volatile * );
+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}.
@@ -1241 +1225 @@
 The \lstinline$restrict$ qualifier is handled just like \lstinline$const$ and \lstinline$volatile$ in the previous case:
 \begin{lstlisting}
-forall( otype T ) T restrict * ?++( T restrict *restrict volatile * );
+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.
@@ -1299 +1283 @@
 long double ++?( volatile long double * ), ++?( _Atomic volatile long double * );
 
-forall( otype T ) T * ++?( T * restrict volatile * ), * ++?( T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic T * ++?( _Atomic T * restrict volatile * ), * ++?( _Atomic T * _Atomic restrict volatile * );
-forall( otype T ) const T * ++?( const T * restrict volatile * ), * ++?( const T * _Atomic restrict volatile * );
-forall( otype T ) volatile T * ++?( volatile T * restrict volatile * ), * ++?( volatile T * _Atomic restrict volatile * );
-forall( otype T ) restrict T * ++?( restrict T * restrict volatile * ), * ++?( restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const T * ++?( _Atomic const T * restrict volatile * ),
+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( otype T ) _Atomic volatile T * ++?( _Atomic volatile T * restrict volatile * ),
+forall( type T ) _Atomic volatile T * ++?( _Atomic volatile T * restrict volatile * ),
         * ++?( _Atomic volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic restrict T * ++?( _Atomic restrict T * restrict volatile * ),
+forall( type T ) _Atomic restrict T * ++?( _Atomic restrict T * restrict volatile * ),
         * ++?( _Atomic restrict T * _Atomic restrict volatile * );
-forall( otype T ) const volatile T * ++?( const volatile T * restrict volatile * ),
+forall( type T ) const volatile T * ++?( const volatile T * restrict volatile * ),
         * ++?( const volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict T * ++?( const restrict T * restrict volatile * ),
+forall( type T ) const restrict T * ++?( const restrict T * restrict volatile * ),
         * ++?( const restrict T * _Atomic restrict volatile * );
-forall( otype T ) restrict volatile T * ++?( restrict volatile T * restrict volatile * ),
+forall( type T ) restrict volatile T * ++?( restrict volatile T * restrict volatile * ),
         * ++?( restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const volatile T * ++?( _Atomic const volatile T * restrict volatile * ),
+forall( type T ) _Atomic const volatile T * ++?( _Atomic const volatile T * restrict volatile * ),
         * ++?( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict T * ++?( _Atomic const restrict T * restrict volatile * ),
+forall( type T ) _Atomic const restrict T * ++?( _Atomic const restrict T * restrict volatile * ),
         * ++?( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic restrict volatile T * ++?( _Atomic restrict volatile T * restrict volatile * ),
+forall( type T ) _Atomic restrict volatile T * ++?( _Atomic restrict volatile T * restrict volatile * ),
         * ++?( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict volatile T * ++?( const restrict volatile T * restrict volatile * ),
+forall( type T ) const restrict volatile T * ++?( const restrict volatile T * restrict volatile * ),
         * ++?( const restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict volatile T * ++?( _Atomic const restrict volatile T * 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 * );
 
@@ -1343 +1327 @@
 long double --?( volatile long double * ), --?( _Atomic volatile long double * );
 
-forall( otype T ) T * --?( T * restrict volatile * ), * --?( T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic T * --?( _Atomic T * restrict volatile * ), * --?( _Atomic T * _Atomic restrict volatile * );
-forall( otype T ) const T * --?( const T * restrict volatile * ), * --?( const T * _Atomic restrict volatile * );
-forall( otype T ) volatile T * --?( volatile T * restrict volatile * ), * --?( volatile T * _Atomic restrict volatile * );
-forall( otype T ) restrict T * --?( restrict T * restrict volatile * ), * --?( restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const T * --?( _Atomic const T * restrict volatile * ),
+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( otype T ) _Atomic volatile T * --?( _Atomic volatile T * restrict volatile * ),
+forall( type T ) _Atomic volatile T * --?( _Atomic volatile T * restrict volatile * ),
         * --?( _Atomic volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic restrict T * --?( _Atomic restrict T * restrict volatile * ),
+forall( type T ) _Atomic restrict T * --?( _Atomic restrict T * restrict volatile * ),
         * --?( _Atomic restrict T * _Atomic restrict volatile * );
-forall( otype T ) const volatile T * --?( const volatile T * restrict volatile * ),
+forall( type T ) const volatile T * --?( const volatile T * restrict volatile * ),
         * --?( const volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict T * --?( const restrict T * restrict volatile * ),
+forall( type T ) const restrict T * --?( const restrict T * restrict volatile * ),
         * --?( const restrict T * _Atomic restrict volatile * );
-forall( otype T ) restrict volatile T * --?( restrict volatile T * restrict volatile * ),
+forall( type T ) restrict volatile T * --?( restrict volatile T * restrict volatile * ),
         * --?( restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const volatile T * --?( _Atomic const volatile T * restrict volatile * ),
+forall( type T ) _Atomic const volatile T * --?( _Atomic const volatile T * restrict volatile * ),
         * --?( _Atomic const volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict T * --?( _Atomic const restrict T * restrict volatile * ),
+forall( type T ) _Atomic const restrict T * --?( _Atomic const restrict T * restrict volatile * ),
         * --?( _Atomic const restrict T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic restrict volatile T * --?( _Atomic restrict volatile T * restrict volatile * ),
+forall( type T ) _Atomic restrict volatile T * --?( _Atomic restrict volatile T * restrict volatile * ),
         * --?( _Atomic restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) const restrict volatile T * --?( const restrict volatile T * restrict volatile * ),
+forall( type T ) const restrict volatile T * --?( const restrict volatile T * restrict volatile * ),
         * --?( const restrict volatile T * _Atomic restrict volatile * );
-forall( otype T ) _Atomic const restrict volatile T * --?( _Atomic const restrict volatile T * 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 * );
 \end{lstlisting}
@@ -1396 +1380 @@
 \predefined
 \begin{lstlisting}
-forall( otype T ) lvalue T *?( T * );
-forall( otype T ) _Atomic lvalue T *?( _Atomic T * );
-forall( otype T ) const lvalue T *?( const T * );
-forall( otype T ) volatile lvalue T *?( volatile T * );
-forall( otype T ) restrict lvalue T *?( restrict T * );
-forall( otype T ) _Atomic const lvalue T *?( _Atomic const T * );
-forall( otype T ) _Atomic volatile lvalue T *?( _Atomic volatile T * );
-forall( otype T ) _Atomic restrict lvalue T *?( _Atomic restrict T * );
-forall( otype T ) const volatile lvalue T *?( const volatile T * );
-forall( otype T ) const restrict lvalue T *?( const restrict T * );
-forall( otype T ) restrict volatile lvalue T *?( restrict volatile T * );
-forall( otype T ) _Atomic const volatile lvalue T *?( _Atomic const volatile T * );
-forall( otype T ) _Atomic const restrict lvalue T *?( _Atomic const restrict T * );
-forall( otype T ) _Atomic restrict volatile lvalue T *?( _Atomic restrict volatile T * );
-forall( otype T ) const restrict volatile lvalue T *?( const restrict volatile T * );
-forall( otype T ) _Atomic const restrict volatile lvalue T *?( _Atomic const restrict volatile T * );
+forall( type T ) lvalue T *?( T * );
+forall( type T ) _Atomic lvalue T *?( _Atomic T * );
+forall( type T ) const lvalue T *?( const T * );
+forall( type T ) volatile lvalue T *?( volatile T * );
+forall( type T ) restrict lvalue T *?( restrict T * );
+forall( type T ) _Atomic const lvalue T *?( _Atomic const T * );
+forall( type T ) _Atomic volatile lvalue T *?( _Atomic volatile T * );
+forall( type T ) _Atomic restrict lvalue T *?( _Atomic restrict T * );
+forall( type T ) const volatile lvalue T *?( const volatile T * );
+forall( type T ) const restrict lvalue T *?( const restrict T * );
+forall( type T ) restrict volatile lvalue T *?( restrict volatile T * );
+forall( type T ) _Atomic const volatile lvalue T *?( _Atomic const volatile T * );
+forall( type T ) _Atomic const restrict lvalue T *?( _Atomic const restrict T * );
+forall( type T ) _Atomic restrict volatile lvalue T *?( _Atomic restrict volatile T * );
+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}
@@ -1526 +1510 @@
 \begin{rationale}
 \begin{lstlisting}
-otype Pair = struct { int first, second; };
+type Pair = struct { int first, second; };
 size_t p_size = sizeof(Pair);           // constant expression 
-extern otype Rational;@\use{Rational}@
+extern type Rational;@\use{Rational}@
 size_t c_size = sizeof(Rational);       // non-constant expression 
 forall(type T) T f(T p1, T p2) {
@@ -1652 +1636 @@
 Consider
 \begin{lstlisting}
-forall( otype T | T ?*?( T, T ) ) T square( T );
+forall( type T | T ?*?( T, T ) ) T square( T );
 short s;
 square( s );
@@ -1663 +1647 @@
 A more troubling example is
 \begin{lstlisting}
-forall( otype T | ?*?( T, T ) ) T product( T[], int n );
+forall( type T | ?*?( T, T ) ) T product( T[], int n );
 short sa[5];
 product( sa, 5);
@@ -1720 +1704 @@
         ?+?( _Complex long double, _Complex long double ), ?-?( _Complex long double, _Complex long double );
 
-forall( otype T ) T * ?+?( T *, ptrdiff_t ), * ?+?( ptrdiff_t, T * ), * ?-?( T *, ptrdiff_t );
-forall( otype T ) _Atomic T * ?+?( _Atomic T *, ptrdiff_t ), * ?+?( ptrdiff_t, _Atomic T * ),
+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( otype 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( otype 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( otype 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( otype 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( otype 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( otype 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( otype 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( otype 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( otype 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( otype 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( otype 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 * );
@@ -2068 +2052 @@
 
 \begin{lstlisting}
-extern otype Rational;@\use{Rational}@
+extern type Rational;@\use{Rational}@
 extern const Rational 0;@\use{0}@
 extern int ?!=?( Rational, Rational );
@@ -2111 +2095 @@
 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( otype T ) T cond( int, T, T );
+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(
@@ -2471 +2455 @@
 \predefined
 \begin{lstlisting}
-forall( otype T ) T
+forall( type T ) T
         * ?+=?( T * restrict volatile *, ptrdiff_t ),
         * ?-=?( T * restrict volatile *, ptrdiff_t ),
         * ?+=?( T * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T _Atomic
+forall( type T ) T _Atomic
         * ?+=?( T _Atomic * restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic * restrict volatile *, ptrdiff_t ),
         * ?+=?( T _Atomic * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T const
+forall( type T ) T const
         * ?+=?( T const * restrict volatile *, ptrdiff_t ),
         * ?-=?( T const * restrict volatile *, ptrdiff_t ),
         * ?+=?( T const * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T restrict
+forall( type T ) T restrict
         * ?+=?( T restrict * restrict volatile *, ptrdiff_t ),
         * ?-=?( T restrict * restrict volatile *, ptrdiff_t ),
         * ?+=?( T restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T volatile
+forall( type T ) T volatile
         * ?+=?( T volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( T volatile * restrict volatile *, ptrdiff_t ),
         * ?+=?( T volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T _Atomic const
+forall( type T ) T _Atomic const
         * ?+=?( T _Atomic const restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic const restrict volatile *, ptrdiff_t ),
         * ?+=?( T _Atomic const _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic const _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T _Atomic restrict
+forall( type T ) T _Atomic restrict
         * ?+=?( T _Atomic restrict * restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic restrict * restrict volatile *, ptrdiff_t ),
         * ?+=?( T _Atomic restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T _Atomic volatile
+forall( type T ) T _Atomic volatile
         * ?+=?( T _Atomic volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic volatile * restrict volatile *, ptrdiff_t ),
         * ?+=?( T _Atomic volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T const restrict
+forall( type T ) T const restrict
         * ?+=?( T const restrict * restrict volatile *, ptrdiff_t ),
         * ?-=?( T const restrict * restrict volatile *, ptrdiff_t ),
         * ?+=?( T const restrict * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const restrict * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T const volatile
+forall( type T ) T const volatile
         * ?+=?( T const volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( T const volatile * restrict volatile *, ptrdiff_t ),
         * ?+=?( T const volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T const volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T restrict volatile
+forall( type T ) T restrict volatile
         * ?+=?( T restrict volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( T restrict volatile * restrict volatile *, ptrdiff_t ),
         * ?+=?( T restrict volatile * _Atomic restrict volatile *, ptrdiff_t ),
         * ?-=?( T restrict volatile * _Atomic restrict volatile *, ptrdiff_t );
-forall( otype T ) T _Atomic const restrict
+forall( type T ) T _Atomic const restrict
         * ?+=?( T _Atomic const restrict * restrict volatile *, ptrdiff_t ),
         * ?-=?( 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( otype T ) T _Atomic const volatile
+forall( type T ) T _Atomic const volatile
         * ?+=?( T _Atomic const volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( 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( otype T ) T _Atomic restrict volatile
+forall( type T ) T _Atomic restrict volatile
         * ?+=?( T _Atomic restrict volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( 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( otype T ) T const restrict volatile
+forall( type T ) T const restrict volatile
         * ?+=?( T const restrict volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( 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( otype T ) T _Atomic const restrict volatile
+forall( type T ) T _Atomic const restrict volatile
         * ?+=?( T _Atomic const restrict volatile * restrict volatile *, ptrdiff_t ),
         * ?-=?( T _Atomic const restrict volatile * restrict volatile *, ptrdiff_t ),
@@ -2858 +2842 @@
 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( otype T ) struct Pair { T a, b;
+forall( type T ) struct Pair { T a, b;
 } mkPair( T, T ); // illegal 
 \end{lstlisting}
@@ -2883 +2867 @@
 If this restriction were lifted, it would be possible to write
 \begin{lstlisting}
-forall( otype 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
@@ -2892 +2876 @@
 \lstinline$T$:
 \begin{lstlisting}
-forall( otype T ) T * alloc( T initial_value );@\use{alloc}@
+forall( type T ) T * alloc( T initial_value );@\use{alloc}@
 \end{lstlisting}
 \end{rationale}
@@ -2915 +2899 @@
 \begin{lstlisting}
 int fi( int );
-forall( otype T ) T fT( T );
+forall( type T ) T fT( T );
 \end{lstlisting}
 \lstinline$fi()$ takes an \lstinline$int$ and returns an \lstinline$int$. \lstinline$fT()$ takes a
@@ -2921 +2905 @@
 \begin{lstlisting}
 int (*pfi )( int ) = fi;
-forall( otype T ) T (*pfT )( T ) = fT;
+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.
@@ -2928 +2912 @@
         return pfi;
 }
-forall( otype T ) T (*fvpfT( void ))( T ) {
+forall( type T ) T (*fvpfT( void ))( T ) {
         return pfT;
 }
@@ -2934 +2918 @@
 \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( otype T ) int ( *fTpfi( T ) )( int );
-forall( otype T ) T ( *fTpfT( T ) )( T );
-forall( otype T, otype U ) U ( *fTpfU( T ) )( U );
+forall( type T ) int ( *fTpfi( T ) )( int );
+forall( type T ) T ( *fTpfT( T ) )( T );
+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.
@@ -2946 +2930 @@
 \lstinline$char *$.
 \begin{lstlisting}
-forall( otype T, otype U, otype V ) U * f( T *, U, V * const );
-forall( otype U, otype V, otype W ) U * g( V *, U, W * const );
+forall( type T, type U, type V ) U * f( T *, U, V * const );
+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.
@@ -2955 +2939 @@
 Replacing every \(f_i\) by \(g_i\) in \(f\) gives
 \begin{lstlisting}
-forall( otype V, otype U, otype W ) U * f( V *, U, W * const );
+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}
@@ -3143 +3127 @@
 \examples
 \begin{lstlisting}
-forall( otype T | T ?*?( T, T ))@\use{?*?}@
+forall( type T | T ?*?( T, T ))@\use{?*?}@
 T square( T val ) {@\impl{square}@
         return val + val;
 }
-trait summable( otype T ) {@\impl{summable}@
+context summable( type T ) {@\impl{summable}@
         T ?+=?( T *, T );@\use{?+=?}@
         const T 0;@\use{0}@
 };
-trait list_of( otype List, otype Element ) {@\impl{list_of}@
+context list_of( type List, type Element ) {@\impl{list_of}@
         Element car( List );
         List cdr( List );
@@ -3158 +3142 @@
         int is_nil( List );
 };
-trait sum_list( otype List, otype Element | summable( Element ) | list_of( List, Element ) ) {};
+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.
@@ -3220 +3204 @@
 Incomplete type declarations allow compact mutually-recursive types.
 \begin{lstlisting}
-otype t1; // incomplete type declaration
-otype t2 = struct { t1 * p; ... };
-otype t1 = struct { t2 * p; ... };
+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.
 \begin{lstlisting}
 struct s1;
-otype t2 = struct s2 { struct s1 * p; ... };
-otype t1 = struct s1 { struct s2 * p; ... };
+type t2 = struct s2 { struct s1 * p; ... };
+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.
@@ -3283 +3267 @@
 This prevents the declaration of types that contain each other.
 \begin{lstlisting}
-otype t1;
-otype t2 = t1; // illegal: incomplete type t1
-otype t1 = t2;
+type t1;
+type t2 = t1; // illegal: incomplete type t1
+type t1 = t2;
 \end{lstlisting}
 
@@ -3292 +3276 @@
  types}.
 \begin{lstlisting}
-extern otype Huge; // extended-precision integer type
-otype Rational = struct {
+extern type Huge; // extended-precision integer type
+type Rational = struct {
         Huge numerator, denominator;    // illegal 
 };
@@ -3332 +3316 @@
 \begin{lstlisting}
 #include <stdlib.h>
-T * new( otype T ) { return ( T * )malloc( sizeof( T) ); };
+T * new( type T ) { return ( T * )malloc( sizeof( T) ); };
 @\ldots@ int * ip = new( int );
 \end{lstlisting}
@@ -3343 +3327 @@
 Since type declarations create new types, instances of types are always passed by value.
 \begin{lstlisting}
-otype A1 = int[2];
+type A1 = int[2];
 void f1( A1 a ) { a[0] = 0; };
-otypedef int A2[2];
+typedef int A2[2];
 void f2( A2 a ) { a[0] = 0; };
 A1 v1;
@@ -3362 +3346 @@
 That unit might contain the declarations
 \begin{lstlisting}
-otype Complex = struct { float re, im; };@\impl{Complex}@
+type Complex = struct { float re, im; };@\impl{Complex}@
 Complex cplx_i = { 0.0, 1.0 };@\impl{cplx_i}@
 float abs( Complex c ) {@\impl{abs( Complex )}@
@@ -3371 +3355 @@
 
 \begin{lstlisting}
-otype Time_of_day = int;@\impl{Time_of_day}@ // seconds since midnight. 
+type Time_of_day = int;@\impl{Time_of_day}@ // seconds since midnight. 
 Time_of_day ?+?( Time_of_day t1, int seconds ) {@\impl{?+?}@
         return (( int)t1 + seconds ) % 86400;
@@ -3445 +3429 @@
 \examples
 \begin{lstlisting}
-trait s( otype T ) {
+context s( type T ) {
         T a, b;
 } struct impl { int left, right; } a = { 0, 0 };
-otype Pair | s( Pair ) = struct impl;
+type Pair | s( Pair ) = struct impl;
 Pair b = { 1, 1 };
 \end{lstlisting}
@@ -3456 +3440 @@
 \lstinline$Pair b$ is compulsory because there is no \lstinline$struct impl b$ to construct a value from.
 \begin{lstlisting}
-trait ss( otype T ) {
+context ss( type T ) {
         T clone( T );
         void munge( T * );
 }
-otype Whatsit | ss( Whatsit );@\use{Whatsit}@
-otype Doodad | ss( Doodad ) = struct doodad {@\use{Doodad}@
+type Whatsit | ss( Whatsit );@\use{Whatsit}@
+type Doodad | ss( Doodad ) = struct doodad {@\use{Doodad}@
         Whatsit; // anonymous member 
         int extra;
@@ -3482 +3466 @@
 Default functions and objects are subject to the normal scope rules.
 \begin{lstlisting}
-otype T = @\ldots@;
+type T = @\ldots@;
 T a_T = @\ldots@;               // Default assignment used. 
 T ?=?( T *, T );
@@ -3751 +3735 @@
 The assertion ``\lstinline$scalar( Complex )$'' should be read as ``type \lstinline$Complex$ is scalar''.
 \begin{lstlisting}
-trait scalar( otype T ) {@\impl{scalar}@
+context scalar( type T ) {@\impl{scalar}@
         int !?( T );
         int ?<?( T, T ), ?<=?( T, T ), ?==?( T, T ), ?>=?( T, T ), ?>?( T, T ), ?!=?( T, T );
@@ -3761 +3745 @@
 This is equivalent to inheritance of specifications.
 \begin{lstlisting}
-trait arithmetic( otype T | scalar( T ) ) {@\impl{arithmetic}@@\use{scalar}@
+context arithmetic( type T | scalar( T ) ) {@\impl{arithmetic}@@\use{scalar}@
         T +?( T ), -?( T );
         T ?*?( T, T ), ?/?( T, T ), ?+?( T, T ), ?-?( T, T );
@@ -3770 +3754 @@
 \define{integral types}.
 \begin{lstlisting}
-trait integral( otype T | arithmetic( T ) ) {@\impl{integral}@@\use{arithmetic}@
+context integral( type T | arithmetic( T ) ) {@\impl{integral}@@\use{arithmetic}@
         T ~?( T );
         T ?&?( T, T ), ?|?( T, T ), ?^?( T, T );
@@ -3784 +3768 @@
 The only operation that can be applied to all modifiable lvalues is simple assignment.
 \begin{lstlisting}
-trait m_lvalue( otype T ) {@\impl{m_lvalue}@
+context m_lvalue( type T ) {@\impl{m_lvalue}@
         T ?=?( T *, T );
 };
@@ -3794 +3778 @@
 Scalars can also be incremented and decremented.
 \begin{lstlisting}
-trait m_l_scalar( otype T | scalar( T ) | m_lvalue( T ) ) {@\impl{m_l_scalar}@
+context m_l_scalar( type T | scalar( T ) | m_lvalue( T ) ) {@\impl{m_l_scalar}@
         T ?++( T * ), ?--( T * );@\use{scalar}@@\use{m_lvalue}@
         T ++?( T * ), --?( T * );
@@ -3803 +3787 @@
 Note that this results in the ``inheritance'' of \lstinline$scalar$ along both paths.
 \begin{lstlisting}
-trait m_l_arithmetic( otype T | m_l_scalar( T ) | arithmetic( T ) ) {@\impl{m_l_arithmetic}@
+context m_l_arithmetic( type T | m_l_scalar( T ) | arithmetic( T ) ) {@\impl{m_l_arithmetic}@
         T ?/=?( T *, T ), ?*=?( T *, T );@\use{m_l_scalar}@@\use{arithmetic}@
         T ?+=?( T *, T ), ?-=?( T *, T );
 };
-trait m_l_integral( otype T | m_l_arithmetic( T ) | integral( T ) ) {@\impl{m_l_integral}@
+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}@
         T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );@\use{integral}@
@@ -3827 +3811 @@
 \lstinline$arithmetic$, so these operators cannot be consolidated in \lstinline$scalar$.
 \begin{lstlisting}
-trait pointer( type P | scalar( P ) ) {@\impl{pointer}@@\use{scalar}@
+context pointer( type P | scalar( P ) ) {@\impl{pointer}@@\use{scalar}@
         P ?+?( P, long int ), ?+?( long int, P ), ?-?( P, long int );
         ptrdiff_t ?-?( P, P );
 };
-trait m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {@\impl{m_l_pointer}@
+context m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {@\impl{m_l_pointer}@
         P ?+=?( P *, long int ), ?-=?( P *, long int );
         P ?=?( P *, void * );
@@ -3843 +3827 @@
 ``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''.
 \begin{lstlisting}
-trait ptr_to( type P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@
+context ptr_to( type P | pointer( P ), type T ) {@\impl{ptr_to}@@\use{pointer}@
         lvalue T *?( P );
         lvalue T ?[?]( P, long int );
 };
-trait ptr_to_const( type P | pointer( P ), otype T ) {@\impl{ptr_to_const}@
+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}@
 };
-trait ptr_to_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@
+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}@
 };
-trait ptr_to_const_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@
+context ptr_to_const_volatile( type P | pointer( P ), type T ) }@\impl{ptr_to_const_volatile}@
         const volatile lvalue T *?( P );@\use{pointer}@
         const volatile lvalue T ?[?]( P, long int );
@@ -3865 +3849 @@
 ``\lstinline$ptr_to$'' specifications.
 \begin{lstlisting}
-trait m_l_ptr_to( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ otype T | ptr_to( P, T )@\use{ptr_to}@ {
+context m_l_ptr_to( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ type T | ptr_to( P, T )@\use{ptr_to}@ {
         P ?=?( P *, T * );
         T * ?=?( T **, P );
 };
-trait m_l_ptr_to_const( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ otype T | ptr_to_const( P, T )@\use{ptr_to_const}@) {
+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 );
 };
-trait m_l_ptr_to_volatile( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ otype T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@
+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 );
 };
-trait 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}@
+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}@
         P ?=?( P *, const volatile T * );
@@ -3887 +3871 @@
 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}
-trait 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 ) ) {
+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 ) ) {
         MyP ?=?( MyP *, CP );
         CP ?=?( CP *, MyP );
@@ -3920 +3904 @@
 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}
-trait comparable( otype T ) {
+context comparable( type T ) {
         const T 0;
         int compare( T, T );
 }
-forall( otype T | comparable( T ) ) int ?<?( T l, T r ) {
+forall( type T | comparable( T ) ) int ?<?( T l, T r ) {
         return compare( l, r ) < 0;
 }
 // ... similarly for <=, ==, >=, >, and !=. 
-forall( otype T | comparable( T ) ) int !?( T operand ) {
+forall( type T | comparable( T ) ) int !?( T operand ) {
         return !compare( operand, 0 );
 }
@@ -3940 +3924 @@
 Similarly, a complete integral type would provide integral operations based on integral assignment operations.
 \begin{lstlisting}
-trait arith_base( otype T ) {
+context arith_base( type T ) {
         const T 1;
         T ?+=?( T *, T ), ?-=?( T *, T ), ?*=?( T *, T ), ?/=?( T *, T );
 }
-forall( otype T | arith_base( T ) ) T ?+?( T l, T r ) {
+forall( type T | arith_base( T ) ) T ?+?( T l, T r ) {
         return l += r;
 }
-forall( otype T | arith_base( T ) ) T ?++( T * operand ) {
+forall( type T | arith_base( T ) ) T ?++( T * operand ) {
         T temporary = *operand;
         *operand += 1;
         return temporary;
 }
-forall( otype T | arith_base( T ) ) T ++?( T * operand ) {
+forall( type T | arith_base( T ) ) T ++?( T * operand ) {
         return *operand += 1;
 }
 // ... similarly for -, --, *, and /. 
-trait int_base( otype T ) {
+context int_base( type T ) {
         T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );
         T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );
 }
-forall( otype T | int_base( T ) ) T ?&?( T l, T r ) {
+forall( type T | int_base( T ) ) T ?&?( T l, T r ) {
         return l &= r;
 }