fix: improve fuzzy-matching heuristics (#1710)

2022-10-14 07:17:14 -07:00 · 2022-10-14 07:17:14 -07:00 · 76c4693c95
commit 76c4693c95
parent f7651de424
7 changed files with 230 additions and 155 deletions
--- a/src/Lean/Data/FuzzyMatching.lean
+++ b/src/Lean/Data/FuzzyMatching.lean
@ -92,64 +92,91 @@ In addition to the current characters in the pattern and the word, the
 algorithm uses different scores for the last operation (miss/match). This is
 necessary to give consecutive character matches a bonus. -/
 private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Array CharRole) : Option Int := Id.run do
-  let mut result : Array (Option Int) := Array.mkArray ((pattern.length + 1) * (word.length + 1) * 2) none
+  /- Flattened array where the value at index (i, j, k) represents the best possible score of a fuzzy match
+  between the substrings pattern[:i+1] and word[:j+1] assuming that pattern[i] misses at word[j] (k = 0, i.e.
+  it was matched earlier), or matches at word[j] (k = 1). A value of `none` corresponds to a score of -∞, and is used
+  where no such match/miss is possible or for unneeded parts of the table. -/
+  let mut result : Array (Option Int) := Array.mkArray (pattern.length * word.length * 2) none
+  let mut runLengths : Array Int := Array.mkArray (pattern.length * word.length) 0

-  result := set result 0 0 (some 0) none
+  -- penalty for starting a consecutive run at each index
+  let mut startPenalties : Array Int := Array.mkArray word.length 0

-  let mut penalty := 0
-  for wordIdx in [:word.length - pattern.length] do
-    penalty := penalty - skipPenalty (wordRoles.get! wordIdx) false (wordIdx == 0)
-    result := set result 0 (wordIdx+1) (some penalty) none
+  let mut lastSepIdx := 0
+  let mut penaltyNs : Int := 0
+  let mut penaltySkip : Int := 0
+  for wordIdx in [:word.length] do
+    if (wordIdx != 0) && (wordRoles.get! wordIdx) matches .separator then
+      -- reset skip penalty at namespace separator
+      penaltySkip := 0
+      -- add constant penalty for each namespace to prefer shorter namespace nestings
+      penaltyNs := penaltyNs + 1
+      lastSepIdx := wordIdx
+    penaltySkip := penaltySkip + skipPenalty (wordRoles.get! wordIdx) (wordIdx == 0)
+    startPenalties := startPenalties.set! wordIdx $ penaltySkip + penaltyNs

  -- TODO: the following code is assuming all characters are ASCII
  for patternIdx in [:pattern.length] do
-    let patternComplete := patternIdx == pattern.length - 1
-
+    /- For this dynamic program to be correct, it's only necessary to populate a range of length
+   `word.length - pattern.length` at each index (because at the very end, we can only consider fuzzy matches
+    of `pattern` with a longer substring of `word`). -/
    for wordIdx in [patternIdx:word.length-(pattern.length - patternIdx - 1)] do
-      let missScore? := selectBest
-        (getMiss result (patternIdx + 1) wordIdx)
-        (getMatch result (patternIdx + 1) wordIdx)
-        |>.map (· - skipPenalty (wordRoles.get! wordIdx) patternComplete (wordIdx == 0))
-
-      let matchScore? :=
-        if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) then
+      let missScore? := 
+        if wordIdx >= 1 then 
          selectBest
-            (getMiss result patternIdx wordIdx |>.map (· + matchResult
-              (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩)
-              (patternRoles.get! patternIdx) (wordRoles.get! wordIdx)
-              false
-              (wordIdx == 0)
-            ))
-            (getMatch result patternIdx wordIdx |>.map (· + matchResult
-              (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩)
-              (patternRoles.get! patternIdx) (wordRoles.get! wordIdx)
-              true
-              (wordIdx == 0)
-            ))
+            (getMiss result patternIdx (wordIdx - 1))
+            (getMatch result patternIdx (wordIdx - 1))
        else none

-      result := set result (patternIdx + 1) (wordIdx + 1) missScore? matchScore?
+      let mut matchScore? := none

