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