diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/prompt.lem | 33 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 14 |
2 files changed, 24 insertions, 23 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 0b616b7e..8e1e1f67 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -133,25 +133,26 @@ type M 'a = outcome 'a val return : forall 'a. 'a -> M 'a let return a = Done a -val bind : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b -let rec bind m f = match m with +val (>>=) : forall 'a 'b. M 'a -> ('a -> M 'b) -> M 'b +val (>>>) : forall 'a 'b 'c. ('a -> M 'b) -> ('b -> M 'c) -> ('a -> M 'c) + +let rec (>>=) m f = match m with | Done a -> f a - | Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> bind (k v) f) - | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> bind (k b) f) - | Write_ea wk addr sz rs k -> Write_ea wk addr sz rs (bind k f) - | Write_memv v rs k -> Write_memv v rs (fun b -> bind (k b) f) - | Barrier bk k -> Barrier bk (bind k f) - | Footprint k -> Footprint (bind k f) - | Read_reg reg k -> Read_reg reg (fun v -> bind (k v) f) - | Write_reg reg v k -> Write_reg reg v (bind k f) - | Nondet_choice actions k -> Nondet_choice actions (fun c -> bind (k c) f) + | Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> (k v) >>= f) + | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> (k b) >>= f) + | Write_ea wk addr sz rs k -> Write_ea wk addr sz rs (k >>= f) + | Write_memv v rs k -> Write_memv v rs (fun b -> (k b) >>= f) + | Barrier bk k -> Barrier bk (k >>= f) + | Footprint k -> Footprint (k >>= f) + | Read_reg reg k -> Read_reg reg (fun v -> (k v) >>= f) + | Write_reg reg v k -> Write_reg reg v (k >>= f) + | Nondet_choice actions k -> Nondet_choice actions (fun c -> (k c) >>= f) | Escape -> Escape end val exit : forall 'a 'e. 'e -> M 'a let exit _ = Escape -let (>>=) = bind let (>>) m n = m >>= fun _ -> n val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) @@ -240,11 +241,11 @@ let read_reg_field reg rfield = val write_reg_field : register -> register_field -> vector bit -> M unit let write_reg_field reg rfield = write_reg_range reg (field_indices rfield) -val read_reg_field_bit : register -> register_field_bit -> M bit -let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit) +val read_reg_bitfield : register -> register_bitfield -> M bit +let read_reg_bitfield reg rbit = read_reg_bit reg (field_index_bit rbit) -val write_reg_field_bit : register -> register_field_bit -> bit -> M unit -let write_reg_field_bit reg rbit = write_reg_bit reg (field_index_bit rbit) +val write_reg_bitfield : register -> register_bitfield -> bit -> M unit +let write_reg_bitfield reg rbit = write_reg_bit reg (field_index_bit rbit) val foreach_inc : forall 'vars. (integer * integer * integer) (*(nat * nat * nat)*) -> 'vars -> (integer (*nat*) -> 'vars -> (unit * 'vars)) -> (unit * 'vars) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 481a4e5b..2681d334 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -329,15 +329,15 @@ let bitwise_leftshift = shift_op_vec LL (*"<<"*) let bitwise_rightshift = shift_op_vec RR (*">>"*) let bitwise_rotate = shift_op_vec LLL (*"<<<"*) -let rec arith_op_no0 (op : integer -> integer -> integer) (l,r) = +let rec arith_op_no0 (op : integer -> integer -> integer) l r = if r = 0 then Nothing else Just (op l r) -let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size (((V _ start is_inc) as l),r) = +let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((V _ start is_inc) as l) r = let act_size = length l * size in let (l',r') = (to_num sign l,to_num sign r) in - let n = arith_op_no0 op (l',r') in + let n = arith_op_no0 op l' r' in let (representable,n') = match n with | Just n' -> @@ -353,13 +353,13 @@ let mod_VVV = arith_op_vec_no0 integerMod false 1 let quot_VVV = arith_op_vec_no0 integerDiv false 1 let quotS_VVV = arith_op_vec_no0 integerDiv true 1 -let arith_op_overflow_no0_vec op sign size (((V _ start is_inc) as l),r) = +let arith_op_overflow_no0_vec op sign size ((V _ start is_inc) as l) r = let rep_size = length r * size in let act_size = length l * size in let (l',r') = (to_num sign l,to_num sign r) in let (l_u,r_u) = (to_num false l,to_num false r) in - let n = arith_op_no0 op (l',r') in - let n_u = arith_op_no0 op (l_u,r_u) in + let n = arith_op_no0 op l' r' in + let n_u = arith_op_no0 op l_u r_u in let (representable,n',n_u') = match (n, n_u) with | (Just n',Just n_u') -> @@ -380,7 +380,7 @@ let quotO_VVV = arith_op_overflow_no0_vec integerDiv false 1 let quotSO_VVV = arith_op_overflow_no0_vec integerDiv true 1 let arith_op_vec_range_no0 op sign size (V _ _ is_inc as l) r = - arith_op_vec_no0 op sign size (l,to_vec is_inc (length l,r)) + arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r)) let mod_VIV = arith_op_vec_range_no0 integerMod false 1 |