Idris String Replace (Total)

module Main

total
strReplace : String -> String -> String -> String
strReplace needle replacement = go "" Z (unpack needle) . unpack

where
  go : String -> Nat -> List Char -> List Char -> String
  go acc _ [] text = acc ++ pack text
  go acc _ _ [] = acc
  go acc (S k) needle (x::xs) = go acc k needle xs
  go acc _ (n::ns) (x::xs) =
    if isPrefixOf (n::ns) (x::xs)
    then go (acc ++ replacement) (length ns) (n::ns) xs
    else go (acc ++ cast x) Z (n::ns) xs

main : IO ()
main = putStrLn $ strReplace "foo" "bar" "foo"