def Regex.IsSearchRegex (re : Regex) : Prop

Equations

• re.IsSearchRegex = ∃ (e : Regex.Data.Expr), re.nfa = Regex.NFA.compile (Regex.Data.Expr.group 0 e) ∧ (Regex.Data.Expr.group 0 e).Disjoint ∧ re.maxTag = re.nfa.maxTag

theorem Regex.IsSearchRegex.of_parse {s : String} {re : Regex} (h : parse s = Except.ok re) : re.IsSearchRegex

noncomputable def Regex.IsSearchRegex.inner {re : Regex} (s : re.IsSearchRegex) : Data.Expr

Equations

• s.inner = Exists.choose s

noncomputable def Regex.IsSearchRegex.expr {re : Regex} (s : re.IsSearchRegex) : Data.Expr

Equations

• s.expr = Regex.Data.Expr.group 0 s.inner

theorem Regex.IsSearchRegex.nfa_eq {re : Regex} (s : re.IsSearchRegex) : re.nfa = NFA.compile s.expr

theorem Regex.IsSearchRegex.disj {re : Regex} (s : re.IsSearchRegex) : s.expr.Disjoint

theorem Regex.IsSearchRegex.maxTag_eq {re : Regex} (s : re.IsSearchRegex) : re.maxTag = re.nfa.maxTag

theorem Regex.IsSearchRegex.le_maxTag {re : Regex} (s : re.IsSearchRegex) : 1 ≤ re.maxTag

theorem Regex.IsSearchRegex.captureNextBuf_soundness' {re : Regex} {bufferSize : ℕ} {it : String.Iterator} {matched : Vector (Option String.Pos) bufferSize} (h : re.captureNextBuf bufferSize it = some matched) (s : re.IsSearchRegex) (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 s.expr ∧ Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) matched

theorem Regex.IsSearchRegex.captureNextBuf_soundness {re : Regex} {bufferSize : ℕ} {it : String.Iterator} {matched : Vector (Option String.Pos) bufferSize} (h : re.captureNextBuf bufferSize it = some matched) (s : re.IsSearchRegex) (v : it.Valid) (le : 2 ≤ bufferSize) : ∃ (it' : String.Iterator) (it'' : String.Iterator) (groups : Data.CaptureGroups), it'.toString = it.toString ∧ it.pos ≤ it'.pos ∧ Data.Expr.Captures it' it'' groups s.expr ∧ Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) matched ∧ matched[0] = some it'.pos ∧ matched[1] = some it''.pos

theorem Regex.IsSearchRegex.captureNextBuf_completeness {re : Regex} {bufferSize : ℕ} {it : String.Iterator} (h : re.captureNextBuf bufferSize it = none) (s : re.IsSearchRegex) (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 s.expr

theorem Regex.IsSearchRegex.searchNext_some {re : Regex} {it : String.Iterator} {str : Substring} (h : re.searchNext it = some str) (s : re.IsSearchRegex) (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 s.expr ∧ str.startPos = it'.pos ∧ str.stopPos = it''.pos