Documentation

Lean.Util.Diff

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

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

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

      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

      Instances For
        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 α] :

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

        Equations
        Instances For
          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.
          Instances For
            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.
            Instances For
              def Lean.Diff.matchPrefix {α : Type u_1} [BEq α] (left : Subarray α) (right : Subarray α) :

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

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

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

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

                      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 α) :

                      Computes an edit script to transform left into right.

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

                        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.
                        Instances For