From f7decd2d464ab679cb73212fb9674aeb92bfe184 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 24 Nov 2021 11:21:05 +0100 Subject: [PATCH] fix: go to definition for `macro_rules` etc. --- src/Lean/Elab/AuxDef.lean | 2 +- src/Lean/Elab/Macro.lean | 8 ++++---- src/Lean/Elab/MacroRules.lean | 16 ++++++++-------- tests/lean/interactive/goTo.lean | 4 ++++ tests/lean/interactive/goTo.lean.expected.out | 10 ++++++++++ tests/lean/scopedMacros.lean.expected.out | 2 +- 6 files changed, 28 insertions(+), 14 deletions(-) diff --git a/src/Lean/Elab/AuxDef.lean b/src/Lean/Elab/AuxDef.lean index fd7cedc7e2..33cce375b0 100644 --- a/src/Lean/Elab/AuxDef.lean +++ b/src/Lean/Elab/AuxDef.lean @@ -28,5 +28,5 @@ def elabAuxDef : CommandElab let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id elabCommand <| ← `($[$doc?:docComment]? $[$attrs?:attributes]? - def $(mkIdent id):ident : $ty := $body) + def $(mkIdentFrom (mkNullNode suggestion) id):ident : $ty := $body) | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean index 708869a655..c1321de30b 100644 --- a/src/Lean/Elab/Macro.lean +++ b/src/Lean/Elab/Macro.lean @@ -12,7 +12,7 @@ open Lean.Parser.Command @[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro | `($[$doc?:docComment]? $attrKind:attrKind - macro$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* : + macro%$tk$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* : $cat => $rhs) => do let prio ← evalOptPrio prio? let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip @@ -24,16 +24,16 @@ open Lean.Parser.Command So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/ let pat := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind - syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat) + syntax%$tk$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat) let macroRulesCmd ← if rhs.getArgs.size == 1 then -- `rhs` is a `term` let rhs := rhs[0] - `($[$doc?:docComment]? macro_rules | `($pat) => $rhs) + `($[$doc?:docComment]? macro_rules%$tk | `($pat) => $rhs) else -- `rhs` is of the form `` `( $body ) `` let rhsBody := rhs[1] - `($[$doc?:docComment]? macro_rules | `($pat) => `($rhsBody)) + `($[$doc?:docComment]? macro_rules%$tk | `($pat) => `($rhsBody)) return mkNullNode #[stxCmd, macroRulesCmd] | _ => Macro.throwUnsupported diff --git a/src/Lean/Elab/MacroRules.lean b/src/Lean/Elab/MacroRules.lean index e0125c1ff5..a6f047deba 100644 --- a/src/Lean/Elab/MacroRules.lean +++ b/src/Lean/Elab/MacroRules.lean @@ -15,7 +15,7 @@ open Lean.Parser.Command Remark: `k` is the user provided kind with the current namespace included. Recall that syntax node kinds contain the current namespace. -/ -def elabMacroRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do +def elabMacroRulesAux (doc? : Option Syntax) (attrKind tk : Syntax) (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do let alts ← alts.mapM fun alt => match alt with | `(matchAltExpr| | $pats,* => $rhs) => do let pat := pats.elemsAndSeps[0] @@ -36,19 +36,19 @@ def elabMacroRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNode throwErrorAt alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'" | _ => throwUnsupportedSyntax `($[$doc?:docComment]? @[$attrKind:attrKind macro $(Lean.mkIdent k)] - aux_def macroRules $(mkIdent k) : Macro := + aux_def macroRules $(mkIdentFrom tk k) : Macro := fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax) @[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab := adaptExpander fun stx => match stx with - | `($[$doc?:docComment]? $attrKind:attrKind macro_rules $alts:matchAlt*) => + | `($[$doc?:docComment]? $attrKind:attrKind macro_rules%$tk $alts:matchAlt*) => expandNoKindMacroRulesAux alts "macro_rules" fun kind? alts => - `($[$doc?:docComment]? $attrKind:attrKind macro_rules $[(kind := $(mkIdent <$> kind?))]? $alts:matchAlt*) - | `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) | $x:ident => $rhs) => + `($[$doc?:docComment]? $attrKind:attrKind macro_rules%$tk $[(kind := $(mkIdent <$> kind?))]? $alts:matchAlt*) + | `($[$doc?:docComment]? $attrKind:attrKind macro_rules%$tk (kind := $kind) | $x:ident => $rhs) => `($[$doc?:docComment]? @[$attrKind:attrKind macro $kind] - aux_def macroRules $kind : Macro := fun $x:ident => $rhs) - | `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) $alts:matchAlt*) => - do elabMacroRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) alts + aux_def $(mkIdentFrom tk kind.getId) $kind : Macro := fun $x:ident => $rhs) + | `($[$doc?:docComment]? $attrKind:attrKind macro_rules%$tk (kind := $kind) $alts:matchAlt*) => + do elabMacroRulesAux doc? attrKind tk (← resolveSyntaxKind kind.getId) alts | _ => throwUnsupportedSyntax end Lean.Elab.Command diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean index 899664ada7..5882374e2f 100644 --- a/tests/lean/interactive/goTo.lean +++ b/tests/lean/interactive/goTo.lean @@ -52,3 +52,7 @@ example : Nat := --^ textDocument/definition where b := 2 + +macro_rules | `(test) => `(3) +#check test + --^ textDocument/definition diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out index 69e46bf30b..b8a7d1fd6e 100644 --- a/tests/lean/interactive/goTo.lean.expected.out +++ b/tests/lean/interactive/goTo.lean.expected.out @@ -105,3 +105,13 @@ {"start": {"line": 53, "character": 2}, "end": {"line": 53, "character": 3}}, "originSelectionRange": {"start": {"line": 50, "character": 6}, "end": {"line": 50, "character": 7}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 56, "character": 7}} +[{"targetUri": "file://goTo.lean", + "targetSelectionRange": + {"start": {"line": 55, "character": 0}, "end": {"line": 55, "character": 11}}, + "targetRange": + {"start": {"line": 55, "character": 0}, "end": {"line": 55, "character": 29}}, + "originSelectionRange": + {"start": {"line": 56, "character": 7}, + "end": {"line": 56, "character": 11}}}] diff --git a/tests/lean/scopedMacros.lean.expected.out b/tests/lean/scopedMacros.lean.expected.out index eaeb8cf436..08d8154d9e 100644 --- a/tests/lean/scopedMacros.lean.expected.out +++ b/tests/lean/scopedMacros.lean.expected.out @@ -2,7 +2,7 @@ scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!' 10 + 1 : Nat scopedMacros.lean:19:0-19:50: error: scoped attributes must be used inside namespaces -scopedMacros.lean:19:0-19:50: error: invalid syntax node kind 'termBla!_' +scopedMacros.lean:19:7-19:50: error: invalid syntax node kind 'termBla!_' scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!' scopedMacros.lean:36:0-36:45: error: scoped attributes must be used inside namespaces 10 + 20 : Nat