refactor: move ppGoal to Meta

We need `MetaM` methods such as `isProp` to improve `ppGoal`.
This commit also moves `currNamespace` and `openDecls` to
`Core.Context`. Without this change, `Meta.ppExpr` was not taking
`open` commands into account.

src/Lean/Attributes.lean

@@ -20,21 +20,12 @@ def AttributeApplicationTime.beq : AttributeApplicationTime → AttributeApplica
 
 instance : BEq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩
 
-structure Attr.Context :=
-  (currNamespace : Name)
-  (openDecls     : List OpenDecl)
-
-abbrev AttrM := ReaderT Attr.Context CoreM
+abbrev AttrM := CoreM
 
 instance : MonadLift ImportM AttrM := {
   monadLift := fun x => do liftM (m := IO) (x { env := (← getEnv), opts := (← getOptions) })
 }
 
-instance : MonadResolveName AttrM := {
-  getCurrNamespace := do pure (← read).currNamespace,
-  getOpenDecls     := do pure (← read).openDecls
-}
-
 structure AttributeImplCore :=
   (name : Name)
   (descr : String)

src/Lean/CoreM.lean

@@ -10,6 +10,7 @@ import Lean.Exception
 import Lean.InternalExceptionId
 import Lean.Eval
 import Lean.MonadEnv
+import Lean.ResolveName
 
 namespace Lean
 namespace Core
@@ -27,6 +28,8 @@ structure Context :=
   (currRecDepth   : Nat := 0)
   (maxRecDepth    : Nat := 1000)
   (ref            : Syntax := Syntax.missing)
+  (currNamespace  : Name := Name.anonymous)
+  (openDecls      : List OpenDecl := [])
 
 abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception)
 
@@ -60,6 +63,11 @@ instance : MonadRecDepth CoreM := {
   getMaxRecDepth := do pure (← read).maxRecDepth
 }
 
+instance : MonadResolveName CoreM := {
+  getCurrNamespace := do pure (← read).currNamespace,
+  getOpenDecls     := do pure (← read).openDecls
+}
+
 @[inline] def liftIOCore (x : IO α) : CoreM α := do
   let ref ← getRef
   IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x

src/Lean/Elab/Command.lean

@@ -97,11 +97,13 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
   mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
 
 private def mkCoreContext (ctx : Context) (s : State) : Core.Context :=
-  let scope      := s.scopes.head!;
-  { options      := scope.opts,
-    currRecDepth := ctx.currRecDepth,
-    maxRecDepth  := s.maxRecDepth,
-    ref          := ctx.ref }
+  let scope       := s.scopes.head!
+  { options       := scope.opts
+    currRecDepth  := ctx.currRecDepth
+    maxRecDepth   := s.maxRecDepth
+    ref           := ctx.ref
+    currNamespace := scope.currNamespace
+    openDecls     := scope.openDecls }
 
 def liftCoreM {α} (x : CoreM α) : CommandElabM α := do
   let s ← get
@@ -260,9 +262,7 @@ private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name)
     fileName       := ctx.fileName,
     fileMap        := ctx.fileMap,
     currMacroScope := ctx.currMacroScope,
-    currNamespace  := scope.currNamespace,
     levelNames     := scope.levelNames,
