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.lt_of_mem_tags {re : Regex} {tag : ℕ} (s : re.IsSearchRegex) (h : tag ∈ s.expr.tags) :

2 * tag < re.maxTag

theorem Regex.IsSearchRegex.captureNextBuf_soundness' {s : String} {re : Regex} {bufferSize : ℕ} {pos : s.ValidPos} {matched : Buffer s bufferSize} (h : re.captureNextBuf bufferSize pos = some matched) (s✝ : re.IsSearchRegex) :

∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s), pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups s✝.expr ∧ Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) matched

theorem Regex.IsSearchRegex.captureNextBuf_soundness {s : String} {re : Regex} {bufferSize : ℕ} {pos : s.ValidPos} {matched : Buffer s bufferSize} (h : re.captureNextBuf bufferSize pos = some matched) (s✝ : re.IsSearchRegex) (le : 2 ≤ bufferSize) :

∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s), pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups s✝.expr ∧ Strategy.EquivMaterializedUpdate (Strategy.materializeRegexGroups groups) matched ∧ matched[0] = String.ValidPosPlusOne.validPos pos' ∧ matched[1] = String.ValidPosPlusOne.validPos pos''

theorem Regex.IsSearchRegex.captureNextBuf_completeness' {s : String} {re : Regex} {bufferSize : ℕ} {pos : s.ValidPos} (h : re.captureNextBuf bufferSize pos = none) (isr : re.IsSearchRegex) (pos' pos'' : s.ValidPos) (groups : Data.CaptureGroups s) (le : pos ≤ pos') (c : Data.Expr.Captures pos' pos'' groups isr.expr) :

theorem Regex.IsSearchRegex.captureNextBuf_completeness {s : String} {re : Regex} {bufferSize : ℕ} {pos : s.ValidPos} (h : re.captureNextBuf bufferSize pos = none) (isr : re.IsSearchRegex) :

¬∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s), pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups isr.expr

theorem Regex.IsSearchRegex.searchNext_some {s : String} {re : Regex} {pos : s.ValidPos} {slice : String.Slice} (h : re.searchNext pos = some slice) (isr : re.IsSearchRegex) :

∃ (pos' : s.ValidPos) (pos'' : s.ValidPos) (groups : Data.CaptureGroups s), pos ≤ pos' ∧ Data.Expr.Captures pos' pos'' groups isr.expr ∧ slice.startInclusive = ⋯ ▸ pos' ∧ slice.endExclusive = ⋯ ▸ pos''