To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
This module implements diffing over lists of arbitrary content. It is parameterized by
- The content of the two lists
- The equality witness when an element is kept
- The diffing witness when an element is changed
Diffing is extended to maintain state depending on the computed changes while walking through the two lists.
The underlying algorithm is a modified Wagner-Fischer algorithm (see <https://en.wikipedia.org/wiki/Wagner%E2%80%93Fischer_algorithm>).
We provide the following guarantee: Given two lists
r, if different patches result in different states, we say that the state diverges.
- We always return the optimal patch on prefixes of
ron which state does not diverge.
- Otherwise, we return a correct but non-optimal patch where subpatches with no divergent states are optimal for the given initial state.
More precisely, the optimality of Wagner-Fischer depends on the property that the edit-distance between a k-prefix of the left input and a l-prefix of the right input d(k,l) satisfies
d(k,l) = min ( del_cost + d(k-1,l), insert_cost + d(k,l-1), change_cost + d(k-1,l-1) )
Under this hypothesis, it is optimal to choose greedily the state of the minimal patch transforming the left k-prefix into the right l-prefix as a representative of the states of all possible patches transforming the left k-prefix into the right l-prefix.
If this property is not satisfied, we can still choose greedily a representative state. However, the computed patch is no more guaranteed to be globally optimal. Nevertheless, it is still a correct patch, which is even optimal among all explored patches.
type ('left, 'right, 'eq, 'diff) change =
The type of potential changes on a list.
type ('l, 'r, 'eq, 'diff) patch = ('l, 'r, 'eq, 'diff) change list
A patch is an ordered list of changes.
val diff : weight:(('l, 'r, 'eq, 'diff) change -> int) -> test:('state -> 'l -> 'r -> ('eq, 'diff) result) -> update:(('l, 'r, 'eq, 'diff) change -> 'state -> 'state) -> 'state -> 'l array -> 'r array -> ('l, 'r, 'eq, 'diff) patch
diff ~weight ~test ~update state l r computes the diff between
r, using the initial state
test st xl xrtests if the elements
xrare compatible (
Ok) or not (
weight chreturns the weight of the change
ch. Used to find the smallest patch.
update ch streturns the new state after applying a change.
Variadic diffing allows to expand the lists being diffed during diffing.
val variadic_diff : weight:(('l, 'r, 'eq, 'diff) change -> int) -> test:('state -> 'l -> 'r -> ('eq, 'diff) result) -> update:('l, 'r, 'eq, 'diff, 'state) update -> 'state -> 'l array -> 'r array -> ('l, 'r, 'eq, 'diff) patch
variadic_diff ~weight ~test ~update state l r behaves as
diff with the following difference:
updatemust now be an
updatewhich indicates in which direction the expansion takes place.