UTF-16 Utilities

def Lapis.VFS.Position.utf16Length (s : String) : Nat

Count UTF-16 code units in a string

Equations

• Lapis.VFS.Position.utf16Length s = String.foldl (fun (count : Nat) (c : Char) => have cp := c.toNat; if cp ≥ 65536 then count + 2 else count + 1) 0 s

def Lapis.VFS.Position.utf8OffsetToUtf16 (s : String) (utf8Offset : Nat) : Nat

Convert a UTF-8 byte offset to a UTF-16 offset within a string

Equations

• Lapis.VFS.Position.utf8OffsetToUtf16 s utf8Offset = Lapis.VFS.Position.utf8OffsetToUtf16.utf8ToUtf16Aux utf8Offset s 0 0 0

@[irreducible]

def Lapis.VFS.Position.utf8OffsetToUtf16.utf8ToUtf16Aux (utf8Offset : Nat) (s : String) (charIdx bytePos utf16Pos : Nat) : Nat

Equations

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

def Lapis.VFS.Position.utf16OffsetToUtf8 (s : String) (utf16Offset : Nat) : Nat

Convert a UTF-16 offset to a UTF-8 byte offset within a string

Equations

• Lapis.VFS.Position.utf16OffsetToUtf8 s utf16Offset = Lapis.VFS.Position.utf16OffsetToUtf8.utf16ToUtf8Aux utf16Offset s 0 0 0

@[irreducible]

def Lapis.VFS.Position.utf16OffsetToUtf8.utf16ToUtf8Aux (utf16Offset : Nat) (s : String) (charIdx bytePos utf16Pos : Nat) : Nat

Equations

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

def Lapis.VFS.Position.utf8BytesUpToChar (s : String) (charIdx : Nat) : Nat

Get the UTF-8 byte length up to a character index

Equations

• Lapis.VFS.Position.utf8BytesUpToChar s charIdx = Lapis.VFS.Position.utf8BytesUpToChar.bytesUpToCharAux charIdx s 0 0

@[irreducible]

def Lapis.VFS.Position.utf8BytesUpToChar.bytesUpToCharAux (charIdx : Nat) (s : String) (idx bytes : Nat) : Nat

Equations

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

LSP Position Type

structure Lapis.VFS.Position.LspPosition : Type

LSP Position (0-indexed line and UTF-16 character offset)

• line : Nat
• character : Nat

instance Lapis.VFS.Position.instInhabitedLspPosition : Inhabited LspPosition

Equations

• Lapis.VFS.Position.instInhabitedLspPosition = { default := Lapis.VFS.Position.instInhabitedLspPosition.default }

def Lapis.VFS.Position.instInhabitedLspPosition.default : LspPosition

Equations

• Lapis.VFS.Position.instInhabitedLspPosition.default = { line := default, character := default }

def Lapis.VFS.Position.instReprLspPosition.repr : LspPosition → Nat → Std.Format

Equations

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

instance Lapis.VFS.Position.instReprLspPosition : Repr LspPosition

Equations

• Lapis.VFS.Position.instReprLspPosition = { reprPrec := Lapis.VFS.Position.instReprLspPosition.repr }

instance Lapis.VFS.Position.instBEqLspPosition : BEq LspPosition

Equations

• Lapis.VFS.Position.instBEqLspPosition = { beq := Lapis.VFS.Position.instBEqLspPosition.beq }

def Lapis.VFS.Position.instBEqLspPosition.beq : LspPosition → LspPosition → Bool

Equations

• Lapis.VFS.Position.instBEqLspPosition.beq { line := a, character := a_1 } { line := b, character := b_1 } = (a == b && a_1 == b_1)
• Lapis.VFS.Position.instBEqLspPosition.beq x✝¹ x✝ = false

structure Lapis.VFS.Position.LspRange : Type

LSP Range

• start : LspPosition
• end : LspPosition

instance Lapis.VFS.Position.instInhabitedLspRange : Inhabited LspRange

Equations

• Lapis.VFS.Position.instInhabitedLspRange = { default := Lapis.VFS.Position.instInhabitedLspRange.default }

def Lapis.VFS.Position.instInhabitedLspRange.default : LspRange

Equations

• Lapis.VFS.Position.instInhabitedLspRange.default = { start := default, «end» := default }

instance Lapis.VFS.Position.instReprLspRange : Repr LspRange

Equations

• Lapis.VFS.Position.instReprLspRange = { reprPrec := Lapis.VFS.Position.instReprLspRange.repr }

