Merge branch 'sail2' into asl_flow2

5 files changed, 145 insertions, 61 deletions

diff --git a/doc/Makefile b/doc/Makefile
index ae542571..981463ca 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -52,14 +52,18 @@ ifeq ($(shell which sail),)
 $(error Cannot find sail executable, make sure it is in PATH)
 endif
 
+SAIL_RISCV=../../sail-riscv
+
+all: manual.pdf
+
 .PHONY: clean
 
-code_riscv.tex: ../riscv/prelude.sail ../riscv/riscv_duopod.sail
-	sail -o code_riscv -latex ../riscv/prelude.sail ../riscv/riscv_duopod.sail
+code_riscv.tex: ${SAIL_RISCV}/model/prelude.sail ${SAIL_RISCV}/model/riscv_duopod.sail
+	sail -o code_riscv -latex -latex_full_valspecs ${SAIL_RISCV}/model/prelude.sail ${SAIL_RISCV}/model/riscv_duopod.sail
 	cp code_riscv/commands.tex code_riscv.tex
 
 code_myreplicatebits.tex: examples/my_replicate_bits.sail
-	sail -o code_myreplicatebits -latex -latex_prefix mrb examples/my_replicate_bits.sail
+	sail -o code_myreplicatebits -latex -latex_full_valspecs -latex_prefix mrb examples/my_replicate_bits.sail
 	cp code_myreplicatebits/commands.tex code_myreplicatebits.tex
 
 grammar.tex: ../language/sail.ott
diff --git a/doc/manual.tex b/doc/manual.tex
index d731ecd3..1cab3afa 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1,5 +1,6 @@
 \documentclass[a4paper]{article}
 
+\usepackage{etoolbox}
 \usepackage[nounderscore]{syntax}
 \usepackage{amsmath,amssymb}
 \usepackage[svgnames]{xcolor}
@@ -25,7 +26,7 @@
 \lstdefinelanguage{sail}
   { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof,
       scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct,
-      foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw},
+      foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint},
     keywordstyle={\bf\ttfamily\color{blue}},
     morestring=[b]",
     stringstyle={\ttfamily\color{red}},
@@ -44,6 +45,22 @@
 \def\sail{\trivlist \item\relax}
 \def\endsail{\endtrivlist}
 
