An Insert as bs x is a witness that you can insert x into some position in list as to produce list bs. It is essentially Delete flipped.

Some examples:

InsZ                   :: Insert '[1,2,3] '[4,1,2,3] 4
InsS InsZ              :: Insert '[1,2,3] '[1,4,2,3] 4
InsS (InsS InsZ)       :: Insert '[1,2,3] '[1,2,4,3] 4
InsS (InsS (InsS InsZ) :: Insert '[1,2,3] '[1,2,3,4] 4

bs will always be exactly one item longer than as.

Automatically generate an Insert if as, bs and x are known statically.

Prefers the earlier insertion if there is an ambiguity.

InsS InsZ        :: Insert '[1,2] '[1,2,2] 2
InsS (InsS InsZ) :: Insert '[1,2] '[1,2,2] 2
autoInsert '[1,2] '[1,2,2] @2 == InsS InsZ

Since: 0.1.2.0

A Delete as bs x is a witness that you can delete item x from as to produce the list bs. It is essentially Insert flipped.

Some examples:

DelZ             :: Delete '[1,2,3] '[2,3] 1
DelS DelZ        :: Delete '[1,2,3] '[2,3] 2
DelS (DelS DelZ) :: Delete '[1,2,3] '[1,2] 3

bs will always be exactly one item shorter than as.

Automatically generate an Delete if as, bs and x are known statically.

Prefers the earlier deletion if there is an ambiguity.

DelS DelZ        :: Delete '[1,2,2] '[1,2] 2
DelS (DelS DelZ) :: Delete '[1,2,2] '[1,2] 2
autoDelete '[1,2,2] '[1,2] @2 == DelS DelZ

Since: 0.1.2.0

Flip an insertion.

Flip a deletion.

A Substitute as bs x y is a witness that you can replace item x in as with item y to produce bs.

Some examples:

SubZ             :: Substitute '[1,2,3] '[4,2,3] 1 4
SubS SubZ        :: Substitute '[1,2,3] '[1,4,3] 2 4
SubS (SubS SubZ) :: Substitute '[1,2,3] '[1,2,4] 3 4

Automatically generate an Substitute if as, bs, x, and y are known statically.

Prefers the "earlier" substitution if there is an ambiguity

SubZ      :: Substitute '[1,1] '[1,1] 1 1
SubS SubZ :: Substitute '[1,1] '[1,1] 1 1
autoSubstitute '[1,1] '[1,1] 1 1 == SubZ

Since: 0.1.2.0

Flip a substitution

Decompose a Substitute into a Delete followed by an Insert.

A type-level predicate that a given value can be used as an insertion to change as to bs.

Since: 0.1.2.0

If bs satisfies InsertedInto as, it means that there exists some element x such that IsInsert as bs @@ x: you can get bs by inserting x into as somewhere.

In other words, InsertedInto as is satisfied by bs if you can turn as into bs by inserting one individual item.

You can find this element (if it exists) using search, or the Decidable instance of Found (InsertedInto as):

searchTC :: SingI as => Sing bs -> Decision (Σ k (IsInsert as bs))

This will find you the single element you need to insert into as to get bs, if it exists.

Since: 0.1.2.0

A type-level predicate that a given value can be used as a deletion to change as to bs.

Since: 0.1.2.0

If bs satisfies DeletedFrom as, it means that there exists some element x such that IsDelete as bs @@ x: you can get bs by deleting x from as somewhere.

In other words, DeletedFrom as is satisfied by bs if you can turn as into bs by deleting one individual item.

You can find this element (if it exists) using search, or the Decidable instance of Found (DeletedFrom as).

searchTC :: SingI as => Sing bs -> Decision (Σ k (IsDelete as bs))

This will find you the single element you need to delete from as to get bs, if it exists.

Since: 0.1.2.0

A type-level predicate that a given value can be used as a substitution of x to change as to bs.

Since: 0.1.2.0

Kind-indexed singleton for Insert.

Kind-indexed singleton for Delete.

Kind-indexed singleton for Substitute.

An Edit as bs is a reversible edit script transforming as into bs through successive insertions, deletions, and substitutions.

TODO: implement Wagner-Fischer or something similar to minimize find a minimal edit distance

Compose two Edits

Reverse an Edit script. O(n^2). Please do not use ever in any circumstance.

TODO: Make O(n) using diff lists.

Insert a value into a Rec, at a position indicated by the Insert.

Delete a value in a Rec, at a position indicated by the Delete.

Retrieve and delete a value in a Rec, at a position indicated by the Delete.

A type-changing lens into a value in a Rec, given a Substitute indicating which value.

For example:

recLens (SubS SubZ)
     :: Lens (Rec f '[a,b,c,d]) (Rec f '[a,e,c,d])
             (f b)              (f e)

The number of SubS in the index essentially indicates the index to edit at.

This is similar to rlensC from vinyl, but is built explicitly and inductively, instead of using typeclass magic.

Substitute a value in a Rec at a given position, indicated by the Substitute. This is essentially a specialized version of recLens.

If you add an item to as to create bs, you also need to shift an Index as y to Index bs y. This shifts the Index in as to become an Index in bs, but makes sure that the index points to the same original value.

Used as the return type of deleteIndex. An DeletedIx bs x y is like a Maybe (Index bs y), except the Nothing case witnesses that x ~ y.

If you delete an item in as to create bs, you also need to move Index as y into Index bs y. This transforms the Index in as to become an Index in bs, making sure the index points to the same original value.

However, there is a possibility that the deleted item is the item that the index was originally pointing to. If this is the case, this function returns GotDeleted, a witness that x ~ y. Otherwise, it returns NotDeleted with the unshifted index.

A version of deleteIndex returning a simple Maybe. This can be used if you don't care about witnessing that x ~ y in the case that the index is the item that is deleted.

Used as the return type of substituteIndex. An SubstitutedIx bs x y z is like an Either (Index bs y) (Index bs z), except the Left case witnesses that x ~ z.

If you substitute an item in as to create bs, you also need to reshift Index as z into Index bs z. This reshifts the Index in as to become an Index in bs, making sure the index points to the same original value.

However, there is a possibility that the substituted item is the item that the index was originally pointing to. If this is the case, this function returns GotSubbed, a witness that x ~ z. Otherwise, it returns NotSubbed. Both contain the updated index.

A version of substituteIndex returning a simple Either. This can be the case if you don't care about witnessing x ~ z in the case that the index is the item that was substituted.

Given an Index pointing to an element, create a Delete corresponding to the given item. The type of the resulting list is existentially quantified, is guaranteed to be just exactly the original list minus the specified element.

Given an Index pointing to an element, create an Insert placing an item directly before the given element. The type is existentailly quantified.

Given an Index pointing to an element, create an Insert placing an item directly after the given element. The type is existentailly quantified.

Type-level version of insertIndex. Because of how GADTs and type families interact, the type-level lists and kinds of the insertion and index must be provided.

Singleton witness for InsertIndex.

Kind-indexed singleton for DeletedIx.

Type-level version of deleteIndex. Because of how GADTs and type families interact, the type-level lists and kinds of the insertion and index must be provided.

Singleton witness for DeleteIndex.

Kind-indexed singleton for SubstitutedIx.

Type-level version of substituteIndex. Because of how GADTs and type families interact, the type-level lists and kinds of the insertion and index must be provided.

Singleton witness for SubstituteIndex.

Defunctionalization symbol for InsertIndex, expecting only the kind variables.

Defunctionalization symbol for InsertIndex, expecting the Insert along with the kind variables.

Defunctionalization symbol for DeleteIndex, expecting only the kind variables.

Defunctionalization symbol for DeleteIndex, expecting the Delete along with the kind variables.

Defunctionalization symbol for SubstituteIndex, expecting only the kind variables.

Defunctionalization symbol for SubstituteIndex, expecting the Substitute along with the kind variables.