Macro using ← notation

Stream: lean4

[Parth Shastri]

I want to define a macro which expands into something of the form ← e. However, I am getting an error saying that it must be nested inside a do expression. Is there a way to write such a macro?

macro "yield " t:term : term => `(← M.yield $t)

#check do _ := ← M.yield ()
#check do _ := yield () -- invalid use of `(<- ...)`, must be nested inside a 'do' expression

[Marcus Rossel]

Does it work if you have your macro return a doElem instead of a term?

macro "yield " t:term : doElem => `(← M.yield $t)

[Parth Shastri]

No, I want to use the macro in term position. Here's another example:

structure State

def foo : State → State
  | s => s

def bar : State → StateM State Unit
  | _ => return ()

macro "getFooState" : term => `(return foo (← getThe State))

macro "fooState" : term => `(foo (← getThe State))

#check do bar (foo (← getThe State))
#check do bar (← getFooState) -- this works, but still requires wrapping with (← _)
#check do bar fooState -- invalid use of `(<- ...)`, must be nested inside a 'do' expression

[Parth Shastri]

I figured out a hacky way to do this. I'm not yet sure how to make it extensible, as right now it requires declaring ahead of time all of the macros that are to be pre-expanded.

structure State

def foo : State → State
  | s => s

def bar : State → StateM State Unit
  | _ => return ()

macro (name := fooStateMacro) "fooState" : term => `(foo (← getThe State))


def doMacros : NameSet := .ofList [``fooStateMacro]

partial def expandDoMacros (stx : Syntax) : MacroM Syntax :=
  match stx with
  | .node info kind args => do
    if doMacros.contains kind then
      if let some stx := ← expandMacro? stx then
        return ← expandDoMacros stx
    return .node info kind (← args.mapM expandDoMacros)
  | _ => return stx

macro (name := processedDoMacros) "processedDoMacros% " t:term : term => return t

def processDoMacros (stx : TSyntax `term) : MacroM (TSyntax `term) :=
  if stx.raw.getKind == ``processedDoMacros
  then throw .unsupportedSyntax
  else do `(processedDoMacros% $(⟨← expandDoMacros stx⟩))

macro_rules | `(doElem| return $t) => do `(doElem| return $(← processDoMacros t))
-- macro_rules | `(doElem| $t:term) => do `(doElem| $(← processDoMacros t))
macro_rules | `(doElem| $t:term) => return .node1 (← MonadRef.mkInfoFromRefPos) `Lean.Parser.Term.doExpr (← processDoMacros t)


#check do bar (foo (← getThe State))
#check do bar fooState
#check return ← bar (foo (← getThe State))
#check return ← bar fooState

[Chris Bailey]

Macro expansion and elaboration are interleaved, and I think the built-in parsers and elaborators happen to be written in a way that makes bolting on this specific extension inconvenient. The arrow part of your expansion (← getThe State) gets parsed as a liftMethod and the builtin term elaborator for that is set to throw the error you're getting if it's elaborated outside of the other do machinery.

[Florin Dinu]

Hi! I'm new to Lean, I've installed it and can't run a simple script (both with nightly and stable toolchains). I've made a file called test.lean in which I wrote 2 lines

import Leanpkg
#eval Leanpkg.leanVersionString

When I run lean test.lean I get

test.lean:1:0: error: unknown package 'Leanpkg'
test.lean:2:6: error: unknown identifier 'Leanpkg.leanVersionString'
test.lean:2:0: error: unknown constant 'sorryAx'

[Kevin Buzzard]

This is a thread about macros using certain notation. Can you ask your question in a new thread?

[Florin Dinu]

Kevin Buzzard said:

This is a thread about macros using certain notation. Can you ask your question in a new thread?

Sorry, I'm new to Zulip Chat, didn't know this is a thread.

[James Gallicchio]

Maybe when the do notation is eventually rewritten, it'll become easier to extend :fingers_crossed:

[Parth Shastri]

The essence of my workaround is a way to mark a macro as needing to be expanded before do notation is elaborated (doMacros is the list of such macros). While this allows creating term macros that expands to uses of ←, it is still very limited.