staload UN = "prelude/SATS/unsafe.sats" // Ported over from https://en.wikibooks.org/wiki/Algorithm_Implementation/Strings/Levenshtein_distance#C fn levenshtein {m:nat}{n:nat}(s1 : string(m), s2 : string(n)) : int = let val s1_l: size_t(m) = length(s1) val s2_l: size_t(n) = length(s2) val column: arrayref(int, m+1) = arrayref_make_elt(s1_l + 1, 0) var i: int = sz2i(s1_l) fun loop1 { i : nat | i <= m } .. (i : int(i)) : void = case+ i of | 0 => () | i =>> { val () = column[i] := i val () = loop1(i - 1) } val () = loop1(sz2i(s1_l)) val () = while* {i:nat} .. (i: int(i)) => (i > 0)(column[i] := i ; i := i - 1) val () = while(i > 0)(column[i] := i ; i := i - 1) val () = for* { i : nat | i <= m } .. (i : int(i)) => (i := sz2i(s1_l) ; i > 0 ; i := i - 1) (column[i] := i) fun loop2 { i : nat | i > 0 && i <= n+1 } .. (x : int(i)) : void = if x <= sz2i(s2_l) then { val () = column[0] := x val () = let fun inner_loop { j : nat | j > 0 && j <= m+1 } .. (y : int(j), last_diag : int) : void = if y <= sz2i(s1_l) then let var old_diag = column[y] fun min_3(x : int, y : int, z : int) : int = min(x, (min(y, z))) fun bool2int(c0 : char, c1 : char) : int = if c0 = c1 then 0 else 1 val () = column[y] := min_3( column[y] + 1 , column[y - 1] + 1 , last_diag + bool2int(s1[y - 1], s2[x - 1]) ) in inner_loop(y + 1, old_diag) end in inner_loop(1, x - 1) end val () = loop2(x + 1) } val () = loop2(1) in column[s1_l] end fn levenshtein_vt {m:nat}{n:nat}(s1 : !strnptr(m), s2 : !strnptr(n)) : int = let var p1 = strnptr2ptr(s1) var p2 = strnptr2ptr(s2) var s1 = $UN.ptr0_get(p1) var s2 = $UN.ptr0_get(p2) in levenshtein(s1, s2) end