\documentclass[a4paper]{article} \usepackage{etoolbox} \usepackage[nounderscore]{syntax} \usepackage{amsmath,amssymb} \usepackage[svgnames]{xcolor} \usepackage{algorithmicx} \usepackage{algpseudocode} \usepackage{fullpage} \usepackage{listings} \usepackage{tikz} \usetikzlibrary{arrows} \usepackage{hyperref} \hypersetup{colorlinks=true,linkcolor=DarkRed} \newcommand{\TODO}[1]{{\color{red}{TODO: #1}}} \lstset{ basicstyle=\ttfamily\small, columns=fullflexible, breaklines=true, postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space}, } \lstdefinelanguage{sail} { morekeywords={val,function,mapping,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct, foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint}, keywordstyle={\bf\ttfamily\color{blue}}, morestring=[b]", stringstyle={\ttfamily\color{red}}, morecomment=[l][\itshape\color{DarkGreen}]{//}, morecomment=[s][\itshape\color{DarkGreen}]{/*}{*/}, deletestring=[bd]{'}, escapechar=\#, emphstyle={\it}, literate= {\{|}{{$\{|$}}1 {|\}}{{$|\}$}}1 } \lstset{language=sail} \def\sail{\trivlist \item\relax} \def\endsail{\endtrivlist} \newcommand{\saildocval}[2]{ #1 #2 } \newcommand{\saildocfcl}[2]{ #1 #2 } \newcommand{\saildoctype}[2]{ #1 #2 } \newcommand{\saildocfn}[2]{ #1 #2 } \newcommand{\saildocoverload}[2]{ #1 #2 } \renewcommand{\ll}[1]{\lstinline{#1}} \newcommand{\riscv}{RISC-V} %% \input{grammar} %% \renewcommand{\ottkw}[1]{\mbox{\ttfamily\bfseries{#1}}} %% \renewcommand{\ottsym}[1]{\mathop{\mbox{\ttfamily{#1}}}} %% %\renewcommand{\ottgrammartabular}[1]{\begin{center}\begin{tabular}{llcllllll}#1\end{tabular}\end{center}} %% \renewcommand{\ottgrammartabular}[1]{\medskip\par\begin{supertabular}{llcllllll}#1\end{supertabular}\medskip\par\noindent} %% \newcommand{\ottpartialrulehead}[3]{$#1$ & & $#2$ & $\ldots$ & & \multicolumn{2}{l}{#3}} %% \renewcommand{\ottrulehead}[3]{\multicolumn{9}{l}{$#1$\quad $#2$}}% %% \renewcommand{\ottprodline}[6]{\multicolumn{9}{l}{\quad$#1$\quad $#2$}}% % Pandoc 2.0 and above wrap lstinline with a dummy passthrough command for escaping purposes \newcommand{\passthrough}[1]{#1} \begin{document} \input{code_riscv} \title{The Sail instruction-set semantics specification language} \ifdefined\ANON \author{Anonymous} \newcommand\anonymise[1]{\emph{redacted}} \newcommand\anonymiseomit[1]{} \else \author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and Peter Sewell} \newcommand\anonymise[1]{#1} \newcommand\anonymiseomit[1]{#1} \fi \maketitle \tableofcontents \include{introduction} \include{riscv} \include{usage} \include{tutorial} \lstset{language={},escapechar=\`} \include{internals} % Remove for now since incomplete %\include{types} \bibliographystyle{unsrt} \bibliography{manual} \end{document}