Buffer Identifier

inductive Lapis.VFS.PieceTable.Buffer : Type

Identifies which buffer a piece points to

• original : Buffer
• add : Buffer

def Lapis.VFS.PieceTable.instInhabitedBuffer.default : Buffer

Equations

• Lapis.VFS.PieceTable.instInhabitedBuffer.default = Lapis.VFS.PieceTable.Buffer.original

instance Lapis.VFS.PieceTable.instInhabitedBuffer : Inhabited Buffer

Equations

• Lapis.VFS.PieceTable.instInhabitedBuffer = { default := Lapis.VFS.PieceTable.instInhabitedBuffer.default }

instance Lapis.VFS.PieceTable.instBEqBuffer : BEq Buffer

Equations

• Lapis.VFS.PieceTable.instBEqBuffer = { beq := Lapis.VFS.PieceTable.instBEqBuffer.beq }

def Lapis.VFS.PieceTable.instBEqBuffer.beq : Buffer → Buffer → Bool

Equations

• Lapis.VFS.PieceTable.instBEqBuffer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lapis.VFS.PieceTable.instReprBuffer : Repr Buffer

Equations

• Lapis.VFS.PieceTable.instReprBuffer = { reprPrec := Lapis.VFS.PieceTable.instReprBuffer.repr }

def Lapis.VFS.PieceTable.instReprBuffer.repr : Buffer → Nat → Std.Format

Equations

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

instance Lapis.VFS.PieceTable.instDecidableEqBuffer : DecidableEq Buffer

Equations

• Lapis.VFS.PieceTable.instDecidableEqBuffer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Piece Descriptor

structure Lapis.VFS.PieceTable.Piece : Type

A piece describes a contiguous range of text in one of the buffers

• buffer : Buffer
• start : Nat
• length : Nat
• lineBreaks : Nat
• utf16Length : Nat

def Lapis.VFS.PieceTable.instInhabitedPiece.default : Piece

Equations

• Lapis.VFS.PieceTable.instInhabitedPiece.default = { buffer := default, start := default, length := default, lineBreaks := default, utf16Length := default }

instance Lapis.VFS.PieceTable.instInhabitedPiece : Inhabited Piece

Equations

• Lapis.VFS.PieceTable.instInhabitedPiece = { default := Lapis.VFS.PieceTable.instInhabitedPiece.default }

def Lapis.VFS.PieceTable.instReprPiece.repr : Piece → Nat → Std.Format

Equations

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

instance Lapis.VFS.PieceTable.instReprPiece : Repr Piece

Equations

• Lapis.VFS.PieceTable.instReprPiece = { reprPrec := Lapis.VFS.PieceTable.instReprPiece.repr }

def Lapis.VFS.PieceTable.Piece.fromText (buffer : Buffer) (start : Nat) (text : String) : Piece

Create a piece from text content, computing metrics

Equations

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

def Lapis.VFS.PieceTable.Piece.empty : Piece

Create an empty piece

Equations

• Lapis.VFS.PieceTable.Piece.empty = { buffer := Lapis.VFS.PieceTable.Buffer.original, start := 0, length := 0, lineBreaks := 0, utf16Length := 0 }

def Lapis.VFS.PieceTable.Piece.isEmpty (p : Piece) : Bool

Check if piece is empty

Equations

• p.isEmpty = (p.length == 0)

instance Lapis.VFS.PieceTable.instMeasurablePiece : FingerTree.Measurable Piece

Pieces are measurable for the finger tree

Equations

• Lapis.VFS.PieceTable.instMeasurablePiece = { measure := fun (p : Lapis.VFS.PieceTable.Piece) => { bytes := p.length, utf16Units := p.utf16Length, lines := p.lineBreaks } }

Text Buffers

structure Lapis.VFS.PieceTable.TextBuffers : Type

The two text buffers backing the piece table

• original : String
• add : String

def Lapis.VFS.PieceTable.instInhabitedTextBuffers.default : TextBuffers

Equations

• Lapis.VFS.PieceTable.instInhabitedTextBuffers.default = { original := default, add := default }

instance Lapis.VFS.PieceTable.instInhabitedTextBuffers : Inhabited TextBuffers

Equations

