inductive Lean.Diff.Action : Type

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

• insert: Lean.Diff.Action

  Insert the item into the source

• delete: Lean.Diff.Action

  Delete the item from the source

• skip: Lean.Diff.Action

  Leave the item in the source

instance Lean.Diff.instReprAction : Repr Lean.Diff.Action

Equations

• Lean.Diff.instReprAction = { reprPrec := Lean.Diff.reprAction✝ }

instance Lean.Diff.instBEqAction : BEq Lean.Diff.Action

Equations

• Lean.Diff.instBEqAction = { beq := Lean.Diff.beqAction✝ }

instance Lean.Diff.instHashableAction : Hashable Lean.Diff.Action

Equations

• Lean.Diff.instHashableAction = { hash := Lean.Diff.hashAction✝ }

instance Lean.Diff.instToStringAction : ToString Lean.Diff.Action

Equations

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

def Lean.Diff.Action.linePrefix (action : Lean.Diff.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

• Lean.Diff.Action.delete.linePrefix = "-"
• Lean.Diff.Action.insert.linePrefix = "+"
• Lean.Diff.Action.skip.linePrefix = " "

structure Lean.Diff.Histogram.Entry (α : Type u) (lsize : Nat) (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

theorem Lean.Diff.Histogram.Entry.leftWF {α : Type u} {lsize : Nat} {rsize : Nat} (self : Lean.Diff.Histogram.Entry α lsize rsize) : self.leftCount = 0 ↔ self.leftIndex = none

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

theorem Lean.Diff.Histogram.Entry.rightWF {α : Type u} {lsize : Nat} {rsize : Nat} (self : Lean.Diff.Histogram.Entry α lsize rsize) : self.rightCount = 0 ↔ self.rightIndex = none

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

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

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

Equations

• Lean.Diff.Histogram α lsize rsize = Std.HashMap α (Lean.Diff.Histogram.Entry α lsize rsize)

def Lean.Diff.Histogram.addLeft {α : Type u_1} [BEq α] [Hashable α] {lsize : Nat} {rsize : Nat} (histogram : Lean.Diff.Histogram α lsize rsize) (index : Fin lsize) (val : α) : Lean.Diff.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.

def Lean.Diff.Histogram.addRight {α : Type u_1} [BEq α] [Hashable α] {lsize : Nat} {rsize : Nat} (histogram : Lean.Diff.Histogram α lsize rsize) (index : Fin rsize) (val : α) : Lean.Diff.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.

def Lean.Diff.matchPrefix {α : Type u_1} [BEq α] (left : Subarray α) (right : Subarray α) : Array α × Subarray α × Subarray α

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

Equations

• Lean.Diff.matchPrefix left right = Lean.Diff.matchPrefix.go left right #[]

@[irreducible]

def Lean.Diff.matchPrefix.go {α : Type u_1} [BEq α] (left : Subarray α) (right : Subarray α) (pref : Array α) : Array α × Subarray α × Subarray α

Equations

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

def Lean.Diff.matchSuffix {α : Type u_1} [BEq α] (left : Subarray α) (right : Subarray α) : Subarray α × Subarray α × Array α

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

Equations

• Lean.Diff.matchSuffix left right = Lean.Diff.matchSuffix.go left right 0

@[irreducible]

def Lean.Diff.matchSuffix.go {α : Type u_1} [BEq α] (left : Subarray α) (right : Subarray α) (i : Nat) : Subarray α × Subarray α × Array α

Equations

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

partial def Lean.Diff.lcs {α : Type u_1} [BEq α] [Hashable α] (left : Subarray α) (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.

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

Computes an edit script to transform left into right.

Equations

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

def Lean.Diff.linesToString {α : Type u_1} [ToString α] (lines : Array (Lean.Diff.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.