-  return selectBest (getMiss result pattern.length word.length) (getMatch result pattern.length word.length)
+      if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) (patternRoles.get! patternIdx) (wordRoles.get! wordIdx) then
+        if patternIdx >= 1 then 
+          let runLength := runLengths.get! (getIdx (patternIdx - 1) (wordIdx - 1)) + 1
+          runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength
+
+          matchScore? := selectBest
+            (getMiss result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult
+              (pattern.get ⟨patternIdx⟩) (word.get ⟨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⟩)
+              (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⟩)
+              (patternRoles.get! patternIdx) (wordRoles.get! wordIdx)
+              none
+              (wordIdx == 0) - startPenalties.get! wordIdx
+
+      result := set result patternIdx wordIdx missScore? matchScore?
+
+  return selectBest (getMiss result (pattern.length - 1) (word.length - 1)) (getMatch result (pattern.length - 1) (word.length - 1))

  where
+    getDoubleIdx (patternIdx wordIdx : Nat) := patternIdx * word.length * 2 + wordIdx * 2
+
+    getIdx (patternIdx wordIdx : Nat) := patternIdx * word.length + wordIdx
+
    getMiss (result : Array (Option Int)) (patternIdx wordIdx : Nat) : Option Int :=
-      let idx := patternIdx * (word.length + 1) * 2 + wordIdx * 2
-      result.get! idx
+      result.get! $ getDoubleIdx patternIdx wordIdx

    getMatch (result : Array (Option Int)) (patternIdx wordIdx : Nat) : Option Int :=
-      let idx := patternIdx * (word.length + 1) * 2 + wordIdx * 2 + 1
-      result.get! idx
+      result.get! $ getDoubleIdx patternIdx wordIdx + 1

    set (result : Array (Option Int)) (patternIdx wordIdx : Nat) (missValue matchValue : Option Int) : Array (Option Int) :=
-      let idx := patternIdx * (word.length + 1) * 2 + wordIdx * 2
+      let idx := getDoubleIdx patternIdx wordIdx
      result |>.set! idx missValue |>.set! (idx + 1) matchValue

    /-- Heuristic to penalize skipping characters in the word. -/
-    skipPenalty (wordRole : CharRole) (patternComplete : Bool) (wordStart : Bool) : Int := Id.run do
-      /- Skipping characters if the match is already completed is free. -/
-      if patternComplete then
-        return 0
+    skipPenalty (wordRole : CharRole) (wordStart : Bool) : Int := Id.run do
      /- Skipping the beginning of the word. -/
      if wordStart then
        return 3
@ -171,18 +198,18 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr
      return true

    /-- Heuristic to rate a match. -/
-    matchResult (patternChar wordChar : Char) (patternRole wordRole : CharRole) (consecutive : Bool) (wordStart : Bool) : Int := Id.run do
-      let mut score := 1
+    matchResult (patternChar wordChar : Char) (patternRole wordRole : CharRole) (consecutive : Option Int) (wordStart : Bool) : 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
        score := score + 1
-      /- Beginning of the word or consecutive character match. -/
-      if wordStart || consecutive then
+      /- Beginning of the word. -/
+      if wordStart then
        score := score + 2
-      /- Match starts in the middle of a segment. -/
-      if wordRole matches CharRole.tail && !consecutive then
-        score := score - 3
-
+      /- Consecutive character match. -/
+      if let some bonus := consecutive then
+        /- consecutive run bonus -/
+        score := score + bonus 
      return score

 /-- Match the given pattern with the given word using a fuzzy matching
@ -205,13 +232,16 @@ def fuzzyMatchScore? (pattern word : String) : Option Float := Id.run do
  if pattern.length == word.length then
    score := score * 2

-  /- Perfect score per character given the heuristic in `matchResult`. -/
+  /- Perfect score per character. -/
  let perfect := 4
-  let normScore := Float.ofInt score / Float.ofInt (perfect * pattern.length)
+  /- Perfect score for full match given the heuristic in `matchResult`;
+  the latter term represents the bonus of a perfect consecutive run. -/
+  let perfectMatch := (perfect * pattern.length + ((pattern.length * (pattern.length + 1) / 2) - 1))
+  let normScore := Float.ofInt score / Float.ofInt perfectMatch

  return some <| min 1 (max 0 normScore)

-def fuzzyMatchScoreWithThreshold? (pattern word : String) (threshold := 0.2) : Option Float :=
+def fuzzyMatchScoreWithThreshold? (pattern word : String) (threshold := 0.1) : Option Float :=
  fuzzyMatchScore? pattern word |>.filter (· > threshold)

 /-- Match the given pattern with the given word using a fuzzy matching
--- a/tests/lean/interactive/863.lean.expected.out
+++ b/tests/lean/interactive/863.lean.expected.out
@ -1,14 +1,7 @@
 {"textDocument": {"uri": "file://863.lean"},
 "position": {"line": 3, "character": 12}}
 {"items":
- [{"label": "getRecAppSyntax?",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Retrieve (if available) the syntax object attached to a recursive application.\n",
-    "kind": "markdown"},
-   "detail": "Expr → Option Syntax"},
-  {"label": "getReducibilityStatus",
+ [{"label": "getReducibilityStatus",
   "kind": 3,
   "documentation":
   {"value": "Return the reducibility attribute for the given declaration. ",
@ -34,12 +27,19 @@
    "Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)\n",
    "kind": "markdown"},
   "detail": "[inst : Monad m] → [inst : MonadLog m] → m Position"},
-  {"label": "getRegularInitFnNameFor?",
-   "kind": 3,
-   "detail": "Environment → Name → Option Name"},
  {"label": "getRevAliases",
   "kind": 3,
   "detail": "Environment → Name → List Name"},
+  {"label": "getRecAppSyntax?",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "Retrieve (if available) the syntax object attached to a recursive application.\n",
+    "kind": "markdown"},
+   "detail": "Expr → Option Syntax"},
+  {"label": "getRegularInitFnNameFor?",
+   "kind": 3,
+   "detail": "Environment → Name → Option Name"},
  {"label": "getConstInfoRec",
   "kind": 3,
   "detail":
@ -48,14 +48,7 @@
 {"textDocument": {"uri": "file://863.lean"},
 "position": {"line": 7, "character": 12}}
 {"items":
- [{"label": "getRecAppSyntax?",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Retrieve (if available) the syntax object attached to a recursive application.\n",
-    "kind": "markdown"},
-   "detail": "Expr → Option Syntax"},
-  {"label": "getReducibilityStatus",
+ [{"label": "getReducibilityStatus",
   "kind": 3,
   "documentation":
   {"value": "Return the reducibility attribute for the given declaration. ",
@ -81,12 +74,19 @@
    "Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)\n",
    "kind": "markdown"},
   "detail": "[inst : Monad m] → [inst : MonadLog m] → m Position"},
-  {"label": "getRegularInitFnNameFor?",
-   "kind": 3,
-   "detail": "Environment → Name → Option Name"},
  {"label": "getRevAliases",
   "kind": 3,
   "detail": "Environment → Name → List Name"},
+  {"label": "getRecAppSyntax?",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "Retrieve (if available) the syntax object attached to a recursive application.\n",
+    "kind": "markdown"},
+   "detail": "Expr → Option Syntax"},
+  {"label": "getRegularInitFnNameFor?",
+   "kind": 3,
+   "detail": "Environment → Name → Option Name"},
  {"label": "getConstInfoRec",
   "kind": 3,
   "detail":
--- a/tests/lean/interactive/completion7.lean.expected.out
+++ b/tests/lean/interactive/completion7.lean.expected.out
@ -8,6 +8,13 @@
    "`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be\nconstructed and destructed like a pair: if `ha : a` and `hb : b` then\n`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.\n",
    "kind": "markdown"},
   "detail": "Prop → Prop → Prop"},
+  {"label": "and",
+   "kind": 3,
+   "documentation":
+   {"value":
+    "`and x y`, or `x && y`, is the boolean \"and\" operation (not to be confused\nwith `And : Prop → Prop → Prop`, which is the propositional connective).\nIt is `@[macroInline]` because it has C-like short-circuiting behavior:\nif `x` is false then `y` is not evaluated.\n",
+    "kind": "markdown"},
+   "detail": "Bool → Bool → Bool"},
  {"label": "AndOp",
   "kind": 7,
   "documentation":
@ -22,28 +29,18 @@
    "The homogeneous version of `HAndThen`: `a >> b : α` where `a b : α`.\nBecause `b` is \"lazy\" in this notation, it is passed as `Unit → α` to the\nimplementation so it can decide when to evaluate it.\n",
    "kind": "markdown"},
   "detail": "Type u → Type u"},
-  {"label": "and",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "`and x y`, or `x && y`, is the boolean \"and\" operation (not to be confused\nwith `And : Prop → Prop → Prop`, which is the propositional connective).\nIt is `@[macroInline]` because it has C-like short-circuiting behavior:\nif `x` is false then `y` is not evaluated.\n",
-    "kind": "markdown"},
-   "detail": "Bool → Bool → Bool"},
  {"label": "andM",
   "kind": 3,
   "detail": "[inst : Monad m] → [inst : ToBool β] → m β → m β → m β"},
+  {"label": "false_and",
+   "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": "Append",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. ",
-    "kind": "markdown"},
-   "detail": "Type u → Type u"},
  {"label": "HAnd",
   "kind": 7,
   "documentation":
@ -58,9 +55,6 @@
    "The typeclass behind the notation `a >> b : γ` where `a : α`, `b : β`.\nBecause `b` is \"lazy\" in this notation, it is passed as `Unit → β` to the\nimplementation so it can decide when to evaluate it.\n",
    "kind": "markdown"},
   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "false_and",
-   "kind": 3,
-   "detail": "∀ (p : Prop), (False ∧ p) = False"},
  {"label": "instAndOpUInt16", "kind": 21, "detail": "AndOp UInt16"},
  {"label": "instAndOpUInt32", "kind": 21, "detail": "AndOp UInt32"},
  {"label": "instAndOpUInt64", "kind": 21, "detail": "AndOp UInt64"},
@ -73,7 +67,6 @@
    "`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": "true_and", "kind": 3, "detail": "∀ (p : Prop), (True ∧ p) = p"},
  {"label": "instDecidableAnd",
   "kind": 3,
   "detail": "[dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)"},
