diff options
| author | Kathy Gray | 2016-02-05 13:13:18 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-02-05 13:13:42 +0000 |
| commit | e148fa2ae5686c13d319d960c798cc542066be8c (patch) | |
| tree | f7b1c931b4aa72a6bd501b7584d27d9229a0c3ee /src | |
| parent | a9c9ebaf06ea86af4f8540ff27b6b645138fb150 (diff) | |
change signed mod behaviour for numbers to match that of vectors
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 1 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index d494ab12..c16b6c3d 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -686,6 +686,7 @@ let library_functions direction = [ ("bitwise_rightshift", shift_op_vec ">>"); ("bitwise_rotate", shift_op_vec "<<<"); ("modulo", arith_op_no0 (mod)); + ("mod_signed", arith_op_no0 hardwaer_mod); ("mod_vec", arith_op_vec_no0 hardware_mod "mod" Unsigned 1); ("mod_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Unsigned 1); ("mod_signed_vec", arith_op_vec_no0 hardware_mod "mod" Signed 1); diff --git a/src/type_internal.ml b/src/type_internal.ml index 7ef085b9..81a8e681 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1967,12 +1967,12 @@ let initial_typ_env = Overload( Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), - (External (Some "modulo")),[],pure_e,pure_e,nob), + (External (Some "mod_signed")),[],pure_e,pure_e,nob), true, [Base(((mk_nat_params["n";"o";]), (mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ; mk_atom (mk_nv "o")]) (mk_range n_zero (mk_sub (mk_nv "o") n_one)))), - (External (Some "modulo")), + (External (Some "mod_signed")), [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob); Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); |