Diffing − Parametric diffing
Module Diffing
Module
Diffing
: sig end
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 <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.
−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 =
| Deletion
| Insertion
| Modification
| 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 -> Misc.Color.style list
type
(’left, ’right, ’eq, ’diff)
change =
| Delete of ’left
| Insert of ’right
| Keep of ’left * ’right * ’eq
| Change of ’left * ’right *
’diff
val classify : (’a, ’b, ’c, ’d) change -> change_kind
module Define : functor (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