@ -88,6 +81,13 @@
  {"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":
--- a/tests/lean/interactive/completionOption.lean.expected.out
+++ b/tests/lean/interactive/completionOption.lean.expected.out
@ -33,12 +33,48 @@
     "end": {"line": 1, "character": 13}}},
   "label": "format.width",
   "kind": 10,
-   "detail": "(120), indentation"}],
+   "detail": "(120), indentation"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 1, "character": 11},
+     "end": {"line": 1, "character": 13}},
+    "newText": "trace.PrettyPrinter.format",
+    "insert":
+    {"start": {"line": 1, "character": 11},
+     "end": {"line": 1, "character": 13}}},
+   "label": "trace.PrettyPrinter.format",
+   "kind": 10,
+   "detail":
+   "(false), enable/disable tracing for the given module and submodules"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 1, "character": 11},
+     "end": {"line": 1, "character": 13}},
+    "newText": "trace.Meta.isDefEq.foApprox",
+    "insert":
+    {"start": {"line": 1, "character": 11},
+     "end": {"line": 1, "character": 13}}},
+   "label": "trace.Meta.isDefEq.foApprox",
+   "kind": 10,
+   "detail":
+   "(false), enable/disable tracing for the given module and submodules"}],
 "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
 "position": {"line": 4, "character": 17}}
 {"items":
 [{"textEdit":
+   {"replace":
+    {"start": {"line": 4, "character": 11},
+     "end": {"line": 4, "character": 17}},
+    "newText": "trace.PrettyPrinter.format",
+    "insert":
+    {"start": {"line": 4, "character": 11},
+     "end": {"line": 4, "character": 17}}},
+   "label": "trace.PrettyPrinter.format",
+   "kind": 10,
+   "detail":
+   "(false), enable/disable tracing for the given module and submodules"},
+  {"textEdit":
   {"replace":
    {"start": {"line": 4, "character": 11},
     "end": {"line": 4, "character": 17}},
@ -70,19 +106,7 @@
     "end": {"line": 4, "character": 17}}},
   "label": "format.width",
   "kind": 10,
-   "detail": "(120), indentation"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 4, "character": 11},
-     "end": {"line": 4, "character": 17}},
-    "newText": "trace.PrettyPrinter.format",
-    "insert":
-    {"start": {"line": 4, "character": 11},
-     "end": {"line": 4, "character": 17}}},
-   "label": "trace.PrettyPrinter.format",
-   "kind": 10,
-   "detail":
-   "(false), enable/disable tracing for the given module and submodules"}],
+   "detail": "(120), indentation"}],
 "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
 "position": {"line": 7, "character": 20}}
