Implicit parameters are always integers, and they must appear first before any other parameters in the function type signature. The first argument can then just be omitted when calling the function, like so:
Functions may also have implicit parameters, e.g. we can implement a zero extension function that implicitly picks up its result length from the calling context as follows:
Sail will also ensure that the output of our function has precisely the length bits('n * 'm) for all possible inputs (hence why the keyword uses the mathematical forall quantifier).
The type bits('m) is a bitvector of length 'm , and int('n) is an integer with the value 'n . The result of this function will therefore be a bitvector of length 'n * 'm . We can also add constraints on these types. Here we require that we are replicating the input bitvector at least once with the 'n >= 1 constraint, and that the input bitvector length is at least one with the 'm >= 1 constraint. Sail will check that all callers of this function are guaranteed to satisfy these constraints.
This signature shows how Sail can track the length of bitvectors and the value of integer variables in type signatures, using type variables. Type variables are written with a leading 'tick', so 'n and 'm are the type variables in the above signature.
In Sail, we often define functions in two parts. First we can write the type signature for the function using the val keyword, then define the body of the function using the function keyword. In this Subsection, we will write our own version of the replicate_bits function from the Sail library. This function takes a number n and a bitvector, and creates a new bitvector containing that bitvector copied n times.
You may have noticed that in the definition of my_replicate_bits above, there was no return keyword. This is because unlike languages such as C and C++, and more similar to languages like OCaml and Rust, everything in Sail is an expression which evaluates to a value. A block in Sail is simply a sequence of expressions surrounded by curly braces { and } , and separated by semicolons. The value returned by a block is the value returned by the last expressions, and likewise the type of a block is determined by it’s final expressions, so { A; B; C } , will evaluate to the value of C after evaluating A and B in order. The expressions other than the final expression in the block must have type unit , which is discussed in the following section. Within blocks we can declare immutable variables using let , and mutable variables using var , for example:
The wikipedia page for the unit type , goes into further details on the difference between unit and void.
In Sail unit plays a similar role to void in C and C++, except unlike void it is an ordinary type and can appear anywhere and be used in generic functions.
The simplest type in Sail is the unit type unit . It is a type with a single member () . Rather than have functions that takes zero arguments, we have functions that take a single unit argument. Similarly, rather than having functions that return no results, a function with no meaningful return value can return () . The () notation reflects the fact that the unit type can be thought of as an empty tuple (see Tuples ).
... continue reading