Diffing(3o) OCaml library Diffing(3o)
NAME
Diffing - Parametric diffing
Module
Module Diffing
Documentation
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 dif-
ferent patches result in different states, we say that the state di-
verges.
-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 prop-
erty 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-pre-
fix as a representative of the states of all possible patches trans-
forming the left k-prefix into the right l-prefix.
If this property is not satisfied, we can still choose greedily a rep-
resentative 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.
type ('left, 'right, 'eq, 'diff) change =
| Delete of 'left
| Insert of 'right
| Keep of 'left * 'right * 'eq
| Change of 'left * 'right * 'diff
The type of potential changes on a list.
val map : ('l1 -> 'l2) -> ('r1 -> 'r2) -> ('l1, 'r1, 'eq, 'diff) change
-> ('l2, 'r2, 'eq, 'diff) change
type ('l, 'r, 'eq, 'diff) patch = ('l, 'r, 'eq, 'diff) change list
A patch is an ordered list of changes.
val diff : weight:(('l, 'r, 'eq, 'diff) change -> int) -> test:('state
-> 'l -> 'r -> ('eq, 'diff) result) -> update:(('l, 'r, 'eq, 'diff)
change -> 'state -> 'state) -> 'state -> 'l array -> 'r array -> ('l,
'r, 'eq, 'diff) patch
diff ~weight ~test ~update state l r computes the diff between l and r
, using the initial state state .
- test st xl xr tests if the elements xl and xr are compatible ( Ok )
or not ( Error ).
- weight ch returns the weight of the change ch . Used to find the
smallest patch.
- update ch st returns the new state after applying a change.
Variadic diffing
Variadic diffing allows to expand the lists being diffed during diff-
ing.
type ('l, 'r, 'e, 'd, 'state) update =
| Without_extensions of (('l, 'r, 'e, 'd) change -> 'state -> 'state)
| With_left_extensions of (('l, 'r, 'e, 'd) change -> 'state -> 'state
* 'l array)
| With_right_extensions of (('l, 'r, 'e, 'd) change -> 'state ->
'state * 'r array)
val variadic_diff : weight:(('l, 'r, 'eq, 'diff) change -> int) ->
test:('state -> 'l -> 'r -> ('eq, 'diff) result) -> update:('l, 'r,
'eq, 'diff, 'state) update -> 'state -> 'l array -> 'r array -> ('l,
'r, 'eq, 'diff) patch
variadic_diff ~weight ~test ~update state l r behaves as diff with the
following difference:
- update must now be an Diffing.update which indicates in which direc-
tion the expansion takes place.
OCamldoc 2023-02-12 Diffing(3o)
Generated by dwww version 1.15 on Sun Jun 23 03:48:14 CEST 2024.