diff options
Diffstat (limited to 'src/gen_lib/state.lem')
| -rw-r--r-- | src/gen_lib/state.lem | 34 |
1 files changed, 26 insertions, 8 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 7777cf5e..f79f8eff 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -128,8 +128,8 @@ let rec foreach_dec (i,stop,by) vars body = else ((),vars) -val foreachM_inc : forall 's 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) +val foreachM_inc : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) let rec foreachM_inc (i,stop,by) vars body = if i <= stop then @@ -138,8 +138,8 @@ let rec foreachM_inc (i,stop,by) vars body = else return ((),vars) -val foreachM_dec : forall 's 'e 'vars. (nat * nat * nat) -> 'vars -> - (nat -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) +val foreachM_dec : forall 's 'e 'vars. (integer * integer * integer) -> 'vars -> + (integer -> 'vars -> M 's 'e (unit * 'vars)) -> M 's 'e (unit * 'vars) let rec foreachM_dec (i,stop,by) vars body = if i >= stop then @@ -153,11 +153,24 @@ let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfie val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield) -val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit -let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit) +val read_reg_bitfield : forall 'e. register -> register_bitfield -> M state 'e bit +let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) + +val write_reg_bitfield : forall 'e. register -> register_bitfield -> bit -> M state 'e unit +let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) + +val write_reg_field_range : forall 'e. register -> register_field -> integer -> integer -> + vector bit -> M state 'e unit +let write_reg_field_range reg rfield i j v = + let (i',j') = field_indices rfield in + write_reg_range reg i' j' v + +val write_reg_field_bit : forall 'e. register -> register_field -> integer -> + bit -> M state 'e unit +let write_reg_field_bit reg rfield i v = + let (i',_) = field_indices rfield in + write_reg_bit reg (i + i') v -val write_reg_field_bit : forall 'e. register -> register_field_bit -> bit -> M state 'e unit -let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit) let length l = integerFromNat (length l) @@ -172,3 +185,8 @@ let write_two_regs r1 r2 vec = (if defaultDir then size - start else start - size) (if defaultDir then vsize - start else start - vsize) in write_reg r1 r1_v >> write_reg r2 r2_v + +let read_two_regs r1 r2 = + read_reg r1 >>= fun v1 -> + read_reg r2 >>= fun v2 -> + return (v1 ^^ v2) |