-    openDecls      := scope.openDecls,
     declName?      := declName? }
 
 private def addTraceAsMessages (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog :=

src/Lean/Elab/Term.lean

@@ -69,10 +69,8 @@ def setElabConfig (cfg : Meta.Config) : Meta.Config :=
 structure Context :=
   (fileName        : String)
   (fileMap         : FileMap)
-  (currNamespace   : Name)
   (declName?       : Option Name     := none)
   (levelNames      : List Name       := [])
-  (openDecls       : List OpenDecl   := [])
   (macroStack      : MacroStack      := [])
   (currMacroScope  : MacroScope      := firstFrontendMacroScope)
   /- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
@@ -236,7 +234,7 @@ instance : MonadLog TermElabM := {
   getFileMap  := do pure (← read).fileMap,
   getFileName := do pure (← read).fileName,
   logMessage  := fun msg => do
-    let ctx ← read
+    let ctx ← readThe Core.Context
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
     modify fun s => { s with messages := s.messages.add msg }
 }
@@ -278,11 +276,6 @@ instance : ToString LVal := ⟨fun
   | LVal.fieldName n => n
   | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩
 
-instance : MonadResolveName TermElabM := {
-  getCurrNamespace := do pure (← read).currNamespace,
-  getOpenDecls     := do pure (← read).openDecls
-}
-
 def getDeclName? : TermElabM (Option Name) := return (← read).declName?
 def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecsToLift
 def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := return (← getMCtx).isExprAssigned mvarId
@@ -465,7 +458,7 @@ def mkFreshIdent (ref : Syntax) : TermElabM Syntax :=
 
 private def liftAttrM {α} (x : AttrM α) : TermElabM α := do
   let ctx ← read
-  liftCoreM $ x.run { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls }
+  liftCoreM x
 
 private def applyAttributesCore
     (declName : Name) (attrs : Array Attribute)
@@ -1275,9 +1268,8 @@ fun stx _ =>
   | some msg => elabTermEnsuringType stx[2] expectedType? true msg
 
 private def mkSomeContext : Context := {
-  fileName      := "<TermElabM>",
-  fileMap       := arbitrary,
-  currNamespace := Name.anonymous
+  fileName      := "<TermElabM>"
+  fileMap       := arbitrary
 }
 
 @[inline] def TermElabM.run {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM (α × State) :=

src/Lean/Message.lean

@@ -11,7 +11,6 @@ import Lean.Syntax
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Util.PPExt
-import Lean.Util.PPGoal
 
 namespace Lean
 

src/Lean/Meta.lean

@@ -25,3 +25,4 @@ import Lean.Meta.Closure
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
 import Lean.Meta.Transform
+import Lean.Meta.PPGoal

src/Lean/Meta/Basic.lean

@@ -995,7 +995,8 @@ def ppExprImp (e : Expr) : MetaM Format := do
   let mctx ← getMCtx
   let lctx ← getLCtx
   let opts ← getOptions
-  Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e
+  let ctxCore  ← readThe Core.Context
+  Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts, currNamespace := ctxCore.currNamespace, openDecls := ctxCore.openDecls  } e
 
 def ppExpr (e : Expr) : m Format :=
   liftMetaM $ ppExprImp e

src/Lean/Meta/PPGoal.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Lean.Util.PPExt
+import Lean.Meta.Basic
 
-namespace Lean
+namespace Lean.Meta
 
 def ppAuxDeclsDefault := false
 builtin_initialize
@@ -13,24 +13,26 @@ builtin_initialize
 def getAuxDeclsOption (o : Options) : Bool :=
   o.get `pp.auxDecls ppAuxDeclsDefault
 
-def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
-  let env  := ppCtx.env
-  let mctx := ppCtx.mctx
-  let opts := ppCtx.opts
-  match mctx.findDecl? mvarId with
+def ppInaccessibleDefault := false
+builtin_initialize
+  registerOption `pp.inaccessible { defValue := ppInaccessibleDefault, group := "pp", descr := "display inaccessible declarations in the local context" }
+def getInaccessibleOption (o : Options) : Bool :=
+  o.get `pp.inaccessible ppInaccessibleDefault
+
+def ppGoal (mvarId : MVarId) : MetaM Format := do
+  match (← getMCtx).findDecl? mvarId with
   | none          => pure "unknown goal"
   | some mvarDecl => do
-    let indent       := 2 -- Use option
-    let ppAuxDecls   := getAuxDeclsOption opts
-    let lctx         := mvarDecl.lctx
-    let lctx         := lctx.sanitizeNames.run' { options := 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
+    let indent         := 2 -- Use option
+    let ppAuxDecls     := getAuxDeclsOption (← getOptions)
+    let ppInaccessible := getInaccessibleOption (← getOptions)
+    let lctx           := mvarDecl.lctx
+    let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
+    withLCtx lctx mvarDecl.localInstances do
     let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line
     -- The followint two `let rec`s are being used to control the generated code size.
     -- Then should be remove after we rewrite the compiler in Lean
-    let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : IO Format :=
+    let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format :=
       if ids.isEmpty then
         pure fmt
       else
@@ -39,13 +41,13 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
         | [], _        => pure fmt
         | _, none      => pure fmt
         | _, some type => do
-          let typeFmt ← pp type
+          let typeFmt ← ppExpr type
           pure $ fmt ++ (Format.joinSep ids.reverse " " ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group
-    let rec ppVars (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : IO (List Name × Option Expr × Format) := do
+    let rec ppVars (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : MetaM (List Name × Option Expr × Format) := do
       match localDecl with
       | LocalDecl.cdecl _ _ varName type _   =>
         let varName := varName.simpMacroScopes
-        let type := instMVars type
+        let type ← instantiateMVars type
         if prevType? == none || prevType? == some type then
           pure (varName :: varNames, some type, fmt)
         else do
@@ -55,10 +57,10 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
         let varName := varName.simpMacroScopes
         let fmt ← pushPending varNames prevType? fmt
         let fmt  := addLine fmt
-        let type := instMVars type
-        let val  := instMVars val
-        let typeFmt ← pp type
-        let valFmt ← pp val
+        let type ← instantiateMVars type
+        let val  ← instantiateMVars val
+        let typeFmt ← ppExpr type
+        let valFmt ← ppExpr val
         let fmt  := fmt ++ (format varName ++ " : " ++ typeFmt ++ " :=" ++ Format.nest indent (Format.line ++ valFmt)).group
         pure ([], none, fmt)
     let (varNames, type?, fmt) ← lctx.foldlM (init := ([], none, Format.nil)) fun (varNames, prevType?, fmt) (localDecl : LocalDecl) =>
@@ -68,10 +70,10 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
          ppVars varNames prevType? fmt localDecl
     let fmt ← pushPending varNames type? fmt
     let fmt := addLine fmt
-    let typeFmt ← pp mvarDecl.type
+    let typeFmt ← ppExpr mvarDecl.type
     let fmt := fmt ++ "⊢" ++ " " ++ Format.nest indent typeFmt
     match mvarDecl.userName with
     | Name.anonymous => pure fmt
-    | name           => pure $ "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
+    | name           => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
 
-end Lean
+end Lean.Meta

src/Lean/Meta/Tactic/Util.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.LevelDefEq
+import Lean.Meta.PPGoal
 
 namespace Lean.Meta
 
@@ -42,9 +43,6 @@ def getMVarType (mvarId : MVarId) : MetaM Expr := do
 def getMVarType' (mvarId : MVarId) : MetaM Expr := do
   whnf (← instantiateMVars (← getMVarDecl mvarId).type)
 
-def ppGoal (mvarId : MVarId) : MetaM Format := do
-  Lean.ppGoal { env := (← getEnv), mctx := (← getMCtx), opts := (← getOptions) } mvarId
-
 builtin_initialize registerTraceClass `Meta.Tactic
 
 /-- Assign `mvarId` to `sorryAx` -/

src/Lean/PrettyPrinter.lean

@@ -12,10 +12,10 @@ import Lean.ParserCompiler
 namespace Lean
 
 def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
-  Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }
+  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls } { env := ppCtx.env }
 
 def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
