Snapshot Types

inductive Lapis.VFS.Document.SnapshotReason : Type

Reason for creating a snapshot

• documentOpen : SnapshotReason
• preBatch : SnapshotReason
• analysisCheckpoint : SnapshotReason
• clientRequest : SnapshotReason

instance Lapis.VFS.Document.instInhabitedSnapshotReason : Inhabited SnapshotReason

Equations

• Lapis.VFS.Document.instInhabitedSnapshotReason = { default := Lapis.VFS.Document.instInhabitedSnapshotReason.default }

def Lapis.VFS.Document.instInhabitedSnapshotReason.default : SnapshotReason

Equations

• Lapis.VFS.Document.instInhabitedSnapshotReason.default = Lapis.VFS.Document.SnapshotReason.documentOpen

instance Lapis.VFS.Document.instBEqSnapshotReason : BEq SnapshotReason

Equations

• Lapis.VFS.Document.instBEqSnapshotReason = { beq := Lapis.VFS.Document.instBEqSnapshotReason.beq }

def Lapis.VFS.Document.instBEqSnapshotReason.beq : SnapshotReason → SnapshotReason → Bool

Equations

• Lapis.VFS.Document.instBEqSnapshotReason.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Lapis.VFS.Document.instReprSnapshotReason.repr : SnapshotReason → Nat → Std.Format

Equations

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

instance Lapis.VFS.Document.instReprSnapshotReason : Repr SnapshotReason

Equations

• Lapis.VFS.Document.instReprSnapshotReason = { reprPrec := Lapis.VFS.Document.instReprSnapshotReason.repr }

structure Lapis.VFS.Document.SnapshotId : Type

Unique identifier for a snapshot

• id : Nat

instance Lapis.VFS.Document.instInhabitedSnapshotId : Inhabited SnapshotId

Equations

• Lapis.VFS.Document.instInhabitedSnapshotId = { default := Lapis.VFS.Document.instInhabitedSnapshotId.default }

def Lapis.VFS.Document.instInhabitedSnapshotId.default : SnapshotId

Equations

• Lapis.VFS.Document.instInhabitedSnapshotId.default = { id := default }

instance Lapis.VFS.Document.instBEqSnapshotId : BEq SnapshotId

Equations

• Lapis.VFS.Document.instBEqSnapshotId = { beq := Lapis.VFS.Document.instBEqSnapshotId.beq }

def Lapis.VFS.Document.instBEqSnapshotId.beq : SnapshotId → SnapshotId → Bool

Equations

• Lapis.VFS.Document.instBEqSnapshotId.beq { id := a } { id := b } = (a == b)
• Lapis.VFS.Document.instBEqSnapshotId.beq x✝¹ x✝ = false

instance Lapis.VFS.Document.instReprSnapshotId : Repr SnapshotId

Equations

• Lapis.VFS.Document.instReprSnapshotId = { reprPrec := Lapis.VFS.Document.instReprSnapshotId.repr }

def Lapis.VFS.Document.instReprSnapshotId.repr : SnapshotId → Nat → Std.Format

Equations

• Lapis.VFS.Document.instReprSnapshotId.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

instance Lapis.VFS.Document.instHashableSnapshotId : Hashable SnapshotId

Equations

• Lapis.VFS.Document.instHashableSnapshotId = { hash := Lapis.VFS.Document.instHashableSnapshotId.hash }

def Lapis.VFS.Document.instHashableSnapshotId.hash : SnapshotId → UInt64

Equations

• Lapis.VFS.Document.instHashableSnapshotId.hash { id := a } = mixHash 0 (hash a)

def Lapis.VFS.Document.instDecidableEqSnapshotId.decEq (x✝ x✝¹ : SnapshotId) : Decidable (x✝ = x✝¹)

Equations

• Lapis.VFS.Document.instDecidableEqSnapshotId.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Lapis.VFS.Document.instDecidableEqSnapshotId : DecidableEq SnapshotId

Equations

• Lapis.VFS.Document.instDecidableEqSnapshotId = Lapis.VFS.Document.instDecidableEqSnapshotId.decEq

def Lapis.VFS.Document.SnapshotId.zero : SnapshotId

