manual.tex

\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}
\usepackage{parser_package}

\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,monadic},
    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}

\appendix
\include{grammar_section}

\bibliographystyle{unsrt}
\bibliography{manual}

\end{document}