diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 15 | ||||
| -rw-r--r-- | src/type_internal.ml | 6 |
2 files changed, 20 insertions, 1 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 141dd6f4..f7b29a33 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -846,8 +846,21 @@ let mask direction v = | _ -> fail () end +let s_append v = + let fail () = Assert_extra.failwith ("append given unexpected " ^ (string_of_value v)) in + match v with + | (V_tuple [l1;l2]) -> + retaint v (match (detaint l1,detaint l2) with + | (V_list vs1, V_list vs2) -> V_list (vs1++vs2) + | (V_unknown, _) -> V_unknown + | (_,V_unknown) -> V_unknown + | _ -> fail () end) + | _ -> fail () +end + let library_functions direction = [ - ("ignore", ignore_sail); + ("ignore", ignore_sail); + ("append", s_append); ("length", v_length); ("add", arith_op (+)); ("add_vec", arith_op_vec (+) Unsigned 1); diff --git a/src/type_internal.ml b/src/type_internal.ml index 4f232ca6..285c1ad6 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1959,6 +1959,12 @@ let initial_typ_env = Constructor 2,[],pure_e,pure_e,nob)); ("None", Base((["a", {k=K_Typ}], mk_pure_fun unit_t {t=Tapp("option", [TA_typ {t=Tvar "a"}])}), Constructor 2,[],pure_e,pure_e,nob)); + ("append", + lib_tannot + (["a",{k=K_Typ}], mk_pure_fun (mk_tup [{t=Tapp("list", [TA_typ {t=Tvar "a"}])}; + {t=Tapp("list", [TA_typ {t=Tvar "a"}])}]) + {t=Tapp("list",[TA_typ {t=Tvar "a"}])}) + None []); ("most_significant", lib_tannot ((mk_nat_params ["n";"m"]@(mk_ord_params ["ord"])), (mk_pure_fun (mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")) bit_t)) None []); |