module Diffing_with_keys:sig
..end
When diffing lists where each element has a distinct key, we can refine the diffing patch by introducing two composite edit moves: swaps and moves.
Swap
s exchange the position of two elements. Swap
cost is set to
2 * change - epsilon
.
Move
s change the position of one element. Move
cost is set to
delete + addition - epsilon
.
When the cost delete + addition
is greater than change
and with those
specific weights, the optimal patch with Swap
s and Move
s can be computed
directly and cheaply from the original optimal patch.
type 'a
with_pos = {
|
pos : |
|
data : |
}
val with_pos : 'a list -> 'a with_pos list
type ('l, 'r, 'diff)
mismatch =
| |
Name of |
||||||||
| |
Type of |
type ('l, 'r, 'diff)
change =
| |
Change of |
||||||
| |
Swap of |
||||||
| |
Move of |
||||||
| |
Insert of |
||||||
| |
Delete of |
This specialized version of changes introduces two composite
changes: Move
and Swap
val prefix : Format.formatter -> ('l, 'r, 'diff) change -> unit
module Define: