feat: improved name-unresolving in delab

Fixes #641

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -57,72 +57,39 @@ def delabSort : Delab := do
     | some l' => `(Type $(Level.quote l' max_prec))
     | none    => `(Sort $(Level.quote l max_prec))
 
--- find shorter names for constants, in reverse to Lean.Elab.ResolveName
 
-private def unresolveQualifiedName (ns : Name) (c : Name) : DelabM Name := do
-  let c' := c.replacePrefix ns Name.anonymous;
-  let env ← getEnv
-  guard $ c' != c && !c'.isAnonymous && (!c'.isAtomic || !isProtected env c)
-  pure c'
-
-private def checkForNameClash (nsOrig nsPfix candidate : Name) : DelabM Unit := do
-  -- Suppose the current namespace is `Foo.Bar`, we are delaborating `Foo.rig`, and `Foo.Bar.rig`
-  -- already exists. This function will detect the clash and fail.
-  let rest := nsOrig.components.drop nsPfix.components.length
-  let mut nsPfix := nsPfix
-  for component in rest do
-    nsPfix := nsPfix ++ component
-    let candidate := nsPfix ++ candidate
-    -- TODO: what are the elab rules for 'protected' declarations?
-    guard ((← getEnv).find? candidate |>.isNone)
-
-private partial def unresolveUsingNamespace (c ns : Name) : DelabM Name := core ns where
-  core
-    | nsPfix@(Name.str p _ _) =>
-      (do let candidate ← unresolveQualifiedName nsPfix c; checkForNameClash ns nsPfix candidate; candidate)
-      <|> core p
-    | _ => failure
-
-private def unresolveOpenDecls (c : Name) : List OpenDecl → DelabM Name
-  | [] => failure
-  | OpenDecl.simple ns exs :: openDecls =>
-    let c' := c.replacePrefix ns Name.anonymous
-    if c' == c || exs.elem c' then unresolveOpenDecls c openDecls
-    else unresolveQualifiedName ns c <|> unresolveOpenDecls c openDecls
-  | OpenDecl.explicit openedId resolvedId :: openDecls =>
-    (guard (c == resolvedId) *> pure openedId) <|> unresolveOpenDecls c openDecls
+def unresolveNameGlobal (n₀ : Name) : DelabM Name := do
+  if n₀.hasMacroScopes then return n₀
+  let mut initialNames := #[]
+  if !(← getPPOption getPPFullNames) then initialNames := initialNames ++ getRevAliases (← getEnv) n₀
+  initialNames := initialNames.push (rootNamespace ++ n₀)
+  for initialName in initialNames do
+    match (← unresolveNameCore initialName) with
+    | none => continue
+    | some n => return n
+  return n₀ -- if can't resolve, return the original
+where
+  unresolveNameCore (n : Name) : DelabM (Option Name) := do
+    let mut revComponents := n.components'
+    let mut candidate := Name.anonymous
+    for i in [:revComponents.length] do
+      match revComponents with
+      | [] => return none
+      | cmpt::rest => candidate := cmpt ++ candidate; revComponents := rest
+      match (← resolveGlobalName candidate) with
+      | [(potentialMatch, _)] => if potentialMatch == n₀ then return some candidate else continue
+      | _ => continue
+    return none
 
 -- NOTE: not a registered delaborator, as `const` is never called (see [delab] description)
 def delabConst : Delab := do
-  let Expr.const c ls _ ← getExpr | unreachable!
-  let c₀ := c
+  let Expr.const c₀ ls _ ← getExpr | unreachable!
   let ctx ← read
-  let maybeAddRoot (c : Name) : DelabM Name := do
-    (do checkForNameClash ctx.currNamespace Name.anonymous c
-        pure c)
-    <|>
-    (do guard (c == c₀)
-        guard (! (← read).inPattern)
-        guard ((← getEnv).contains c)
-        pure (`_root_ ++ c))
-    <|> (pure c₀)
-
-  let mut c ← if (← getPPOption getPPFullNames) then maybeAddRoot c else
-    let env ← getEnv
-    let as := getRevAliases env c
-    -- might want to use a more clever heuristic such as selecting the shortest alias...
-    let c := as.headD c
-    unresolveUsingNamespace c ctx.currNamespace
-      <|> unresolveOpenDecls c ctx.openDecls
-      <|> maybeAddRoot c
-
-  unless (← getPPOption getPPPrivateNames) do
-    c := (privateToUserName? c).getD c
-
-  let ppUnivs ← getPPOption getPPUniverses
+  let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
 
