theorem
Regex.Backtracker.captureNext_soundness
{e : Data.Expr}
{bufferSize : ℕ}
{it : String.Iterator}
{matchedB : (BufferStrategy bufferSize).Update}
(disj : e.Disjoint)
(hresB : captureNext (BufferStrategy bufferSize) (NFA.compile e) ⋯ it = some matchedB)
(v : it.Valid)
:
∃ (it' : String.Iterator) (it'' : String.Iterator) (groups : Data.CaptureGroups),
it'.toString = it.toString ∧ it.pos ≤ it'.pos ∧ Data.Expr.Captures it' it'' groups e ∧ Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) matchedB
theorem
Regex.Backtracker.captureNext_completeness
{e : Data.Expr}
{bufferSize : ℕ}
{it : String.Iterator}
(hresB : captureNext (BufferStrategy bufferSize) (NFA.compile e) ⋯ it = none)
(v : it.Valid)
:
¬∃ (it' : String.Iterator) (it'' : String.Iterator) (groups : Data.CaptureGroups),
it'.toString = it.toString ∧ it.pos ≤ it'.pos ∧ Data.Expr.Captures it' it'' groups e
def
Regex.Backtracker.decideSearchProblem
(e : Data.Expr)
(it : String.Iterator)
(disj : e.Disjoint)
(v : it.Valid)
:
Equations
- One or more equations did not get rendered due to their size.