From 59b32da2d9aeb254a9bc687b3ef023f5bfda7ddf Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 6 Aug 2022 05:32:56 -0400 Subject: [PATCH] feat: go to def on parser aliases --- src/Lean/Elab/Syntax.lean | 24 ++- src/Lean/Parser.lean | 2 +- src/Lean/Parser/Extension.lean | 5 +- src/Lean/Parser/Extra.lean | 2 +- tests/lean/interactive/hover.lean | 6 +- .../lean/interactive/hover.lean.expected.out | 182 ++++++++++-------- tests/lean/syntaxPrec.lean.expected.out | 3 +- 7 files changed, 130 insertions(+), 94 deletions(-) diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index e65c7ac53e..343c10332e 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -53,11 +53,17 @@ def ensureUnaryOutput (x : Term × Nat) : Term := @[inline] private def withNestedParser (x : ToParserDescr) : ToParserDescr := do withReader (fun ctx => { ctx with leftRec := false, first := false }) x -/-- (Try to) a term info for the category `catName` at `ref`. -/ +/-- (Try to) add a term info for the category `catName` at `ref`. -/ def addCategoryInfo (ref : Syntax) (catName : Name) : TermElabM Unit := do - let declName := ``Lean.Parser.Category ++ catName - if (← getEnv).contains declName then - addTermInfo' ref (Lean.mkConst declName) + let declName := ``Lean.Parser.Category ++ catName + if (← getEnv).contains declName then + addTermInfo' ref (Lean.mkConst declName) + +/-- (Try to) add a term info for the alias with info `info` at `ref`. -/ +def addAliasInfo (ref : Syntax) (info : Parser.ParserAliasInfo) : TermElabM Unit := do + if (← getInfoState).enabled then + if (← getEnv).contains info.declName then + addTermInfo' ref (Lean.mkConst info.declName) def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do let ctx ← read @@ -161,6 +167,7 @@ where processAlias (id : Syntax) (args : Array Syntax) := do let aliasName := id.getId.eraseMacroScopes let info ← Parser.getParserAliasInfo aliasName + addAliasInfo id info let args ← args.mapM (withNestedParser ∘ process) let (args, stackSz) := if let some stackSz := info.stackSz? then if !info.autoGroupArgs then @@ -205,14 +212,14 @@ where let sep := stx[3] let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else ensureUnaryOutput <$> withNestedParser do process stx[4][1] let allowTrailingSep := !stx[5].isNone - return (← `(ParserDescr.sepBy $p $sep $psep $(quote allowTrailingSep)), 1) + return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy) $p $sep $psep $(quote allowTrailingSep)), 1) processSepBy1 (stx : Syntax) := do let p ← ensureUnaryOutput <$> withNestedParser do process stx[1] let sep := stx[3] let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else ensureUnaryOutput <$> withNestedParser do process stx[4][1] let allowTrailingSep := !stx[5].isNone - return (← `(ParserDescr.sepBy1 $p $sep $psep $(quote allowTrailingSep)), 1) + return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy1) $p $sep $psep $(quote allowTrailingSep)), 1) isValidAtom (s : String) : Bool := !s.isEmpty && @@ -235,9 +242,8 @@ where | none => throwUnsupportedSyntax processNonReserved (stx : Syntax) := do - match stx[1].isStrLit? with - | some atom => return (← `(ParserDescr.nonReservedSymbol $(quote atom) false), 1) - | none => throwUnsupportedSyntax + let some atom := stx[1].isStrLit? | throwUnsupportedSyntax + return (← `((with_annotate_term $(stx[0]) @ParserDescr.nonReservedSymbol) $(quote atom) false), 1) end Term diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 80abaea491..6974b1e620 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -42,7 +42,7 @@ builtin_initialize register_parser_alias orelse register_parser_alias andthen { stackSz? := none } - registerAlias "notFollowedBy" (notFollowedBy · "element") + registerAlias "notFollowedBy" ``notFollowedBy (notFollowedBy · "element") Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer Formatter.registerAlias "notFollowedBy" notFollowedBy.formatter diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 7799a4678e..35e724664f 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -210,6 +210,7 @@ def getBinaryAlias {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : I abbrev ParserAliasValue := AliasValue Parser structure ParserAliasInfo where + declName : Name := .anonymous /-- Number of syntax nodes produced by this parser. `none` means "sum of input sizes". -/ stackSz? : Option Nat := some 1 /-- Whether arguments should be wrapped in `group(·)` if they do not produce exactly one syntax node. -/ @@ -223,11 +224,11 @@ def getParserAliasInfo (aliasName : Name) : IO ParserAliasInfo := do return (← parserAliases2infoRef.get).findD aliasName {} -- Later, we define macro `register_parser_alias` which registers a parser, formatter and parenthesizer -def registerAlias (aliasName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) (info : ParserAliasInfo := {}) : IO Unit := do +def registerAlias (aliasName declName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) (info : ParserAliasInfo := {}) : IO Unit := do registerAliasCore parserAliasesRef aliasName p if let some kind := kind? then parserAlias2kindRef.modify (·.insert aliasName kind) - parserAliases2infoRef.modify (·.insert aliasName info) + parserAliases2infoRef.modify (·.insert aliasName { info with declName }) instance : Coe Parser ParserAliasValue := { coe := AliasValue.const } instance : Coe (Parser → Parser) ParserAliasValue := { coe := AliasValue.unary } diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index e365fe6bc6..85a33bd3a6 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -175,7 +175,7 @@ macro_rules let [(fullDeclName, [])] ← Macro.resolveGlobalName declName.getId | Macro.throwError "expected non-overloaded constant name" let aliasName := aliasName?.getD (Syntax.mkStrLit declName.getId.toString) - `(do Parser.registerAlias $aliasName $declName $(info?.getD (Unhygienic.run `({}))) (kind? := some $(kind?.getD (quote fullDeclName))) + `(do Parser.registerAlias $aliasName ``$declName $declName $(info?.getD (Unhygienic.run `({}))) (kind? := some $(kind?.getD (quote fullDeclName))) PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter)) PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer))) diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index f9a80200c0..3266c8348d 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -78,7 +78,11 @@ macro_rules mycmd 1 --^ textDocument/hover -syntax "mycmd'" term : command +syntax "mycmd'" ppSpace sepBy1(term, " + ") : command + --^ textDocument/hover + --^ textDocument/hover + --^ textDocument/hover + /-- My ultimate command -/ elab_rules : command | `(mycmd' $e) => do Lean.Elab.Command.elabCommand (← `(/-- hi -/ @[inline] def hi := $e)) diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 809a18c6c8..ad75a1f40d 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -77,185 +77,209 @@ {"start": {"line": 77, "character": 0}, "end": {"line": 77, "character": 7}}, "contents": {"value": "My way better command ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 85, "character": 2}} + "position": {"line": 80, "character": 16}} {"range": - {"start": {"line": 85, "character": 0}, "end": {"line": 85, "character": 8}}, + {"start": {"line": 80, "character": 16}, "end": {"line": 80, "character": 23}}, + "contents": + {"value": + "```lean\nLean.Parser.ppSpace : Lean.Parser.Parser\n```\n***\nNo-op parser that advises the pretty printer to emit a space/soft line break. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 80, "character": 24}} +{"range": + {"start": {"line": 80, "character": 24}, "end": {"line": 80, "character": 31}}, + "contents": + {"value": + "```lean\nLean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr\n```", + "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 80, "character": 31}} +{"range": + {"start": {"line": 80, "character": 31}, "end": {"line": 80, "character": 35}}, + "contents": + {"value": + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 89, "character": 2}} +{"range": + {"start": {"line": 89, "character": 0}, "end": {"line": 89, "character": 8}}, "contents": {"value": "My ultimate command ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 89, "character": 10}} + "position": {"line": 93, "character": 10}} null {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 93, "character": 8}} + "position": {"line": 97, "character": 8}} {"range": - {"start": {"line": 93, "character": 8}, "end": {"line": 93, "character": 10}}, + {"start": {"line": 97, "character": 8}, "end": {"line": 97, "character": 10}}, "contents": {"value": "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nIdentity function ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 93, "character": 10}} + "position": {"line": 97, "character": 10}} {"range": - {"start": {"line": 93, "character": 8}, "end": {"line": 93, "character": 21}}, + {"start": {"line": 97, "character": 8}, "end": {"line": 97, "character": 21}}, "contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 100, "character": 2}} + "position": {"line": 104, "character": 2}} {"range": - {"start": {"line": 100, "character": 2}, "end": {"line": 100, "character": 3}}, + {"start": {"line": 104, "character": 2}, "end": {"line": 104, "character": 3}}, "contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 107, "character": 9}} + "position": {"line": 111, "character": 9}} {"range": - {"start": {"line": 107, "character": 7}, - "end": {"line": 107, "character": 17}}, + {"start": {"line": 111, "character": 7}, + "end": {"line": 111, "character": 17}}, "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 112, "character": 7}} + "position": {"line": 116, "character": 7}} {"range": - {"start": {"line": 112, "character": 7}, - "end": {"line": 112, "character": 10}}, + {"start": {"line": 116, "character": 7}, + "end": {"line": 116, "character": 10}}, "contents": {"value": "```lean\nBar.foo : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 115, "character": 9}} + "position": {"line": 119, "character": 9}} {"range": - {"start": {"line": 115, "character": 7}, - "end": {"line": 115, "character": 17}}, + {"start": {"line": 119, "character": 7}, + "end": {"line": 119, "character": 17}}, "contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 118, "character": 4}} + "position": {"line": 122, "character": 4}} {"range": - {"start": {"line": 118, "character": 4}, "end": {"line": 118, "character": 7}}, + {"start": {"line": 122, "character": 4}, "end": {"line": 122, "character": 7}}, "contents": {"value": "```lean\nBar.bar : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 121, "character": 10}} + "position": {"line": 125, "character": 10}} {"range": - {"start": {"line": 121, "character": 10}, - "end": {"line": 121, "character": 13}}, + {"start": {"line": 125, "character": 10}, + "end": {"line": 125, "character": 13}}, "contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 121, "character": 17}} + "position": {"line": 125, "character": 17}} {"range": - {"start": {"line": 121, "character": 17}, - "end": {"line": 121, "character": 19}}, + {"start": {"line": 125, "character": 17}, + "end": {"line": 125, "character": 19}}, "contents": {"value": "```lean\nBar.Foo.mk : Nat → Foo\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 124, "character": 2}} + "position": {"line": 128, "character": 2}} {"range": - {"start": {"line": 124, "character": 2}, "end": {"line": 124, "character": 4}}, + {"start": {"line": 128, "character": 2}, "end": {"line": 128, "character": 4}}, "contents": {"value": "```lean\nBar.Foo.hi : Foo → Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 127, "character": 10}} + "position": {"line": 131, "character": 10}} {"range": - {"start": {"line": 127, "character": 10}, - "end": {"line": 127, "character": 13}}, + {"start": {"line": 131, "character": 10}, + "end": {"line": 131, "character": 13}}, "contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 129, "character": 4}} + "position": {"line": 133, "character": 4}} {"range": - {"start": {"line": 129, "character": 4}, "end": {"line": 129, "character": 6}}, + {"start": {"line": 133, "character": 4}, "end": {"line": 133, "character": 6}}, "contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 132, "character": 2}} + "position": {"line": 136, "character": 2}} {"range": - {"start": {"line": 132, "character": 0}, "end": {"line": 132, "character": 8}}, + {"start": {"line": 136, "character": 0}, "end": {"line": 136, "character": 8}}, "contents": {"value": "```lean\nBar.instToStringNat : ToString Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 134, "character": 9}} + "position": {"line": 138, "character": 9}} {"range": - {"start": {"line": 134, "character": 9}, - "end": {"line": 134, "character": 10}}, + {"start": {"line": 138, "character": 9}, + "end": {"line": 138, "character": 10}}, "contents": {"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 137, "character": 10}} + "position": {"line": 141, "character": 10}} {"range": - {"start": {"line": 137, "character": 10}, - "end": {"line": 137, "character": 16}}, + {"start": {"line": 141, "character": 10}, + "end": {"line": 141, "character": 16}}, "contents": {"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 140, "character": 4}} + "position": {"line": 144, "character": 4}} {"range": - {"start": {"line": 140, "character": 4}, - "end": {"line": 140, "character": 11}}, + {"start": {"line": 144, "character": 4}, + "end": {"line": 144, "character": 11}}, "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 140, "character": 8}} + "position": {"line": 144, "character": 8}} {"range": - {"start": {"line": 140, "character": 4}, - "end": {"line": 140, "character": 11}}, + {"start": {"line": 144, "character": 4}, + "end": {"line": 144, "character": 11}}, "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 145, "character": 6}} + "position": {"line": 149, "character": 6}} {"range": - {"start": {"line": 145, "character": 6}, "end": {"line": 145, "character": 7}}, + {"start": {"line": 149, "character": 6}, "end": {"line": 149, "character": 7}}, "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 148, "character": 4}} + "position": {"line": 152, "character": 4}} [{"targetUri": "file://hover.lean", "targetSelectionRange": - {"start": {"line": 145, "character": 6}, - "end": {"line": 145, "character": 7}}, + {"start": {"line": 149, "character": 6}, + "end": {"line": 149, "character": 7}}, "targetRange": - {"start": {"line": 145, "character": 6}, - "end": {"line": 145, "character": 7}}, + {"start": {"line": 149, "character": 6}, + "end": {"line": 149, "character": 7}}, "originSelectionRange": - {"start": {"line": 148, "character": 4}, - "end": {"line": 148, "character": 5}}}] + {"start": {"line": 152, "character": 4}, + "end": {"line": 152, "character": 5}}}] {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 148, "character": 4}} + "position": {"line": 152, "character": 4}} {"range": - {"start": {"line": 148, "character": 4}, "end": {"line": 148, "character": 5}}, + {"start": {"line": 152, "character": 4}, "end": {"line": 152, "character": 5}}, "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 152, "character": 8}} + "position": {"line": 156, "character": 8}} {"range": - {"start": {"line": 152, "character": 8}, "end": {"line": 152, "character": 9}}, + {"start": {"line": 156, "character": 8}, "end": {"line": 156, "character": 9}}, "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 155, "character": 8}} + "position": {"line": 159, "character": 8}} [{"targetUri": "file://hover.lean", "targetSelectionRange": - {"start": {"line": 152, "character": 8}, - "end": {"line": 152, "character": 9}}, + {"start": {"line": 156, "character": 8}, + "end": {"line": 156, "character": 9}}, "targetRange": - {"start": {"line": 152, "character": 8}, - "end": {"line": 152, "character": 9}}, + {"start": {"line": 156, "character": 8}, + "end": {"line": 156, "character": 9}}, "originSelectionRange": - {"start": {"line": 155, "character": 8}, - "end": {"line": 155, "character": 9}}}] + {"start": {"line": 159, "character": 8}, + "end": {"line": 159, "character": 9}}}] {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 155, "character": 8}} + "position": {"line": 159, "character": 8}} {"range": - {"start": {"line": 155, "character": 8}, "end": {"line": 155, "character": 9}}, + {"start": {"line": 159, "character": 8}, "end": {"line": 159, "character": 9}}, "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 160, "character": 25}} + "position": {"line": 164, "character": 25}} {"range": - {"start": {"line": 160, "character": 25}, - "end": {"line": 160, "character": 26}}, + {"start": {"line": 164, "character": 25}, + "end": {"line": 164, "character": 26}}, "contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 163, "character": 2}} + "position": {"line": 167, "character": 2}} null {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 169, "character": 2}} + "position": {"line": 173, "character": 2}} {"range": - {"start": {"line": 169, "character": 2}, - "end": {"line": 169, "character": 15}}, + {"start": {"line": 173, "character": 2}, + "end": {"line": 173, "character": 15}}, "contents": {"value": "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 172, "character": 28}} + "position": {"line": 176, "character": 28}} {"range": - {"start": {"line": 172, "character": 27}, - "end": {"line": 172, "character": 32}}, + {"start": {"line": 176, "character": 27}, + "end": {"line": 176, "character": 32}}, "contents": {"value": "```lean\nId Nat\n```\n***\nYou can use parentheses for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- Creating simple functions when combined with `·`. Here are some examples:\n - `(· + 1)` is shorthand for `fun x => x + 1`\n - `(· + ·)` is shorthand for `fun x y => x + y`\n - `(f · a b)` is shorthand for `fun x => f x a b`\n - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n", diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out index 48052c3434..3d1ad2db0e 100644 --- a/tests/lean/syntaxPrec.lean.expected.out +++ b/tests/lean/syntaxPrec.lean.expected.out @@ -5,4 +5,5 @@ def «termFoo*_» : Lean.ParserDescr✝ := ParserDescr.node✝ `«termFoo*_» 1022 (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*") - (ParserDescr.sepBy1✝ (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ") Bool.false✝))) + ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ") + Bool.false✝)))