代码之家 › 专栏 › 技术社区 › Keith Pinson sumit vedi

IDRIS中的字符串替换函数

idris replace string

Keith Pinson sumit vedi · 技术社区 · 6 年前

在idris中,字符串是基元,而不是像haskell中那样的列表。因此,我希望有某种原始的 replace : (needle : String) -> (replacement : String) -> (haystack : String) -> String 函数A Data.Text.replace . 我找不到这个。但我想,也许我能找到一些 replace : Eq a => (needle : List a) -> (replacement : List a) -> (haystack : List a) -> List a 函数A Data.List.Utils.replace ,因为IDRIS确实提供 unpack : String -> List Char 和 pack : Foldable t => t Char -> String . 但是,我一直找不到 replace 对于IDRIS中定义的列表,也可以。我已经搜索了文档和 GitHub repo 为了一些事情 :browse 在回复中,但都没有运气。当然,好的老伊德里斯 代替 函数用于处理类型,而不是字符串…(这在某种程度上让我很高兴,但并不能解决我的问题)。

最后,我预告了 data.list.utils.replace替换 从哈斯克尔那边过来,但我想知道它的性能,更糟糕的是,它不是完全的。另外,对于我通常认为的原始操作(假定字符串是原始操作),它需要大量的代码。

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

我要重新塑造这个,直到我得到它的总数,因为我看不出任何理由不能使它成为总数,但同时,我错过了什么?人们真的在idris中做了这么小的字符串操作以至于根本无法使用吗?我想至少在 contrib . 如何在IDRIS中进行字符串替换?

1 回复 | 直到 6 年前

Keith Pinson sumit vedi 6 年前

对于以后发现这一点并希望实现的任何人来说,我在这一点上的经验如下:

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

我可能会尝试提交一个公关回来,让这包括在IDRIS的基础库。警告 :我没有对它进行性能测试,甚至根本没有对它进行严格的测试;我已经对大约十几个案例进行了测试,看起来是正确的。如果你只分析算法,你会发现它没有你希望的那么有效。到目前为止,我还没有成功地在维护总体性的同时实现更高效的版本。