Documentation

Std.Data.Array.Match

structure Array.PrefixTable (α : Type u_1) extends Array :
Type u_1
  • data : List (α × Nat)
  • valid : ∀ {i : Nat} (h : i < Array.size s.toArray), s.toArray[i].snd i

    Validity condition to help with termination proofs

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.

Instances For
    Equations
    • Array.instInhabitedPrefixTable = { default := { toArray := #[], valid := (_ : ∀ {i : Nat} (a : i < Array.size #[]), #[][i].snd i) } }
    @[inline, reducible]
    abbrev Array.PrefixTable.size {α : Type u_1} (t : Array.PrefixTable α) :

    Returns the size of the prefix table

    Equations
    Instances For

      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.
      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
        • One or more equations did not get rendered due to their size.
        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

              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.