diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 0934e6bfd3..d40b951713 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -264,16 +264,15 @@ def expandMutualElement : Macro := fun stx => do for elem in stx[1].getArgs do -- Don't trigger the `expandNamespacedDecl` macro, the namespace is handled by the mutual def -- elaborator directly instead - if elem.isOfKind ``Parser.Command.declaration then - continue - match (← expandMacro? elem) with - | some elemNew => - if elemNew.isOfKind nullKind then - elemsNew := elemsNew ++ elemNew.getArgs - else - elemsNew := elemsNew.push elemNew - modified := true - | none => elemsNew := elemsNew.push elem + if !elem.isOfKind ``Parser.Command.declaration then + if let some elemNew ← expandMacro? elem then + if elemNew.isOfKind nullKind then + elemsNew := elemsNew ++ elemNew.getArgs + else + elemsNew := elemsNew.push elemNew + modified := true + continue + elemsNew := elemsNew.push elem if modified then return stx.setArg 1 (mkNullNode elemsNew) else diff --git a/tests/lean/run/10687.lean b/tests/lean/run/10687.lean new file mode 100644 index 0000000000..21fa0cac65 --- /dev/null +++ b/tests/lean/run/10687.lean @@ -0,0 +1,48 @@ +import Lean + +/-! Macros in `mutual` should preserve remaining `mutual` items. -/ + +open Lean Elab Command Lean.PrettyPrinter + +private def trace [Repr α] (name : String) (p : IO α) : IO α := do + IO.println s!"tracing: {name}" + p + +syntax (name := traced) "#traced " declModifiers "def " ident optDeclSig " := " term : command + +@[macro traced] def elabTracedDef : Macro := fun stx => do + match stx with + | `(command| #traced $mods:declModifiers def $name:ident $sig:optDeclSig := $body:term) => do + let nameStr := name.getId.toString + let name_ := mkIdent (name.getId.appendAfter "_") + let args := sig.raw[0].getArgs + let mut argNames := #[] + for arg in args do + argNames := argNames.push (mkIdent (arg[1][0].getId)) + -- Generate the first definition: def foo_ : Type := body + let def1 := ← `(command| $mods:declModifiers def $name_ $sig:optDeclSig := $body) + -- Generate the second definition: def foo : Type := trace "foo" foo_ + let traceCall := ← `(trace $(quote nameStr) ($name_ $[ $argNames:ident ]*)) + let def2 := ← `(command| $mods:declModifiers def $name $sig:optDeclSig := $traceCall) + let res <- `($def1:command + $def2:command) + dbg_trace "{res.raw.prettyPrint}" + return res + | _ => Macro.throwUnsupported + +#traced +def foo (x : IO Nat) : IO Nat := x + +#eval foo (pure 5) + +mutual + +--#traced +private partial def baz (x : IO Nat) : IO Nat := + bar (pure 7) + +#traced -- this previously discarded `baz` +private partial def bar (x : IO Nat) : IO Nat := + baz (pure 5) + +end -- mutual