diff options
| author | Kathy Gray | 2014-05-01 11:25:43 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-05-01 11:25:43 +0100 |
| commit | dc13a04f0209df5281454464fda359e5b0f72f98 (patch) | |
| tree | 8fe1508dfc8ec1b1c7731e5953189de63614822d /src | |
| parent | 803426ca4b53021960d921e8f6d863c5cadfc8ea (diff) | |
Make an overloading type decision (all + operations return ranges, never vectors) and make the test suite pass again
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"]), |