
  0 | module Libraries.Text.Distance.Levenshtein
  1 | 
  2 | import Data.String
  3 | import Libraries.Data.IOMatrix
  4 | 
  5 | %default total
  6 | 
  7 | ||| Self-evidently correct but O(3 ^ (min mn)) complexity
  8 | spec : String -> String -> Nat
  9 | spec a b = loop (fastUnpack a) (fastUnpack b) where
 10 | 
 11 |   loop : List Char -> List Char -> Nat
 12 |   loop [] ys = length ys -- deletions
 13 |   loop xs [] = length xs -- insertions
 14 |   loop (x :: xs) (y :: ys)
 15 |     = if x == y then loop xs ys -- match
 16 |       else 1 + minimum
 17 |            [ loop (x :: xs) ys -- insert y
 18 |            , loop xs (y :: ys) -- delete x
 19 |            , loop xs ys        -- substitute y for x
 20 |            ]
 21 | 
 22 | ||| Dynamic programming
 23 | export
 24 | compute : HasIO io => String -> String -> io Nat
 25 | compute a b = do
 26 |   let w = strLength a
 27 |   let h = strLength b
 28 |   -- In mat[i][j], we store the distance between
 29 |   -- * the suffix of a of size i
 30 |   -- * the suffix of b of size j
 31 |   -- So we need a matrix of size (|a|+1) * (|b|+1)
 32 |   mat <- new (w+1) (h+1)
 33 |   -- Whenever one of the two suffixes of interest is empty, the only
 34 |   -- winning move is to:
 35 |   -- * delete all of the first
 36 |   -- * insert all of the second
 37 |   -- i.e. the cost is the length of the non-zero suffix
 38 |   for_ [0..w] $ \ i => write mat i 0 i -- deletions
 39 |   for_ [0..h] $ \ j => write mat 0 j j -- insertions
 40 | 
 41 |   -- We introduce a specialised `read` for ease of use
 42 |   let get = \i, j => case !(read {io} mat i j) of
 43 |         Nothing => assert_total $
 44 |           idris_crash "INTERNAL ERROR: compute -> Badly initialised matrix"
 45 |         Just n => pure n
 46 | 
 47 |   -- We fill the matrix from the bottom up, using the same formula we used
 48 |   -- in the specification's `loop`.
 49 |   for_ [1..h] $ \ j => do
 50 |     for_ [1..w] $ \ i => do
 51 |       -- here we change Levenshtein slightly so that we may only substitute
 52 |       -- alpha / numerical characters for similar ones. This avoids suggesting
 53 |       -- "#" as a replacement for an out of scope "n".
 54 |       let cost = let c = assert_total $ strIndex a (i-1)
 55 |                      d = assert_total $ strIndex b (j-1)
 56 |                  in if c == d then 0 else
 57 |                     if isAlpha c && isAlpha d then 1 else
 58 |                     if isDigit c && isDigit d then 1 else 2
 59 |       write mat i j $ minimum
 60 |         [ 1    + !(get i (j-1))     -- insert y
 61 |         , 1    + !(get (i-1) j)     -- delete x
 62 |         , cost + !(get (i-1) (j-1)) -- equal or substitute y for x
 63 |         ]
 64 | 
 65 |   -- Once the matrix is fully filled, we can simply read the top right corner
 66 |   integerToNat . cast <$> get w h
 67 |