@ -250,11 +274,11 @@
   {"replace":
    {"start": {"line": 10, "character": 11},
     "end": {"line": 10, "character": 18}},
-    "newText": "trace.Meta.IndPredBelow.match",
+    "newText": "trace.Meta.isLevelDefEq.postponed",
    "insert":
    {"start": {"line": 10, "character": 11},
     "end": {"line": 10, "character": 18}}},
-   "label": "trace.Meta.IndPredBelow.match",
+   "label": "trace.Meta.isLevelDefEq.postponed",
   "kind": 10,
   "detail":
   "(false), enable/disable tracing for the given module and submodules"},
@ -270,18 +294,6 @@
   "kind": 10,
   "detail":
   "(false), enable/disable tracing for the given module and submodules"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 10, "character": 11},
-     "end": {"line": 10, "character": 18}},
-    "newText": "trace.compiler.ir.push_proj",
-    "insert":
-    {"start": {"line": 10, "character": 11},
-     "end": {"line": 10, "character": 18}}},
-   "label": "trace.compiler.ir.push_proj",
-   "kind": 10,
-   "detail":
-   "(false), (trace) enable/disable tracing for the given module and submodules"},
  {"textEdit":
   {"replace":
    {"start": {"line": 10, "character": 11},
@ -322,14 +334,26 @@
   {"replace":
    {"start": {"line": 10, "character": 11},
     "end": {"line": 10, "character": 18}},
-    "newText": "trace.Meta.isLevelDefEq.postponed",
+    "newText": "trace.Meta.IndPredBelow.match",
    "insert":
    {"start": {"line": 10, "character": 11},
     "end": {"line": 10, "character": 18}}},
-   "label": "trace.Meta.isLevelDefEq.postponed",
+   "label": "trace.Meta.IndPredBelow.match",
   "kind": 10,
   "detail":
-   "(false), enable/disable tracing for the given module and submodules"}],
+   "(false), enable/disable tracing for the given module and submodules"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 10, "character": 11},
+     "end": {"line": 10, "character": 18}},
+    "newText": "trace.compiler.ir.push_proj",
+    "insert":
+    {"start": {"line": 10, "character": 11},
+     "end": {"line": 10, "character": 18}}},
+   "label": "trace.compiler.ir.push_proj",
+   "kind": 10,
+   "detail":
+   "(false), (trace) enable/disable tracing for the given module and submodules"}],
 "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
 "position": {"line": 13, "character": 19}}