Equations

• Lapis.VFS.Document.SnapshotId.zero = { id := 0 }

def Lapis.VFS.Document.SnapshotId.next (id : SnapshotId) : SnapshotId

Equations

• id.next = { id := id.id + 1 }

structure Lapis.VFS.Document.Snapshot : Type

A snapshot of document state at a point in time

• id : SnapshotId
• reason : SnapshotReason
• pieceTable : PieceTable.PieceTableState
• lineIndex : LineIndex.LineIndex
• version : Int
• refCount : Nat

def Lapis.VFS.Document.instInhabitedSnapshot.default : Snapshot

Equations

• Lapis.VFS.Document.instInhabitedSnapshot.default = { id := default, reason := default, pieceTable := default, lineIndex := default, version := default, refCount := default }

instance Lapis.VFS.Document.instInhabitedSnapshot : Inhabited Snapshot

Equations

• Lapis.VFS.Document.instInhabitedSnapshot = { default := Lapis.VFS.Document.instInhabitedSnapshot.default }

def Lapis.VFS.Document.Snapshot.create (id : SnapshotId) (reason : SnapshotReason) (pt : PieceTable.PieceTableState) (li : LineIndex.LineIndex) (version : Int) : Snapshot

Create a new snapshot from current document state

Equations

• Lapis.VFS.Document.Snapshot.create id reason pt li version = { id := id, reason := reason, pieceTable := pt, lineIndex := li, version := version, refCount := 0 }

def Lapis.VFS.Document.Snapshot.acquire (s : Snapshot) : Snapshot

Increment reference count

Equations

• s.acquire = { id := s.id, reason := s.reason, pieceTable := s.pieceTable, lineIndex := s.lineIndex, version := s.version, refCount := s.refCount + 1 }

def Lapis.VFS.Document.Snapshot.release (s : Snapshot) : Snapshot

Decrement reference count

Equations

• s.release = { id := s.id, reason := s.reason, pieceTable := s.pieceTable, lineIndex := s.lineIndex, version := s.version, refCount := if s.refCount > 0 then s.refCount - 1 else 0 }

def Lapis.VFS.Document.Snapshot.canPrune (s : Snapshot) : Bool

Check if snapshot can be pruned

Equations

• s.canPrune = (s.refCount == 0)

Document State

structure Lapis.VFS.Document.Document : Type

Complete state of a single document

• uri : String
• languageId : String
• version : Int
• pieceTable : PieceTable.PieceTableState
• lineIndex : LineIndex.LineIndex
• nextSnapshotId : Nat
• snapshots : Array Snapshot

def Lapis.VFS.Document.instInhabitedDocument.default : Document

Equations

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

instance Lapis.VFS.Document.instInhabitedDocument : Inhabited Document

Equations

• Lapis.VFS.Document.instInhabitedDocument = { default := Lapis.VFS.Document.instInhabitedDocument.default }

def Lapis.VFS.Document.Document.create (uri languageId : String) (version : Int) (content : String) : Document

Create a new document from initial content

Equations

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

def Lapis.VFS.Document.Document.byteLength (doc : Document) : Nat

Get total byte length of document

Equations

• doc.byteLength = doc.pieceTable.byteLength

def Lapis.VFS.Document.Document.lineCount (doc : Document) : Nat

Get total line count

Equations

• doc.lineCount = doc.lineIndex.lineCount

def Lapis.VFS.Document.Document.getContent (doc : Document) : String

Get full document content as string

Equations

• doc.getContent = doc.pieceTable.getContent

def Lapis.VFS.Document.Document.conversionContext (doc : Document) : Position.ConversionContext

Create a conversion context for position operations

Equations

• doc.conversionContext = { pieceTable := doc.pieceTable, lineIndex := doc.lineIndex }

Text Operations

def Lapis.VFS.Document.Document.getTextByteRange (doc : Document) (startByte endByte : Nat) : String

Get text in a byte range

Equations

• doc.getTextByteRange startByte endByte = doc.pieceTable.getTextByteRange startByte endByte

def Lapis.VFS.Document.Document.getLine (doc : Document) (line : Nat) : Option String

