diff options
Diffstat (limited to 'src/gen_lib/sail2_state_monad.lem')
| -rw-r--r-- | src/gen_lib/sail2_state_monad.lem | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem index b2a7bb31..18e57b30 100644 --- a/src/gen_lib/sail2_state_monad.lem +++ b/src/gen_lib/sail2_state_monad.lem @@ -130,26 +130,26 @@ let get_mem_bytes addr sz s = (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs))) (just_list (List.map (read_byte s) addrs)) -val read_tagged_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e -let read_tagged_mem_bytesS _ addr sz = +val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e +let read_memt_bytesS _ addr sz = readS (get_mem_bytes addr sz) >>$= maybe_failS "read_memS" val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e let read_mem_bytesS rk addr sz = - read_tagged_mem_bytesS rk addr sz >>$= (fun (bytes, _) -> + read_memt_bytesS rk addr sz >>$= (fun (bytes, _) -> returnS bytes) -val read_tagged_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e -let read_tagged_memS rk a sz = +val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e +let read_memtS rk a sz = maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a -> - read_tagged_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) -> + read_memt_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) -> maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val -> returnS (mem_val, tag)))) val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e let read_memS rk a sz = - read_tagged_memS rk a sz >>$= (fun (bytes, _) -> + read_memtS rk a sz >>$= (fun (bytes, _) -> returnS bytes) val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e |