From b36baa143faee0b016b190913c6c176b352bde2f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 21 Aug 2021 11:36:54 -0700 Subject: [PATCH] feat: improved name-unresolving in delab Fixes #641 --- .../PrettyPrinter/Delaborator/Builtins.lean | 85 ++++++------------- tests/lean/236.lean.expected.out | 4 +- tests/lean/243.lean.expected.out | 4 +- tests/lean/593.lean.expected.out | 4 +- tests/lean/641.lean | 15 ++++ tests/lean/641.lean.expected.out | 8 ++ .../lean/eagerCoeExpansion.lean.expected.out | 8 +- tests/lean/infoFromFailure.lean.expected.out | 2 +- tests/lean/interactive/amb.lean.expected.out | 5 +- 9 files changed, 63 insertions(+), 72 deletions(-) create mode 100644 tests/lean/641.lean create mode 100644 tests/lean/641.lean.expected.out diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 195b34b73a..a25cc1c739 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/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 diff --git a/tests/lean/236.lean.expected.out b/tests/lean/236.lean.expected.out index 226d08e3ac..c655f84b70 100644 --- a/tests/lean/236.lean.expected.out +++ b/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 diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out index a036080057..43b4d5473d 100644 --- a/tests/lean/243.lean.expected.out +++ b/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 diff --git a/tests/lean/593.lean.expected.out b/tests/lean/593.lean.expected.out index 72801ee021..e2a8396f88 100644 --- a/tests/lean/593.lean.expected.out +++ b/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 diff --git a/tests/lean/641.lean b/tests/lean/641.lean new file mode 100644 index 0000000000..eea9d35928 --- /dev/null +++ b/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 diff --git a/tests/lean/641.lean.expected.out b/tests/lean/641.lean.expected.out new file mode 100644 index 0000000000..121e2d76dc --- /dev/null +++ b/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 diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out index 302ae9104f..d22e494825 100644 --- a/tests/lean/eagerCoeExpansion.lean.expected.out +++ b/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 diff --git a/tests/lean/infoFromFailure.lean.expected.out b/tests/lean/infoFromFailure.lean.expected.out index 09da1a7d4b..c523330fa4 100644 --- a/tests/lean/infoFromFailure.lean.expected.out +++ b/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 diff --git a/tests/lean/interactive/amb.lean.expected.out b/tests/lean/interactive/amb.lean.expected.out index bd11b94bea..31b6c70a09 100644 --- a/tests/lean/interactive/amb.lean.expected.out +++ b/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"}}