-  ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
+  ppCtx.runCoreM <| x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
 
 namespace PrettyPrinter
 
@@ -60,8 +60,9 @@ private def withoutContext {m} [MonadExcept Exception m] (x : m Format) : m Form
 
 builtin_initialize
   ppFnsRef.set {
-    ppExpr := fun ctx e   => ctx.runMetaM $ withoutContext $ ppExpr ctx.currNamespace ctx.openDecls e,
-    ppTerm := fun ctx stx => ctx.runCoreM $ withoutContext $ ppTerm stx,
+    ppExpr := fun ctx e      => ctx.runMetaM $ withoutContext $ ppExpr ctx.currNamespace ctx.openDecls e,
+    ppTerm := fun ctx stx    => ctx.runCoreM $ withoutContext $ ppTerm stx,
+    ppGoal := fun ctx mvarId => ctx.runMetaM $ withoutContext $ Meta.ppGoal mvarId
   }
 
 builtin_initialize

src/Lean/Util.lean

@@ -9,7 +9,6 @@ import Lean.Util.CollectMVars
 import Lean.Util.FindMVar
 import Lean.Util.MonadCache
 import Lean.Util.PPExt
-import Lean.Util.PPGoal
 import Lean.Util.Path
 import Lean.Util.Profile
 import Lean.Util.RecDepth

