Fix `str.replace_re` and `str.replace_re_all` (#6615)

Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.

1 files changed, 4 insertions, 0 deletions

diff --git a/NEWS b/NEWS
index 26e0edbb6..54575dcc2 100644
--- a/NEWS
+++ b/NEWS
@@ -15,6 +15,10 @@ New Features:
   if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
 * Support for an integer operator `(_ iand n)` that returns the bitwise `and`
   of two integers, seen as integers modulo n.
+* Strings:
+  * Support for `str.indexof_re(s, r, n)`, which returns the index of the first
+    occurrence of a regular expression `r` in a string `s` after index `n` or
+    -1 if `r` does not match a substring after `n`.
 
 Improvements:
 * New API: Added functions to retrieve the heap/nil term when using separation