Documentation

RegexCorrectness.Regex.Basic

def Regex.IsSearchRegex (re : Regex) :

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Regex.IsSearchRegex.of_fromExpr {e : Data.Expr} (h : (Data.Expr.group 0 e).Disjoint) :

(fromExpr (Data.Expr.group 0 e)).IsSearchRegex

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) :

Equations

s.inner = Exists.choose s

Instances For

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

Equations

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

Instances For

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.optimizationInfo_eq {re : Regex} (s : re.IsSearchRegex) :

re.optimizationInfo = OptimizationInfo.fromExpr s.expr

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' it'' : String.Iterator) (groups : Data.CaptureGroups) (eqs : it'.toString = it.toString) (le : it.pos ≤ it'.pos) (c : Data.Expr.Captures it' it'' groups s.expr) :

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