Documentation

Lean.Util.Diff

source
inductive Lean.Diff.Action :
Type

An action in an edit script to transform one source sequence into a target sequence.

  • insert : Action

    Insert the item into the source

  • delete : Action

    Delete the item from the source

  • skip : Action

    Leave the item in the source

Instances For
source
instance Lean.Diff.instReprAction :
Repr Action
Equations
source
instance Lean.Diff.instBEqAction :
BEq Action
Equations
source
instance Lean.Diff.instHashableAction :
Hashable Action
Equations
source
instance Lean.Diff.instToStringAction :
ToString Action
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Diff.Action.linePrefix (action : Action) :
String

Determines a prefix to show on a given line when printing diff results.

For delete, the prefix is "-", for insert, it is "+", and for skip it is " ".

Equations
source
structure Lean.Diff.Histogram.Entry (α : Type u) (lsize rsize : Nat) :
Type

A histogram entry consists of the number of times the element occurs in the left and right input arrays along with an index at which the element can be found, if applicable.

  • leftCount : Nat

    How many times the element occurs in the left array

  • leftIndex : Option (Fin lsize)

    An index of the element in the left array, if applicable

  • leftWF : self.leftCount = 0 ↔ self.leftIndex = none

    Invariant: the count is non-zero iff there is a saved index

  • rightCount : Nat

    How many times the element occurs in the right array

  • rightIndex : Option (Fin rsize)

    An index of the element in the right array, if applicable

  • rightWF : self.rightCount = 0 ↔ self.rightIndex = none

    Invariant: the count is non-zero iff there is a saved index

source
def Lean.Diff.Histogram (α : Type u) (lsize rsize : Nat) [BEq α] [Hashable α] :
Type u

A histogram for arrays maps each element to a count and, if applicable, an index.

Equations
source
def Lean.Diff.Histogram.addLeft {α : Type u_1} [BEq α] [Hashable α] {lsize rsize : Nat} (histogram : Histogram α lsize rsize) (index : Fin lsize) (val : α) :
Histogram α lsize rsize

Add an element from the left array to a histogram

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Diff.Histogram.addRight {α : Type u_1} [BEq α] [Hashable α] {lsize rsize : Nat} (histogram : Histogram α lsize rsize) (index : Fin rsize) (val : α) :
Histogram α lsize rsize

Add an element from the right array to a histogram

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Diff.matchPrefix {α : Type u_1} [BEq α] (left right : Subarray α) :
Array α × Subarray α × Subarray α

Given two Subarrays, find their common prefix and return their differing suffixes

Equations
source
@[irreducible]
def Lean.Diff.matchPrefix.go {α : Type u_1} [BEq α] (left right : Subarray α) (pref : Array α) :
Array α × Subarray α × Subarray α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Diff.matchSuffix {α : Type u_1} [BEq α] (left right : Subarray α) :
Subarray α × Subarray α × Array α

Given two Subarrays, find their common suffix and return their differing prefixes

Equations
source
@[irreducible]
def Lean.Diff.matchSuffix.go {α : Type u_1} [BEq α] (left right : Subarray α) (i : Nat) :
Subarray α × Subarray α × Array α
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Diff.lcs {α : Type u_1} [BEq α] [Hashable α] (left right : Subarray α) :
Array α

Finds the least common subsequence of two arrays using a variant of jgit's histogram diff algorithm.

Unlike jgit's implementation, this one does not perform a cutoff on histogram bucket sizes, nor does it fall back to the Myers diff algorithm. This means that it has quadratic worst-case complexity. Empirically, however, even quadratic cases of this implementation can handle hundreds of megabytes in a second or so, and it is intended to be used for short strings like error messages. Be cautious when applying it to larger workloads.

source
def Lean.Diff.diff {α : Type} [BEq α] [Hashable α] [Inhabited α] (original edited : Array α) :
Array (Action × α)

Computes an edit script to transform left into right.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Diff.linesToString {α : Type u_1} [ToString α] (lines : Array (Action × α)) :
String

Shows a line-by-line edit script with markers for added and removed lines.

Equations
  • One or more equations did not get rendered due to their size.