Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

For gory implementation details, please see Data.Patch.Internal

- data Patch a
- toList :: Patch a -> [Edit a]
- fromList :: Eq a => [Edit a] -> Patch a
- unsafeFromList :: [Edit a] -> Patch a
- inverse :: Patch a -> Patch a
- apply :: Patch a -> Vector a -> Vector a
- diff :: Eq a => Vector a -> Vector a -> Patch a
- data Edit a
- index :: Lens' (Edit a) Int
- old :: Traversal' (Edit a) a
- new :: Traversal' (Edit a) a

# Patches

A *patch* is a collection of edits performed to a *document*, in this case a `Vector`

. They are
implemented as a list
of `Edit`

, and can be converted to and from raw lists of edits using `toList`

and `fromList`

respectively.

Patches form a group (a `Monoid`

with inverses), where the inverse element can be computed with
`inverse`

and the group operation is *composition* of patches. Applying `p1 <> p2`

is the
same as applying `p1`

*then* `p2`

(see `apply`

). This composition operator may produce structurally
different patches depending on associativity, however the patches are guaranteed to be *equivalent*
in the sense that the resultant document will be the same when they are applied.

forAll (patchesFrom d) $ \a -> a <> mempty == a

forAll (patchesFrom d) $ \a -> mempty <> a == a

forAll (historyFrom d 3) $ \[a, b, c] -> apply (a <> (b <> c)) d == apply ((a <> b) <> c) d

The indices of the `Edit`

s are all based on the *original document*, so:

`>>>`

"a1b23"`apply (fromList [Insert 0 'a', Insert 1 'b']) (Vector.fromList "123")`

`>>>`

"ab123"`apply (fromList [Insert 0 'a', Insert 0 'b']) (Vector.fromList "123")`

Note that the first `Insert`

didn't introduce an offset for the second.

fromList :: Eq a => [Edit a] -> Patch a Source

Convert a list of edits to a patch, making sure to eliminate conflicting edits and sorting by index.

unsafeFromList :: [Edit a] -> Patch a Source

Directly convert a list of edits to a patch, without sorting edits by index, and resolving contradictory edits. Use this function if you know that the input list is already a wellformed patch.

inverse :: Patch a -> Patch a Source

Compute the inverse of a patch, such that:

forAll (patchesFrom d) $ \p -> p <> inverse p == mempty

forAll (patchesFrom d) $ \p -> inverse p <> p == mempty

forAll (patchesFrom d) $ \p -> inverse (inverse p) == p

forAll (historyFrom d 2) $ \[p, q] -> inverse (p <> q) == inverse q <> inverse p

forAll (patchesFrom d) $ \p -> inverse mempty == mempty

# Documents

apply :: Patch a -> Vector a -> Vector a Source

Apply a patch to a document.

Technically, `apply`

is a _monoid morphism_ to the monoid of endomorphisms `Vector a -> Vector a`

,
and that's how we can derive the following two laws:

forAll (historyFrom d 2) $ \[a, b] -> apply b (apply a d) == apply (a <> b) d

apply mempty d == d

diff :: Eq a => Vector a -> Vector a -> Patch a Source

Compute the difference between two documents, using the Wagner-Fischer algorithm. O(mn) time and space.

apply (diff d e) d == e

apply (diff d e) d == apply (inverse (diff e d)) d

apply (diff a b <> diff b c) a == apply (diff a c) a

# Edits

An `Edit`

is a single alteration of the vector, either inserting, removing, or replacing an element.

Useful optics are provided below, for the `index`

, the `old`

element, and the `new`

element.

index :: Lens' (Edit a) Int Source

A lens for the index where an edit is to be performed.

nonEmpty d ==> forAll (editsTo d) $ \e -> set index v e ^. index == v

nonEmpty d ==> forAll (editsTo d) $ \e -> set index (e ^. index) e == e

nonEmpty d ==> forAll (editsTo d) $ \e -> set index v' (set index v e) == set index v' e

old :: Traversal' (Edit a) a Source

A traversal for the old element to be replaced/deleted. Empty in the case of an `Insert`

.

new :: Traversal' (Edit a) a Source

A traversal for the new value to be inserted or replacing the old value. Empty in the case of a `Delete`

.