1 files changed, 0 insertions, 95 deletions
diff --git a/language/manual.tex b/language/manual.tex
index 86aaa8b0..5d4b9d6a 100644
--- a/language/manual.tex
+++ b/language/manual.tex
@@ -17,101 +17,6 @@
 
 \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{