diff options
| author | Christopher Pulte | 2016-11-08 13:12:19 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2016-11-08 13:12:19 +0000 |
| commit | 6d946135e6b7117e7f3a1c3758bd985a5bf319fd (patch) | |
| tree | 90dea1a2046a89dfb8064710db7e57c30276846d /src/gen_lib/prompt.lem | |
| parent | 6ffc9f189fda1be0c592e8fbb70e404e49040d58 (diff) | |
fixes
Diffstat (limited to 'src/gen_lib/prompt.lem')
| -rw-r--r-- | src/gen_lib/prompt.lem | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 6d895a87..4018fd54 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -32,8 +32,8 @@ let inline (>>=) = bind val (>>) : forall 'b. M unit -> M 'b -> M 'b let inline (>>) m n = m >>= fun _ -> n -val exit : forall 'a. string -> M 'a -let exit s = Fail (Just s) +val exit : forall 'a 'b. 'b -> M 'a +let exit s = Fail Nothing val read_mem : end_flag -> bool -> read_kind -> vector bitU -> integer -> M (vector bitU) let read_mem endian dir rk addr sz = @@ -93,6 +93,9 @@ let write_reg_field reg regfield v = let write_reg_bitfield reg regfield bit = write_reg_aux (extern_reg_field_whole reg regfield) (Vector [bit] 0 (is_inc_of_reg reg)) +let write_reg_field_range reg regfield i j v = + write_reg_aux (extern_reg_field_slice reg regfield (natFromInteger i,natFromInteger j)) v + val barrier : barrier_kind -> M unit |
