Make partiality more explicit in library functions of Lem shallow embedding

Some functions are partial, e.g. converting a bitvector to an integer, which
might fail for the bit list representation due to undefined bits.  Undefined
cases can be handled in different ways:

- call Lem's failwith, which maps to undefined/ARB in Isabelle and HOL (the
  default so far),
- return an option type,
- raise a failure  in the monad, or
- use a bitstream oracle to resolve undefined bits.

This patch adds different versions of partial functions corresponding to those
options.  The desired behaviour can be selected by choosing a binding in the
Sail prelude.  The naming scheme is that the failwith version is the default,
while the other versions have the suffixes _maybe, _fail, and _oracle,
respectively.

2 files changed, 5 insertions, 5 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index b6c80ffb..f6532215 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -110,9 +110,9 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys)
 
 overload operator | = {or_bool, or_vec}
 
-val unsigned = {ocaml: "uint", lem: "unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
+val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
-val signed = {ocaml: "sint", lem: "signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
 val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
 
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 49499445..9d9ccf89 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -49,7 +49,7 @@ let get_slice_int len n lo =
   (* TODO: Is this the intended behaviour? *)
   let hi = lo + len - 1 in
   let bits = bits_of_int (hi + 1) n in
-  of_bits (get_bits false bits hi lo)
+  of_bits_failwith (subrange_list false bits hi lo)
 
 val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
 let sign_extend v len = exts_vec len v
@@ -57,9 +57,9 @@ val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> b
 let zero_extend v len = extz_vec len v
 
 val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_right v m = shiftr v (unsigned m)
+let shift_bits_right v m = shiftr v (uint m)
 val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_left v m = shiftl v (unsigned m)
+let shift_bits_left v m = shiftl v (uint m)
 
 val prerr_endline : string -> unit
 let prerr_endline _ = ()