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

Equations

• nfa.pushNode node = { nodes := nfa.nodes.push node, start := nfa.nodes.size }

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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 (r₁.concat r₂) = (nfa.pushRegex next r₂).pushRegex (nfa.pushRegex next r₂).start r₁

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

Equations

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