def Lapis.VFS.Position.instReprLspRange.repr : LspRange → Nat → Std.Format

Equations

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

instance Lapis.VFS.Position.instBEqLspRange : BEq LspRange

Equations

• Lapis.VFS.Position.instBEqLspRange = { beq := Lapis.VFS.Position.instBEqLspRange.beq }

def Lapis.VFS.Position.instBEqLspRange.beq : LspRange → LspRange → Bool

Equations

• Lapis.VFS.Position.instBEqLspRange.beq { start := a, «end» := a_1 } { start := b, «end» := b_1 } = (a == b && a_1 == b_1)
• Lapis.VFS.Position.instBEqLspRange.beq x✝¹ x✝ = false

def Lapis.VFS.Position.LspPosition.zero : LspPosition

Equations

• Lapis.VFS.Position.LspPosition.zero = { line := 0, character := 0 }

def Lapis.VFS.Position.LspRange.empty : LspRange

Equations

• Lapis.VFS.Position.LspRange.empty = { start := Lapis.VFS.Position.LspPosition.zero, «end» := Lapis.VFS.Position.LspPosition.zero }

def Lapis.VFS.Position.LspRange.point (pos : LspPosition) : LspRange

Create a range from a single position (zero-width)

Equations

• Lapis.VFS.Position.LspRange.point pos = { start := pos, «end» := pos }

Position Conversion Context

structure Lapis.VFS.Position.ConversionContext : Type

Context needed for position conversions

• pieceTable : PieceTable.PieceTableState
• lineIndex : LineIndex.LineIndex

instance Lapis.VFS.Position.instInhabitedConversionContext : Inhabited ConversionContext

Equations

• Lapis.VFS.Position.instInhabitedConversionContext = { default := Lapis.VFS.Position.instInhabitedConversionContext.default }

def Lapis.VFS.Position.instInhabitedConversionContext.default : ConversionContext

Equations

• Lapis.VFS.Position.instInhabitedConversionContext.default = { pieceTable := default, lineIndex := default }

def Lapis.VFS.Position.ConversionContext.getLineContent (ctx : ConversionContext) (line : Nat) : Option String

Get the line content as a string

Equations

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

def Lapis.VFS.Position.ConversionContext.getLineContentTrimmed (ctx : ConversionContext) (line : Nat) : Option String

Get line content up to (but not including) the newline

Equations

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

Position to Byte Offset

def Lapis.VFS.Position.positionToByteOffset (ctx : ConversionContext) (pos : LspPosition) : Option Nat

Convert an LSP position to a byte offset

Equations

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

def Lapis.VFS.Position.byteOffsetToPosition (ctx : ConversionContext) (byteOffset : Nat) : LspPosition

Convert a byte offset to an LSP position

Equations

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

Range Conversions

def Lapis.VFS.Position.rangeToByteRange (ctx : ConversionContext) (range : LspRange) : Option (Nat × Nat)

Convert an LSP range to a byte range

Equations

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

def Lapis.VFS.Position.byteRangeToRange (ctx : ConversionContext) (startByte endByte : Nat) : LspRange

Convert a byte range to an LSP range

Equations

• Lapis.VFS.Position.byteRangeToRange ctx startByte endByte = { start := Lapis.VFS.Position.byteOffsetToPosition ctx startByte, «end» := Lapis.VFS.Position.byteOffsetToPosition ctx endByte }

Offset Utilities

def Lapis.VFS.Position.clampOffset (ctx : ConversionContext) (offset : Nat) : Nat

Clamp a byte offset to valid document bounds

Equations

• Lapis.VFS.Position.clampOffset ctx offset = min offset ctx.pieceTable.byteLength

def Lapis.VFS.Position.isValidPosition (ctx : ConversionContext) (pos : LspPosition) : Bool

Check if a position is valid for the document

Equations

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

def Lapis.VFS.Position.endPosition (ctx : ConversionContext) : LspPosition

Get the position at the end of the document

Equations

• Lapis.VFS.Position.endPosition ctx = Lapis.VFS.Position.byteOffsetToPosition ctx ctx.pieceTable.byteLength

def Lapis.VFS.Position.endOfLine (ctx : ConversionContext) (line : Nat) : Option LspPosition

Get the position at the end of a specific line

Equations

• Lapis.VFS.Position.endOfLine ctx line = match ctx.getLineContentTrimmed line with | none => none | some content => some { line := line, character := Lapis.VFS.Position.utf16Length content }