diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 13 | ||||
| -rw-r--r-- | src/type_internal.ml | 2 |
2 files changed, 14 insertions, 1 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index e83f409f..a7cf265f 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -70,6 +70,17 @@ let arith_op_vec op (V_tuple args) = match args with let (l1',l2') = (to_num true l1,to_num true l2) in arith_op op (V_tuple [l1';l2']) end ;; +let arith_op_range_vec op (V_tuple args) = match args with + | [l1; (V_vector _ _ _ as l2)] -> + let l2 = (to_num true l2) in + arith_op op (V_tuple [l1;l2]) +end ;; +let arith_op_vec_range op (V_tuple args) = match args with + | [(V_vector _ _ _ as l1);l2] -> + let l1 = (to_num true l1) in + arith_op op (V_tuple [l1;l2]) +end ;; + let compare_op op (V_tuple args) = match args with | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> if (op x y) @@ -94,6 +105,8 @@ let function_map = [ ("ignore", ignore_sail); ("add", arith_op (+)); ("add_vec", arith_op_vec (+)); + ("add_vec_range", arith_op_vec_range (+)); + ("add_range_vec", arith_op_range_vec (+)); ("minus", arith_op (-)); ("minus_vec", arith_op_vec (-)); ("eq", eq); diff --git a/src/type_internal.ml b/src/type_internal.ml index 2bb566dd..827c5525 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -548,7 +548,7 @@ let initial_typ_env = Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) - (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), + (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m")})))), External (Some "add_vec_range"), [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m")})],pure_e); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), |