stringreplaceidris

String replace function in Idris

In Idris, strings are primitives, not lists like they are in Haskell. Thus, I would expect there to be some sort of primitive replace : (needle : String) -> (replacement : String) -> (haystack : String) -> String function a la Data.Text.replace. I have not been able to find this. But I thought, perhaps I will be able to find some replace : Eq a => (needle : List a) -> (replacement : List a) -> (haystack : List a) -> List a function a la Data.List.Utils.replace, since Idris does provide unpack : String -> List Char and pack : Foldable t => t Char -> String. However, I have not been able to find replace for Lists defined in Idris, either. I have searched the documentation and the GitHub repo for several things and poked around with :browse in the REPL, but all to no luck. Of course, good old Idris' replace function is for working on types, not strings... (this makes me very happy at one level but does not solve my problem).

Finally, I have ported Data.List.Utils.replace over from Haskell, but I wonder about its performance, and much worse, it is not total. Also, it takes a surprisingly large amount of code for what I normally would think of as a primitive operation (given that strings are primitives).

    spanList : (List a -> Bool) -> List a -> (List a, List a)
    spanList _ [] = ([],[])
    spanList func list@(x::xs) =
      if func list
      then
        let (ys,zs) = spanList func xs
        in (x::ys,zs)
      else ([],list)

    breakList : (List a -> Bool) -> List a -> (List a, List a)
    breakList func = spanList (not . func)

    partial
    split : Eq a => List a -> List a -> List (List a)
    split _ [] = []
    split delim str =
      let (firstline, remainder) = breakList (isPrefixOf delim) str in
      firstline :: case remainder of
                        [] => []
                        x => if x == delim
                             then [] :: []
                             else split delim (drop (length delim) x)

    partial
    strReplace : String -> String -> String -> String
    strReplace needle replacement =
      pack . intercalate (unpack replacement) . split (unpack needle) . unpack

I am going to reshape this until I get it total because I see no reason why it couldn't be made total, but in the meantime, what am I missing? Do people really do so little string manipulation in Idris that this is not available at all? I would assume that there would at least be something in contrib. How do you do string replacement in Idris?

Solution

  • For anyone who finds this later, wanting an implementation, here is what I have at this point:

    module ListExt

%default total
%access public export

splitOnL' : Eq a => (delim : List a)    -> {auto dprf : NonEmpty delim   }
                 -> (matching : List a) -> {auto mprf : NonEmpty matching}
                 -> List a -> (List a, List (List a))
splitOnL' _ _ [] = ([], [])
splitOnL' delim m@(_::m') list@(x::xs) =
  if isPrefixOf m list
  then
    case m' of
      [] => ([], uncurry (::) $ splitOnL' delim delim xs)
      (m_ :: ms) => splitOnL' delim (m_ :: ms) xs
  else
    let (l, ls) = splitOnL' delim delim xs in
    (x :: l, ls)

splitOnL : Eq a => (delim : List a) -> {auto dprf : NonEmpty delim}
                -> List a -> List (List a)
splitOnL delim [] = []
splitOnL delim list@(_::_) = uncurry (::) $ splitOnL' delim delim list

substitute : Eq a => List a -> List a -> List a -> List a
substitute [] replacement = id
substitute (n :: ns) replacement = intercalate replacement . splitOnL (n :: ns)

strReplace : String -> String -> String -> String
strReplace needle replacement = pack . substitute (unpack needle) (unpack replacement) . unpack

    I may try to submit a PR back to get this included in Idris' base libraries. Warning: I have not performance tested this, or even tested it rigorously at all; I have run it on about a dozen cases, and it seem right. If you just analyze the algorithm you will see it is not as efficient as you could wish. I have not succeeded at getting a more efficient version implemented while maintaining totality thus far.