def Regex.NFA.pushNode (nfa : NFA) (node : Node) : NFA

Equations

• nfa.pushNode node = { nodes := nfa.nodes.push node }

@[simp]

theorem Regex.NFA.pushNode_size {nfa : NFA} {node : Node} : (nfa.pushNode node).size = nfa.size + 1

theorem Regex.NFA.pushNode_get_lt {nfa : NFA} {node : Node} (i : Nat) (h : i < nfa.size) : (nfa.pushNode node)[i] = nfa[i]

@[simp]

theorem Regex.NFA.pushNode_get_eq {nfa : NFA} {node : Node} : (nfa.pushNode node)[nfa.size] = node

theorem Regex.NFA.pushNode_get {nfa : NFA} {node : Node} (i : Nat) (h : i < (nfa.pushNode node).size) : (nfa.pushNode node)[i] = if h' : i < nfa.size then nfa[i] else node

@[simp]

theorem Regex.NFA.pushNode_start {nfa : NFA} {node : Node} : (nfa.pushNode node).start = nfa.size

theorem Regex.NFA.pushNode_wf {nfa : NFA} {node : Node} (wf : nfa.WellFormed) (inBounds : node.inBounds (nfa.size + 1)) : (nfa.pushNode node).WellFormed

def Regex.NFA.pushRegex (nfa : NFA) (next : Nat) : Data.Expr → NFA

Compile a Regex and append the resulting nodes to the NFA. The nodes will transition to next on match.

Equations

• One or more equations did not get rendered due to their size.
• nfa.pushRegex next Regex.Data.Expr.empty = nfa.pushNode Regex.NFA.Node.fail
• nfa.pushRegex next Regex.Data.Expr.epsilon = nfa.pushNode (Regex.NFA.Node.epsilon next)
• nfa.pushRegex next (Regex.Data.Expr.anchor a) = nfa.pushNode (Regex.NFA.Node.anchor a next)
• nfa.pushRegex next (Regex.Data.Expr.char c) = nfa.pushNode (Regex.NFA.Node.char c next)
• nfa.pushRegex next (Regex.Data.Expr.classes cs) = nfa.pushNode (Regex.NFA.Node.sparse cs next)
• nfa.pushRegex next (e₁.concat e₂) = (nfa.pushRegex next e₂).pushRegex (nfa.pushRegex next e₂).start e₁

def Regex.NFA.compile (r : Data.Expr) : NFA

Equations

• Regex.NFA.compile r = Regex.NFA.done.pushRegex 0 r