search

tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

Add SequencesExt!Replace(First|All)SubSeq operators #52

Closed lemmy closed 3 years ago

lemmy commented 3 years ago

Question: Do we want ReplaceFirstSubSeq(<<1>>, <<>>, <<>>) to equal <<>> or <<1>>? The latter would be in line with e.g. Java's String#replaceFirst, and, thus, what users expect.

Note: Not using DOMAIN in the definition of the ops to support strings. Module override will be added later.

(Inspired by a private patch shared by @afonsonf with me)

Partially related: https://github.com/tlaplus/CommunityModules/issues/40

lemmy commented 3 years ago

@muenchnerkindl Can you please review the (non-recursive) ReplaceAllSubSeqs in https://github.com/tlaplus/CommunityModules/pull/52/commits/0f53203e8a52d46097979140e1885c30684f1ec4 ?

lemmy commented 3 years ago

Thanks for the reviews!

By the way, I learned that Java and Dotnet handle the empty sequence differently in their replace* methods.