%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- 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. %% %% common.tex -- %% %% Author : Peter A. Buhr %% Created On : Sat Apr 9 10:06:17 2016 %% Last Modified By : Peter A. Buhr %% Last Modified On : Fri Jun 10 16:35:25 2016 %% Update Count : 101 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \setlength{\textheight}{9in} %\oddsidemargin 0.0in \renewcommand{\topfraction}{0.8} % float must be greater than X of the page before it is forced onto its own page \renewcommand{\bottomfraction}{0.8} % float must be greater than X of the page before it is forced onto its own page \renewcommand{\floatpagefraction}{0.8} % float must be greater than X of the page before it is forced onto its own page \renewcommand{\textfraction}{0.0} % the entire page maybe devoted to floats with no text on the page at all \usepackage{pslatex} % reduce size of san serif font % Names used in the document. \newcommand{\CFA}{C$\mathbf\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) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \makeatletter % parindent is relative, i.e., toggled on/off in environments like itemize, % so store the value for use rather than use \parident directly. \newlength{\parindentlength} \setlength{\parindentlength}{\parindent} % allow escape sequence in lstinline %\usepackage{etoolbox} %\patchcmd{\lsthk@TextStyle}{\let\lst@DefEsc\@empty}{}{}{\errmessage{failed to patch}} % make fontsize "small" slightly larger, specifically for san serif (helvetica) in program code %\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{pslatex} % reduce size of san serif font \usepackage{relsize} % must be after change to small or selects old size % 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.5ex \@plus -1ex \@minus -.2ex}{1.75ex \@plus .2ex}{\normalfont\large\bfseries}} \renewcommand\subsection{\@startsection{subsection}{2}{\z@}{-3.25ex \@plus -1ex \@minus -.2ex}{1.5ex \@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} % reduce bullet size and spacing for "itemize" macro \renewcommand{\labelitemi}{{\raisebox{0.25ex}{\footnotesize$\bullet$}}} \renewenvironment{itemize}{\begin{list}{\labelitemi}{\topsep=5pt\itemsep=5pt\parsep=0pt}}{\end{list}} % 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} \newcommand{\Indexc}[1]{\lstinline$#1$\index{#1@\lstinline$#1$}} \newcommand{\indexc}[1]{\index{#1@\lstinline$#1$}} \newcommand{\newtermFontInline}{\emph} \newcommand{\newterm}{\@ifstar\@snewterm\@newterm} \newcommand{\@newterm}[2][\@empty]{\lowercase{\def\temp{#2}}{\newtermFontInline{#2}}\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi} \newcommand{\@snewterm}[2][\@empty]{{\newtermFontInline{#2}}\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi} \makeatother \newenvironment{quote2}{% \list{}{\lstset{resetmargins=true,aboveskip=0pt,belowskip=0pt}\topsep=4pt\parsep=0pt\leftmargin=\parindent\rightmargin\leftmargin}% \item\relax }{% \endlist }% quote2 \newenvironment{rationale}{% \begin{quotation}\noindent$\Box$\enspace }{% \hfill\enspace$\Box$\end{quotation} }% % blocks and titles \newcommand{\define}[1]{\emph{#1\/}\index{#1}} \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: \dots}\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}} % Go programming language \lstdefinelanguage{Golang}{ morekeywords=[1]{package,import,func,type,struct,return,defer,panic, recover,select,var,const,iota,},% morekeywords=[2]{string,uint,uint8,uint16,uint32,uint64,int,int8,int16, int32,int64, bool,float32,float64,complex64,complex128,byte,rune,uintptr, error,interface},% morekeywords=[3]{map,slice,make,new,nil,len,cap,copy,close,true,false, delete,append,real,imag,complex,chan,},% morekeywords=[4]{for,break,continue,range,goto,switch,case,fallthrough,if, else,default,},% morekeywords=[5]{Println,Printf,Error,},% sensitive=true,% morecomment=[l]{//},% morecomment=[s]{/*}{*/},% morestring=[b]',% morestring=[b]",% morestring=[s]{`}{`},% } % CFA programming language, based on ANSI C \lstdefinelanguage{CFA}[ANSI]{C}{ morekeywords={_Alignas,_Alignof,__alignof,__alignof__,asm,__asm,__asm__,_At,_Atomic,__attribute,__attribute__,auto, _Bool,catch,catchResume,choose,_Complex,__complex,__complex__,__const,__const__,disable,dtype,enable,__extension__, fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,__label__,lvalue,_Noreturn,otype,restrict,_Static_assert, _Thread_local,throw,throwResume,trait,try,typeof,__typeof,__typeof__,}, }% \lstset{ language=CFA, columns=flexible, basicstyle=\linespread{0.9}\sf, stringstyle=\tt, tabsize=4, xleftmargin=\parindentlength, extendedchars=true, escapechar=§, mathescape=true, keepspaces=true, showstringspaces=false, showlines=true, aboveskip=4pt, belowskip=3pt, moredelim=**[is][\color{red}]{®}{®}, % red highlighting moredelim=**[is][\color{blue}]{ß}{ß}, % blue highlighting moredelim=**[is][\color{OliveGreen}]{¢}{¢}, % green highlighting moredelim=[is][\lstset{keywords={}}]{¶}{¶}, % temporarily turn off keywords % replace/adjust listing characters that look bad in sanserif literate={-}{\raisebox{-0.15ex}{\texttt{-}}}1 {^}{\raisebox{0.6ex}{$\scriptscriptstyle\land\,$}}1 {~}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}}1 {_}{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}1 {`}{\ttfamily\upshape\hspace*{-0.1ex}`}1 {<-}{$\leftarrow$}2 {=>}{$\Rightarrow$}2 {...}{$\dots$}2, }% \lstMakeShortInline© % single-character for \lstinline % Local Variables: % % tab-width: 4 % % fill-column: 100 % % End: %