diff options
| author | Kathy Gray | 2016-02-04 13:11:41 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-02-04 13:11:41 +0000 |
| commit | 18df38a268b17d9a9b9b284efd8065951a702040 (patch) | |
| tree | fbf1715261589ab359db2fd5955d7ed71e1e1f29 | |
| parent | 6a6ac097204ca9c7dffe6bd8bda2f970fac7876b (diff) | |
Add mod_s
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 22 |
2 files changed, 24 insertions, 0 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 03c59edf..d494ab12 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -688,6 +688,8 @@ let library_functions direction = [ ("modulo", arith_op_no0 (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); + ("mod_signed_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Signed 1); ("quot", arith_op_no0 hardware_quot); ("quot_signed", arith_op_no0 hardware_quot); ("quot_vec", arith_op_vec_no0 hardware_quot "quot" Unsigned 1); diff --git a/src/type_internal.ml b/src/type_internal.ml index 95c9c245..7ef085b9 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1963,6 +1963,28 @@ let initial_typ_env = mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "mod_vec")),[],pure_e,pure_e,nob)])); + ("mod_s", + 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), + 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")), + [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"); + mk_range n_one (mk_nv "o")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (External (Some "mod_signed_vec_range")), + [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,pure_e,nob); + Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m"); + mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) + (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), + (External (Some "mod_signed_vec")),[],pure_e,pure_e,nob)])); ("quot", Overload( Base(((mk_typ_params ["a";"b";"c"]), |