diff options
| author | Kathy Gray | 2014-11-25 13:10:50 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-11-25 13:10:50 +0000 |
| commit | fb9bb05ae50ab3c7191ef5ba27e033fd6b97958e (patch) | |
| tree | 01b443c2467db4b746f058c58f2b11500caeed31 /src | |
| parent | b9f0f707fa86b258ae34ae9d4e4eba0837bc6534 (diff) | |
refine quot and mod
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 8115f3d6..3589c84f 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -12,11 +12,16 @@ declare ocaml target_rep function quomod = `Big_int.quomod_big_int` let hardware_mod a b = let (q,r) = quomod a b in - if q < 0 then r-b else r + if q < 0 then r-b + else + if a > b && a < 0 + then a else r let hardware_quot a b = let (q,r) = quomod a b in - if q < 0 then q+1 else q + if q < 0 then q+1 + else if a > b && a < 0 + then 0 else q let ignore_sail x = V_lit (L_aux L_unit Unknown) ;; |