Get text for a specific line

Equations

• doc.getLine line = doc.conversionContext.getLineContentTrimmed line

def Lapis.VFS.Document.Document.getText (doc : Document) (range : Position.LspRange) : Option String

Get text in an LSP range

Equations

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

Edit Operations

def Lapis.VFS.Document.Document.applyByteEdit (doc : Document) (startByte endByte : Nat) (newText : String) (newVersion : Int) : Document

Apply a single edit at a byte range

Equations

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

def Lapis.VFS.Document.Document.applyEdit (doc : Document) (range : Position.LspRange) (newText : String) (newVersion : Int) : Document

Apply an edit using LSP positions

Equations

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

def Lapis.VFS.Document.Document.applyEdits (doc : Document) (edits : List (Position.LspRange × String)) (newVersion : Int) : Document

Apply multiple edits (must be in reverse document order)

Equations

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

def Lapis.VFS.Document.Document.insertAt (doc : Document) (pos : Position.LspPosition) (text : String) (newVersion : Int) : Document

Insert text at a position

Equations

• doc.insertAt pos text newVersion = doc.applyEdit { start := pos, «end» := pos } text newVersion

def Lapis.VFS.Document.Document.deleteRange (doc : Document) (range : Position.LspRange) (newVersion : Int) : Document

Delete text in a range

Equations

• doc.deleteRange range newVersion = doc.applyEdit range "" newVersion

Position Conversion

def Lapis.VFS.Document.Document.positionToOffset (doc : Document) (pos : Position.LspPosition) : Option Nat

Convert LSP position to byte offset

Equations

• doc.positionToOffset pos = Lapis.VFS.Position.positionToByteOffset doc.conversionContext pos

def Lapis.VFS.Document.Document.offsetToPosition (doc : Document) (offset : Nat) : Position.LspPosition

Convert byte offset to LSP position

Equations

• doc.offsetToPosition offset = Lapis.VFS.Position.byteOffsetToPosition doc.conversionContext offset

Snapshot Operations

def Lapis.VFS.Document.Document.createSnapshot (doc : Document) (reason : SnapshotReason) : Document × SnapshotId

Create a new snapshot of current state

Equations

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

def Lapis.VFS.Document.Document.findSnapshot (doc : Document) (id : SnapshotId) : Option (Nat × Snapshot)

Find a snapshot by ID

Equations

• doc.findSnapshot id = Option.map (fun (idx : Nat) => (idx, doc.snapshots[idx]!)) (Array.findIdx? (fun (x : Lapis.VFS.Document.Snapshot) => x.id == id) doc.snapshots)

def Lapis.VFS.Document.Document.acquireSnapshot (doc : Document) (id : SnapshotId) : Option (Document × Snapshot)

Acquire a snapshot (increment ref count)

Equations

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

def Lapis.VFS.Document.Document.releaseSnapshot (doc : Document) (id : SnapshotId) : Document

Release a snapshot (decrement ref count)

Equations

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

def Lapis.VFS.Document.Document.pruneSnapshots (doc : Document) (keep : Snapshot → Bool := fun (x : Snapshot) => false) : Document

Prune snapshots that are no longer needed

Equations

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

def Lapis.VFS.Document.Document.getSnapshotPieceTable (doc : Document) (id : SnapshotId) : Option PieceTable.PieceTableState

Get the piece table from a snapshot

Equations

• doc.getSnapshotPieceTable id = match doc.findSnapshot id with | none => none | some (fst, snap) => some snap.pieceTable

def Lapis.VFS.Document.Document.getSnapshotLineIndex (doc : Document) (id : SnapshotId) : Option LineIndex.LineIndex

Get the line index from a snapshot

Equations

• doc.getSnapshotLineIndex id = match doc.findSnapshot id with | none => none | some (fst, snap) => some snap.lineIndex

Line Index Management

def Lapis.VFS.Document.Document.rebuildLineIndex (doc : Document) : Document

Force a full rebuild of the line index

Equations

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

def Lapis.VFS.Document.Document.compact (doc : Document) : Document

Compact the piece table (merge adjacent pieces)

Equations

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