structure Regex.Strategy (s : String) : Type 1

• Update : Type
• empty : self.Update
• write : self.Update → Nat → s.Pos → self.Update

@[reducible, inline]

abbrev Regex.Buffer (s : String) (size : Nat) : Type

Equations

• Regex.Buffer s size = Vector s.PosPlusOne size

def Regex.Buffer.empty {s : String} {size : Nat} : Buffer s size

Equations

• Regex.Buffer.empty = Vector.replicate size (String.PosPlusOne.sentinel s)

def Regex.BufferStrategy (s : String) (size : Nat) : Strategy s

Equations

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

def Regex.instReprPos_regex {s : String} : Repr s.Pos

Equations

• Regex.instReprPos_regex = { reprPrec := fun (p : s.Pos) (n : Nat) => reprPrec p.offset n }

instance Regex.instReprUpdateBufferStrategy {s : String} {size : Nat} : Repr (BufferStrategy s size).Update

Equations

• Regex.instReprUpdateBufferStrategy = inferInstanceAs (Repr (Vector s.PosPlusOne size))

instance Regex.instInhabitedUpdateBufferStrategy {s : String} {size : Nat} : Inhabited (BufferStrategy s size).Update

Equations

• Regex.instInhabitedUpdateBufferStrategy = inferInstanceAs (Inhabited (Vector s.PosPlusOne size))

instance Regex.instDecidableEqUpdateBufferStrategy {s : String} {size : Nat} : DecidableEq (BufferStrategy s size).Update

Equations

• Regex.instDecidableEqUpdateBufferStrategy = inferInstanceAs (DecidableEq (Vector s.PosPlusOne size))

instance Regex.instGetElemUpdateBufferStrategyNatPosPlusOneLt {s : String} {size : Nat} : GetElem (BufferStrategy s size).Update Nat s.PosPlusOne fun (x : (BufferStrategy s size).Update) (i : Nat) => i < size

Equations

• Regex.instGetElemUpdateBufferStrategyNatPosPlusOneLt = inferInstanceAs (GetElem (Vector s.PosPlusOne size) Nat s.PosPlusOne fun (x : Vector s.PosPlusOne size) (i : Nat) => i < size)

@[simp]

theorem Regex.BufferStrategy.update_def {s : String} {size : Nat} : (BufferStrategy s size).Update = Buffer s size

@[simp]

theorem Regex.BufferStrategy.empty_def {s : String} {size : Nat} : (BufferStrategy s size).empty = Buffer.empty

@[simp]

theorem Regex.BufferStrategy.write_def {s : String} {size : Nat} {buffer : (BufferStrategy s size).Update} {offset : Nat} {pos : s.Pos} : (BufferStrategy s size).write buffer offset pos = Vector.setIfInBounds buffer offset (String.PosPlusOne.pos pos)

def Regex.HistoryStrategy (s : String) : Strategy s

This strategy is inefficient and used only for proofs.

Equations

• Regex.HistoryStrategy s = { Update := List (Nat × s.Pos), empty := [], write := fun (update : List (Nat × s.Pos)) (offset : Nat) (pos : s.Pos) => update ++ [(offset, pos)] }

@[simp]

theorem Regex.HistoryStrategy.update_def {s : String} : (HistoryStrategy s).Update = List (Nat × s.Pos)

@[simp]

theorem Regex.HistoryStrategy.empty_def {s : String} : (HistoryStrategy s).empty = []

@[simp]

theorem Regex.HistoryStrategy.write_def {s : String} {update : (HistoryStrategy s).Update} {offset : Nat} {pos : s.Pos} : (HistoryStrategy s).write update offset pos = List.append update [(offset, pos)]