diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index dbfe4cbe254b..3dd9d6024f5b 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -492,25 +492,141 @@ partial def collectSyntaxBasedSemanticTokens (text : FileMap) : (stx : Syntax) return tokens return tokens.push { stx, type := keywordSemanticTokenMap.getD val .keyword } +private partial def forallBody : Expr → Expr + | .forallE _ _ body _ => forallBody body + | type => type + +private def typeForSortResult? (type : Expr) : Option SemanticTokenType := + match forallBody type with + | .sort u => + if u.isAlwaysZero then + some .enum + else + some .type + | _ => none + +private partial def typeExprResult? (env : Environment) (lctx : LocalContext) (type : Expr) : + Option SemanticTokenType := + match typeForSortResult? type with + | some tokenType => some tokenType + | none => + match type.getAppFn with + | .const declName us => + match env.find? declName with + | some info => typeForSortResult? (info.instantiateTypeLevelParams us) + | none => none + | .fvar fvarId => + match lctx.find? fvarId with + | some localDecl => typeForSortResult? localDecl.type + | none => none + | _ => none + +private def classifyLocal (env : Environment) (ti : Elab.TermInfo) (localDecl : LocalDecl) : + Option SemanticTokenType := Id.run do + let localType := localDecl.type + -- Recall that `isAuxDecl` is used for declarations currently being elaborated, e.g. recursive + -- functions and inductive types while their constructors are being processed. + if localDecl.isAuxDecl then + if let some tokenType := typeForSortResult? localType then + return some tokenType + else + return some .function + if let some tokenType := typeForSortResult? localType then + if localType.isSort && tokenType == .type then + return some .typeParameter + else + return some tokenType + if localDecl.isImplementationDetail then + return none + if typeExprResult? env ti.lctx localType == some .enum then + return some .variable + if ti.isBinder then + return some .parameter + return some .variable + +private def classifyConstant (env : Environment) (declName : Name) (info : ConstantInfo) (expr : Expr) : + SemanticTokenType := + if env.isProjectionFn declName then + .property + else match info with + | .ctorInfo _ => .enumMember + | .inductInfo info => + if isClass env info.name then + .interface + else if isStructure env info.name then + .struct + else if let some tokenType := typeExprResult? env {} expr then + tokenType + else + .type + | .thmInfo _ | .recInfo _ => .function + | _ => + if let some tokenType := typeExprResult? env {} expr then + tokenType + else + .function + +private def findConstInfoWithEnv? (ctx : Elab.ContextInfo) (declName : Name) : + Option (Environment × ConstantInfo) := + match ctx.env.find? declName with + | some info => some (ctx.env, info) + | none => ctx.cmdEnv?.bind fun env => (env.find? declName).map (env, ·) + +private def getSemanticTokenSyntax (stx : Syntax) : Syntax := + match stx with + | `(Parser.Command.declId|$id$[.{$_ls,*}]?) => id.raw + | _ => stx + +private def getAppFnSyntax? (stx : Syntax) : Option Syntax := + if stx.isOfKind ``Parser.Term.app then + some stx[0] + else + none + +private def collectTermInfoBasedSemanticToken (ctx : Elab.ContextInfo) (ti : Elab.TermInfo) : + Option LeanSemanticToken := Id.run do + let stx := getSemanticTokenSyntax ti.stx + if ti.expr.isSort then + let .original .. := stx.getHeadInfo + | return none + return some { stx, type := .class } + if stx.getKind == Parser.Term.identProjKind then + let .original .. := stx.getHeadInfo + | return none + return some { stx, type := .property } + match ti.expr.getAppFn with + | Expr.fvar fvarId .. => + let some localDecl := ti.lctx.find? fvarId + | return none + let some stx := + if let `($_:ident) := stx then + some stx + else if localDecl.isAuxDecl then + getAppFnSyntax? stx + else + none + | return none + let .original .. := stx.getHeadInfo + | return none + let `($_:ident) := stx + | return none + return (classifyLocal ctx.env ti localDecl).map fun tokenType => ⟨stx, tokenType, 5⟩ + | Expr.const declName .. => + let `($_:ident) := stx + | return none + let .original .. := stx.getHeadInfo + | return none + match findConstInfoWithEnv? ctx declName with + | some (env, info) => return some ⟨stx, classifyConstant env declName info ti.expr, 5⟩ + | none => return none + | _ => return none + /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken := - List.toArray <| i.deepestNodes fun _ info _ => do + List.toArray <| i.deepestNodes fun ctx info _ => do let .ofTermInfo ti := info | none - let .original .. := ti.stx.getHeadInfo - | none - if let `($_:ident) := ti.stx then - if let Expr.fvar fvarId .. := ti.expr then - if let some localDecl := ti.lctx.find? fvarId then - -- Recall that `isAuxDecl` is an auxiliary declaration used to elaborate a recursive definition. - if localDecl.isAuxDecl then - if ti.isBinder then - return { stx := ti.stx, type := SemanticTokenType.function } - else if ! localDecl.isImplementationDetail then - return { stx := ti.stx, type := SemanticTokenType.variable } - if ti.stx.getKind == Parser.Term.identProjKind then - return {stx := ti.stx, type := SemanticTokenType.property } - none + collectTermInfoBasedSemanticToken ctx ti /-- A debugging utility for inspecting sets of collected tokens, classified by line and sorted by diff --git a/tests/server_interactive/semanticTokens.lean b/tests/server_interactive/semanticTokens.lean index b50d09157bf6..e26d970bfe53 100644 --- a/tests/server_interactive/semanticTokens.lean +++ b/tests/server_interactive/semanticTokens.lean @@ -1,7 +1,48 @@ +/-! This file tests semantic token kinds. -/ + +universe u + +inductive SemanticTokenData where + | atom : SemanticTokenData + +inductive SemanticTokenProp (A : Type u) : A → Prop where + | intro (a : A) : SemanticTokenProp A a + +structure SemanticTokenStruct where + field : Nat + +class SemanticTokenInterface (A : Type u) where + op : A → A + +def SemanticTokenFamily (A : Type u) : Type u := List A + +def SemanticTokenPredicate (A : Type u) (a : A) : Prop := a = a + +def semanticTokenValue : Nat := 1 + +def semanticTokenRecursive : Nat → Nat + | 0 => 0 + | n + 1 => semanticTokenRecursive n + +theorem semanticTokenProof (A : Type u) (a : A) : SemanticTokenPredicate A a := rfl + +def semanticTokenUse (A : Type u) [SemanticTokenInterface A] (a : A) + (h : SemanticTokenProp A a) : SemanticTokenFamily Nat := + let s : SemanticTokenStruct := { field := semanticTokenValue } + let d : SemanticTokenData := SemanticTokenData.atom + let p : SemanticTokenPredicate A a := semanticTokenProof A a + let q : SemanticTokenProp A a := h + match d with + | .atom => + let _ : SemanticTokenPredicate A a := p + let _ : SemanticTokenProp A a := q + List.cons s.field List.nil + def foo1 (x : Nat) := x.succ def foo2 (x : Nat) := x |>.succ theorem foo3 (x : Nat) : True := let y := x.succ + have : y = y := rfl True.intro #eval 1 diff --git a/tests/server_interactive/semanticTokens.lean.out.expected b/tests/server_interactive/semanticTokens.lean.out.expected index 1951312f859a..fd125dcf50a9 100644 --- a/tests/server_interactive/semanticTokens.lean.out.expected +++ b/tests/server_interactive/semanticTokens.lean.out.expected @@ -5,103 +5,782 @@ [{"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 2, "character": 0}, "end": {"line": 3, "character": 0}}, + {"start": {"line": 26, "character": 0}, + "end": {"line": 26, "character": 83}}, "message": "Goals accomplished!", "leanTags": [2], "isSilent": true, "fullRange": - {"start": {"line": 2, "character": 0}, "end": {"line": 4, "character": 12}}}, - {"tags": [1], - "source": "Lean 4", - "severity": 2, + {"start": {"line": 26, "character": 0}, + "end": {"line": 26, "character": 83}}}, + {"source": "Lean 4", + "severity": 3, "range": - {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}, - "message": - "Variable name `y` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`", + {"start": {"line": 42, "character": 0}, "end": {"line": 43, "character": 0}}, + "message": "Goals accomplished!", + "leanTags": [2], + "isSilent": true, "fullRange": - {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}}, + {"start": {"line": 42, "character": 0}, + "end": {"line": 45, "character": 12}}}, {"source": "Lean 4", "severity": 3, "range": - {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 5}}, + {"start": {"line": 47, "character": 0}, "end": {"line": 47, "character": 5}}, "message": "1", "fullRange": - {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 5}}}]} + {"start": {"line": 47, "character": 0}, + "end": {"line": 47, "character": 5}}}]} {"textDocument": {"uri": "file:///semanticTokens.lean"}, - "position": {"line": 6, "character": 2}} + "position": {"line": 47, "character": 2}} {"data": - [0, + [2, + 0, + 8, + 0, + 0, + 2, + 0, + 9, + 0, + 0, + 0, + 10, + 17, + 5, 0, - 3, + 0, + 18, + 5, + 0, + 0, + 1, + 4, + 4, + 12, + 0, + 0, + 7, + 17, + 5, + 0, + 2, + 0, + 9, 0, 0, 0, 10, + 17, + 7, + 0, + 0, + 19, 1, + 10, + 0, + 0, + 4, + 6, + 6, + 0, + 0, + 10, 1, + 10, + 0, + 0, + 4, + 4, + 6, + 0, + 0, + 5, + 5, 0, 0, + 1, + 4, + 5, 12, + 0, + 0, + 7, + 1, + 11, + 0, + 0, + 4, + 1, + 10, + 0, + 0, + 5, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, 1, + 0, + 2, + 0, + 9, + 0, + 0, + 0, + 10, + 19, + 9, + 0, + 0, + 20, + 5, + 0, + 0, 1, + 2, + 5, + 2, + 0, 0, + 8, + 3, + 5, 0, 2, + 0, + 5, + 0, + 0, + 0, + 6, + 22, + 8, + 0, + 0, + 24, + 1, + 10, + 0, + 0, 4, + 6, + 6, + 0, + 0, + 8, + 5, + 0, + 0, + 1, + 2, 2, + 2, + 0, 0, + 5, + 1, + 10, + 0, + 0, + 4, 1, + 10, + 0, + 2, 0, 3, 0, 0, 0, + 4, + 19, + 5, + 0, + 0, + 21, + 1, + 10, + 0, + 0, + 4, + 6, + 6, + 0, + 0, + 10, + 6, + 6, + 0, + 0, 10, + 4, + 5, + 0, + 0, + 5, 1, + 10, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 22, + 7, + 0, + 0, + 24, 1, + 10, 0, 0, - 12, + 4, + 6, + 6, + 0, + 0, + 9, 1, + 11, + 0, + 0, + 4, 1, + 10, 0, 0, 5, 4, + 6, + 0, + 0, + 8, + 1, + 1, + 0, + 0, + 4, + 1, + 1, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 18, + 3, + 0, + 0, + 21, + 3, + 5, + 0, 2, 0, + 3, + 0, + 0, + 0, + 4, + 22, + 3, + 0, + 0, + 25, + 3, + 5, + 0, + 0, + 6, + 3, + 5, + 0, + 2, + 4, 1, + 11, 0, - 7, 0, + 9, + 22, + 3, 0, 0, - 14, + 23, 1, 1, 0, - 1, 2, + 0, + 7, + 0, + 0, + 0, + 8, + 18, 3, 0, 0, + 20, + 1, + 10, + 0, 0, 4, + 6, + 6, + 0, + 0, + 9, 1, + 11, + 0, + 0, + 4, 1, + 10, 0, 0, 5, + 22, + 7, + 0, + 0, + 23, 1, - 1, + 10, 0, 0, 2, - 4, + 1, + 1, + 0, + 0, + 5, + 3, + 3, + 0, 2, 0, 3, 0, + 0, + 0, + 4, + 16, + 3, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 4, + 6, + 6, + 0, + 0, + 9, + 22, + 8, + 0, + 0, + 23, + 1, + 10, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 4, + 1, + 10, + 0, + 1, + 5, + 1, + 1, + 0, + 0, + 4, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 19, + 5, + 0, + 0, + 20, + 3, + 5, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 4, + 19, + 9, + 0, + 0, + 34, + 18, + 3, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 4, + 17, + 5, + 0, + 0, + 21, + 22, + 12, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 4, + 22, + 7, + 0, + 0, + 23, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 18, + 3, + 0, + 0, + 19, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 4, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 1, + 1, + 0, + 1, + 2, + 5, + 0, + 0, + 0, + 6, + 1, + 1, + 0, + 0, + 2, + 4, + 0, + 0, + 2, + 4, + 3, + 0, + 0, + 0, + 4, + 1, + 0, + 0, + 0, + 4, + 22, + 7, + 0, + 0, + 23, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 1, + 1, + 0, + 1, + 4, + 3, + 0, + 0, + 0, + 4, + 1, + 0, + 0, + 0, + 4, + 17, + 7, + 0, + 0, + 18, + 1, + 10, + 0, + 0, + 2, + 1, + 1, + 0, + 0, + 5, + 1, + 1, + 0, + 1, + 4, + 9, + 12, + 0, + 0, + 10, + 1, + 1, + 0, + 0, + 2, + 5, + 2, + 0, + 0, + 6, + 8, + 12, + 0, + 2, + 0, + 3, + 0, + 0, + 0, + 4, + 4, + 3, + 0, + 0, + 6, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 8, + 1, + 1, + 0, + 0, + 2, + 4, + 2, + 0, + 1, + 0, + 3, + 0, + 0, + 0, + 4, + 4, + 3, + 0, + 0, + 6, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 8, + 1, + 1, + 0, + 0, + 5, + 4, + 2, + 0, + 1, + 0, + 7, + 0, + 0, + 0, + 8, + 4, + 3, + 0, + 0, + 6, + 1, + 11, + 0, + 0, + 4, + 3, + 5, + 0, + 0, + 7, + 4, + 7, + 0, + 1, + 2, + 3, + 0, + 0, + 0, + 4, + 1, + 11, + 0, + 0, + 5, + 1, + 1, + 0, + 0, + 2, + 4, + 2, + 0, + 1, + 2, + 4, + 0, + 0, + 0, + 7, + 1, + 1, + 0, + 0, + 4, + 1, + 1, + 0, + 0, + 5, + 3, + 3, + 0, + 1, + 2, + 10, + 12, + 0, + 2, + 0, 5, 0, 0]} diff --git a/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected b/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected index 236c9a2f483b..81a695a2f663 100644 --- a/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected +++ b/tests/server_interactive/semanticTokensVersoDocs.lean.out.expected @@ -68,7 +68,7 @@ 0, 1, 4, - 18, + 3, 0, 0, 4, @@ -97,11 +97,16 @@ 0, 0, 1, - 5, + 4, + 3, + 0, + 0, + 4, + 1, 18, 0, 0, - 5, + 1, 1, 1, 0, @@ -132,11 +137,16 @@ 0, 0, 1, - 10, + 4, + 3, + 0, + 0, + 4, + 6, 18, 0, 0, - 10, + 6, 1, 0, 0, @@ -146,12 +156,22 @@ 0, 0, 0, - 10, + 4, + 4, + 3, + 0, + 0, + 6, 1, 1, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, @@ -183,7 +203,7 @@ 0, 1, 4, - 18, + 3, 0, 0, 4, @@ -212,11 +232,16 @@ 0, 0, 1, - 5, + 4, + 3, + 0, + 0, + 4, + 1, 18, 0, 0, - 5, + 1, 1, 1, 0, @@ -247,11 +272,21 @@ 0, 0, 1, - 11, + 4, + 3, + 0, + 0, + 4, + 3, 18, 0, 0, - 11, + 3, + 4, + 3, + 0, + 0, + 4, 1, 0, 0, @@ -261,12 +296,22 @@ 0, 0, 0, - 10, + 4, + 4, + 3, + 0, + 0, + 6, 1, 1, 0, 0, - 12, + 4, + 3, + 5, + 0, + 0, + 8, 1, 1, 0, @@ -357,21 +402,51 @@ 0, 1, 0, + 10, 18, - 18, 0, 0, + 10, + 3, + 3, + 0, + 0, + 3, + 5, 18, + 0, + 0, + 5, 1, + 11, + 0, + 0, 1, + 3, + 18, + 0, + 0, + 3, + 4, + 5, + 0, 0, + 4, + 2, + 18, 0, + 0, + 2, 1, - 13, + 3, + 0, + 0, + 1, + 3, 18, 0, 0, - 13, + 3, 1, 1, 0, @@ -504,4 +579,9 @@ 0, 3, 0, + 0, + 0, + 4, + 1, + 3, 0]}