src/Lean/Util/PPExt.lean

@@ -19,40 +19,45 @@ def getSyntaxMaxDepth (opts : Options) : Nat :=
 def getPPRaw (opts : Options) : Bool :=
   opts.getBool `pp.raw false
 
-structure PPContext :=
-  (env           : Environment)
-  (mctx          : MetavarContext := {})
-  (lctx          : LocalContext := {})
-  (opts          : Options := {})
-  (currNamespace : Name := Name.anonymous)
-  (openDecls     : List OpenDecl := [])
+structure PPContext where
+  env           : Environment
+  mctx          : MetavarContext := {}
+  lctx          : LocalContext := {}
+  opts          : Options := {}
+  currNamespace : Name := Name.anonymous
+  openDecls     : List OpenDecl := []
 
-structure PPFns :=
-  (ppExpr : PPContext → Expr → IO Format)
-  (ppTerm : PPContext → Syntax → IO Format)
+structure PPFns where
+  ppExpr : PPContext → Expr → IO Format
+  ppTerm : PPContext → Syntax → IO Format
+  ppGoal : PPContext → MVarId → IO Format
 
-instance : Inhabited PPFns := ⟨⟨arbitrary, arbitrary⟩⟩
+instance : Inhabited PPFns := ⟨⟨arbitrary, arbitrary, arbitrary⟩⟩
 
 builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
-    ppExpr := fun ctx e   => pure $ format (toString e),
-    ppTerm := fun ctx stx => pure $ stx.formatStx (getSyntaxMaxDepth ctx.opts),
+    ppExpr := fun ctx e      => return format (toString e),
+    ppTerm := fun ctx stx    => return stx.formatStx (getSyntaxMaxDepth ctx.opts)
+    ppGoal := fun ctx mvarId => return "goal"
   }
 
 builtin_initialize ppExt : EnvExtension PPFns ←
-  registerEnvExtension $ ppFnsRef.get
+  registerEnvExtension ppFnsRef.get
 
 def ppExpr (ctx : PPContext) (e : Expr) : IO Format :=
   let e := ctx.mctx.instantiateMVars e |>.1
   if getPPRaw ctx.opts then
-    pure $ format (toString e)
+    return format (toString e)
   else
-    (ppExt.getState ctx.env).ppExpr ctx e
+    ppExt.getState ctx.env |>.ppExpr ctx e
 
 def ppTerm (ctx : PPContext) (stx : Syntax) : IO Format :=
   if getPPRaw ctx.opts then
-    pure $ stx.formatStx (getSyntaxMaxDepth ctx.opts)
+    return stx.formatStx (getSyntaxMaxDepth ctx.opts)
   else
-    (ppExt.getState ctx.env).ppTerm ctx stx
+    ppExt.getState ctx.env |>.ppTerm ctx stx
+
+def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format :=
+    ppExt.getState ctx.env |>.ppGoal ctx mvarId
 
 end Lean