1

我正在研究 Idris 中的快速搜索字符串搜索算法的一个版本，并提出了这个：

quickSearch : (needle       : String) ->
              (haystack     : String) ->
              {auto lengths : (length needle) `LTE` (length haystack)} ->
              Maybe Nat
quickSearch needle haystack = let n = length needle in
                              let h = length haystack in
                                  go (makeBadShift needle) n (h - n)
  where
    go : (badShift : CharShift) ->
         (n        : Nat) ->
         (last     : Nat) ->
         Maybe Nat
    go badShift n last = go' 0
      where
        go' : Nat -> Maybe Nat
        go' i = if i > last then Nothing
                else if (substr i n haystack) == needle then Just i
                else if i == last then Nothing
                else let ch = strIndex haystack (cast (n + i)) in
                     let shift = lookupChar badShift ch in
                         go' (i + shift)

（lookupChar 和 makeBadShift 在别处。）

这很好用，但我想让它更正式地正确。首先，由于使用了 strIndex，它并不完全。创建 strIndex 的总版本并不难（通过 List Char 或这个:)

strIndex' : (str : String) ->
            (n : Nat) ->
            {auto ok : (n `LT` (Strings.length str))} ->
            Char
strIndex' str n = assert_total $ prim__strIndex str (cast n)

但是我必须有一种方法来证明 (n + i) 小于 h。（是的，因为那时 i < h - n。）

如果我直接将“>”和“==”替换为它们的表亲，我最终会看到否定：

iNEQlast : (i = last) -> Void

和

iNGTlast : (S last) `LTE` i -> Void

这让我很难过。

另一方面，我可以颠倒条件，最终得到

"quicksearch.idr" 115L, 4588C written
  needle : String
  haystack : String
  lengths : LTE (fromIntegerNat (prim__zextInt_BigInt (prim_lenString needle))) (fromIntegerNat (prim__zextInt_BigInt (prim_lenString haystack)))
  badShift : CharShift
  n : Nat
  h : Nat
  nh : LTE n h
  i : Nat
  iLTlast : LTE (S i) (minus h n)
  iLTElast : LTE i (minus h n)
--------------------------------------
go'_rhs_1 : Maybe Nat

但在这一点上，我完全糊涂了，不知道如何前进。

现在最好的事情是什么？

4

0 回答 0