A bit better readme

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

4 files changed, 162 insertions, 52 deletions

diff --git a/README b/README
index f4daaf40..30cebd99 100644
--- a/README
+++ b/README
@@ -2,12 +2,61 @@
 
 Guide to Sail, as of Feb 25, 2016. 
 
-Note: the repository name intends to change to sail for a public release
-
+Note: the repository name will change to sail for a public release
+
+********************************************************************
+OVERVIEW
+
+This repository provides several tools relating to the Sail
+specification language. There is sail, the type checker and compiler
+for programs in the Sail language; a sequential Sail interpreter,
+which evaluates an Elf binary for an architecture that has been
+specified using Sail; an interface to the PPCMEM concurrent
+evaluation and exploration tool; and a formal definition of the Sail
+language and type system.
+
+There is an example Sail specification of a MIPS processor in the mips
+subdirectory, mips.sail
+
+To check the types of definitions within a specification, one uses the
+sail executable:
+./sail mips/mips.sail
+
+There is a first-draft manual describing the language, common library,
+and some tips for sail development in manual.pdf
+
+Once sufficient instructions have been represented in a
+specification,then it may become desirable to run an executable
+sequentially to debug the specification and begin testing. For this,
+there is the sequential sail interpreter, which evaluates the
+specification on an ELF file. At present, this will require
+conversations with Kathy Gray, as connections within the sail
+interpreter implementation to the architecture being simulated have
+not been factored out into external specification files.
+
+Building the architecture for compilation to connect to the
+interpreter, one uses the sail executable:
+./sail mips/mips.sail -lem_ast
+which will generate a mips.lem file in the current directory, which
+will be linked with the sail interpreter. (It is not recommended to
+read this file, as the output is a verbose representation of the sail AST.)
+
+*** In progress. Does not work yet ***
+To generate Lem specifications for theorem proving, one uses the sail
+executable with flag:
+./sail mips/mips.sail -lem
+
+*** In progress. Does not work yet ***
+To generate OCaml output for fast sequential evaluation, one uses the
+sail executable with flag:
+./sail mips/mips.sail -ocaml
+
+**************************************************************************
 BUILDING
 
-The Sail type checker and compiler requires OCaml; it is tested
-on version 4.02.3.
+SAIL COMPILER
+
+The Sail compiler requires OCaml; it is tested on version 4.02.3.
 
 Run make in the top level l2 directory; this will generate an executable
 called sail in this directory. 
@@ -15,11 +64,17 @@ called sail in this directory.
 make clean will remove this executable as well as the build files in
 subdirectories.
 
-The Sail interpreter relies on external access to Lem and Linksem
-for building and running the interpreter.
+SAIL INTERPRETER
 
-Lem is a public bitbucket git repository. Linksem is a private bitbucket
-mercurial repsotory
+The Sail interpreter relies on external access to two external tools:
+    Lem: a specification language that generates theorem prover code
+    for HOL4, Isabelle, and Coq, and executable OCaml code from a
+    specification.
+    It is a publicly available Bitbucket repository
+    https://bitbucket.org/Peter_Sewell/lem
+    Linksem: a formal specification of ELF that includes the facility
+    to read in an ELF file and represent them in uniform ways. 
+    It is a private Bitbucket repository. 
 
 The Sail build system expects to find these repositories in in the same
 directory as the l2 repository by default. This can be changed with
@@ -34,10 +89,24 @@ to a file within the src/lem_interp directory to support new architectures.
 There is 'bit-rotted' support for evaluating separate sail files and function
 calls. 
 
+MIPS SEQUENTIAL EVALUATOR
+
+With the sail interpreter and the linksem repository explained above,
+the mips sequential interpreter can be build in the src/ subdirectory
+with
+make run_mips.native
+
+This will then evaluate any statically linked mips elf file (without
+syscalls). Use --help for command line options
+
+Todo: describe interpreter commands
+
+**************************************************************************
 EMACS MODE
 
 There is an emacs mode implementation very similar to the Tuareg mode in l2/editors 
 
+***************************************************************************
 RUNNING SAIL compiler
 
 ./sail test.sail   % Type check sail file, do not generate any output.
@@ -71,6 +140,7 @@ IN PROGRESS COMMANDS: -lem -ocaml
 The resulting output of these commands may well be untype checkable Lem or OCaml
 
 
+******************************************************************************
 DIRECTORY STRUCTURE
 
 Sail sources and binaries are to be found in the directories of
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 }}