diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 4 | ||||
| -rw-r--r-- | doc/examples/my_replicate_bits.sail | 4 | ||||
| -rw-r--r-- | doc/riscv.tex | 4 | ||||
| -rw-r--r-- | doc/tutorial.tex | 8 |
4 files changed, 10 insertions, 10 deletions
diff --git a/doc/Makefile b/doc/Makefile index 981463ca..7afebdf2 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -85,5 +85,5 @@ clean: -rm -f code_riscv.tex -rm -rf code_myreplicatebits/ -rm -f code_myreplicatebits.tex - -rm *.aux - -rm *.log + -rm -f *.aux + -rm -f *.log diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail index 8c3c9458..9334163b 100644 --- a/doc/examples/my_replicate_bits.sail +++ b/doc/examples/my_replicate_bits.sail @@ -44,9 +44,9 @@ function my_replicate_bits_2(n, xs) = { ys } -val cast extz : forall 'n 'm, 'm >= 'n. bits('n) -> bits('m) +val cast extz : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) -function extz(xs) = zero_extend(xs, 'm) +function extz(m, xs) = zero_extend(xs, m) val my_replicate_bits_3 : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm) diff --git a/doc/riscv.tex b/doc/riscv.tex index 586efdf4..ee0c07e1 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -61,7 +61,7 @@ register Xs : vector(32, dec, xlen_t) \sailval{wX} \sailfn{wX} -\sailoverloadHHX +\sailoverloadIIX We also give a function \ll{MEMr} for reading memory, this function just points at a builtin we have defined elsewhere. Note that @@ -138,4 +138,4 @@ end execute The actual code for this example, as well as our more complete \riscv\ specification can be found on our github at -\anonymise{\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}}. +\anonymise{\url{https://github.com/rems-project/sail-riscv/blob/master/model/riscv_duopod.sail}}. diff --git a/doc/tutorial.tex b/doc/tutorial.tex index dcac1c13..9bf47f5b 100644 --- a/doc/tutorial.tex +++ b/doc/tutorial.tex @@ -372,7 +372,7 @@ Sail allows numerous ways to match on bitvectors, for example: \begin{lstlisting} match v { 0xFF => print("hex match"), - 0x0000_0001 => print("binary match"), + 0b0000_0001 => print("binary match"), 0xF @ v : bits(4) => print("vector concatenation pattern"), 0xF @ [bitone, _, b1, b0] => print("vector pattern"), _ : bits(4) @ v : bits(4) => print("annotated wildcard pattern") @@ -499,7 +499,7 @@ written \end{lstlisting} but it would not have type-checked. The reason for this is if a mutable variable is declared without a type, Sail will try to infer -the most specific type from the left hand side of the +the most specific type from the right hand side of the expression. However, in this case Sail will infer the type as \ll{int(3)} and will therefore complain when we try to reassign it to \ll{2}, as the type \ll{int(2)} is not a subtype of \ll{int(3)}. We @@ -629,7 +629,7 @@ implicitly 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} +val cast auto_reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} \end{lstlisting} @@ -687,7 +687,7 @@ the names of its fields. \subsubsection{Unions} \label{sec:union} -As an example, the \ll{maybe} type \'{a} la Haskell could be defined +As an example, the \ll{maybe} type \`{a} la Haskell could be defined in Sail as follows: \begin{lstlisting} union maybe ('a : Type) = { |