Documentation

Lean.Data.Position

structure Lean.Position :

Type

line : Nat
column : Nat

instance Lean.instDecidableEqPosition :

DecidableEq Lean.Position

Equations

Lean.instDecidableEqPosition = [anonymous]

instance Lean.instReprPosition :

Repr Lean.Position

Equations

Lean.instReprPosition = { reprPrec := [anonymous] }

instance Lean.instInhabitedPosition :

Inhabited Lean.Position

Equations

Lean.instInhabitedPosition = { default := { line := default, column := default } }

def Lean.Position.lt :

Lean.Position → Lean.Position → Bool

Equations

Lean.Position.lt x x = match x, x with | { line := l₁, column := c₁ }, { line := l₂, column := c₂ } => decide ((l₁, c₁) < (l₂, c₂))

instance Lean.Position.instToFormatPosition :

Lean.ToFormat Lean.Position

Equations

Lean.Position.instToFormatPosition = { format := fun x => match x with | { line := l, column := c } => Std.Format.text "⟨" ++ Lean.format l ++ Std.Format.text ", " ++ Lean.format c ++ Std.Format.text "⟩" }

instance Lean.Position.instToStringPosition :

ToString Lean.Position

Equations

Lean.Position.instToStringPosition = { toString := fun x => match x with | { line := l, column := c } => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩" }

instance Lean.Position.instToExprPosition :

Lean.ToExpr Lean.Position

Equations

Lean.Position.instToExprPosition = { toExpr := fun p => Lean.mkAppN (Lean.mkConst `Lean.Position.mk) #[Lean.toExpr p.line, Lean.toExpr p.column], toTypeExpr := Lean.mkConst `Lean.Position }

structure Lean.FileMap :

Type

source : String
positions : Array String.Pos
lines : Array Nat

instance Lean.instInhabitedFileMap :

Inhabited Lean.FileMap

Equations

Lean.instInhabitedFileMap = { default := { source := default, positions := default, lines := default } }

class Lean.MonadFileMap (m : Type → Type) :

Type

getFileMap : m Lean.FileMap

Instances

Lean.Elab.MonadLog.toMonadFileMap

def Lean.FileMap.ofString (s : String) :

Equations

Lean.FileMap.ofString s = (fun loop => loop 0 1 #[0] #[1]) (Lean.FileMap.ofString.loop s)

partial def Lean.FileMap.ofString.loop (s : String) (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) :

def Lean.FileMap.toPosition (fmap : Lean.FileMap) (pos : String.Pos) :

Equations

Lean.FileMap.toPosition fmap pos = match fmap with | { source := str, positions := ps, lines := lines } => if (decide (Array.size ps ≥ 2) && decide (pos ≤ Array.back ps)) = true then (fun toColumn => (fun loop => loop 0 (Array.size ps - 1)) (Lean.FileMap.toPosition.loop pos str ps lines)) (Lean.FileMap.toPosition.toColumn pos str) else if Array.isEmpty lines = true then { line := 0, column := 0 } else { line := Array.back lines, column := pos - Array.back ps }

partial def Lean.FileMap.toPosition.toColumn (pos : String.Pos) (str : String) (i : String.Pos) (c : Nat) :

partial def Lean.FileMap.toPosition.loop (pos : String.Pos) (str : String) (ps : Array String.Pos) (lines : Array Nat) (b : Nat) (e : Nat) :

def String.toFileMap (s : String) :

Equations

String.toFileMap s = Lean.FileMap.ofString s