@ -394,6 +418,18 @@
   "kind": 10,
   "detail":
   "(false), enable/disable tracing for the given module and submodules"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 13, "character": 11},
+     "end": {"line": 13, "character": 19}},
+    "newText": "trace.PrettyPrinter.parenthesize",
+    "insert":
+    {"start": {"line": 13, "character": 11},
+     "end": {"line": 13, "character": 19}}},
+   "label": "trace.PrettyPrinter.parenthesize",
+   "kind": 10,
+   "detail":
+   "(false), enable/disable tracing for the given module and submodules"},
  {"textEdit":
   {"replace":
    {"start": {"line": 13, "character": 11},
@ -418,30 +454,6 @@
   "kind": 10,
   "detail":
   "(false), enable/disable tracing for the given module and submodules"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 13, "character": 11},
-     "end": {"line": 13, "character": 19}},
-    "newText": "trace.PrettyPrinter.parenthesize",
-    "insert":
-    {"start": {"line": 13, "character": 11},
-     "end": {"line": 13, "character": 19}}},
-   "label": "trace.PrettyPrinter.parenthesize",
-   "kind": 10,
-   "detail":
-   "(false), enable/disable tracing for the given module and submodules"},
-  {"textEdit":
-   {"replace":
-    {"start": {"line": 13, "character": 11},
-     "end": {"line": 13, "character": 19}},
-    "newText": "trace.compiler.ir.push_proj",
-    "insert":
-    {"start": {"line": 13, "character": 11},
-     "end": {"line": 13, "character": 19}}},
-   "label": "trace.compiler.ir.push_proj",
-   "kind": 10,
-   "detail":
-   "(false), (trace) enable/disable tracing for the given module and submodules"},
  {"textEdit":
   {"replace":
    {"start": {"line": 13, "character": 11},
@ -465,7 +477,19 @@
   "label": "trace.Meta.isLevelDefEq.postponed",
   "kind": 10,
   "detail":
-   "(false), enable/disable tracing for the given module and submodules"}],
+   "(false), enable/disable tracing for the given module and submodules"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 13, "character": 11},
+     "end": {"line": 13, "character": 19}},
+    "newText": "trace.compiler.ir.push_proj",
+    "insert":
+    {"start": {"line": 13, "character": 11},
+     "end": {"line": 13, "character": 19}}},
+   "label": "trace.compiler.ir.push_proj",
+   "kind": 10,
+   "detail":
+   "(false), (trace) enable/disable tracing for the given module and submodules"}],
 "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
 "position": {"line": 16, "character": 23}}
