From 14510c80fa9d105ab61f0ecfb96ea89f7edf6587 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 23 Apr 2018 16:04:37 +0100 Subject: start of string pattern matching: currently only literals --- src/ast_util.ml | 2 + src/initial_check.ml | 1 + src/lexer.mll | 1 + src/parse_ast.ml | 1 + src/parser.mly | 4 +- src/pattern_completeness.ml | 7 +++ src/rewriter.ml | 5 ++ src/rewriter.mli | 1 + src/rewrites.ml | 109 ++++++++++++++++++++++++++++++++++++++++++++ src/sail_lib.ml | 6 +++ src/type_check.ml | 20 ++++++++ src/value.ml | 15 ++++++ 12 files changed, 171 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/ast_util.ml b/src/ast_util.ml index 2f2d27d8..0817e46c 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -438,6 +438,7 @@ and map_pat_annot_aux f = function | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats) | P_vector pats -> P_vector (List.map (map_pat_annot f) pats) | P_cons (pat1, pat2) -> P_cons (map_pat_annot f pat1, map_pat_annot f pat2) + | P_string_append (pat1, pat2) -> P_string_append (map_pat_annot f pat1, map_pat_annot f pat2) and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot) and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot) and map_letbind_annot_aux f = function @@ -710,6 +711,7 @@ and string_of_pat (P_aux (pat, l)) = | P_vector_concat pats -> string_of_list " : " string_of_pat pats | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]" | P_as (pat, id) -> string_of_pat pat ^ " as " ^ string_of_id id + | P_string_append (pat1, pat2) -> string_of_pat pat1 ^ " ^^ " ^ string_of_pat pat2 | _ -> "PAT" and string_of_lexp (LEXP_aux (lexp, _)) = match lexp with diff --git a/src/initial_check.ml b/src/initial_check.ml index 62c1af02..a294d70a 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -468,6 +468,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_cons(pat1, pat2) -> P_cons (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) + | Parse_ast.P_string_append (pat1, pat2) -> P_string_append (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) ), (l,())) diff --git a/src/lexer.mll b/src/lexer.mll index 1fe2a849..f3d93d95 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -215,6 +215,7 @@ rule token = parse | "2" ws "^" { TwoCaret } | "^" { (Caret(r"^")) } | "::" { ColonColon(r "::") } + | "^^" { CaretCaret(r "^^") } | "~~" { TildeTilde(r "~~") } | ":" { Colon(r ":") } | "," { Comma } diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 635caa9c..f71498be 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -251,6 +251,7 @@ pat_aux = (* Pattern *) | P_tup of (pat) list (* tuple pattern *) | P_list of (pat) list (* list pattern *) | P_cons of pat * pat (* cons pattern *) + | P_string_append of pat * pat (* string append pattern, x ^^ y *) and pat = P_aux of pat_aux * l diff --git a/src/parser.mly b/src/parser.mly index d126e253..cf2d50a7 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -177,7 +177,7 @@ let rec desugar_rchain chain s e = %token String Bin Hex Real %token Amp At Caret Eq Gt Lt Plus Star EqGt Unit -%token Colon ColonColon TildeTilde ExclEq +%token Colon ColonColon CaretCaret TildeTilde ExclEq %token GtEq %token LtEq @@ -651,6 +651,8 @@ pat1: { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos } | atomic_pat ColonColon pat1 { mk_pat (P_cons ($1, $3)) $startpos $endpos } + | atomic_pat CaretCaret pat1 + { mk_pat (P_string_append ($1, $3)) $startpos $endpos } pat_concat: | atomic_pat diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml index c13452ff..3797354c 100644 --- a/src/pattern_completeness.ml +++ b/src/pattern_completeness.ml @@ -68,6 +68,7 @@ type gpat = | GP_cons of gpat * gpat | GP_app of (gpat Bindings.t) | GP_record of (gpat Bindings.t) + | GP_string_append of gpat * gpat let rec string_of_gpat = function | GP_lit lit -> string_of_lit lit @@ -80,12 +81,14 @@ let rec string_of_gpat = function | GP_app app -> Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app) | GP_record _ -> "GP RECORD" + | GP_string_append (gpat1, gpat2) -> string_of_gpat gpat1 ^ " ^^" ^ string_of_gpat gpat2 let is_wild = function | GP_wild -> true | _ -> false let rec generalize ctx (P_aux (p_aux, _) as pat) = + match p_aux with | P_lit lit -> GP_lit lit | P_wild -> GP_wild @@ -116,6 +119,10 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) = let ghd_pat = generalize ctx hd_pat in let gtl_pat = generalize ctx tl_pat in if is_wild ghd_pat && is_wild gtl_pat then GP_wild else GP_cons (ghd_pat, gtl_pat) + | P_string_append (pat1, pat2) -> + let gpat1 = generalize ctx pat1 in + let gpat2 = generalize ctx pat2 in + if is_wild gpat1 && is_wild gpat2 then GP_wild else GP_string_append (gpat1, gpat2) | P_app (f, pats) -> let gpats = List.map (generalize ctx) pats in if List.for_all is_wild gpats then diff --git a/src/rewriter.ml b/src/rewriter.ml index 203e8a58..63a1c77f 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -304,6 +304,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) = | P_tup pats -> rewrap (P_tup (List.map rewrite pats)) | P_list pats -> rewrap (P_list (List.map rewrite pats)) | P_cons (pat1, pat2) -> rewrap (P_cons (rewrite pat1, rewrite pat2)) + | P_string_append (pat1, pat2) -> rewrap (P_string_append (rewrite pat1, rewrite pat2)) let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = let rewrap e = E_aux (e,(l,annot)) in @@ -452,6 +453,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux ; p_cons : 'pat * 'pat -> 'pat_aux + ; p_string_append : 'pat * 'pat -> 'pat_aux ; p_aux : 'pat_aux * 'a annot -> 'pat ; fP_aux : 'fpat_aux * 'a annot -> 'fpat ; fP_Fpat : id * 'pat -> 'fpat_aux @@ -472,6 +474,7 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat | P_tup ps -> alg.p_tup (List.map (fold_pat alg) ps) | P_list ps -> alg.p_list (List.map (fold_pat alg) ps) | P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt) + | P_string_append (p1, p2) -> alg.p_string_append (fold_pat alg p1, fold_pat alg p2) and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat = function @@ -498,6 +501,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = ; p_tup = (fun ps -> P_tup ps) ; p_list = (fun ps -> P_list ps) ; p_cons = (fun (ph,pt) -> P_cons (ph,pt)) + ; p_string_append = (fun (p1,p2) -> P_string_append (p1,p2)) ; p_aux = (fun (pat,annot) -> P_aux (pat,annot)) ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat)) @@ -744,6 +748,7 @@ let compute_pat_alg bot join = ; p_tup = split_join (fun ps -> P_tup ps) ; p_list = split_join (fun ps -> P_list ps) ; p_cons = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt))) + ; p_string_append = (fun ((v1,p1),(v2,p2)) -> (join v1 v2, P_string_append (p1,p2))) ; p_aux = (fun ((v,pat),annot) -> (v, P_aux (pat,annot))) ; fP_aux = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot))) ; fP_Fpat = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat))) diff --git a/src/rewriter.mli b/src/rewriter.mli index f8982d69..70c894c4 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -95,6 +95,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux ; p_cons : 'pat * 'pat -> 'pat_aux + ; p_string_append : 'pat * 'pat -> 'pat_aux ; p_aux : 'pat_aux * 'a annot -> 'pat ; fP_aux : 'fpat_aux * 'a annot -> 'fpat ; fP_Fpat : id * 'pat -> 'fpat_aux diff --git a/src/rewrites.ml b/src/rewrites.ml index 591bc276..3b5a1736 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -676,6 +676,7 @@ let remove_vector_concat_pat pat = ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_cons = (fun (p,ps) -> P_cons (p false, ps false)) + ; p_string_append = (fun (p1,p2) -> P_string_append (p1 false, p2 false)) ; p_aux = (fun (pat,((l,_) as annot)) contained_in_p_as -> match pat with @@ -819,6 +820,7 @@ let remove_vector_concat_pat pat = ; p_list = (fun ps -> let (ps,decls) = List.split ps in (P_list ps,List.flatten decls)) ; p_cons = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls')) + ; p_string_append = (fun ((p1,decls1),(p2,decls2)) -> (P_string_append (p1,p2), decls1 @ decls2)) ; p_aux = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot)) ; fP_aux = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls)) ; fP_Fpat = (fun (id,(pat,decls)) -> (FP_Fpat (id,pat),decls)) @@ -1072,6 +1074,8 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) = | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats)) | P_list pats -> rewrap (E_list (List.map pat_to_exp pats)) | P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps)) + | P_string_append (p,ps) -> raise (Reporting_basic.err_unreachable l + "pat_to_exp not implemented for P_string_append") and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) = FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot)) @@ -1160,6 +1164,7 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with | P_app (_,pats) | P_tup pats | P_list pats -> List.exists contains_bitvector_pat pats | P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps +| P_string_append (p1,p2) -> contains_bitvector_pat p1 || contains_bitvector_pat p2 | P_record (fpats,_) -> List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats @@ -1188,6 +1193,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_cons = (fun (p,ps) -> P_cons (p false, ps false)) + ; p_string_append = (fun (p1,p2) -> P_string_append (p1 false, p2 false)) ; p_aux = (fun (pat,annot) contained_in_p_as -> let env = env_of_annot annot in @@ -1342,6 +1348,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = (P_list ps, flatten_guards_decls gdls)) ; p_cons = (fun ((p,gdls),(p',gdls')) -> (P_cons (p,p'), flatten_guards_decls [gdls;gdls'])) + ; p_string_append = (fun ((p1,gdls1),(p2,gdls2)) -> + (P_string_append (p1,p2), flatten_guards_decls [gdls1;gdls2])) ; p_aux = (fun ((pat,gdls),annot) -> let env = env_of_annot annot in let t = Env.base_typ_of env (typ_of_annot annot) in @@ -2801,6 +2809,103 @@ let pexp_rewriters rewrite_pexp = rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } +let stringappend_counter = ref 0 + +let rec rewrite_defs_pat_string_append = + let rec rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = + + (* utils *) + let (pat, _, _, _) = destruct_pexp pexp in + let env = pat_env_of pat in + let assert_false = mk_exp (E_assert (mk_exp (E_lit (mk_lit L_false)), mk_exp (E_lit (mk_lit (L_string "unreachable"))))) in + let construct_single_match match_on pattern maybe_expr = + let (true_exp, false_exp) = + match maybe_expr with + | Some expr -> expr, assert_false + | None -> (mk_exp (E_lit (mk_lit L_true))), (mk_exp (E_lit (mk_lit L_false))) + in + mk_exp (E_case (match_on, [mk_pexp (Pat_exp (pattern, true_exp)); + mk_pexp (Pat_exp (mk_pat P_wild, false_exp))])) + in + + (* merge cases of Pat_exp and Pat_when *) + let (P_aux (p_aux, p_annot), guards, expr) = + match pexp_aux with + | Pat_exp (pat, expr) -> (pat, [], expr) + | Pat_when (pat, guard, expr) -> (pat, [guard], expr) + in + + let (new_pat, new_guards, new_expr) = + match (p_aux, p_annot) with + (* + "lit" ^^ pat2 => expr ---> s# if startswith(s#, "lit") + && match str_drop(s#, strlen("lit")) { + pat2 => true, _ => false + } + => match str_drop(s#, strlen("lit")) { + pat2 => expr + } + *) + | P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _), pat2), p_annot -> + + (* common things *) + let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in + stringappend_counter := !stringappend_counter + 1; + let env = Env.add_local id (Immutable, string_typ) env in + + (* construct drop expression -- string_drop(s#, strlen("lit")) *) + let drop_exp = mk_exp (E_app (mk_id "string_drop", [mk_exp (E_id id); mk_exp (E_app (mk_id "string_length", [mk_exp (E_lit lit)]))])) in + + (* construct the two new guards *) + let guard1 = mk_exp (E_app (mk_id "string_startswith", [mk_exp (E_id id); mk_exp (E_lit lit)])) in + let guard2 = construct_single_match drop_exp (strip_pat pat2) None in + + (* recurse into pat2 *) + let new_pat2_pexp = mk_pexp (Pat_exp (strip_pat pat2, strip_exp expr)) in + let new_pat2_pexp = check_case env (pat_typ_of pat2) new_pat2_pexp (typ_of expr) in + let new_pat2_pexp = rewrite_pexp new_pat2_pexp in + let new_pat2_pexp = strip_pexp new_pat2_pexp in + + (* construct new match expr *) + let new_expr = mk_exp (E_case (drop_exp, [new_pat2_pexp])) in + + (* construct final result. TODO FIXME: *way* too much type-checking/stripping/rechecking *) + (mk_pat (P_id id)), guard1 :: guard2 :: (List.map strip_exp guards), new_expr + + (* + (builtin x) ^^ pat2 => expr ---> s# if match maybe_atoi s# { + Some (n#, len#) => + match string_drop(s#, len#) { + pat2 => true, _ => false + } + None => false + } + => let (x, len#) = match maybe_atoi s# { + Some (n#, len#) => (n#, len#) + } in + match string_drop(s#, len#) { + pat2 => expr + } + *) + | P_string_append (P_aux (P_lit (L_aux (L_string s, _) as lit), _), pat2), p_annot -> + assert false + | P_string_append _, _ -> + failwith ("encountered a variety of string append pattern that is not yet implemented: " ^ string_of_pat (P_aux (p_aux, p_annot))) + + | _ -> strip_pat (P_aux (p_aux, p_annot)), (List.map strip_exp guards), (strip_exp expr) + in + + (* un-merge Pat_exp and Pat_when cases *) + let new_pexp = match new_guards with + | [] -> mk_pexp (Pat_exp (new_pat, new_expr)) + | gs -> mk_pexp (Pat_when (new_pat, fold_guards gs, new_expr)) + in + check_case env string_typ new_pexp (typ_of expr) + + in + pexp_rewriters rewrite_pexp + + let rewrite_defs_pat_lits = let counter = ref 0 in let rewrite_pat guards = function @@ -3213,6 +3318,7 @@ let rewrite_defs_lem = [ ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); ("remove_numeral_pats", rewrite_defs_remove_numeral_pats); + ("pat_string_append", rewrite_defs_pat_string_append); ("guarded_pats", rewrite_defs_guarded_pats); ("bitvector_exps", rewrite_bitvector_exps); (* ("register_ref_writes", rewrite_register_ref_writes); *) @@ -3241,6 +3347,7 @@ let rewrite_defs_lem = [ let rewrite_defs_ocaml = [ (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); + ("pat_string_append", rewrite_defs_pat_string_append); ("pat_lits", rewrite_defs_pat_lits); ("tuple_vector_assignments", rewrite_tuple_vector_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -3260,6 +3367,7 @@ let rewrite_defs_ocaml = [ let rewrite_defs_c = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); + ("pat_string_append", rewrite_defs_pat_string_append); ("pat_lits", rewrite_defs_pat_lits); ("tuple_vector_assignments", rewrite_tuple_vector_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -3277,6 +3385,7 @@ let rewrite_defs_c = [ let rewrite_defs_interpreter = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); + ("pat_string_append", rewrite_defs_pat_string_append); ("tuple_vector_assignments", rewrite_tuple_vector_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 47acae88..34d34993 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -461,6 +461,12 @@ let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 let eq_string (str1, str2) = String.compare str1 str2 == 0 +let string_startswith (str1, str2) = String.compare (String.sub str1 0 (String.length str2)) str2 == 0 + +let string_drop (str, n) = let n = Big_int.to_int n in String.sub str n (String.length str - n) + +let string_length str = String.length str + let lt_int (x, y) = Big_int.less x y let set_slice (out_len, slice_len, out, n, slice) = diff --git a/src/type_check.ml b/src/type_check.ml index 63fab70e..523802cc 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2471,6 +2471,16 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) annot_pat (P_cons (hd_pat, tl_pat)) typ, env, hd_guards @ tl_guards | _ -> typ_error l "Cannot match cons pattern against non-list type" end + | P_string_append (pat1, pat2) -> + begin + let matcher = Env.expand_synonyms env typ in + match matcher with + | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 -> + let pat1, env, guards1 = bind_pat env pat1 typ in + let pat2, env, guards2 = bind_pat env pat2 typ in + annot_pat (P_string_append (pat1, pat2)) typ, env, guards1 @ guards2 + | _ -> typ_error l "Cannot match string-append pattern against non-string type" + end | P_list pats -> begin match Env.expand_synonyms env typ with @@ -2600,6 +2610,12 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env, guards + | P_string_append (pat1, pat2) -> + let typed_pat1, env, guards1 = infer_pat env pat1 in + let typed_pat2, env, guards2 = infer_pat env pat2 in + typ_equality l env (pat_typ_of typed_pat1) (string_typ); + typ_equality l env (pat_typ_of typed_pat2) (string_typ); + annot_pat (P_string_append (typed_pat1, typed_pat2)) string_typ, env, guards1 @ guards2 | P_as (pat, id) -> let (typed_pat, env, guards) = infer_pat env pat in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), @@ -3415,6 +3431,10 @@ and propagate_pat_effect_aux = function let p_pat1 = propagate_pat_effect pat1 in let p_pat2 = propagate_pat_effect pat2 in P_cons (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2) + | P_string_append (pat1, pat2) -> + let p_pat1 = propagate_pat_effect pat1 in + let p_pat2 = propagate_pat_effect pat2 in + P_string_append (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2) | P_as (pat, id) -> let p_pat = propagate_pat_effect pat in P_as (p_pat, id), effect_of_pat p_pat diff --git a/src/value.ml b/src/value.ml index 4b4f0865..4848721d 100644 --- a/src/value.ml +++ b/src/value.ml @@ -183,6 +183,18 @@ 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 |> Big_int.of_int) + | _ -> failwith "value string_length" + let value_length = function | [v] -> V_int (coerce_gv v |> List.length |> Big_int.of_int) | _ -> failwith "value length" @@ -417,6 +429,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_anything", value_eq_anything); ("length", value_length); ("subrange", value_subrange); -- cgit v1.2.3