Documentation

Batteries.Data.Array.Match

structure Array.PrefixTable (α : Type u_1) extends Array :
Type u_1

Prefix table for the Knuth-Morris-Pratt matching algorithm

This is an array of the form t = [(x₀,n₀), (x₁,n₁), (x₂, n₂), ...] where for each i, nᵢ is the length of the longest proper prefix of xs = [x₀,x₁,...,xᵢ] which is also a suffix of xs.

  • toList : List (α × Nat)
  • valid : ∀ {i : Nat} (h : i < self.size), self.toArray[i].snd i

    Validity condition to help with termination proofs

Instances For
    theorem Array.PrefixTable.valid {α : Type u_1} (self : Array.PrefixTable α) {i : Nat} (h : i < self.size) :
    self.toArray[i].snd i

    Validity condition to help with termination proofs

    Equations
    • Array.instInhabitedPrefixTable = { default := { toArray := #[], valid := } }
    @[reducible, inline]
    abbrev Array.PrefixTable.size {α : Type u_1} (t : Array.PrefixTable α) :

    Returns the size of the prefix table

    Equations
    • t.size = t.size
    Instances For
      @[irreducible]
      def Array.PrefixTable.step {α : Type u_1} [BEq α] (t : Array.PrefixTable α) (x : α) :
      Fin (t.size + 1)Fin (t.size + 1)

      Transition function for the KMP matcher

      Assuming we have an input xs with a suffix that matches the pattern prefix t.pattern[:len] where len : Fin (t.size+1). Then xs.push x has a suffix that matches the pattern prefix t.pattern[:t.step x len]. If len is as large as possible then t.step x len will also be as large as possible.

      Equations
      • One or more equations did not get rendered due to their size.
      • t.step x 0, hk_2 = if h : 0 < t.size then if (x == t.toArray[0].fst) = true then 0 + 1, else (fun (x : Unit) => 0, ) () else (fun (x : Unit) => 0, ) ()
      Instances For
        def Array.PrefixTable.extend {α : Type u_1} [BEq α] (t : Array.PrefixTable α) (x : α) :

        Extend a prefix table by one element

        If t is the prefix table for xs then t.extend x is the prefix table for xs.push x.

        Equations
        • t.extend x = { toArray := t.push (x, (t.step x t.size, )), valid := }
        Instances For
          def Array.mkPrefixTable {α : Type u_1} [BEq α] (xs : Array α) :

          Make prefix table from a pattern array

          Equations
          Instances For
            def Array.mkPrefixTableOfStream {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (stream : σ) :

            Make prefix table from a pattern stream

            Equations
            Instances For
              partial def Array.mkPrefixTableOfStream.loop {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (t : Array.PrefixTable α) (stream : σ) :

              Inner loop for mkPrefixTableOfStream

              structure Array.Matcher (α : Type u_1) :
              Type u_1

              KMP matcher structure

              • Prefix table for the pattern

              • state : Fin (self.table.size + 1)

                Current longest matching prefix

              Instances For
                def Array.Matcher.ofArray {α : Type u_1} [BEq α] (pat : Array α) :

                Make a KMP matcher for a given pattern array

                Equations
                Instances For
                  def Array.Matcher.ofStream {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (pat : σ) :

                  Make a KMP matcher for a given a pattern stream

                  Equations
                  Instances For
                    partial def Array.Matcher.next? {α : Type u_1} {σ : Type u_2} [BEq α] [Stream σ α] (m : Array.Matcher α) (stream : σ) :

                    Find next match from a given stream

                    Runs the stream until it reads a sequence that matches the sought pattern, then returns the stream state at that point and an updated matcher state.