Missing string services.

[Mallku2]

We need to provide semantics for the following string services, which are needed for our "Rare as Eunoia" benchmarks:

• str.indexof_re
• str.to_upper
• str.to_lower
• re.+
• re.^
• re.loop

Is somebody already working on them?

[jjakpor]

Hi Mallku, yes, I think we have semantics ready for all of these except for str.indexof_re, and str.indexof_re is a work in progress. I will push the operators I have already added soon.

[jjakpor]

re.^, re.+, and re.loop are already provided by the Lotz et al. formalization in string_library under the names re_pow, re_plus, and re_loop. I just pushed formalizations of str.to_upper and str.to_lower in string_library/Strings.thy. I'm still working on str.indexof_re though.

[Mallku2]

Many thanks, Jibiana! I see that re_pow, re_plus, and re_loop are mentioned in the src/string_parser.ML file, but still require some fixes for them to properly work. I will open a PR dealing with that. Also, thanks for the formalizations of str.to_upper and str.to_lower. And no hurries at all with str.indexof_re, I see that we have just a couple of cases that use it, so it is not that important right now.