![]() |
![]()
| ![]() |
![]()
NAMEDiffing_with_keys - 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. ModuleModule Diffing_with_keys DocumentationModule Diffing_with_keys
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 = {
val with_pos : 'a list -> 'a with_pos list type ('l, 'r, 'diff) mismatch =
type ('l, 'r, 'diff) change =
This specialized version of changes introduces two composite changes: Move and Swap val prefix : Format.formatter -> ('l, 'r, 'diff) change -> unit module Define : functor (D : sig end) -> sig end
|