should we redefine `String.splitOnAux`?

Stream: lean4

[Bulhwi Cha]

I think there are redundant parts of the definitions of String.splitOnAux and String.splitOn. See my commit. The redefined splitOnAux is not equal to the previous one, but this is what I intended. I guess the new splitOn equals the old one.

Redefined functions

namespace String

def splitOnAux' (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
  if h : s.atEnd i then
    let r := (s.extract b i)::r
    r.reverse
  else
    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
    if s.get i == sep.get j then
      let i := s.next i
      let j := sep.next j
      if sep.atEnd j then
        splitOnAux' s sep i i 0 (s.extract b (i - j)::r)
      else
        splitOnAux' s sep b i j r
    else
      splitOnAux' s sep b (s.next i) 0 r
termination_by _ => s.endPos.1 - i.1

def splitOn' (s : String) (sep : String := " ") : List String :=
  splitOnAux' s sep 0 0 0 []

end String

def chabulhwi := "차_!_불_!_휘_!_"

#eval chabulhwi.splitOn "_!_" -- output: ["차", "불", "휘", ""]
#eval chabulhwi.splitOnAux "_!_" ⟨18⟩ ⟨18⟩ ⟨0⟩ ["휘", "불", "차"] -- ["차", "불", "휘", ""]
#eval chabulhwi.splitOnAux "_!_" ⟨18⟩ ⟨18⟩ ⟨3⟩ ["휘", "불", "차"] -- ["차", "불", "휘", "", ""]

#eval chabulhwi.splitOn' "_!_" -- ["차", "불", "휘", ""]
#eval chabulhwi.splitOnAux' "_!_" ⟨18⟩ ⟨18⟩ ⟨0⟩ ["휘", "불", "차"] -- ["차", "불", "휘", ""]
#eval chabulhwi.splitOnAux' "_!_" ⟨18⟩ ⟨18⟩ ⟨3⟩ ["휘", "불", "차"] -- ["차", "불", "휘", ""]

[Mauricio Collares]

Did you try testing chabulhwi.splitOn ""?

[Mauricio Collares]

I think the other change looks correct, though, because assuming sep is not empty one can prove that sep.atEnd j is always false at the start of the function.

[Bulhwi Cha]

Mauricio Collares said:

Did you try testing chabulhwi.splitOn ""?

#eval chabulhwi.splitOn  "" -- ["차_!_불_!_휘_!_"]
#eval chabulhwi.splitOn' "" -- ["차_!_불_!_휘_!_", ""]

Oh. Then I suggest redefining only splitOnAux, not splitOn.

[Mauricio Collares]

That being said, the original function looks a bit buggy. Does "ababcab".splitOn "abc" work there? It does look like it is missing some partial match handling (KMP-style or otherwise).

[Bulhwi Cha]

I don't think it works.

#eval "ababcab".splitOn "abc" -- ["ababcab"]

[Mauricio Collares]

I probably shouldn't have used the word "buggy". Proper handling of this case would either increase memory costs or time costs, which might be undesirable depending on how the function is used. But that output is not what I expect from the function name.

[Bulhwi Cha]

GitHub PR: lean4#2271

[Bulhwi Cha]

Bulhwi Cha said:

#eval chabulhwi.splitOn  "" -- ["차_!_불_!_휘_!_"]
#eval chabulhwi.splitOn' "" -- ["차_!_불_!_휘_!_", ""]

Oh. Then I suggest redefining only splitOnAux, not splitOn.

There was a mistake: I used the old functions in the body of the redefined ones. The correct results are the following:

#eval chabulhwi.splitOn  "" -- ["차_!_불_!_휘_!_"]
#eval chabulhwi.splitOn' "" -- ["차_!_불_!_휘_!_"]