diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index 22bcdb2cba..2bc6f96dcf 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/src/Lean/Data/FuzzyMatching.lean @@ -137,24 +137,22 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr matchScore? := selectBest (getMiss result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult - (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) + patternIdx wordIdx (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) none - (wordIdx == 0) - startPenalties.get! wordIdx)) (getMatch result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult - (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) + patternIdx wordIdx (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) (.some runLength) - (wordIdx == 0) )) |>.map fun score => if wordIdx >= lastSepIdx then score + 1 else score -- main identifier bonus else runLengths := runLengths.set! (getIdx patternIdx wordIdx) 1 matchScore? := .some $ matchResult - (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) + patternIdx wordIdx (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) none - (wordIdx == 0) - startPenalties.get! wordIdx + - startPenalties.get! wordIdx result := set result patternIdx wordIdx missScore? matchScore? @@ -198,14 +196,17 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr return true /-- Heuristic to rate a match. -/ - matchResult (patternChar wordChar : Char) (patternRole wordRole : CharRole) (consecutive : Option Int) (wordStart : Bool) : Int := Id.run do + matchResult (patternIdx wordIdx : Nat) (patternRole wordRole : CharRole) (consecutive : Option Int) : Int := Id.run do let mut score : Int := 1 /- Case-sensitive equality or beginning of a segment in pattern and word. -/ - if patternChar == wordChar || (patternRole matches CharRole.head && wordRole matches CharRole.head) then + if (pattern.get ⟨patternIdx⟩) == (word.get ⟨wordIdx⟩) || (patternRole matches CharRole.head && wordRole matches CharRole.head) then score := score + 1 - /- Beginning of the word. -/ - if wordStart then + /- Matched end of word with end of pattern -/ + if wordIdx == word.length - 1 && patternIdx == pattern.length - 1 then score := score + 2 + /- Matched beginning of the word. -/ + if (wordIdx == 0) then + score := score + 3 /- Consecutive character match. -/ if let some bonus := consecutive then /- consecutive run bonus -/ diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index b8c9e593d0..2e2d053325 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -36,11 +36,6 @@ "kind": 3, "detail": "∀ (p : Prop), (False ∧ p) = False"}, {"label": "true_and", "kind": 3, "detail": "∀ (p : Prop), (True ∧ p) = p"}, - {"label": "and_false", - "kind": 3, - "detail": "∀ (p : Prop), (p ∧ False) = False"}, - {"label": "and_self", "kind": 3, "detail": "∀ (p : Prop), (p ∧ p) = p"}, - {"label": "and_true", "kind": 3, "detail": "∀ (p : Prop), (p ∧ True) = p"}, {"label": "HAnd", "kind": 7, "documentation": @@ -48,6 +43,29 @@ "The typeclass behind the notation `a &&& b : γ` where `a : α`, `b : β`. ", "kind": "markdown"}, "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"}, + {"label": "and_false", + "kind": 3, + "detail": "∀ (p : Prop), (p ∧ False) = False"}, + {"label": "and_self", "kind": 3, "detail": "∀ (p : Prop), (p ∧ p) = p"}, + {"label": "and_true", "kind": 3, "detail": "∀ (p : Prop), (p ∧ True) = p"}, + {"label": "strictAnd", + "kind": 3, + "documentation": + {"value": + "`strictAnd` is the same as `and`, but it does not use short-circuit evaluation semantics:\nboth sides are evaluated, even if the first value is `false`.\n", + "kind": "markdown"}, + "detail": "Bool → Bool → Bool"}, + {"label": "instDecidableAnd", + "kind": 3, + "detail": "[dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)"}, + {"label": "instHAnd", "kind": 3, "detail": "[inst : AndOp α] → HAnd α α α"}, + {"label": "Append", + "kind": 7, + "documentation": + {"value": + "The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. ", + "kind": "markdown"}, + "detail": "Type u → Type u"}, {"label": "HAndThen", "kind": 7, "documentation": @@ -60,17 +78,6 @@ {"label": "instAndOpUInt64", "kind": 21, "detail": "AndOp UInt64"}, {"label": "instAndOpUInt8", "kind": 21, "detail": "AndOp UInt8"}, {"label": "instAndOpUSize", "kind": 21, "detail": "AndOp USize"}, - {"label": "strictAnd", - "kind": 3, - "documentation": - {"value": - "`strictAnd` is the same as `and`, but it does not use short-circuit evaluation semantics:\nboth sides are evaluated, even if the first value is `false`.\n", - "kind": "markdown"}, - "detail": "Bool → Bool → Bool"}, - {"label": "instDecidableAnd", - "kind": 3, - "detail": "[dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)"}, - {"label": "instHAnd", "kind": 3, "detail": "[inst : AndOp α] → HAnd α α α"}, {"label": "instHAndThen", "kind": 3, "detail": "[inst : AndThen α] → HAndThen α α α"}, @@ -81,13 +88,6 @@ {"label": "iff_iff_implies_and_implies", "kind": 3, "detail": "∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)"}, - {"label": "Append", - "kind": 7, - "documentation": - {"value": - "The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. ", - "kind": "markdown"}, - "detail": "Type u → Type u"}, {"label": "HAppend", "kind": 7, "documentation": @@ -95,7 +95,10 @@ "The notation typeclass for heterogeneous append.\nThis enables the notation `a ++ b : γ` where `a : α`, `b : β`.\n", "kind": "markdown"}, "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"}, - {"label": "instAppendSubarray", "kind": 3, "detail": "Append (Subarray α)"}], + {"label": "instAppendSubarray", "kind": 3, "detail": "Append (Subarray α)"}, + {"label": "instHAppend", + "kind": 3, + "detail": "[inst : Append α] → HAppend α α α"}], "isIncomplete": true} {"textDocument": {"uri": "file://completion7.lean"}, "position": {"line": 2, "character": 11}} diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out index 9e358e8dcf..5b378eb440 100644 --- a/tests/lean/interactive/keywordCompletion.lean.expected.out +++ b/tests/lean/interactive/keywordCompletion.lean.expected.out @@ -9,12 +9,13 @@ {"items": [{"label": "register_string", "kind": 14, "detail": "keyword"}, {"label": "regular", "kind": 21, "detail": "Nat"}, + {"label": "reprArg", "kind": 3, "detail": "[inst : Repr α] → α → Std.Format"}, {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"}, {"label": "recSubsingleton", "kind": 3, "detail": "∀ [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)]\n [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)], Subsingleton (Decidable.casesOn h h₂ h₁)"}, - {"label": "reprArg", - "kind": 3, - "detail": "[inst : Repr α] → α → Std.Format"}], + {"label": "instReprString", "kind": 21, "detail": "Repr String"}, + {"label": "instReprSubstring", "kind": 21, "detail": "Repr Substring"}, + {"label": "instReprAtomString", "kind": 21, "detail": "ReprAtom String"}], "isIncomplete": true} diff --git a/tests/lean/workspaceSymbols.lean b/tests/lean/workspaceSymbols.lean new file mode 100644 index 0000000000..f009f616ca --- /dev/null +++ b/tests/lean/workspaceSymbols.lean @@ -0,0 +1,9 @@ +import Lean + +open Lean Elab + +def orderFuzzyMatches (names : Array Name) (pattern : String) : Array Name := + names.filterMap (fun n => (n, ·) <$> Lean.FuzzyMatching.fuzzyMatchScoreWithThreshold? pattern n.toString) |>.qsort (·.2 ≥ ·.2) |>.map (·.1) + +-- patterns matching at the end of a name should get a bonus +#eval orderFuzzyMatches #[`Array.extract, `Lean.extractMainModule] "extract" diff --git a/tests/lean/workspaceSymbols.lean.expected.out b/tests/lean/workspaceSymbols.lean.expected.out new file mode 100644 index 0000000000..bbe0396931 --- /dev/null +++ b/tests/lean/workspaceSymbols.lean.expected.out @@ -0,0 +1 @@ +#[`Array.extract, `Lean.extractMainModule]