diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 74 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 1 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 2 |
3 files changed, 38 insertions, 39 deletions
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 44ae9d7c..f10ed9f7 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -118,9 +118,9 @@ let bitwise_not (Bitvector bs start is_inc) = let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) = Bitvector (op bsl bsr) start is_inc -let bitwise_and = bitwise_binop lAnd -let bitwise_or = bitwise_binop lOr -let bitwise_xor = bitwise_binop lXor +let bitwise_and x = bitwise_binop lAnd x +let bitwise_or x = bitwise_binop lOr x +let bitwise_xor x = bitwise_binop lXor x let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs let unsigned_big = unsigned @@ -317,9 +317,9 @@ let arith_op_range_vec_range op sign l r = op l (to_num sign r) * add_range_vec_range_signed * minus_range_vec_range *) -let add_IVI = arith_op_range_vec_range integerAdd false -let addS_IVI = arith_op_range_vec_range integerAdd true -let minus_IVI = arith_op_range_vec_range integerMinus false +let add_IVI x = arith_op_range_vec_range integerAdd false x +let addS_IVI x = arith_op_range_vec_range integerAdd true x +let minus_IVI x = arith_op_range_vec_range integerMinus false x let arith_op_vec_range_range op sign l r = op (to_num sign l) r @@ -327,9 +327,9 @@ let arith_op_vec_range_range op sign l r = op (to_num sign l) r * add_vec_range_range_signed * minus_vec_range_range *) -let add_VII = arith_op_vec_range_range integerAdd false -let addS_VII = arith_op_vec_range_range integerAdd true -let minus_VII = arith_op_vec_range_range integerMinus false +let add_VII x = arith_op_vec_range_range integerAdd false x +let addS_VII x = arith_op_vec_range_range integerAdd true x +let minus_VII x = arith_op_vec_range_range integerMinus false x @@ -340,8 +340,8 @@ let arith_op_vec_vec_range op sign l r = (* add_vec_vec_range * add_vec_vec_range_signed *) -let add_VVI = arith_op_vec_vec_range integerAdd false -let addS_VVI = arith_op_vec_vec_range integerAdd true +let add_VVI x = arith_op_vec_vec_range integerAdd false x +let addS_VVI x = arith_op_vec_vec_range integerAdd true x let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r = let l' = to_num sign l in @@ -352,9 +352,9 @@ let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r = * add_vec_bit_signed * minus_vec_bit_signed *) -let add_VBV = arith_op_vec_bit integerAdd false 1 -let addS_VBV = arith_op_vec_bit integerAdd true 1 -let minus_VBV = arith_op_vec_bit integerMinus true 1 +let add_VBV x = arith_op_vec_bit integerAdd false 1 x +let addS_VBV x = arith_op_vec_bit integerAdd true 1 x +let minus_VBV x = arith_op_vec_bit integerMinus true 1 x (* TODO: these can't be done directly in Lem because of the one_more size calculation val arith_op_overflow_vec : forall 'a 'b. Size 'a, Size 'b => (integer -> integer -> integer) -> bool -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b * bitU * bool @@ -432,9 +432,9 @@ let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) = Bitvector (rotateLeft n bs) start is_inc end -let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*) -let bitwise_rightshift = shift_op_vec RR_shift (*">>"*) -let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*) +let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*) +let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*) +let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*) let shiftl = bitwise_leftshift @@ -508,37 +508,37 @@ let compare_op_vec op sign (l,r) = let (l',r') = (to_num sign l, to_num sign r) in compare_op op (l',r') -let lt_vec = compare_op_vec (<) true -let gt_vec = compare_op_vec (>) true -let lteq_vec = compare_op_vec (<=) true -let gteq_vec = compare_op_vec (>=) true +let lt_vec x = compare_op_vec (<) true x +let gt_vec x = compare_op_vec (>) true x +let lteq_vec x = compare_op_vec (<=) true x +let gteq_vec x = compare_op_vec (>=) true x -let lt_vec_signed = compare_op_vec (<) true -let gt_vec_signed = compare_op_vec (>) true -let lteq_vec_signed = compare_op_vec (<=) true -let gteq_vec_signed = compare_op_vec (>=) true -let lt_vec_unsigned = compare_op_vec (<) false -let gt_vec_unsigned = compare_op_vec (>) false -let lteq_vec_unsigned = compare_op_vec (<=) false -let gteq_vec_unsigned = compare_op_vec (>=) false +let lt_vec_signed x = compare_op_vec (<) true x +let gt_vec_signed x = compare_op_vec (>) true x +let lteq_vec_signed x = compare_op_vec (<=) true x +let gteq_vec_signed x = compare_op_vec (>=) true x +let lt_vec_unsigned x = compare_op_vec (<) false x +let gt_vec_unsigned x = compare_op_vec (>) false x +let lteq_vec_unsigned x = compare_op_vec (<=) false x +let gteq_vec_unsigned x = compare_op_vec (>=) false x let lt_svec = lt_vec_signed let compare_op_vec_range op sign (l,r) = compare_op op ((to_num sign l),r) -let lt_vec_range = compare_op_vec_range (<) true -let gt_vec_range = compare_op_vec_range (>) true -let lteq_vec_range = compare_op_vec_range (<=) true -let gteq_vec_range = compare_op_vec_range (>=) true +let lt_vec_range x = compare_op_vec_range (<) true x +let gt_vec_range x = compare_op_vec_range (>) true x +let lteq_vec_range x = compare_op_vec_range (<=) true x +let gteq_vec_range x = compare_op_vec_range (>=) true x let compare_op_range_vec op sign (l,r) = compare_op op (l, (to_num sign r)) -let lt_range_vec = compare_op_range_vec (<) true -let gt_range_vec = compare_op_range_vec (>) true -let lteq_range_vec = compare_op_range_vec (<=) true -let gteq_range_vec = compare_op_range_vec (>=) true +let lt_range_vec x = compare_op_range_vec (<) true x +let gt_range_vec x = compare_op_range_vec (>) true x +let lteq_range_vec x = compare_op_range_vec (<=) true x +let gteq_range_vec x = compare_op_range_vec (>=) true x val eq : forall 'a. Eq 'a => 'a * 'a -> bool let eq (l,r) = (l = r) diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index e2cbb98a..4d3ddbce 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -260,7 +260,6 @@ let vec_to_bvec (Vector elems start is_inc) = (*** Vector operations *) - (* Bytes and addresses *) val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a) diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 4e649144..fa6515fb 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -181,7 +181,7 @@ val barrier : forall 'regs. barrier_kind -> M 'regs unit let barrier _ = return () val footprint : forall 'regs. M 'regs unit -let footprint = return () +let footprint s = return () s val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars -> |