From 9bd886f37d6e54d8c4f96a9330438086eaff8bd5 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 26 Aug 2022 21:42:39 -0400 Subject: [PATCH] fix: @[inheritDoc] on notation --- src/Lean/Elab/Notation.lean | 2 +- tests/lean/interactive/hover.lean | 5 + .../lean/interactive/hover.lean.expected.out | 238 +++++++++--------- 3 files changed, 130 insertions(+), 115 deletions(-) diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean index 6680bc5a15..072628dcfb 100644 --- a/src/Lean/Elab/Notation.lean +++ b/src/Lean/Elab/Notation.lean @@ -28,7 +28,7 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax Option (TSepArray ``attrInstance ",") := attrs?.map fun attrs => match rhs with - | `($f:ident $_args*) => + | `($f:ident $_args*) | `($f:ident) => attrs.getElems.map fun stx => Unhygienic.run do if let `(attrInstance| $attr:ident) := stx then if attr.getId.eraseMacroScopes == `inheritDoc then diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index 3fd024384e..ae0b3ef899 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -78,6 +78,11 @@ infix:65 (name := myInfix) " >+< " => Nat.add #check 1 >+< 2 --^ textDocument/hover +@[inheritDoc] notation "ℕ" => Nat + +#check ℕ + --^ textDocument/hover + /-- My command -/ macro "mycmd" e:term : command => do let seq ← `(Lean.Parser.Term.doSeq| $e:term) diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index d76a9952fc..aa67081c10 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -131,236 +131,246 @@ "```lean\nNat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 82, "character": 14}} + "position": {"line": 82, "character": 7}} {"range": - {"start": {"line": 82, "character": 14}, "end": {"line": 82, "character": 36}}, + {"start": {"line": 82, "character": 7}, "end": {"line": 82, "character": 8}}, + "contents": + {"value": + "```lean\nNat : Type\n```\n***\nThe type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n", + "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 87, "character": 14}} +{"range": + {"start": {"line": 87, "character": 14}, "end": {"line": 87, "character": 36}}, "contents": {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 84, "character": 30}} + "position": {"line": 89, "character": 30}} {"range": - {"start": {"line": 84, "character": 29}, "end": {"line": 84, "character": 34}}, + {"start": {"line": 89, "character": 29}, "end": {"line": 89, "character": 34}}, "contents": {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 87, "character": 2}} + "position": {"line": 92, "character": 2}} {"range": - {"start": {"line": 87, "character": 0}, "end": {"line": 87, "character": 7}}, + {"start": {"line": 92, "character": 0}, "end": {"line": 92, "character": 7}}, "contents": {"value": "My command ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 94, "character": 2}} + "position": {"line": 99, "character": 2}} {"range": - {"start": {"line": 94, "character": 0}, "end": {"line": 94, "character": 7}}, + {"start": {"line": 99, "character": 0}, "end": {"line": 99, "character": 7}}, "contents": {"value": "My command ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 97, "character": 16}} + "position": {"line": 102, "character": 16}} {"range": - {"start": {"line": 97, "character": 16}, "end": {"line": 97, "character": 23}}, + {"start": {"line": 102, "character": 16}, + "end": {"line": 102, "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": 97, "character": 24}} + "position": {"line": 102, "character": 24}} {"range": - {"start": {"line": 97, "character": 24}, "end": {"line": 97, "character": 31}}, + {"start": {"line": 102, "character": 24}, + "end": {"line": 102, "character": 31}}, "contents": {"value": "```lean\nLean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 97, "character": 31}} + "position": {"line": 102, "character": 31}} {"range": - {"start": {"line": 97, "character": 31}, "end": {"line": 97, "character": 35}}, + {"start": {"line": 102, "character": 31}, + "end": {"line": 102, "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": 106, "character": 2}} + "position": {"line": 111, "character": 2}} {"range": - {"start": {"line": 106, "character": 0}, "end": {"line": 106, "character": 8}}, + {"start": {"line": 111, "character": 0}, "end": {"line": 111, "character": 8}}, "contents": {"value": "My ultimate command ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 110, "character": 10}} + "position": {"line": 115, "character": 10}} null {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 114, "character": 8}} + "position": {"line": 119, "character": 8}} {"range": - {"start": {"line": 114, "character": 8}, - "end": {"line": 114, "character": 10}}, + {"start": {"line": 119, "character": 8}, + "end": {"line": 119, "character": 10}}, "contents": {"value": "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 114, "character": 10}} + "position": {"line": 119, "character": 10}} {"range": - {"start": {"line": 114, "character": 8}, - "end": {"line": 114, "character": 21}}, + {"start": {"line": 119, "character": 8}, + "end": {"line": 119, "character": 21}}, "contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 121, "character": 2}} + "position": {"line": 126, "character": 2}} {"range": - {"start": {"line": 121, "character": 2}, "end": {"line": 121, "character": 3}}, - "contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}} + {"start": {"line": 126, "character": 2}, "end": {"line": 126, "character": 3}}, + "contents": {"value": "```lean\nn : Id ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 128, "character": 9}} -{"range": - {"start": {"line": 128, "character": 7}, - "end": {"line": 128, "character": 17}}, - "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}} -{"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 133, "character": 7}} + "position": {"line": 133, "character": 9}} {"range": {"start": {"line": 133, "character": 7}, - "end": {"line": 133, "character": 10}}, - "contents": {"value": "```lean\nBar.foo : Nat\n```", "kind": "markdown"}} + "end": {"line": 133, "character": 17}}, + "contents": {"value": "```lean\nfoo : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 136, "character": 9}} + "position": {"line": 138, "character": 7}} {"range": - {"start": {"line": 136, "character": 7}, - "end": {"line": 136, "character": 17}}, - "contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}} + {"start": {"line": 138, "character": 7}, + "end": {"line": 138, "character": 10}}, + "contents": {"value": "```lean\nBar.foo : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 139, "character": 4}} + "position": {"line": 141, "character": 9}} {"range": - {"start": {"line": 139, "character": 4}, "end": {"line": 139, "character": 7}}, - "contents": {"value": "```lean\nBar.bar : Nat\n```", "kind": "markdown"}} + {"start": {"line": 141, "character": 7}, + "end": {"line": 141, "character": 17}}, + "contents": {"value": "```lean\n_root_.foo : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 142, "character": 10}} + "position": {"line": 144, "character": 4}} {"range": - {"start": {"line": 142, "character": 10}, - "end": {"line": 142, "character": 13}}, + {"start": {"line": 144, "character": 4}, "end": {"line": 144, "character": 7}}, + "contents": {"value": "```lean\nBar.bar : ℕ\n```", "kind": "markdown"}} +{"textDocument": {"uri": "file://hover.lean"}, + "position": {"line": 147, "character": 10}} +{"range": + {"start": {"line": 147, "character": 10}, + "end": {"line": 147, "character": 13}}, "contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 142, "character": 17}} + "position": {"line": 147, "character": 17}} {"range": - {"start": {"line": 142, "character": 17}, - "end": {"line": 142, "character": 19}}, + {"start": {"line": 147, "character": 17}, + "end": {"line": 147, "character": 19}}, "contents": - {"value": "```lean\nBar.Foo.mk : Nat → Foo\n```", "kind": "markdown"}} + {"value": "```lean\nBar.Foo.mk : ℕ → Foo\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 145, "character": 2}} + "position": {"line": 150, "character": 2}} {"range": - {"start": {"line": 145, "character": 2}, "end": {"line": 145, "character": 4}}, + {"start": {"line": 150, "character": 2}, "end": {"line": 150, "character": 4}}, "contents": - {"value": "```lean\nBar.Foo.hi : Foo → Nat\n```", "kind": "markdown"}} + {"value": "```lean\nBar.Foo.hi : Foo → ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 148, "character": 10}} + "position": {"line": 153, "character": 10}} {"range": - {"start": {"line": 148, "character": 10}, - "end": {"line": 148, "character": 13}}, + {"start": {"line": 153, "character": 10}, + "end": {"line": 153, "character": 13}}, "contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 150, "character": 4}} + "position": {"line": 155, "character": 4}} {"range": - {"start": {"line": 150, "character": 4}, "end": {"line": 150, "character": 6}}, + {"start": {"line": 155, "character": 4}, "end": {"line": 155, "character": 6}}, "contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 153, "character": 2}} + "position": {"line": 158, "character": 2}} {"range": - {"start": {"line": 153, "character": 0}, "end": {"line": 153, "character": 8}}, + {"start": {"line": 158, "character": 0}, "end": {"line": 158, "character": 8}}, "contents": - {"value": "```lean\nBar.instToStringNat : ToString Nat\n```", + {"value": "```lean\nBar.instToStringNat : ToString ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 155, "character": 9}} + "position": {"line": 160, "character": 9}} {"range": - {"start": {"line": 155, "character": 9}, - "end": {"line": 155, "character": 10}}, - "contents": - {"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}} + {"start": {"line": 160, "character": 9}, + "end": {"line": 160, "character": 10}}, + "contents": {"value": "```lean\nBar.f : ToString ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 158, "character": 10}} + "position": {"line": 163, "character": 10}} {"range": - {"start": {"line": 158, "character": 10}, - "end": {"line": 158, "character": 16}}, + {"start": {"line": 163, "character": 10}, + "end": {"line": 163, "character": 16}}, "contents": {"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 161, "character": 4}} + "position": {"line": 166, "character": 4}} {"range": - {"start": {"line": 161, "character": 4}, - "end": {"line": 161, "character": 11}}, - "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}} + {"start": {"line": 166, "character": 4}, + "end": {"line": 166, "character": 11}}, + "contents": {"value": "```lean\nBar.foo.bar : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 161, "character": 8}} + "position": {"line": 166, "character": 8}} {"range": - {"start": {"line": 161, "character": 4}, - "end": {"line": 161, "character": 11}}, - "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}} + {"start": {"line": 166, "character": 4}, + "end": {"line": 166, "character": 11}}, + "contents": {"value": "```lean\nBar.foo.bar : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 166, "character": 6}} + "position": {"line": 171, "character": 6}} {"range": - {"start": {"line": 166, "character": 6}, "end": {"line": 166, "character": 7}}, - "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} + {"start": {"line": 171, "character": 6}, "end": {"line": 171, "character": 7}}, + "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 169, "character": 4}} + "position": {"line": 174, "character": 4}} [{"targetUri": "file://hover.lean", "targetSelectionRange": - {"start": {"line": 166, "character": 6}, - "end": {"line": 166, "character": 7}}, + {"start": {"line": 171, "character": 6}, + "end": {"line": 171, "character": 7}}, "targetRange": - {"start": {"line": 166, "character": 6}, - "end": {"line": 166, "character": 7}}, + {"start": {"line": 171, "character": 6}, + "end": {"line": 171, "character": 7}}, "originSelectionRange": - {"start": {"line": 169, "character": 4}, - "end": {"line": 169, "character": 5}}}] + {"start": {"line": 174, "character": 4}, + "end": {"line": 174, "character": 5}}}] {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 169, "character": 4}} + "position": {"line": 174, "character": 4}} {"range": - {"start": {"line": 169, "character": 4}, "end": {"line": 169, "character": 5}}, - "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} + {"start": {"line": 174, "character": 4}, "end": {"line": 174, "character": 5}}, + "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 173, "character": 8}} + "position": {"line": 178, "character": 8}} {"range": - {"start": {"line": 173, "character": 8}, "end": {"line": 173, "character": 9}}, - "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} + {"start": {"line": 178, "character": 8}, "end": {"line": 178, "character": 9}}, + "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 176, "character": 8}} + "position": {"line": 181, "character": 8}} [{"targetUri": "file://hover.lean", "targetSelectionRange": - {"start": {"line": 173, "character": 8}, - "end": {"line": 173, "character": 9}}, + {"start": {"line": 178, "character": 8}, + "end": {"line": 178, "character": 9}}, "targetRange": - {"start": {"line": 173, "character": 8}, - "end": {"line": 173, "character": 9}}, + {"start": {"line": 178, "character": 8}, + "end": {"line": 178, "character": 9}}, "originSelectionRange": - {"start": {"line": 176, "character": 8}, - "end": {"line": 176, "character": 9}}}] + {"start": {"line": 181, "character": 8}, + "end": {"line": 181, "character": 9}}}] {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 176, "character": 8}} + "position": {"line": 181, "character": 8}} {"range": - {"start": {"line": 176, "character": 8}, "end": {"line": 176, "character": 9}}, - "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}} + {"start": {"line": 181, "character": 8}, "end": {"line": 181, "character": 9}}, + "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 181, "character": 25}} + "position": {"line": 186, "character": 25}} {"range": - {"start": {"line": 181, "character": 25}, - "end": {"line": 181, "character": 26}}, - "contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}} + {"start": {"line": 186, "character": 25}, + "end": {"line": 186, "character": 26}}, + "contents": {"value": "```lean\nn : ℕ\n```", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 184, "character": 2}} + "position": {"line": 189, "character": 2}} null {"textDocument": {"uri": "file://hover.lean"}, - "position": {"line": 190, "character": 2}} + "position": {"line": 195, "character": 2}} {"range": - {"start": {"line": 190, "character": 2}, - "end": {"line": 190, "character": 15}}, + {"start": {"line": 195, "character": 2}, + "end": {"line": 195, "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": 193, "character": 28}} + "position": {"line": 198, "character": 28}} {"range": - {"start": {"line": 193, "character": 27}, - "end": {"line": 193, "character": 32}}, + {"start": {"line": 198, "character": 27}, + "end": {"line": 198, "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", + "```lean\nId ℕ\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", "kind": "markdown"}}