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.

1 files changed, 17 insertions, 8 deletions

diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index edbe1f03..92b9ac5e 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -127,11 +127,20 @@ let try_catchR m h =
       | Right e -> h e
      end)
 
+val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e
+let maybe_fail msg = function
+  | Just a -> return a
+  | Nothing -> Fail msg
+end
+
+val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
+let read_mem_bytes rk addr sz =
+  Read_mem rk (bits_of addr) (nat_of_int sz) return
 
 val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
 let read_mem rk addr sz =
-  let k bytes = Done (bits_of_mem_bytes bytes) in
-  Read_mem rk (bits_of addr) (natFromInteger sz) k
+  read_mem_bytes rk addr sz >>= (fun bytes ->
+  maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
 
 val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
 let read_tag addr = Read_tag (bits_of addr) return
@@ -142,7 +151,7 @@ let excl_result () =
   Excl_res k
 
 val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (natFromInteger sz) (Done ())
+let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
 
 val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
 let write_mem_val v = match mem_bytes_of_bits v with
@@ -166,10 +175,10 @@ let read_reg reg =
 (* TODO
 val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
 let read_reg_range reg i j =
-  read_reg_aux of_bits (external_reg_slice reg (natFromInteger i,natFromInteger j))
+  read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j))
 
 let read_reg_bit reg i =
-  read_reg_aux (fun v -> v) (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
+  read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v ->
   return (extract_only_element v)
 
 let read_reg_field reg regfield =
@@ -188,9 +197,9 @@ let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())
 let write_reg reg v =
   write_reg_aux (external_reg_whole reg) v
 let write_reg_range reg i j v =
-  write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
+  write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v
 let write_reg_pos reg i v =
-  let iN = natFromInteger i in
+  let iN = nat_of_int i in
   write_reg_aux (external_reg_slice reg (iN,iN)) [v]
 let write_reg_bit = write_reg_pos
 let write_reg_field reg regfield v =
@@ -199,7 +208,7 @@ let write_reg_field_bit reg regfield bit =
   write_reg_aux (external_reg_field_whole reg regfield.field_name)
                 (Vector [bit] 0 (is_inc_of_reg reg))
 let write_reg_field_range reg regfield i j v =
-  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
+  write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v
 let write_reg_field_pos reg regfield i v =
   write_reg_field_range reg regfield i i [v]
 let write_reg_field_bit = write_reg_field_pos*)