A bit better readme

A few more tips
Trying to fix up and bring up to date the built-in types and library

1 files changed, 77 insertions, 40 deletions

diff --git a/language/manual.tex b/language/manual.tex
index 25bfbde3..2052ea0e 100644
--- a/language/manual.tex
+++ b/language/manual.tex
@@ -24,6 +24,83 @@ 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 for each
+  kind of access.
+
+For basic user-mode instructions, there should be the need for only
+one memory read and one 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 a \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.
+
+\end{itemize}
+
+
+
 \section{Sail syntax}
 
 \ottgrammartabular{
@@ -85,46 +162,6 @@ developers are highly encouraged.
 \ottfunctionsXXwithXXcoercions\ottinterrule}
 \newpage
 
-\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.
-
-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 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 \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.
-
-\end{itemize}
-
 \section{Sail type system}
 
 \subsection{Internal type syntax}