diff options
Diffstat (limited to 'src/gen_lib/prompt_monad.lem')
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 25 |
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*) |