More work on documentation

Should have all the main language features covered in at least some
detail now.

1 files changed, 240 insertions, 20 deletions

diff --git a/doc/tutorial.tex b/doc/tutorial.tex
index 98a06710..34046e2b 100644
--- a/doc/tutorial.tex
+++ b/doc/tutorial.tex
@@ -60,6 +60,31 @@ does not make any distinction between expressions and statements, so
 since there is only a single line of code within the foreach block, we
 can drop it and simply write: \mrbfnmyreplicatebitsthree
 
+\subsection{External Bindings}
+
+Rather than defining functions within Sail itself, they can be mapped
+onto functions definition within the various backend targets supported
+by Sail. This is primarily used to setup the primitive functions
+defined in the Sail library. These declarations work like much FFI
+bindings in many programming languages---in Sail we provide the
+\ll{val} declaration, except rather than giving a function body we
+supply a string used to identify the external operator in each
+backend. For example, we could link the \ll{>>} operator with the
+\verb|shiftl| primitive as \mrbzeightoperatorzzerozIzIznine If the
+external function has the same name as the sail function, such as
+\ll{shiftl = "shiftl"}, then we can use the shorthand syntax
+\mrbshiftl
+
+We can map onto differently-named operations for different targets by
+using a JSON-like \ll{key: "value"} notation, for example:
+\mrbzeightoperatorzzerozKzKznine We can also omit backends---in which
+case those targets will expect a definition written in Sail. Note that
+no checking is done to ensure that the definition in the target
+matches the type of the Sail function. Finally, the \ll{_} key used
+above is a wildcard that will be used for any backend not otherwise
+included. If we use the wildcard key, then we cannot omit specific
+backends to force them to use a definition in Sail.
+
 \subsection{Numeric Types}
 \label{sec:numeric}
 
@@ -95,7 +120,9 @@ Note that \ll{bit} isn't a numeric type (i.e. it's not
 \ll{range(0,1)}. This is intentional, as otherwise it would be
 possible to write expressions like \ll{(1 : bit) + 5} which would end
 up being equal to \ll{6 : range(5, 6)}. This kind of implicit casting
-from bits to other numeric types would be highly undesirable.
+from bits to other numeric types would be highly undesirable. The
+\ll{bit} type itself is a two-element type with members \ll{bitzero} and
+\ll{bitone}.
 
 \subsection{Vector Type}
 \label{sec:vec}
@@ -236,6 +263,12 @@ Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}
 
 \subsection{Other Types}
 
+Sail also has a \ll{string} type, and a \ll{real} type. The \ll{real}
+type is used to model arbitrary real numbers, so floating point
+instructions could be specified by saying that they are equivalent to
+mapping the floating point inputs to real numbers, performing the
+arithmetic operation on the real numbers, and then mapping back to a
+floating point value of the appropriate precision.
 
 \subsection{Pattern Matching}
 \label{sec:pat}
@@ -307,6 +340,17 @@ somewhat ambiguous. This is the primary reason why we have the basic,
 but incomplete, pattern exhaustiveness check mentioned above---it can
 warn you if removing an enum constructor breaks a pattern match.
 
+\paragraph{Matching on tuples}
+
+We use match to destructure tuple types, for example:
+\begin{lstlisting}
+let x : (int, int) = (2, 3) in
+match x {
+  (y, z) => print("y = 2 and z = 3")
+}
+
+\end{lstlisting}
+
 \paragraph{Matching on unions}
 
 Match can also be used to destructure union constructors, for example
@@ -443,10 +487,10 @@ assignment operator within a block.
 }
 \end{lstlisting}
 The assignment operator is the equality symbol, as in C and other