+\newcommand{\saildocval}[2]{
+#1 #2
+}
+\newcommand{\saildocfcl}[2]{
+#1 #2
+}
+\newcommand{\saildoctype}[2]{
+#1 #2
+}
+\newcommand{\saildocfn}[2]{
+#1 #2
+}
+\newcommand{\saildocoverload}[2]{
+#1 #2
+}
+
 \renewcommand{\ll}[1]{\lstinline{#1}}
 
 \newcommand{\riscv}{RISC-V}
diff --git a/doc/riscv.tex b/doc/riscv.tex
index 299a7bdd..586efdf4 100644
--- a/doc/riscv.tex
+++ b/doc/riscv.tex
@@ -25,11 +25,11 @@ that the constraint on the \ll{regno} type synonym is satisfied, we
 return an existentially quantified type \ll{\{'n, 0 <= 'n <
   32. regno('n)\}}.
 
-\sailxlent
-\sailregno
-\sailregbits
-\sailregbitstoregno
-\sailfnregbitstoregno
+\sailtype{xlen_t}
+\sailtype{regno}
+\sailtype{regbits}
+\sailval{regbits_to_regno}
+\sailfn{regbits_to_regno}
 
 We now set up some basic architectural state. First creating a
 register of type \ll{xlen_t} for both the program counter \ll{PC}, and
@@ -54,13 +54,14 @@ register nextPC : xlen_t
 register Xs : vector(32, dec, xlen_t)
 \end{lstlisting}
 
-\sailrX
-\sailfnrX
-\sailfnrXA
+\sailval{rX}
+% TODO: Fix funcl commands
+\sailfclrX
+\sailfclMMMrX
 
-\sailwX
-\sailfnwX
-\sailX
+\sailval{wX}
+\sailfn{wX}
+\sailoverloadHHX
 
 We also give a function \ll{MEMr} for reading memory, this function
 just points at a builtin we have defined elsewhere. Note that
@@ -71,8 +72,8 @@ well as a host of other concurrency model related effects. They also
 indicate whether a function throws exceptions or has other non-local
 control flow (the escape effect).
 
-\sailMEMr
-\sailfnMEMr
+\sailval{MEMr}
+\sailfn{MEMr}
 
 It's common when defining architecture specifications to break
 instruction semantics down into separate functions that handle
@@ -85,7 +86,7 @@ architecture reference manual. To support this Sail supports
 decode functions, and declare them as scattered functions, as well as
 the \ll{ast} union.
 
-\sailiop
+\sailtype{iop}
 
 \begin{lstlisting}
 scattered union ast
@@ -110,8 +111,8 @@ its argument.
 union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
 \end{lstlisting}
 
-\sailfndecodeSomeITYPE
-\sailfnexecuteITYPE
+%\sailfndecodeSomeITYPE
+%\sailfnexecuteITYPE
 
 \noindent Now we do the same thing for the load-double instruction:
 
@@ -119,15 +120,15 @@ union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
 union clause ast = LOAD : (bits(12), regbits, regbits)
 \end{lstlisting}
 
-\sailfndecodeSomeLOAD
-\sailfnexecuteLOAD
+%\sailfndecodeSomeLOAD
+%\sailfnexecuteLOAD
 
 Finally we define the fallthrough case for the decode function, and
 end all our scattered definitions. Note that the clauses in a
 scattered function will be matched in the order they appear in the
 file.
 
-\sailfndecodeNone
+%\sailfndecodeNone
 
 \begin{lstlisting}
 end ast
diff --git a/doc/tutorial.tex b/doc/tutorial.tex
index 5a362c28..dcac1c13 100644
--- a/doc/tutorial.tex
+++ b/doc/tutorial.tex
@@ -12,14 +12,14 @@ Subsection, we will write our own version of the \ll{replicate_bits}
 function from the Sail library. This function takes a number $n$ and a
 bitvector, and copies that bitvector $n$ times.
 
-\mrbmyreplicatebits
+\mrbval{my_replicate_bits}
 
 \noindent The general syntax for a function type in Sail is as follows:
 \begin{center}
   \ll{val} \textit{name} \ll{:} \ll{forall} \textit{type variables} \ll{,} \textit{constraint} \ll{. (} \textit{type$_1$} \ll{,} $\ldots$ \ll{,} \textit{type$_2$} \ll{)} \ll{->} \textit{return type}
 \end{center}
 An implementation for the \ll{replicate_bits} function would be
-follows \mrbfnmyreplicatebits
+follows \mrbfn{my_replicate_bits}
 
 The general syntax for a function declaration is:
 \begin{center}
@@ -36,7 +36,7 @@ above function, and eventually return the result \verb|0xAAA|. Typing
 to be evaluated fully, rather than stepping through the execution.
 
 Sail allows type variables to be used directly within expressions, so
-the above could be re-written as \mrbfnmyreplicatebitstwo This
+the above could be re-written as \mrbfn{my_replicate_bits_two} This
 notation can be succinct, but should be used with caution. What
 happens is that Sail will try to re-write the type variables using
 expressions of the appropriate size that are available within the
@@ -48,8 +48,8 @@ however very useful for implementing functions with implicit
 parameters, e.g. we can implement a zero extension function that
 implicitly picks up its result length from the calling context as
 follows:
-\mrbextzz
-\mrbfnextzz
+\mrbval{extz}
+\mrbfn{extz}
 
 Notice that we annotated the \ll{val} declaration as a
 \ll{cast}---this means that the type checker is allowed to
@@ -58,32 +58,32 @@ check. This is another feature that must be used carefully, because
 too many implicit casts can quickly result in unreadable code. Sail
 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 function definitions 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 much like 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.
+can drop it and simply write: \mrbfn{my_replicate_bits_three}
+
+%\subsection{External Bindings}
+
+%Rather than defining functions within Sail itself, they can be mapped
+%onto function definitions 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 much like 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}
@@ -265,10 +265,10 @@ Pattern matching can be used to destructure lists, see Section~\ref{sec:pat}.
 
 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.
+instructions could be specified by 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}
@@ -473,8 +473,8 @@ If we were to write
 \end{lstlisting}
 instead, then \textit{pattern} would only be bound within
 $\textit{expression}_1$ and not any further expressions. In general
-the block-form of let statements terminated with a semicolon should be
-preferred within blocks.
+the block-form of let statements terminated with a semicolon should
+always be preferred within blocks.
 
 Variables bound within function arguments, match statement, and
 let-bindings are always immutable, but Sail also allows mutable
diff --git a/doc/usage.tex b/doc/usage.tex
index d4f87393..2711fff5 100644
--- a/doc/usage.tex
+++ b/doc/usage.tex
@@ -147,7 +147,7 @@ files.
   call the \ll{cycle_count} function for this to work.
 \end{itemize}
 
-\subsection{Lem and Isabelle}
+\subsection{Lem, Isabelle \& HOL4}
 
 We have a separate document detailing how to generate Isabelle
 theories from Sail models, and how to work with those models in
@@ -191,6 +191,68 @@ mode, a list of commands can be accessed by typing \verb+:commands+,
 while \verb+:help+ can be used to provide some documentation for each
 command.
 
+\subsection{\LaTeX\ Generation}
+
+Sail can be used to generate latex for inclusion in documentation as:
+\begin{verbatim}
+sail -o DIRECTORY -latex FILES
+\end{verbatim}
+The list of \verb+FILES+ is a list of Sail files to produce latex for,
+and \verb+DIRECTORY+ is the directory where the generated latex will
+be placed. The list of files must be a valid type-checkable series of
+Sail files. The intention behind this latex generation is for it to be
+included within existing ISA manuals written in Latex, as such the
+latex output generates a list of commands for each top-level Sail
+declaration in \verb+DIRECTORY/commands.tex+. The rest of this section
+discusses the stable features of the latex generation process---there
+are additional features for including markdown doc-comments in Sail
+code and formatting them into latex for inclusion id documentation,
+among other things, but these features are not completely stable
+yet. This manual itself makes use of the Sail latex generation, so
+\verb+doc/manual.tex+, and \verb+doc/Makefile+ can be used to see how
+the process is set up.
+
+
+\paragraph{Requirements} The generated latex uses the \emph{listings} package for formatting
+source code, uses the macros in the \emph{etoolbox} package for the
+generated commands, and relies on the \emph{hyperref} package for
+cross-referencing. These packages are available in most TeX
+distributions, and are available as part of thetexlive packages for
+Ubuntu.
+
+\paragraph{Usage} Due to the oddities of latex verbatim environments each Sail
+declaration must be placed in it's own file then the command in
+\verb+commands.tex+ includes in with \verb+\lstinputlisting+. To
+include the generated Sail in a document one would do something like:
+\begin{lstlisting}[language=TeX]
+  \input{commands.tex}
+  \sailval{my_function}
+  \sailfn{my_function}
+\end{lstlisting}
+which would enclude the type declaration (\verb+\sailval+) for
+\verb+my_function+ as well as type body of that function
+(\verb+\sailfn+).
+
+It is sometimes useful to include multiple versions of the same Sail
+definitions in a latex document. In this case the \verb+-latex_prefix+
+option can be used. For example if we used \verb+-latex_prefix prefix+
+then the above example would become:
+\begin{lstlisting}[language=TeX]
+  \input{commands.tex}
+  \prefixval{my_function}
+  \prefixfn{my_function}
+\end{lstlisting}
+
+The generated definitions are created wrapped in customisable macros
+that can be overridden to change the formatting of the Sail code. For
+\verb+\sailfn+ there is a macro \verb+\saildocfn+ that must be defined,
+and similarly for the other Sail toplevel types.
+
+\paragraph{Cross-referencing} For each macro \verb+\sail+\emph{X}\verb+{id}+ there is a macro
+\verb+\sailref+\emph{X}\verb+{id}{text}+ which creates a
+hyper-reference to the original definition. This requires the
+hyper-ref package.
+
 \subsection{Other options}
 
 Here we summarize most of the other options available for