+  let mut c ← unresolveNameGlobal c₀
   let stx ←
-    if ls.isEmpty || !ppUnivs then
+    if ls.isEmpty || !(← getPPOption getPPUniverses) then
       if (← getLCtx).usesUserName c then
         -- `c` is also a local declaration
         if c == c₀ && !(← read).inPattern then

tests/lean/236.lean.expected.out

@@ -1,3 +1,3 @@
 { x := 10, b := true } : Foo
-Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo
-{ x := OfNat.ofNat 10, b := Bool.true : Foo } : Foo
+Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) true : Foo
+{ x := OfNat.ofNat 10, b := true : Foo } : Foo

tests/lean/243.lean.expected.out

@@ -7,9 +7,9 @@ has type
 but is expected to have type
   Bool : Type
 243.lean:13:3-13:8: error: application type mismatch
-  { fst := A, snd := A.a }
+  { fst := A, snd := a }
 argument
-  A.a
+  a
 has type
   Foo.A : Type
 but is expected to have type

tests/lean/593.lean.expected.out

@@ -1,8 +1,8 @@
 Foo.bar : Nat
 bar : Nat
-Foo.bar : Nat
+bar : Nat
 593.lean:21:7-21:10: error: unknown identifier 'boo'
 593.lean:26:7-26:10: error: unknown identifier 'bar'
 boo : Nat
 Foo.bar : Nat
-Foo.bar : Nat
+bar : Nat

tests/lean/641.lean

@@ -0,0 +1,15 @@
+def Foo.x : Unit := ()
+def Bar.x : Unit := ()
+def y : Unit := Foo.x
+
+open Foo Bar
+
+#print y
+
+def y' : Unit := x
+
+def x := 1
+
+namespace Rig
+def x := _root_.x
+#print x

tests/lean/641.lean.expected.out

@@ -0,0 +1,8 @@
+def y : Unit :=
+Foo.x
+641.lean:9:17-9:18: error: ambiguous, possible interpretations 
+  Bar.x
+  
+  Foo.x
+def Rig.x : Nat :=
+_root_.x

tests/lean/eagerCoeExpansion.lean.expected.out

@@ -8,18 +8,18 @@ fun (a : Nat) =>
     (@Eq.{1} Bool
       (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      Bool.true)
+      true)
     (instDecidableEqBool
       (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      Bool.true)
+      true)
     (@Eq.{1} Bool
       (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
-      Bool.true)
+      true)
     (@Eq.{1} Bool
       (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
         (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
-      Bool.true)
+      true)
 def s : Option Nat :=
 ConstantFunction.f myFun 3 <|> ConstantFunction.f myFun 4

tests/lean/infoFromFailure.lean.expected.out

@@ -1,4 +1,4 @@
-foo "hello" : String × String
+B.foo "hello" : String × String
 [Meta.synthInstance] preprocess: Add String ==> Add String
   [Meta.synthInstance] 
     [Meta.synthInstance] main goal Add String

tests/lean/interactive/amb.lean.expected.out

@@ -2,9 +2,10 @@
  "position": {"line": 17, "character": 19}}
 {"range":
  {"start": {"line": 17, "character": 19}, "end": {"line": 17, "character": 20}},
- "contents": {"value": "```lean\nf : Nat → Bool\n```", "kind": "markdown"}}
+ "contents": {"value": "```lean\nFoo.f : Nat → Bool\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://amb.lean"},
  "position": {"line": 19, "character": 19}}
 {"range":
  {"start": {"line": 19, "character": 19}, "end": {"line": 19, "character": 20}},
- "contents": {"value": "```lean\nf : String → String\n```", "kind": "markdown"}}
+ "contents":
+ {"value": "```lean\nBoo.f : String → String\n```", "kind": "markdown"}}