Module Parsing0.Diffing

Parametric diffing

This module implements diffing over lists of arbitrary content. It is parameterized by

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 l and r, if different patches result in different states, we say that the state diverges.

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.

module type Defs = { ... };

The core types of a diffing implementation

type change_kind =
  1. | Deletion
  2. | Insertion
  3. | Modification
  4. | Preservation
;

The kind of changes which is used to share printing and styling across implementation

let prefix: Format.formatter => (int, change_kind) => unit;
let style: change_kind => list(Misc.Color.style);
type change('left, 'right, 'eq, 'diff) =
  1. | Delete('left)
  2. | Insert('right)
  3. | Keep('left, 'right, 'eq)
  4. | Change('left, 'right, 'diff)
;
let classify: change(_, _, _, _) => change_kind;
module Define: (D: Defs) => { ... };

Define(Defs) creates the diffing types from the types defined in Defs and the functors that need to be instantatied with the diffing algorithm parameters