position dependent macros

Stream: lean4

[Mario Carneiro]

One nice thing about the rust panic! macro (and other macros like it) is that it will report the file position of the macro call itself along with the panic message. I'm wondering what it would take to do something like this in lean 4. Here's my attempt:

import Lean
open Lean

macro:max "throw!"%tk interpStr:interpolatedStr(term) : term => do
  let head := Syntax.mkStrLit $ match tk.getPos? with
  | none => "[?]: "
  | some x => s!"[{x}]: "
  let str ← interpStr.expandInterpolatedStr (← `(String)) (← `(toString))
  `(throwError (($head : MessageData) ++ $str))

def foo : CoreM Unit := throw!"nope"
                           -- ^ this is character 343
#eval foo -- [343]: nope

This is okay, but I would much rather get a line number than a byte position in the file, and I'm not sure how to get that info out of MacroM

[Mario Carneiro]

(it's also not clear to me why the position I get is the beginning of the string instead of the throw! token)

[Wojciech Nawrocki]

I wanna say this is currently impossible because MacroM does not contain a FileMap. Probably a way to turn String.Pos into a position could be added to Methods, but why not use a custom elaborator like panic!?

[Mac]

To elaborate on @Wojciech Nawrocki point. The fileMap of a source file is available through an InputContext. Said fileMap has a method toPosition that converts a String.Pos to a Position that consists of a line and column number. An example of this being used in Parsers can be seen here: in toErrorMsg. Unfortunately, neither the InputContext nor an alternative method of producing Position from String.Pos is available to macros.

[Mario Carneiro]

Okay, this is slightly improved:

import Lean
open Lean

elab:max "throw!" interpStr:interpolatedStr(term) : term <= ty => do
  let pos ← Elab.getRefPosition
  let head := Syntax.mkStrLit $ mkErrorStringWithPos (← read).fileName pos ""
  let str ← Elab.liftMacroM <| interpStr.expandInterpolatedStr (← `(String)) (← `(toString))
  Elab.Term.elabTerm (← `(throwError (($head : MessageData) ++ $str))) ty

def foo : CoreM Unit := throw!"nope"

#eval foo -- <input>:10:24: nope

Unfortunately it seems the provided file name is a dummy

[Wojciech Nawrocki]

Try running that from the command line :) <input> is used by the LSP server. I guess we can use the real URI there, although sometimes it is a weird virtual one.