diff options
Diffstat (limited to 'src/value.ml')
| -rw-r--r-- | src/value.ml | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml index 7972c692..8ee219b7 100644 --- a/src/value.ml +++ b/src/value.ml @@ -188,6 +188,17 @@ let value_eq_string = function | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2)) | _ -> failwith "value eq_string" +let value_string_startswith = function + | [v1; v2] -> V_bool (Sail_lib.string_startswith (coerce_string v1, coerce_string v2)) + | _ -> failwith "value string_startswith" + +let value_string_drop = function + | [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2)) + | _ -> failwith "value string_drop" + +let value_string_length = function + | [v] -> V_int (coerce_string v |> Sail_lib.string_length) + | _ -> failwith "value string_length" let value_eq_bit = function | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2)) | _ -> failwith "value eq_bit" @@ -500,6 +511,9 @@ let primops = ("eq_list", value_eq_list); ("eq_bool", value_eq_bool); ("eq_string", value_eq_string); + ("string_startswith", value_string_startswith); + ("string_drop", value_string_drop); + ("string_length", value_string_length); ("eq_bit", value_eq_bit); ("eq_anything", value_eq_anything); ("length", value_length); |