A bit better readme

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

3 files changed, 84 insertions, 44 deletions

diff --git a/language/manual.pdf b/language/manual.pdf
index ef692a90..e5a8e457 100644
--- a/language/manual.pdf
+++ b/language/manual.pdf
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}
diff --git a/language/primitive_doc.ott b/language/primitive_doc.ott
index ae6fcd50..a53f62fe 100644
--- a/language/primitive_doc.ott
+++ b/language/primitive_doc.ott
@@ -5,13 +5,14 @@ built_in_types :: '' ::=
   | bit : Typ :: :: bitDesc
   | unit : Typ :: :: unitDesc
   | forall Nat 'n. Nat 'm. range <'n, 'm> : Nat -> Nat -> Typ :: :: rangeDesc
-  | forall Nat 'n. atom <'n> : Nat -> Typ :: :: atomDesc {{ com singleton number, instead of range<'n,'n> }}
+  | forall Nat 'n. atom <'n> : Nat -> Typ :: :: atomDesc {{ com singleton number, instead of range$< 'n,'n >$ }}
   | forall Nat 'n, Nat 'm, Order 'o, Typ 't. vector < 'n, 'm, 'o, 't > : Nat -> Nat -> Order -> Typ :: :: vectorDesc
+  | forall Typ 'a. option < 'a > : Typ -> Typ :: :: optCtors
   | forall Typ 't. register < 't > : Typ -> Typ :: :: registerDec
   | forall Typ 't. reg < 't > : Typ -> Typ :: :: regDec
     {{ com internal reference cell }}
   | forall Nat 'n . implicit <'n> : Nat -> Typ :: :: implicitDesc
-    {{ com see Kathy for explanation }}
+    {{ com To add to a function val specification indicating that n relies on call site expected value }}
 
 built_in_type_abbreviations :: '' ::=
   | bool => bit :: :: boolDesc
@@ -20,13 +21,15 @@ built_in_type_abbreviations :: '' ::=
   | uint8 => [| 0 '..' 2**8 |] :: :: uinteightDesc
   | uint16 => [| 0 '..' 2**16 |] :: :: uintsixteenDesc
   | uint32 => [| 0 '..' 2**32 |] :: :: uintthirtytwoDesc
-  | uint64 => [| 0 '..' 2**32 |] :: :: uintsixtyfourDesc
+  | uint64 => [| 0 '..' 2**64 |] :: :: uintsixtyfourDesc
 
 
 functions :: '' ::=
   {{ com Built-in functions: all have effect pure, all order polymorphic }}
   | val forall Typ 'a  . 'a -> unit : ignore :: :: ignore
-  | val ( [| 'n '..' 'm |] , [| 'o '..' 'p |] ) -> [| 'n + 'o '..' 'm + 'p |] : + :: :: plusbase
+  | val forall Typ 'a . 'a -> option < 'a > : Some :: :: some
+  | val forall Typ 'a . unit -> option < 'a > : None :: :: none
+  | val ( [: 'n :] , [: 'm :] ) -> [| 'n + 'm |] : + :: :: plusbase
   {{ com arithmetic addition }}
   | val forall Nat 'n . ( bit [ 'n ] , bit ['n] ) -> bit [ 'n ] : + :: :: plusvec
   {{ com unsigned vector addition }}