diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index 3d1bbdbb8e..586a7e4a4b 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -395,13 +395,6 @@ def isInaccessibleUserName : Name → Bool | Name.num p idx _ => isInaccessibleUserName p | _ => false -private def sanitizeMacroScopes (unicode : Bool) (mainModule : Name) (userName : Name) : Name := -if !userName.hasMacroScopes then - userName -else - let userName := if (extractMacroScopes userName).mainModule == mainModule then userName.simpMacroScopes else userName; - mkInaccessibleUserName unicode userName - private partial def mkFreshInaccessibleUserName (unicode : Bool) (usedName2Idx : NameMap Nat) (userName : Name) : Nat → Name × NameMap Nat | idx => let userNameNew := mkInaccessibleUserName unicode (mkNameNum userName idx); @@ -410,21 +403,33 @@ private partial def mkFreshInaccessibleUserName (unicode : Bool) (usedName2Idx : else (userNameNew, usedName2Idx.insert userName (idx+1)) -def sanitizeNames (lctx : LocalContext) (options : Options) (mainModule : Name) : LocalContext := +def sanitizeNamesDefault := true +@[init] def sanitizeNamesOption : IO Unit := +registerOption `pp.sanitizeNames { defValue := sanitizeNamesDefault, group := "pp", descr := "add suffix '_{}' to shadowed variables when pretty printing" } +def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeNamesDefault + +def sanitizeNames (lctx : LocalContext) (options : Options) : LocalContext := +if !getSanitizeNames options then lctx else let unicode := Format.getUnicode options; let (lctx, _) := lctx.decls.size.foldRev (fun i (acc : LocalContext × NameMap Nat) => let (lctx, usedName2Idx) := acc; match lctx.decls.get! i with | none => acc - | some decl => do - let userName := decl.userName.eraseMacroScopes; - match usedName2Idx.find? userName with - | none => (lctx, usedName2Idx.insert userName 1) - | some idx => + | some decl => + let mkFreshUserName (userName : Name) (idx : Nat) : LocalContext × NameMap Nat := let (userNameNew, usedName2Idx) := mkFreshInaccessibleUserName unicode usedName2Idx userName idx; let lctx := lctx.setUserName decl.fvarId userNameNew; - (lctx, usedName2Idx)) + (lctx, usedName2Idx); + let userName := decl.userName; + if userName.hasMacroScopes then + let userName := userName.eraseMacroScopes; + let idx := (usedName2Idx.find? userName).getD 1; + mkFreshUserName userName idx + else + match usedName2Idx.find? userName with + | none => (lctx, usedName2Idx.insert userName 1) + | some idx => mkFreshUserName userName idx) (lctx, {}); lctx diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 71ea3ff1d7..64dd972219 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -58,16 +58,8 @@ registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "m def getSyntaxMaxDepth (opts : Options) : Nat := opts.getNat `syntaxMaxDepth 2 -def sanitizeNamesDefault := true -@[init] def sanitizeNamesOption : IO Unit := -registerOption `pp.sanitizeNames { defValue := sanitizeNamesDefault, group := "pp", descr := "add suffix '_{}' to shadowed variables when pretty printing" } -def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeNamesDefault - private def sanitizeNames (ctx : MessageDataContext) : MessageDataContext := -if getSanitizeNames ctx.opts then - { ctx with lctx := ctx.lctx.sanitizeNames ctx.opts ctx.env.mainModule } -else - ctx +{ ctx with lctx := ctx.lctx.sanitizeNames ctx.opts } def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, diff --git a/src/Lean/Util/PPGoal.lean b/src/Lean/Util/PPGoal.lean index a28294ef46..851347c142 100644 --- a/src/Lean/Util/PPGoal.lean +++ b/src/Lean/Util/PPGoal.lean @@ -22,6 +22,7 @@ match mctx.findDecl? mvarId with let indent := 2; -- Use option let showAuxDecls := getShowAuxDecls opts; let lctx := mvarDecl.lctx; + let lctx := lctx.sanitizeNames opts; let ppCtx := { ppCtx with lctx := lctx }; let pp (e : Expr) : IO Format := ppExpr ppCtx e; let instMVars (e : Expr) : Expr := (mctx.instantiateMVars e).1; @@ -38,7 +39,7 @@ match mctx.findDecl? mvarId with typeFmt ← pp type; pure $ fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group }; - (varNames, type?, fmt) ← mvarDecl.lctx.foldlM + (varNames, type?, fmt) ← lctx.foldlM (fun (acc : List Name × Option Expr × Format) (localDecl : LocalDecl) => if !showAuxDecls && localDecl.isAuxDecl then pure acc else let (varNames, prevType?, fmt) := acc; diff --git a/tests/lean/shadow.lean b/tests/lean/shadow.lean index cf058abc50..166e02105c 100644 --- a/tests/lean/shadow.lean +++ b/tests/lean/shadow.lean @@ -3,7 +3,14 @@ new_frontend theorem ex1 {α} (x : α) (h : x = x) (x : α) : x = x := h -set_option pp.sanitizeNames false - +set_option pp.sanitizeNames false in theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x := h -- this error is confusing because we have disabled `pp.sanitizeNames` + +set_option pp.sanitizeNames true in +def foo {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ := +_ + +set_option pp.sanitizeNames false in +def foo {α} [Inhabited α] (inst inst : α) : {β δ : Type} → α → β → δ → α × β × δ := +_ diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index ef0810763b..ff1852c881 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/tests/lean/shadow.lean.expected.out @@ -6,7 +6,7 @@ but it is expected to have type x=x failed to synthesize instance CoeT (x✝¹=x✝¹) _ (x=x) -shadow.lean:9:0: error: type mismatch +shadow.lean:8:0: error: type mismatch h has type x=x @@ -14,3 +14,26 @@ but it is expected to have type x=x failed to synthesize instance CoeT (x=x) _ (x=x) +with resulting expansion + section set_option pp.sanitizeNames false theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x := + h -- this error is confusing because we have disabled `pp.sanitizeNames` + + end +while expanding + set_option pp.sanitizeNames false in + theorem ex2 {α} (x : α) (h : x = x) (x : α) : x = x := + h +shadow.lean:12:0: error: don't know how to synthesize placeholder +context: +α : Type u_1 +inst✝² : Inhabited α +inst✝¹ inst : α +β✝¹ δ✝¹ : Type +⊢ α → β✝¹ → δ✝¹ → α×β✝¹×δ✝¹ +shadow.lean:16:0: error: don't know how to synthesize placeholder +context: +α : Type u_1 +inst.19 : Inhabited α +inst inst : α +β.44 δ.45 : Type +⊢ α → β.44 → δ.45 → α×β.44×δ.45