package ocaml-base-compiler

  1. Overview
  2. Docs

Parametric diffing

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 <>).

We provide the following guarantee: Given two lists l and r, if different patches result in different states, we say that the state diverges.

  • We always return the optimal patch on prefixes of l and r on 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.

module type Defs = sig ... end

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

val prefix : Format.formatter -> (int * change_kind) -> unit
val style : change_kind -> list
type ('left, 'right, 'eq, 'diff) change =
  1. | Delete of 'left
  2. | Insert of 'right
  3. | Keep of 'left * 'right * 'eq
  4. | Change of 'left * 'right * 'diff
val classify : (_, _, _, _) change -> change_kind
module Define (D : Defs) : sig ... end

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


Innovation. Community. Security.