inductive Regex.Data.Expr.GroupInfo (s : String) : Type

• none {s : String} : GroupInfo s
• started {s : String} (startAt : s.Pos) : GroupInfo s
• closed {s : String} (startAt endAt : s.Pos) : GroupInfo s

def Regex.Data.Expr.instInhabitedGroupInfo.default {a✝ : String} : GroupInfo a✝

Equations

• Regex.Data.Expr.instInhabitedGroupInfo.default = Regex.Data.Expr.GroupInfo.none

instance Regex.Data.Expr.instInhabitedGroupInfo {a✝ : String} : Inhabited (GroupInfo a✝)

Equations

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

instance Regex.Data.Expr.instZeroGroupInfo {s : String} : Zero (GroupInfo s)

Equations

• Regex.Data.Expr.instZeroGroupInfo = { zero := Regex.Data.Expr.GroupInfo.none }

structure Regex.Data.Expr.GroupMap (s : String) : Type

• groups : Π₀ (x : ℕ), GroupInfo s

def Regex.Data.Expr.GroupMap.empty {s : String} : GroupMap s

Equations

• Regex.Data.Expr.GroupMap.empty = { groups := 0 }

def Regex.Data.Expr.GroupMap.get {s : String} (tag : ℕ) (self : GroupMap s) : GroupInfo s

Equations

• Regex.Data.Expr.GroupMap.get tag self = self.groups tag

def Regex.Data.Expr.GroupMap.openGroup {s : String} (tag : ℕ) (startAt : s.Pos) (self : GroupMap s) : GroupMap s

Equations

• Regex.Data.Expr.GroupMap.openGroup tag startAt self = { groups := self.groups.update tag (Regex.Data.Expr.GroupInfo.started startAt) }

def Regex.Data.Expr.GroupMap.closeGroup {s : String} (tag : ℕ) (endAt : s.Pos) (self : GroupMap s) : GroupMap s

Equations

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

def Regex.Data.Expr.GroupMap.setClosed {s : String} (tag : ℕ) (startAt endAt : s.Pos) (self : GroupMap s) : GroupMap s

Equations

• Regex.Data.Expr.GroupMap.setClosed tag startAt endAt self = { groups := self.groups.update tag (Regex.Data.Expr.GroupInfo.closed startAt endAt) }

def Regex.Data.Expr.GroupMap.addCaptures {s : String} (self : GroupMap s) : CaptureGroups s → GroupMap s

Equations

• self.addCaptures Regex.Data.CaptureGroups.empty = self
• self.addCaptures (Regex.Data.CaptureGroups.group tag first last rest) = Regex.Data.Expr.GroupMap.setClosed tag first last (self.addCaptures rest)
• self.addCaptures (g₁.concat g₂) = (self.addCaptures g₁).addCaptures g₂

@[simp]

theorem Regex.Data.Expr.GroupMap.get_openGroup_self {s : String} (self : GroupMap s) (tag : ℕ) (startAt : s.Pos) : get tag (openGroup tag startAt self) = GroupInfo.started startAt

@[simp]

theorem Regex.Data.Expr.GroupMap.get_openGroup_of_ne {s : String} (self : GroupMap s) {tag tag' : ℕ} (startAt : s.Pos) (h : tag' ≠ tag) : get tag' (openGroup tag startAt self) = get tag' self

@[simp]

theorem Regex.Data.Expr.GroupMap.get_setClosed_self {s : String} (self : GroupMap s) (tag : ℕ) (startAt endAt : s.Pos) : get tag (setClosed tag startAt endAt self) = GroupInfo.closed startAt endAt

@[simp]

theorem Regex.Data.Expr.GroupMap.get_setClosed_of_ne {s : String} (self : GroupMap s) {tag tag' : ℕ} (startAt endAt : s.Pos) (h : tag' ≠ tag) : get tag' (setClosed tag startAt endAt self) = get tag' self

@[simp]

theorem Regex.Data.Expr.GroupMap.get_closeGroup_of_ne {s : String} (self : GroupMap s) {tag tag' : ℕ} (endAt : s.Pos) (h : tag' ≠ tag) : get tag' (closeGroup tag endAt self) = get tag' self

@[simp]

theorem Regex.Data.Expr.GroupMap.get_closeGroup_self {s : String} (self : GroupMap s) (tag : ℕ) (endAt : s.Pos) : get tag (closeGroup tag endAt self) = match get tag self with | GroupInfo.started startAt => GroupInfo.closed startAt endAt | x => x

theorem Regex.Data.Expr.GroupMap.ext {s : String} {x y : GroupMap s} (h : ∀ (tag : ℕ), get tag x = get tag y) : x = y

theorem Regex.Data.Expr.GroupMap.openGroup_setClosed_comm {s : String} (self : GroupMap s) {tag tag' : ℕ} {openAt first last : s.Pos} (h : tag' ≠ tag) : setClosed tag' first last (openGroup tag openAt self) = openGroup tag openAt (setClosed tag' first last self)

theorem Regex.Data.Expr.GroupMap.get_addCaptures_eq_self_of_forall_not_mem {s : String} (self : GroupMap s) {groups : CaptureGroups s} {tag : ℕ} (h : ∀ (first last : s.Pos), (tag, first, last) ∉ groups) : get tag (self.addCaptures groups) = get tag self

theorem Regex.Data.Expr.GroupMap.addCaptures_openGroup_comm_of_forall_not_mem {s : String} (self : GroupMap s) {groups : CaptureGroups s} {tag : ℕ} {startAt : s.Pos} (hmem : ∀ (first last : s.Pos), (tag, first, last) ∉ groups) : (openGroup tag startAt self).addCaptures groups = openGroup tag startAt (self.addCaptures groups)

theorem Regex.Data.Expr.GroupMap.get_addCaptures_openGroup_eq_of_ne {s : String} (self : GroupMap s) {groups : CaptureGroups s} {tag tag' : ℕ} {startAt : s.Pos} (hmem : ∀ (first last : s.Pos), (tag, first, last) ∉ groups) (hne : tag' ≠ tag) : get tag' ((openGroup tag startAt self).addCaptures groups) = get tag' (self.addCaptures groups)

theorem Regex.Data.Expr.GroupMap.closeGroup_addCaptures_openGroup_eq_addCaptures_group {s : String} (self : GroupMap s) {groups : CaptureGroups s} {tag : ℕ} {startAt endAt : s.Pos} (hmem : ∀ (first last : s.Pos), (tag, first, last) ∉ groups) : closeGroup tag endAt ((openGroup tag startAt self).addCaptures groups) = self.addCaptures (CaptureGroups.group tag startAt endAt groups)