@[unbox]

structure Cursor : Type

A position, expressed as a pair of numbers of UTF-8 codepoints (rather than byte indices).

• line : Nat
• col : Nat

@[implicit_reducible]

instance instReprCursor : Repr Cursor

Equations

• instReprCursor = { reprPrec := instReprCursor.repr }

def instReprCursor.repr : Cursor → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance instInhabitedCursor : Inhabited Cursor

Equations

• instInhabitedCursor = { default := instInhabitedCursor.default }

def instDecidableEqCursor.decEq (x✝ x✝¹ : Cursor) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqCursor.decEq { line := a, col := a_1 } { line := b, col := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqCursor : DecidableEq Cursor

Equations

• instDecidableEqCursor = instDecidableEqCursor.decEq

def instBEqCursor.beq : Cursor → Cursor → Bool

Equations

• instBEqCursor.beq { line := a, col := a_1 } { line := b, col := b_1 } = (a == b && a_1 == b_1)
• instBEqCursor.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqCursor : BEq Cursor

Equations

• instBEqCursor = { beq := instBEqCursor.beq }

def instHashableCursor.hash : Cursor → UInt64

Equations

• instHashableCursor.hash { line := a, col := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance instHashableCursor : Hashable Cursor

Equations

• instHashableCursor = { hash := instHashableCursor.hash }

@[implicit_reducible]

instance instOfNatCursorOfNatNat : OfNat Cursor 0

Equations

• instOfNatCursorOfNatNat = { ofNat := { line := 0, col := 0 } }

@[implicit_reducible]

instance instToStringCursor : ToString Cursor

Equations

• instToStringCursor = { toString := fun (cursor : Cursor) => toString cursor.line ++ toString ":" ++ toString (cursor.col + 1) }

def Cursor.lt (c₁ c₂ : Cursor) : Prop

Equations

• c₁.lt c₂ = (c₁.line < c₂.line ∨ c₁.line = c₂.line ∧ c₁.col < c₂.col)

def Cursor.le (c₁ c₂ : Cursor) : Prop

Equations

• c₁.le c₂ = (c₁.lt c₂ ∨ c₁ = c₂)

@[implicit_reducible]

instance instLTCursor : LT Cursor

Equations

• instLTCursor = { lt := Cursor.lt }

@[implicit_reducible]

instance instLECursor : LE Cursor

Equations

• instLECursor = { le := Cursor.le }

@[implicit_reducible]

instance instDecidableLtCursor (c₁ c₂ : Cursor) : Decidable (c₁ < c₂)

Equations

• instDecidableLtCursor c₁ c₂ = if h : c₁.line < c₂.line ∨ c₁.line = c₂.line ∧ c₁.col < c₂.col then isTrue h else isFalse h

@[implicit_reducible]

instance instDecidableEqCursor_1 (c₁ c₂ : Cursor) : Decidable (c₁ = c₂)

Equations

• instDecidableEqCursor_1 c₁ c₂ = if h : c₁.line = c₂.line ∧ c₁.col = c₂.col then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableLeCursor (c₁ c₂ : Cursor) : Decidable (c₁ ≤ c₂)

Equations

• instDecidableLeCursor c₁ c₂ = instDecidableLeCursor._aux_1 c₁ c₂

@[implicit_reducible]

instance instDecidableGtCursor (c₁ c₂ : Cursor) : Decidable (c₁ > c₂)

Equations

• instDecidableGtCursor c₁ c₂ = instDecidableGtCursor._aux_1 c₁ c₂

@[implicit_reducible]

instance instMinCursor : Min Cursor

Equations

• instMinCursor = { min := fun (c₁ c₂ : Cursor) => if c₁ < c₂ then c₁ else c₂ }

@[implicit_reducible]

instance instMaxCursor : Max Cursor

Equations

• instMaxCursor = { max := fun (c₁ c₂ : Cursor) => if c₁ < c₂ then c₂ else c₁ }

structure SourceSpan : Type

• start : Cursor
• end : Cursor

def instReprSourceSpan.repr : SourceSpan → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance instReprSourceSpan : Repr SourceSpan

Equations

• instReprSourceSpan = { reprPrec := instReprSourceSpan.repr }

@[implicit_reducible]

instance instInhabitedSourceSpan : Inhabited SourceSpan

Equations

• instInhabitedSourceSpan = { default := instInhabitedSourceSpan.default }

def instDecidableEqSourceSpan.decEq (x✝ x✝¹ : SourceSpan) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqSourceSpan.decEq { start := a, «end» := a_1 } { start := b, «end» := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqSourceSpan : DecidableEq SourceSpan

Equations

• instDecidableEqSourceSpan = instDecidableEqSourceSpan.decEq

@[implicit_reducible]

instance instBEqSourceSpan : BEq SourceSpan

Equations

• instBEqSourceSpan = { beq := instBEqSourceSpan.beq }

def instBEqSourceSpan.beq : SourceSpan → SourceSpan → Bool

Equations

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

def instHashableSourceSpan.hash : SourceSpan → UInt64

Equations

• instHashableSourceSpan.hash { start := a, «end» := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance instHashableSourceSpan : Hashable SourceSpan

Equations

• instHashableSourceSpan = { hash := instHashableSourceSpan.hash }

@[implicit_reducible]

instance instOfNatSourceSpanOfNatNat : OfNat SourceSpan 0

Equations

• instOfNatSourceSpanOfNatNat = { ofNat := { start := 0, «end» := 0 } }

@[implicit_reducible]

instance instToStringSourceSpan : ToString SourceSpan

Equations

• instToStringSourceSpan = { toString := fun (span : SourceSpan) => toString span.start ++ toString "-" ++ toString span.end }

@[implicit_reducible]

instance instToFormatSourceSpan : Std.ToFormat SourceSpan

Equations

• instToFormatSourceSpan = inferInstance

def SourceSpan.merge (p₁ p₂ : SourceSpan) : SourceSpan

Equations

• p₁.merge p₂ = { start := min p₁.start p₂.start, «end» := max p₁.end p₂.end }

def SourceSpan.placeholder : SourceSpan

A placeholder position for diagnostics with no real one to report against. Not default/(0 : SourceSpan) — both are ⟨⟨0,0⟩,⟨0,0⟩⟩, but every real position in this codebase has 1-indexed lines (lexing starts at ⟨1,0⟩), so line 0 would render a wrong, off-by-one line number. Line 1 points at a real line even though the span itself stays meaningless.

Equations

• SourceSpan.placeholder = { start := { line := 1, col := 0 }, «end» := { line := 1, col := 0 } }

@[implicit_reducible]

instance instAppendSourceSpan : Append SourceSpan

Equations

• instAppendSourceSpan = { append := SourceSpan.merge }

@[reducible, never_extract, inline, implemented_by _private.Common.Position.0.Internal.registerSourceImpl]

abbrev registerSource {α : Type} (x : α) : SourceSpan → α

Equations

• x @@ x✝ = x

def «term_@@_» : Lean.TrailingParserDescr

Equations

• «term_@@_» = Lean.ParserDescr.trailingNode `«term_@@_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " @@ ") (Lean.ParserDescr.cat `term 61))

@[reducible, never_extract, inline, implemented_by _private.Common.Position.0.Internal.posOfImpl]

abbrev posOf {α : Type} (x : α) : SourceSpan

Equations

• posOf x = default

Internal.sourceMap has no clear operation: it grows for the life of the process. This is sound for concurrent compiles as much as sequential ones. No two live values share an address, and posOf requires holding the value to read its position — so whatever holds it is, by definition, not dead, and its slot cannot have been reused by anything else in the meantime.

Values that were never registered are a separate matter this map cannot fix by itself: nullary constructors (Expression.true, Statement.skip) share one tagged-scalar address program-wide and so cannot carry per-occurrence positions this way, and some compiled-in constants have no source span to register at all. Annotation's constructors carry an explicit pos : SourceSpan field instead of using registerSource/posOf, for exactly this reason.

def posIndices : Lean.Parser.Parser

Equations

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

def matchSource : Lean.Parser.Parser

Match arbitrary expressions, together with the positions attached to them. If some expressions may not be attached positions (e.g. proofs), one can specify (indices := [n₁ ... nₙ]) to only match on the positions of the nᵢ-th discriminant (1-based indexing).

Equations

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