diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index fe87c9e1..dd39373d 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -66,13 +66,16 @@ let hardware_mod (a: integer) (b:integer) : integer = then (a mod b) - b else a mod b +(* There are different possible answers for integer divide regarding +rounding behaviour on negative operands. Positive operands always +round down so derive the one we want (trucation towards zero) from +that *) let hardware_quot (a:integer) (b:integer) : integer = - if a < 0 && b < 0 - then (abs a) / (abs b) - else if (a < 0 && b > 0) - then (a/b) + 1 - else a/b - + let q = (abs a) / (abs b) in + if ((a<0) = (b<0)) then + q (* same sign -- result positive *) + else + ~q (* different sign -- result negative *) let (max_64u : integer) = integerFromNat ((natPow 2 64) - 1) let (max_64 : integer) = integerFromNat ((natPow 2 63) - 1) |