inductive Regex.Data.Expr.BacktrackingTree : Type

BacktrackingTree records the full backtracking search traces of a regex match.

Leaves represent success or failure, and internal nodes represent the operational effects of backtracking evaluation such as branching, reading one character, checking an anchor, and opening or closing a capture group.

Reference: Barriere, Deng, and Pit-Claudel, "Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)", https://arxiv.org/abs/2507.13091

• complete : BacktrackingTree
• fail : BacktrackingTree
• choice (t₁ t₂ : BacktrackingTree) : BacktrackingTree
• read (next : BacktrackingTree) : BacktrackingTree
• anchorPass (next : BacktrackingTree) : BacktrackingTree
• openGroup (tag : ℕ) (next : BacktrackingTree) : BacktrackingTree
• closeGroup (tag : ℕ) (next : BacktrackingTree) : BacktrackingTree

instance Regex.Data.Expr.instInhabitedBacktrackingTree : Inhabited BacktrackingTree

Equations

• Regex.Data.Expr.instInhabitedBacktrackingTree = { default := Regex.Data.Expr.instInhabitedBacktrackingTree.default }

def Regex.Data.Expr.instInhabitedBacktrackingTree.default : BacktrackingTree

Equations

• Regex.Data.Expr.instInhabitedBacktrackingTree.default = Regex.Data.Expr.BacktrackingTree.complete

inductive Regex.Data.Expr.BacktrackingTree.Action : Type

• expr (e : Expr) : Action
• closeGroup (tag : ℕ) : Action

inductive Regex.Data.Expr.BacktrackingTree.IsValid {s : String} : List Action → s.Pos → GroupMap s → BacktrackingTree → Prop

• complete {s : String} {p : s.Pos} {gs : GroupMap s} : IsValid [] p gs BacktrackingTree.complete
• epsilon {s : String} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (h : IsValid as p gs t) : IsValid (Action.expr Expr.epsilon :: as) p gs t
• anchor {s : String} {a : Anchor} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (ha : Anchor.test p a = true) (h : IsValid as p gs t) : IsValid (Action.expr (Expr.anchor a) :: as) p gs t.anchorPass
• anchorFail {s : String} {a : Anchor} {as : List Action} {p : s.Pos} {gs : GroupMap s} (ha : ¬Anchor.test p a = true) : IsValid (Action.expr (Expr.anchor a) :: as) p gs fail
• char {s : String} {c : Char} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (hp : p ≠ s.endPos) (hc : p.get hp = c) (h : IsValid as (p.next hp) gs t) : IsValid (Action.expr (Expr.char c) :: as) p gs t.read
• charFail {s : String} {c : Char} {as : List Action} {p : s.Pos} {gs : GroupMap s} (hp : p = s.endPos ∨ ∃ (hp' : p ≠ s.endPos), p.get hp' ≠ c) : IsValid (Action.expr (Expr.char c) :: as) p gs fail
• sparse {s : String} {cs : Classes} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (hp : p ≠ s.endPos) (hc : p.get hp ∈ cs) (h : IsValid as (p.next hp) gs t) : IsValid (Action.expr (classes cs) :: as) p gs t.read
• sparseFail {s : String} {cs : Classes} {as : List Action} {p : s.Pos} {gs : GroupMap s} (hp : p = s.endPos ∨ ∃ (hp' : p ≠ s.endPos), p.get hp' ∉ cs) : IsValid (Action.expr (classes cs) :: as) p gs fail
• openGroup {s : String} {tag : ℕ} {e : Expr} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (h : IsValid (Action.expr e :: Action.closeGroup tag :: as) p (GroupMap.openGroup tag p gs) t) : IsValid (Action.expr (group tag e) :: as) p gs (BacktrackingTree.openGroup tag t)
• closeGroup {s : String} {tag : ℕ} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (h : IsValid as p (GroupMap.closeGroup tag p gs) t) : IsValid (Action.closeGroup tag :: as) p gs (BacktrackingTree.closeGroup tag t)
• alternate {s : String} {e₁ e₂ : Expr} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t₁ t₂ : BacktrackingTree} (h₁ : IsValid (Action.expr e₁ :: as) p gs t₁) (h₂ : IsValid (Action.expr e₂ :: as) p gs t₂) : IsValid (Action.expr (e₁.alternate e₂) :: as) p gs (t₁.choice t₂)
• concat {s : String} {e₁ e₂ : Expr} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t : BacktrackingTree} (h : IsValid (Action.expr e₁ :: Action.expr e₂ :: as) p gs t) : IsValid (Action.expr (e₁.concat e₂) :: as) p gs t
• star {s : String} {greedy : Bool} {e : Expr} {as : List Action} {p : s.Pos} {gs : GroupMap s} {tLoop tExit : BacktrackingTree} (h₁ : IsValid (Action.expr e :: Action.expr (Expr.star greedy e) :: as) p gs tLoop) (h₂ : IsValid as p gs tExit) : IsValid (Action.expr (Expr.star greedy e) :: as) p gs (if greedy = true then tLoop.choice tExit else tExit.choice tLoop)

theorem Regex.Data.Expr.BacktrackingTree.deterministic_isValid {s : String} {as : List Action} {p : s.Pos} {gs : GroupMap s} {t₁ t₂ : BacktrackingTree} (h₁ : IsValid as p gs t₁) (h₂ : IsValid as p gs t₂) : t₁ = t₂

def Regex.Data.Expr.BacktrackingTree.firstMatch (t : BacktrackingTree) : Option Unit

Equations

• Regex.Data.Expr.BacktrackingTree.complete.firstMatch = some ()
• Regex.Data.Expr.BacktrackingTree.fail.firstMatch = none
• (t₁.choice t₂).firstMatch = (t₁.firstMatch <|> t₂.firstMatch)
• t_2.read.firstMatch = t_2.firstMatch
• t_2.anchorPass.firstMatch = t_2.firstMatch
• (Regex.Data.Expr.BacktrackingTree.openGroup tag t_2).firstMatch = t_2.firstMatch
• (Regex.Data.Expr.BacktrackingTree.closeGroup tag t_2).firstMatch = t_2.firstMatch

def Regex.Data.Expr.BacktrackingTree.extractCapturesAux {s : String} (p : s.Pos) (gs : GroupMap s) (t : BacktrackingTree) : List (s.Pos × GroupMap s)

Equations

• One or more equations did not get rendered due to their size.
• Regex.Data.Expr.BacktrackingTree.extractCapturesAux p gs Regex.Data.Expr.BacktrackingTree.complete = [(p, gs)]
• Regex.Data.Expr.BacktrackingTree.extractCapturesAux p gs Regex.Data.Expr.BacktrackingTree.fail = []
• Regex.Data.Expr.BacktrackingTree.extractCapturesAux p gs t_2.read = if hp : p ≠ s.endPos then Regex.Data.Expr.BacktrackingTree.extractCapturesAux (p.next hp) gs t_2 else []
• Regex.Data.Expr.BacktrackingTree.extractCapturesAux p gs t_2.anchorPass = Regex.Data.Expr.BacktrackingTree.extractCapturesAux p gs t_2

def Regex.Data.Expr.BacktrackingTree.extractCaptures {s : String} (startAt : s.Pos) (t : BacktrackingTree) : List (s.Pos × GroupMap s)

Equations

• Regex.Data.Expr.BacktrackingTree.extractCaptures startAt t = Regex.Data.Expr.BacktrackingTree.extractCapturesAux startAt Regex.Data.Expr.GroupMap.empty t