Unexpected macro rule firing?

Stream: lean4

[Siddharth Bhat]

Consider the use of macros:

import Lean.Parser
import Init.Data.List
open Lean.Parser
open Std

declare_syntax_cat mlir_type
syntax "i" numLit : mlir_type -- this rule causes problems!

inductive MLIRTy : Type where
| int : Int -> MLIRTy

syntax "[mlir_type|" mlir_type "]": term

macro_rules
  | `([mlir_type| i $x:numLit ]) => `(MLIRTy.int $x)

def tyfoo : MLIRTy := [mlir_type| i 42]
#print tyfoo

def foo (xs: List Int) : IO Unit :=
  xs.forM $ fun i => do
    if i > 0 then IO.println ", "
    IO.println i

Surprisingly to me, the line xs.forM $ fun i => do creates a compile error:

foo.lean:22:16: error: expected '[', '_', '{', '|', '⦃', identifier or term

I don't understand why the elaborator attempts to elaborate the i at fun i => ... As far as I can tell, the i is not followed b a numLit, and thus the rule should not fire?

I'm on a recent nightly:

/tmp$ ~/work/lean4-contrib/build/stage1/bin/lean --version
Lean (version 4.0.0, commit 988e43d2b4a2, Release)

[Gabriel Ebner]

Writing "i" in a syntax declaration will register it as a keyword, i.e., it will no longer be parsed as an identifier. In this case however, there's no need to make it a keyword, you can also match on identifiers: https://github.com/leanprover/lean4/blob/master/tests/lean/nonReserved.lean

[Gabriel Ebner]

Mmmh, apparently writing &"i" numLit doesn't help here either. But ident numLit works.

[Siddharth Bhat]

Thank you for the pointer! Why doesn't &"i" work, though? I'm trying to build a mental model of how the macro system works!

[Jannis Limperg]

Syntax categories declared with declare_syntax_cat do not dispatch rules starting with &"stuff" correctly. To do this, a syntax category must have its LeadingIdentBehavior set to LeadingIdentBehavior.both or LeadingIdentBehavior.symbol, but declare_syntax_cat doesn't allow you to do this (at least last I checked). Here's a variant of declare_syntax_cat that exposes the option:

namespace Lean.Elab.Command

syntax (name := syntaxCatWithUnreservedTokens)
  "declare_syntax_cat' " ident
    (&"allow_leading_unreserved_tokens" <|> &"force_leading_unreserved_tokens")? : command

-- Copied from Lean/Elab/Syntax.lean
private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
  if let Name.str _ suffix _ := catName then
    let quotSymbol := "`(" ++ suffix ++ "|"
    let name := catName ++ `quot
    -- TODO(Sebastian): this might confuse the pretty printer, but it lets us reuse the elaborator
    let kind := ``Lean.Parser.Term.quot
    let cmd ← `(
      @[termParser] def $(mkIdent name) : Lean.ParserDescr :=
        Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec)
          (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
            (Lean.ParserDescr.binary `andthen
              (Lean.ParserDescr.unary `incQuotDepth (Lean.ParserDescr.cat $(quote catName) 0))
              (Lean.ParserDescr.symbol ")"))))
    elabCommand cmd

open Lean.Parser (LeadingIdentBehavior) in
@[commandElab syntaxCatWithUnreservedTokens]
def elabDeclareSyntaxCatWithUnreservedTokens : CommandElab := fun stx => do
  let catName  := stx[1].getId
  let leadingIdentBehavior :=
    match stx[2].getOptional? with
    | none => LeadingIdentBehavior.default
    | some b =>
      match b.getAtomVal! with
      | "allow_leading_unreserved_tokens" => LeadingIdentBehavior.both
      | "force_leading_unreserved_tokens" => LeadingIdentBehavior.symbol
      | _ => unreachable!
  let attrName := catName.appendAfter "Parser"
  let env ← getEnv
  let env ←
    liftIO $ Parser.registerParserCategory env attrName catName
      leadingIdentBehavior
  setEnv env
  declareSyntaxCatQuotParser catName

end Lean.Elab.Command

[Sebastian Ullrich]

declare_syntax_cat conv (behavior := both)

from Init.Conv

[Jannis Limperg]

Oh nice so I can delete that code. :)