diff options
| author | Gabriel Kerneis | 2014-06-19 14:32:47 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-06-19 14:32:47 +0100 |
| commit | f4d86db24045315c87cbe3509485e3524b725a7c (patch) | |
| tree | 0436eb2929655e76bd4d1544f2e10b5fd2192a74 | |
| parent | c08b5c8dbf4b9ad95369c0d21ad6ae6b3729a446 (diff) | |
Add mod:vec->range->vec
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 1 | ||||
| -rw-r--r-- | src/type_internal.ml | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index ac63aebf..a95f4c01 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -151,6 +151,7 @@ let function_map = [ ("minus_vec", arith_op_vec (-)); ("mod", arith_op (mod)); ("mod_vec", arith_op_vec (mod)); + ("mod_vec_range", arith_op_vec_range (mod)); ("eq", eq); ("eq_vec_range", eq_vec_range); ("eq_range_vec", eq_range_vec); diff --git a/src/type_internal.ml b/src/type_internal.ml index d45ce9ae..72f0b3f7 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -896,6 +896,13 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") {nexp = Nconst zero}]) (mk_range {nexp = Nconst zero} (mk_sub (mk_nv "o") {nexp = Nconst one})))), External (Some "mod"),[GtEq(Specc(Parse_ast.Int("mod",None)),(mk_nv "o"),{nexp = Nconst one})],pure_e); + Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); + mk_range (mk_nv "o") {nexp = Nconst zero}]) + (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), + External (Some "mod_vec_range"), + [GtEq(Specc(Parse_ast.Int("mod",None)),(mk_nv "o"),{nexp = Nconst one}); + LtEq(Specc(Parse_ast.Int("mod",None)),(mk_nv "o"),{nexp = N2n (mk_nv "m", None)})],pure_e); Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")]) |