fix: fuzzy-find bonus for matching last characters of pattern and symbol (#1917)

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 -/

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}}

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}

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"

tests/lean/workspaceSymbols.lean.expected.out

@@ -0,0 +1 @@
+#[`Array.extract, `Lean.extractMainModule]