• Lapis.VFS.PieceTable.instInhabitedTextBuffers = { default := Lapis.VFS.PieceTable.instInhabitedTextBuffers.default }

def Lapis.VFS.PieceTable.TextBuffers.fromContent (content : String) : TextBuffers

Create buffers from initial document content

Equations

• Lapis.VFS.PieceTable.TextBuffers.fromContent content = { original := content, add := "" }

def Lapis.VFS.PieceTable.TextBuffers.getPieceText (buffers : TextBuffers) (p : Piece) : String

Get text for a piece from the appropriate buffer

Equations

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

def Lapis.VFS.PieceTable.TextBuffers.appendText (buffers : TextBuffers) (text : String) : TextBuffers × Nat

Append text to the add buffer, returning new buffers and the start position

Equations

• buffers.appendText text = ({ original := buffers.original, add := buffers.add ++ text }, buffers.add.utf8ByteSize)

Piece Table State

structure Lapis.VFS.PieceTable.PieceTableState : Type

The complete piece table state using a finger tree of pieces

• buffers : TextBuffers
• pieces : FingerTree.FingerTree Piece

instance Lapis.VFS.PieceTable.instInhabitedPieceTableState : Inhabited PieceTableState

Equations

• Lapis.VFS.PieceTable.instInhabitedPieceTableState = { default := Lapis.VFS.PieceTable.instInhabitedPieceTableState.default }

def Lapis.VFS.PieceTable.instInhabitedPieceTableState.default : PieceTableState

Equations

• Lapis.VFS.PieceTable.instInhabitedPieceTableState.default = { buffers := default, pieces := default }

def Lapis.VFS.PieceTable.PieceTableState.fromContent (content : String) : PieceTableState

Create a piece table from initial content

Equations

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

def Lapis.VFS.PieceTable.PieceTableState.byteLength (state : PieceTableState) : Nat

Get the total byte length

Equations

• state.byteLength = state.pieces.measure.bytes

def Lapis.VFS.PieceTable.PieceTableState.lineCount (state : PieceTableState) : Nat

Get the total line count

Equations

• state.lineCount = state.pieces.measure.lines

def Lapis.VFS.PieceTable.PieceTableState.utf16Length (state : PieceTableState) : Nat

Get the total UTF-16 length

Equations

• state.utf16Length = state.pieces.measure.utf16Units

def Lapis.VFS.PieceTable.PieceTableState.getContent (state : PieceTableState) : String

Get all text content

Equations

• state.getContent = Lapis.VFS.FingerTree.FingerTree.foldl (fun (acc : String) (p : Lapis.VFS.PieceTable.Piece) => acc ++ state.buffers.getPieceText p) "" state.pieces

def Lapis.VFS.PieceTable.PieceTableState.getTextByteRange (state : PieceTableState) (startByte endByte : Nat) : String

Get text in a byte range

Equations

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

@[irreducible]

def Lapis.VFS.PieceTable.PieceTableState.getTextByteRange.getTextByteRangeAux (pieces : Array Piece) (buffers : TextBuffers) (startByte endByte idx currentByte : Nat) (result : String) : String

Equations

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

def Lapis.VFS.PieceTable.PieceTableState.insertAt (state : PieceTableState) (bytePos : Nat) (text : String) : PieceTableState

Insert text at a byte position - O(log n)

Equations

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

def Lapis.VFS.PieceTable.PieceTableState.deleteRange (state : PieceTableState) (startByte endByte : Nat) : PieceTableState

Delete text in a byte range - O(log n)

Equations

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

def Lapis.VFS.PieceTable.PieceTableState.replaceRange (state : PieceTableState) (startByte endByte : Nat) (text : String) : PieceTableState

Replace text in a byte range - O(log n)

Equations

• state.replaceRange startByte endByte text = (state.deleteRange startByte endByte).insertAt startByte text

Piece Coalescing

def Lapis.VFS.PieceTable.PieceTableState.compact (state : PieceTableState) : PieceTableState

Compact the piece table by merging adjacent same-buffer pieces

Equations

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

def Lapis.VFS.PieceTable.PieceTableState.compact.compactAux (pieces : List Piece) (current : Piece) (result : List Piece) : List Piece

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.PieceTable.PieceTableState.compact.compactAux [] current result = result ++ [current]