Source Location

Stream: lean4

[Henrik Böving]

Do we have a macro or elab thingy that elaborate to the Nat or whatever type of where they are in the source file?

[Kyle Miller]

I didn't see one in core, but here's at least something:

import Lean

open Lean

instance : ToExpr String.Pos where
  toTypeExpr := .const ``String.Pos []
  toExpr e := .app (.const ``String.Pos.mk []) (toExpr e.byteIdx)

elab "pos%" : term => do
  let r ← getRef
  return toExpr r.getPos?

#check pos%
-- some { byteIdx := 243 } : Option String.Pos

[Henrik Böving]

Hmm, can we get a line and maybe a col number as well? Possibly even the file name? :D I want to write a thing that fails and says where it failed.

[Mac Malone]

@Henrik Böving Expanded example:

import Lean.Elab.ElabRules

open Lean in
elab "pos%" : term => do
  let some pos := (← getRef).getPos?
    | throwError "no source info"
  let pos := (← getFileMap).toPosition pos
  return toExpr (← getFileName, pos)

#eval pos% -- ("path/to/module.lean", { line := 10, column := 6 })

[Henrik Böving]

Mac Malone said:

Henrik Böving Expanded example:

import Lean.Elab.ElabRules

open Lean in
elab "pos%" : term => do
  let some pos := (← getRef).getPos?
    | throwError "no source info"
  let pos := (← getFileMap).toPosition pos
  return toExpr (← getFileName, pos)

#eval pos% -- ("path/to/module.lean", { line := 10, column := 6 })

so that's what filemap is good for :D I've wondered this ever since I passed it through in doc-gen