Changes in doc/refrat/refrat.tex [e55ca05:a752883]

File:

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

doc/refrat/refrat.tex

@@ -1 @@
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- Mode: Latex -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% 
-%% Cforall Version 1.0.0 Copyright (C) 2016 University of Waterloo
-%%
-%% The contents of this file are covered under the licence agreement in the
-%% file "LICENCE" distributed with Cforall.
-%% 
-%% refrat.tex -- 
-%% 
-%% Author           : Peter A. Buhr
-%% Created On       : Wed Apr  6 14:52:25 2016
-%% Last Modified By : Peter A. Buhr
-%% Last Modified On : Fri Apr  8 18:32:07 2016
-%% Update Count     : 6
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
 % requires tex packages: texlive-base texlive-latex-base tex-common texlive-humanities texlive-latex-extra texlive-fonts-recommended
 
@@ -21 +5 @@
 
 % Latex packages used in the document.
+
 \usepackage{fullpage,times}
 \usepackage{xspace}
@@ -36 +21 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+% Names used in the document.
+
+\newcommand{\CFA}{C$\forall$\xspace}    % set language symbolic name
+\newcommand{\CFL}{Cforall\xspace}               % set language text 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)
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 % Bespoke macros used in the document.
-\input{common}
+
+\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}}
+
+%  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.5ex \@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{\see}[1]{\emph{see} #1}
+
+% Define some commands that produce formatted index entries suitable for cross-references.
+% ``\spec'' produces entries for specifications of entities.  ``\impl'' produces entries for their
+% implementations, and ``\use'' for their uses.
+
+%  \newcommand{\bold}[1]{{\bf #1}}
+%  \def\spec{\@bsphack\begingroup
+%             \def\protect##1{\string##1\space}\@sanitize
+%             \@wrxref{|bold}}
+\def\impl{\@bsphack\begingroup
+          \def\protect##1{\string##1\space}\@sanitize
+          \@wrxref{|definition}}
+\newcommand{\indexcode}[1]{{\lstinline$#1$}}
+\def\use{\@bsphack\begingroup
+         \def\protect##1{\string##1\space}\@sanitize
+         \@wrxref{|hyperpage}}
+\def\@wrxref#1#2{\let\thepage\relax
+    \xdef\@gtempa{\write\@indexfile{\string
+    \indexentry{#2@{\lstinline$#2$}#1}{\thepage}}}\endgroup\@gtempa
+    \if@nobreak \ifvmode\nobreak\fi\fi\@esphack}
+%\newcommand{\use}[1]{\index{#1@{\lstinline$#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}
+\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}
+\newcommand{\@sIndex}[2][\@empty]{#2\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
+\makeatother
+
+% blocks and titles
+\newenvironment{rationale}{%
+  \begin{quotation}\noindent$\Box$\enspace
+}{%
+  \hfill\enspace$\Box$\end{quotation}
+}%
+\newcommand{\define}[1]{\emph{#1\/}\index{#1}}
+\newcommand{\rewrite}{\(\Rightarrow\)}
+\newcommand{\rewriterules}{\paragraph{Rewrite Rules}~\par\noindent}
+\newcommand{\examples}{\paragraph{Examples}~\par\noindent}
+\newcommand{\semantics}{\paragraph{Semantics}~\par\noindent}
+\newcommand{\constraints}{\paragraph{Constraints}~\par\noindent}
+\newcommand{\predefined}{\paragraph{Predefined Identifiers}~\par\noindent}
+
+% BNF macros
+\def\syntax{\paragraph{Syntax}\trivlist\parindent=.5in\item[\hskip.5in]}
+\let\endsyntax=\endtrivlist
+\newcommand{\lhs}[1]{\par{\emph{#1:}}\index{#1@{\emph{#1}}|italic}}
+\newcommand{\rhs}{\hfil\break\hbox{\hskip1in}}
+\newcommand{\oldlhs}[1]{\emph{#1: \ldots}\index{#1@{\emph{#1}}|italic}}
+\newcommand{\nonterm}[1]{\emph{#1\/}\index{#1@{\emph{#1}}|italic}}
+\newcommand{\opt}{$_{opt}$\ }
+
+% adjust varioref package with default "section" and "page" titles, and optional title with faraway page numbers
+% \VRef{label} => Section 2.7, \VPageref{label} => page 17
+% \VRef[Figure]{label} => Figure 3.4, \VPageref{label} => page 17
+\renewcommand{\reftextfaceafter}{\unskip}
+\renewcommand{\reftextfacebefore}{\unskip}
+\renewcommand{\reftextafter}{\unskip}
+\renewcommand{\reftextbefore}{\unskip}
+\renewcommand{\reftextfaraway}[1]{\unskip, p.~\pageref{#1}}
+\renewcommand{\reftextpagerange}[2]{\unskip, pp.~\pageref{#1}--\pageref{#2}}
+\newcommand{\VRef}[2][Section]{\ifx#1\@empty\else{#1}\nobreakspace\fi\vref{#2}}
+\newcommand{\VPageref}[2][page]{\ifx#1\@empty\else{#1}\nobreakspace\fi\pageref{#2}}
+
+% CFA based on ANSI C
+\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,},
+}%
+
+\lstset{
+language=CFA,
+columns=flexible,
+basicstyle=\sf\relsize{-1},
+tabsize=4,
+xleftmargin=\parindent,
+escapechar=@,
+keepspaces=true,
+showstringspaces=false,
+showlines=true,
+}%
+
+\makeatletter
+% replace/adjust listings characters that look bad in sanserif
+\lst@CCPutMacro
+\lst@ProcessOther{"2D}{\lst@ttfamily{-{}}{{\ttfamily\upshape -}}} % replace minus
+\lst@ProcessOther{"3C}{\lst@ttfamily{<}{\texttt{<}}} % replace less than
+\lst@ProcessOther{"3E}{\lst@ttfamily{<}{\texttt{>}}} % replace greater than
+\lst@ProcessOther{"5E}{\raisebox{0.4ex}{$\scriptstyle\land\,$}} % replace circumflex
+\lst@ProcessLetter{"5F}{\lst@ttfamily{\char95}{{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}}} % replace underscore
+\lst@ProcessOther{"7E}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}} % replace tilde
+%\lst@ProcessOther{"7E}{\raisebox{-.4ex}[1ex][0pt]{\textasciitilde}} % lower tilde
+\@empty\z@\@empty
+\makeatother
 
 \setcounter{secnumdepth}{3}     % number subsubsections
@@ -84 +226 @@
 
 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{C11}, and occasionally compares \CFA to {\CC} \cite{C++}.
+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).
@@ -578 +720 @@
 
 There are two notable differences between \CFA's overload resolution rules and the rules for
-{\CC} defined in \cite{C++}.
+{\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.
@@ -3242 +3384 @@
 \begin{itemize}
 \item
-Inside a Clu cluster \cite{CLU}, the declaration of an instance states which view applies.
+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.
+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.
+\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.
+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.
@@ -3701 +3843 @@
 ``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''.
 \begin{lstlisting}
-trait ptr_to( otype P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@
+trait ptr_to( type P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@
         lvalue T *?( P );
         lvalue T ?[?]( P, long int );
 };
-trait ptr_to_const( otype P | pointer( P ), otype T ) {@\impl{ptr_to_const}@
+trait ptr_to_const( type P | pointer( P ), otype T ) {@\impl{ptr_to_const}@
         const lvalue T *?( P );
         const lvalue T ?[?]( P, long int );@\use{pointer}@
 };
-trait ptr_to_volatile( otype P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@
+trait ptr_to_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@
         volatile lvalue T *?( P );
         volatile lvalue T ?[?]( P, long int );@\use{pointer}@
 };
-trait ptr_to_const_volatile( otype P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@
+trait ptr_to_const_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@
         const volatile lvalue T *?( P );@\use{pointer}@
         const volatile lvalue T ?[?]( P, long int );
@@ -3723 +3865 @@
 ``\lstinline$ptr_to$'' specifications.
 \begin{lstlisting}
-trait m_l_ptr_to( otype P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ otype T | ptr_to( P, T )@\use{ptr_to}@ {
+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}@ {
         P ?=?( P *, T * );
         T * ?=?( T **, P );
 };
-trait m_l_ptr_to_const( otype 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}@) {
+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}@) {
         P ?=?( P *, const T * );
         const T * ?=?( const T **, P );
 };
-trait m_l_ptr_to_volatile( otype 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}@
+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}@
         P ?=?( P *, volatile T * );
         volatile T * ?=?( volatile T **, P );
 };
-trait m_l_ptr_to_const_volatile( otype P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@
-                otype 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}@
+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}@
+                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 * );
         const volatile T * ?=?( const volatile T **, P );
@@ -3864 +4006 @@
 
 \bibliographystyle{plain}
-\bibliography{cfa}
+\bibliography{refrat}