diff options
Diffstat (limited to 'doc/tutorial.tex')
| -rw-r--r-- | doc/tutorial.tex | 74 |
1 files changed, 37 insertions, 37 deletions
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 |