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

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

@[reducible, inline]

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

Equations

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

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

Equations

• Regex.Buffer.empty = Vector.replicate size (String.ValidPosPlusOne.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.instReprValidPos_regex {s : String} : Repr s.ValidPos

Equations

• Regex.instReprValidPos_regex = { reprPrec := fun (p : s.ValidPos) (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.ValidPosPlusOne size))

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

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their 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.ValidPos} : (BufferStrategy s size).write buffer offset pos = Vector.setIfInBounds buffer offset (String.ValidPosPlusOne.validPos 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.ValidPos), empty := [], write := fun (update : List (Nat × s.ValidPos)) (offset : Nat) (pos : s.ValidPos) => update ++ [(offset, pos)] }

@[simp]

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

@[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.ValidPos} : (HistoryStrategy s).write update offset pos = List.append update [(offset, pos)]