@ -606,7 +630,31 @@
     "end": {"line": 22, "character": 13}}},
   "label": "format.width",
   "kind": 10,
-   "detail": "(120), indentation"}],
+   "detail": "(120), indentation"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 22, "character": 11},
+     "end": {"line": 22, "character": 13}},
+    "newText": "trace.PrettyPrinter.format",
+    "insert":
+    {"start": {"line": 22, "character": 11},
+     "end": {"line": 22, "character": 13}}},
+   "label": "trace.PrettyPrinter.format",
+   "kind": 10,
+   "detail":
+   "(false), enable/disable tracing for the given module and submodules"},
+  {"textEdit":
+   {"replace":
+    {"start": {"line": 22, "character": 11},
+     "end": {"line": 22, "character": 13}},
+    "newText": "trace.Meta.isDefEq.foApprox",
+    "insert":
+    {"start": {"line": 22, "character": 11},
+     "end": {"line": 22, "character": 13}}},
+   "label": "trace.Meta.isDefEq.foApprox",
+   "kind": 10,
+   "detail":
+   "(false), enable/disable tracing for the given module and submodules"}],
 "isIncomplete": true}
 {"textDocument": {"uri": "file://completionOption.lean"},
 "position": {"line": 25, "character": 18}}
--- a/tests/lean/interactive/completionPrv.lean.expected.out
+++ b/tests/lean/interactive/completionPrv.lean.expected.out
@ -6,10 +6,7 @@
 "position": {"line": 9, "character": 11}}
 {"items":
 [{"label": "booBoo", "kind": 21, "detail": "Nat"},
-  {"label": "instToBoolBool", "kind": 21, "detail": "ToBool Bool"},
-  {"label": "instLawfulBEqBoolInstBEqInstDecidableEqBool",
-   "kind": 21,
-   "detail": "LawfulBEq Bool"}],
+  {"label": "instToBoolBool", "kind": 21, "detail": "ToBool Bool"}],
 "isIncomplete": true}
 {"textDocument": {"uri": "file://completionPrv.lean"},
 "position": {"line": 21, "character": 5}}
--- a/tests/lean/interactive/dotIdCompletion.lean.expected.out
+++ b/tests/lean/interactive/dotIdCompletion.lean.expected.out
@ -2,6 +2,5 @@
 "position": {"line": 4, "character": 5}}
 {"items":
 [{"label": "true", "kind": 4, "detail": "Boo"},
-  {"label": "truth", "kind": 4, "detail": "Boo"},
-  {"label": "toCtorIdx", "kind": 3, "detail": "Boo → Nat"}],
+  {"label": "truth", "kind": 4, "detail": "Boo"}],
 "isIncomplete": true}
--- a/tests/lean/interactive/keywordCompletion.lean.expected.out
+++ b/tests/lean/interactive/keywordCompletion.lean.expected.out
@ -9,11 +9,12 @@
 {"items":
 [{"label": "register_string", "kind": 14, "detail": "keyword"},
  {"label": "regular", "kind": 21, "detail": "Nat"},
+  {"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": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"},
-  {"label": "instReprStdGen", "kind": 21, "detail": "Repr StdGen"}],
+  {"label": "reprArg",
+   "kind": 3,
+   "detail": "[inst : Repr α] → α → Std.Format"}],
 "isIncomplete": true}