-programming languages. Sail supports a rich language of
-\emph{l-expression} forms, which can appear on the left of an
-assignment. These will be described in Subsection~\ref{sec:lexp}. Note
-that we could have written
+programming languages. Sail supports a rich language of \emph{l-value}
+forms, which can appear on the left of an assignment. These will be
+described in Subsection~\ref{sec:lexp}. Note that we could have
+written
 \begin{lstlisting}
 {
   x = 3;
@@ -473,23 +517,130 @@ the variable \ll{x}, so
 would allow \ll{x} to be either 2 or 3, but not any other value. The
 \lstinline+{|2, 3|}+ syntax is equivalent to \lstinline+{'n, 'n in {2, 3}. int('n)}+.
 
-\subsubsection{l-expressions}
+\subsubsection{Assignment and l-values}
 \label{sec:lexp}
 
-Sail allows for setter functions to be declared in a very simple way:
-\ll{f(x) = y} is sugar for \ll{f(x, y)}. This feature is commonly used
-when setting
+It is common in ISA specifications to assign to complex l-values,
+e.g.~to a subvector or named field of a bitvector register, or to an
+l-value computed with some auxiliary function, e.g.~to select the
+appropriate register for the current execution model.
+
+We have l-values that allow us to write to individual elements of a
+vector:
+\begin{lstlisting}
+{
+  v : bits(8) = 0xFF;
+  v[0] = bitzero;
+  assert(v == 0xFE)
+}
+\end{lstlisting}
+as well as sub ranges of a vector:
+\begin{lstlisting}
+{
+  v : bits(8) = 0xFF;
+  v[4 .. 0] = 0x0; // assume default Order dec
+  assert(v == 0xF0)
+}
+\end{lstlisting}
+We also have vector concatenation l-values, which work much like
+vector concatenation patterns
+\begin{lstlisting}
+{
+  v1 : bits(4) = 0xF;
+  v2 : bits(4) = 0xF;
+  v1 @ v2 = 0xAB;
+  assert(v1 == 0xA & v2 == 0xB)
+}
+\end{lstlisting}
+For structs we can write to an individual struct field as
+\begin{lstlisting}
+{
+  s : S = struct { field = 0xFF }
+  s.field = 0x00
+}
+\end{lstlisting}
+assume we have a struct type \ll{S}, with a field simply called
+\ll{field}. We can do multiple assignment using tuples, e.g.
+\begin{lstlisting}
+{
+  (x, y) = (2, 3);
+  assert(x == 2 & x == 3)
+}
+\end{lstlisting}
+
+Finally, we allow functions to appear in l-values. This is a very
+simple way to declare `setter' functions that look like custom
+l-values, for example:
+\begin{lstlisting}
+{
+  memory(addr) = 0x0F
+}
+\end{lstlisting}
+This works because \ll{f(x) = y} is sugar for \ll{f(x, y)}. This
+feature is commonly used when setting registers or memory that has
+additional semantics for when they are read or written. We commonly
+use the overloading feature to declare what appear to be getter/setter
+pairs, so the above example we could implement a \ll{read_memory}
+function and a \ll{write_memory} function and overload them both as
+\ll{memory} to allow us to write memory using \ll{memory(addr) = data}
+and read memory as \ll{data = memory(addr)}, as so:
+\begin{lstlisting}
+val read_memory : bits(64) -> bits(8)
+val write_memory : (bits(64), bits(8)) -> unit
+
+overload memory = {read_memory, write_memory}
+\end{lstlisting}
+For more details on operator and function overloading see
+Section~\ref{sec:overload}.
+
+\subsection{Registers}
+
+Registers can be declared with a top level
+\begin{center}
+  \ll{register} \textit{name} \ll{:} \textit{type}
+\end{center}
+declaration. Registers are essentially top-level global variables and
+can be set with the previously discussed l-expression forms. There is
+currently no restriction on the type of a register in
+Sail.\footnote{We may at some point want to enforce that they can be
+  mapped to bitvectors.}
+
+Registers differ from ordinary mutable variables as we can pass around
+references to them by name. A reference to a register \ll{R} is
+created as \ll{ref R}. If the register \ll{R} has the type \ll{A},
+then the type of \ll{ref R} will be \ll{register(A)}. There is a
+dereferencing l-value operator \ll{*} for assigning to a register
+reference. One use for register references is to create a list of
+general purpose registers, so they can be indexed using numeric
+variables. For example:
+\lstinputlisting{examples/regref.sail}
+
+We can dereference register references using the \ll{"reg_deref"}
+builtin (see Section~\ref{sec:prelude}), which is set up like so:
+\begin{lstlisting}
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+\end{lstlisting}
+Currently there is no built-in syntactic sugar for dereferencing
+registers in expressions.
+
+Unlike previous versions of Sail, referencing and de-referencing
+registers is done explicitly, although we can use an automatic cast to
+implictly dereference registers if that semantics is desired for a
+specific specification that makes heavy use of register references,
+like so:
+\begin{lstlisting}
+val cast auto_reg_deref = "reg_deref" : forall ('a : Type). register('a) -> a effect {rreg}
+\end{lstlisting}
 
-\fbox{TODO}
 
 \subsection{Type declarations}
 
 \subsubsection{Enumerations}
 
-Enumerations can be defined in either a Haskell-like syntax
-(useful for smaller enums) or a more traditional C-like syntax, which
-is often more readable for enumerations with more members. There are
-no lexical constraints on the identifiers that can be part of an
+Enumerations can be defined in either a Haskell-like syntax (useful
+for smaller enums) or a more traditional C-like syntax, which is often
+more readable for enumerations with more members. There are no lexical
+constraints on the identifiers that can be part of an
 enumeration. There are also no restrictions on the name of a
 enumeration type, other than it must be a valid identifier. For
 example, the following shows two ways to define the enumeration
@@ -658,6 +809,7 @@ vector slicing. Operators used in types always share precedence with
 identically named operators at the expression level.
 
 \subsection{Ad-hoc Overloading}
+\label{sec:overload}
 
 Sail has a flexible overloading mechanism using the \ll{overload}
 keyword
@@ -736,14 +888,14 @@ so we can use this to define functions with optional arguments, e.g.
 \ll{sizeof}, see Section~\ref{sec:sizeof}) or we can provide it
 ourselves as an explicit argument.
 
-\subsection{Getters and Setters}
-\label{sec:getset}
+%% \subsection{Getters and Setters}
+%% \label{sec:getset}
 
-We have already seen some examples of getters and setters in
-Subsection~\ref{sec:bitfield}, but they can be used in many other
-contexts.
+%% We have already seen some examples of getters and setters in
+%% Subsection~\ref{sec:bitfield}, but they can be used in many other
+%% contexts.
 
-\fbox{TODO}
+%% \fbox{TODO}
 
 \subsection{Sizeof and Constraint}
 \label{sec:sizeof}
@@ -793,8 +945,73 @@ otherwise not accessible at runtime, and so can be used to implement
 implicit arguments, as was seen for \ll{replicate_bits} in
 Section~\ref{sec:functions}.
 
+\subsection{Scattered Definitions}
+\label{sec:scattered}
+In a Sail specification, sometimes it is desirable to collect together
+the definitions relating to each machine instruction (or group
+thereof), e.g.~grouping the clauses of an AST type with the associated
+clauses of decode and execute functions, as in
+Section~\ref{sec:riscv}. Sail permits this with syntactic sugar for
+`scattered' definitions. Either functions or union types can be
+scattered.
+
+One begins a scattered definition by declaring the name and kind
+(either function or union) of the scattered definition, e.g.
+\begin{lstlisting}
+scattered function foo
+
+scattered union bar
+\end{lstlisting}
+This is then followed by a list of clauses for either the union or the
+function, which can be freely interleaved with other definitions (such
+as \ll{E} in the below code)
+\begin{lstlisting}[mathescape]
+union clause bar : Baz(int, int)
+
+function clause foo(Baz(x, y)) = $\ldots$
+
+enum E = A | B | C
+
+union clause bar : Quux(string)
+
+function clause foo(Quux(str)) = print(str)
+\end{lstlisting}
+Finally the scattered definition is ended with the \ll{end} keyword, like so:
+\begin{lstlisting}
+end foo
+
+end bar
+\end{lstlisting}
+
+Semantically, scattered definitions of union types appear at the start
+of their definition, and scattered definitions of functions appear at
+the end. A scattered function definition can be recursive, but
+mutually recursive scattered function definitions should be avoided.
+
+\subsection{Exceptions}
+\label{sec:exn}
+
+Perhaps suprisingly for a specification language, Sail has exception
+support. This is because exceptions as a language feature do sometimes
+appear in vendor ISA pseudocode, and such code would be very difficult
+to translate into Sail if Sail did not itself support exceptions. We
+already translate Sail to monadic theorem prover code, so working with
+a monad that supports exceptions there is fairly natural.
+
+For exceptions we have two language features: \ll{throw} statements
+and \ll{try}-\ll{catch} blocks. The throw keyword takes a value of
+type \ll{exception} as an argument, which can be any user defined type
+with that name. There is no builtin exception type, so to use
+exceptions one must be set up on a per-project basis. Usually the
+exception type will be a union, often a scattered union, which allows
+for the exceptions to be declared throughout the specification as they
+would be in OCaml, for example: \lstinputlisting{examples/exn.sail}
+Note how the use of the scattered type allows additional exceptions to
+be declared even after they are used.
+
 \subsection{Preludes and Default Environment}
 \label{sec:prelude}
+
 By default Sail has almost no built-in types or functions, except for
 the primitive types described in this Chapter. This is because
 different vendor-pseudocode's have varying naming conventions and
@@ -834,4 +1051,7 @@ operations. These are listed below:
     the default order (which must be set before including this file).
   \item[smt.sail] Defines operators allowing div, mod, and abs
     to be used in types by exposing them to the Z3 SMT solver.
+  \item[exception\_basic.sail] Defines a trivial exception type, for
+    situations where you don't want to declare your own (see
+    Section~\ref{sec:exn}).
 \end{description}