\documentclass[11pt]{article}

\usepackage{amsmath,amssymb,supertabular,geometry,fullpage}
\geometry{a4paper,twoside,landscape,left=10.5mm,right=10.5mm,top=20mm,bottom=30mm}
\usepackage{color}

\begin{document}

\input{doc_in}

\title{Sail Manual}
\author{Kathryn E Gray, Gabriel Kerneis, Peter Sewell}

\maketitle

\tableofcontents

\newpage

\section{Introduction}

This is a manual describing the Sail specification language, its
common library, compiler, interpreter and type system. However it is
currently in early stages of being written, so questions to the
developers are highly encouraged.

\section{Tips for Writing Sail specifications}

This section attempts to offer advice for writing Sail specifications
that will work well with the Sail executable interpreter and
compilers.

These tips use ideomatic Sail code; the Sail syntax is formally
defined in following section.

Some tips might also be advice for good ways to specify instructions;
this will come from a combination of users and Sail developers.

\begin{itemize}

\item Declare memory access functions as one read, one write announce,
  and one write value for each kind of access.

For basic user-mode instructions, there should be the need for only
one memory read and two memory write function. These should each be
declared using {\tt val extern} and should have effect {\tt wmem} and
{\tt rmem} accordingly. 

Commonly, a memory read function will take as parameters a size (an
number below 32) and an address and return a bit vector with length (8
* size). The sequential and concurrent interpreters both only read and
write memory as a factor of bytes.

\item Declare a default vector order

Vectors can be either decreasing or increasing, i.e. if we have a
vector \emph{a} with elements [1,2,3] then in an increasing specification the 1 is accessed
with {\tt a[0]} but with {\tt a[2]} in a decreasing system. Early in
your specification, it is beneficial to clarity to say default Ord inc
or default Ord dec.

\item Vectors don't necessarily begin indexing at 0 or n-1

Without any additional specification, a vector will begin indexing at
0 in an increasing spec and n-1 in a decreasing specification. A type
declaration can reset this first position to any number. 

Importantly, taking a slice of a vector does not reset the indexes. So
if {\tt a = [1,2,3,4]} in an increasing system the slice {\tt a[2
  ..3]} generates the vector {\tt [3,4]} and the 3 is indexed at 2 in either vector.

\item Be precise in numeric types. 

While Sail includes very wide types like int and nat, consider that
for bounds checking, numeric operations, and and clear understanding,
these really are unbounded quantities. If you know that a number in
the specification will range only between 0 and 32, 0 and 4, $-32$ to
32, it is better to use a specific range type such as $[|32|]$. 

Similarly, if you don't know the range precisely, it may also be best
to remain polymorphic and let Sail's type resolution work out bounds
in a particular use rather than removing all bounds; to do this, use
[:'n:] to say that it will polymorphically take some number.

\item Use bit vectors for registers.

Sail the language will readily allow a register to store a value of
any type. However, the Sail executable interpreter expects that it is
simulating a uni-processor machine where all registers are bit
vectors.

A vector of length one, such as \emph{a} can read the element of \emph{a}
either with {\tt a} or {\tt a[0]}.

\item Have functions named decode and execute to evaluate
  instructions.

The sail interpreter is hard-wired to look for functions with these names.

\item Type annotations are necessary to read the contents of a
  register into a local variable.

The code {\tt x := GPR[4]}, where GPR is a vector of general purpose
registers, will store a local reference to the fourth general purpose
register, not the contents of that registe, i.e. this will not read
the register. To read the register contents into a local variable, the
type is required explicitly so {\tt (bit[64]) x := GPR[4]} reads the
register contents into x. The type annotation may be on either side of
the assignment.

\end{itemize}



\section{Sail syntax}

\ottgrammartabular{
\ottl\ottinterrule
\ottannot\ottinterrule
\ottid\ottinterrule
\ottkid\ottinterrule
\ottbaseXXkind\ottinterrule
\ottkind\ottinterrule
\ottnexp\ottinterrule
\ottorder\ottinterrule
\ottbaseXXeffect\ottinterrule
\otteffect\ottinterrule
\otttyp\ottinterrule
\otttypXXarg\ottinterrule
\ottnXXconstraint\ottinterrule
\ottkindedXXid\ottinterrule
\ottquantXXitem\ottinterrule
\otttypquant\ottinterrule
\otttypschm\ottinterrule
\ottnameXXscmXXopt\ottinterrule
\otttypeXXdef\ottinterrule
\otttypeXXunion\ottinterrule
\ottindexXXrange\ottinterrule
\ottlit\ottinterrule
\ottsemiXXopt\ottinterrule
\ottpat\ottinterrule
\ottfpat\ottinterrule
\ottexp\ottinterrule
\ottlexp\ottinterrule
\ottfexp\ottinterrule
\ottfexps\ottinterrule
\ottoptXXdefault\ottinterrule
\ottpexp\ottinterrule
\otttannotXXopt\ottinterrule
\ottrecXXopt\ottinterrule
\otteffectXXopt\ottinterrule
\ottfuncl\ottinterrule
\ottfundef\ottinterrule
\ottletbind\ottinterrule
\ottvalXXspec\ottinterrule
\ottdefaultXXspec\ottinterrule
\ottscatteredXXdef\ottinterrule
\ottregXXid\ottinterrule
\ottaliasXXspec\ottinterrule
\ottdecXXspec\ottinterrule
\ottdef\ottinterrule
\ottdefs\ottinterrule}

\newpage
\section{Sail primitive types and functions}

\ottgrammartabular{
\ottbuiltXXinXXtypes\ottinterrule}

\ottgrammartabular{
\ottbuiltXXinXXtypeXXabbreviations\ottinterrule
\ottfunctions\ottinterrule
\ottfunctionsXXwithXXcoercions\ottinterrule}
\newpage

\section{Sail type system}

\subsection{Internal type syntax}

\ottgrammartabular{
\ottk\ottinterrule
\ottt\ottinterrule
\ottoptx\ottinterrule
\otttag\ottinterrule
\ottne\ottinterrule
\otttXXarg\ottinterrule
\otttXXargs\ottinterrule
\ottnec\ottinterrule
\ottSXXN\ottinterrule
\ottEXXd\ottinterrule
\ottkinf\ottinterrule
\otttid\ottinterrule
\ottEXXk\ottinterrule
\otttinf\ottinterrule
\ottEXXa\ottinterrule
\ottfieldXXtyps\ottinterrule
\ottEXXr\ottinterrule
\ottenumerateXXmap\ottinterrule
\ottEXXe\ottinterrule
\ottEXXt\ottinterrule
\ottts\ottinterrule
\ottE\ottinterrule
\ottI\ottinterrule
\ottformula\ottinterrule}


\subsection{ Type relations }
\ottdefnss

\section{Sail operational semantics \{TODO\}}

\end{document}