Documentation

RegexCorrectness.VM.Path.CharStep

source
def Regex.NFA.CharStep (nfa : NFA) (it : String.Iterator) (i j : Fin nfa.nodes.size) :
Prop
Equations
Instances For
    source
    @[simp]
    theorem Regex.NFA.CharStep.done {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} (hn : nfa[i] = Node.done) :
    nfa.CharStep it i j ↔ False
    source
    @[simp]
    theorem Regex.NFA.CharStep.fail {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} (hn : nfa[i] = Node.fail) :
    nfa.CharStep it i j ↔ False
    source
    @[simp]
    theorem Regex.NFA.CharStep.epsilon {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {next : ℕ} (hn : nfa[i] = Node.epsilon next) :
    nfa.CharStep it i j ↔ False
    source
    @[simp]
    theorem Regex.NFA.CharStep.anchor {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {anchor : Data.Anchor} {next : ℕ} (hn : nfa[i] = Node.anchor anchor next) :
    nfa.CharStep it i j ↔ False
    source
    @[simp]
    theorem Regex.NFA.CharStep.split {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {next₁ next₂ : ℕ} (hn : nfa[i] = Node.split next₁ next₂) :
    nfa.CharStep it i j ↔ False
    source
    @[simp]
    theorem Regex.NFA.CharStep.save {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {offset next : ℕ} (hn : nfa[i] = Node.save offset next) :
    nfa.CharStep it i j ↔ False
    source
    @[simp]
    theorem Regex.NFA.CharStep.char {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {c : Char} {next : ℕ} (hn : nfa[i] = Node.char c next) :
    nfa.CharStep it i j ↔ ∃ (l : List Char) (r : List Char), ↑j = next ∧ String.Iterator.ValidFor l (c :: r) it
    source
    @[simp]
    theorem Regex.NFA.CharStep.sparse {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} {cs : Data.Classes} {next : ℕ} (hn : nfa[i] = Node.sparse cs next) :
    nfa.CharStep it i j ↔ ∃ (l : List Char) (c : Char) (r : List Char), ↑j = next ∧ String.Iterator.ValidFor l (c :: r) it ∧ c ∈ cs
    source
    theorem Regex.NFA.CharStep.char_or_sparse {nfa : NFA} {it : String.Iterator} {i j : Fin nfa.nodes.size} (step : nfa.CharStep it i j) :
    (∃ (c : Char) (next : ℕ), nfa[i] = Node.char c next) ∨ ∃ (cs : Data.Classes) (next : ℕ), nfa[i] = Node.sparse cs next