feat: pretty print Syntax in messages

src/Lean/Message.lean

@@ -52,12 +52,6 @@ namespace MessageData
 
 instance : Inhabited MessageData := ⟨MessageData.ofFormat (arbitrary _)⟩
 
-@[init] def stxMaxDepthOption : IO Unit :=
-registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "maximum depth when displaying syntax objects in messages" }
-
-def getSyntaxMaxDepth (opts : Options) : Nat :=
-opts.getNat `syntaxMaxDepth 2
-
 private def sanitizeNames (ctx : MessageDataContext) : MessageDataContext :=
 { ctx with lctx := ctx.lctx.sanitizeNames ctx.opts }
 
@@ -69,7 +63,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
 | _,    _,         ofFormat fmt             => pure fmt
 | _,    _,         ofLevel u                => pure $ fmt u
 | _,    _,         ofName n                 => pure $ fmt n
-| _,    some ctx,  ofSyntax s               => pure $ s.formatStx (getSyntaxMaxDepth ctx.opts)
+| nCtx, some ctx,  ofSyntax s               => ppTerm (mkPPContext nCtx ctx) s  -- HACK: might not be a term
 | _,    none,      ofSyntax s               => pure $ s.formatStx
 | _,    none,      ofExpr e                 => pure $ format (toString e)
 | nCtx, some ctx,  ofExpr e                 => ppExpr (mkPPContext nCtx ctx) e

src/Lean/PrettyPrinter.lean

@@ -9,6 +9,13 @@ import Lean.PrettyPrinter.Formatter
 import Lean.Parser.Module
 
 namespace Lean
+
+def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
+Prod.fst <$> x.toIO { options := ppCtx.opts } { env := ppCtx.env }
+
+def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
+ppCtx.runCoreM $ x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
+
 namespace PrettyPrinter
 
 def ppTerm (stx : Syntax) : CoreM Format :=
@@ -28,17 +35,18 @@ private partial def noContext : MessageData → MessageData
 | MessageData.withContext ctx msg => noContext msg
 | msg => msg
 
-def ppExprFn (ppCtx : PPContext) (e : Expr) : IO Format := do
-let pp : MetaM Format := adaptExcept (fun ex => match ex with
-  -- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error
+-- strip context (including environments with registered pretty printers) to prevent infinite recursion when pretty printing pretty printer error
+private def withoutContext {m} [MonadExceptAdapter Exception Exception m m] (x : m Format) : m Format :=
+adaptExcept (fun ex => match ex with
   | Exception.error ref msg => Exception.error ref (noContext msg)
   | e                       => e)
-  (ppExpr ppCtx.currNamespace ppCtx.openDecls e);
-(fmt, _, _) ← pp.toIO { options := ppCtx.opts } { env := ppCtx.env } { lctx := ppCtx.lctx } { mctx := ppCtx.mctx };
-pure fmt
+  x
 
-@[init] def registerPPTerm : IO Unit := do
-ppExprFnRef.set ppExprFn
+@[init] def registerPPExt : IO Unit := do
+ppFnsRef.set {
+  ppExpr := fun ctx e   => ctx.runMetaM $ withoutContext $ ppExpr ctx.currNamespace ctx.openDecls e,
+  ppTerm := fun ctx stx => ctx.runCoreM $ withoutContext $ ppTerm stx,
+}
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `PrettyPrinter;

src/Lean/Util/PPExt.lean

@@ -9,6 +9,16 @@ import Lean.Data.OpenDecl
 
 namespace Lean
 
+@[init] private def registerOptions : IO Unit := do
+registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "maximum depth when displaying syntax objects in messages" };
+registerOption `pp.raw { defValue := false, group := "pp", descr := "(pretty printer) print raw expression/syntax tree" }
+
+def getSyntaxMaxDepth (opts : Options) : Nat :=
+opts.getNat `syntaxMaxDepth 2
+
+def getPPRaw (opts : Options) : Bool :=
+opts.getBool `pp.raw false
+
 structure PPContext :=
 (env           : Environment)
 (mctx          : MetavarContext := {})
@@ -17,30 +27,34 @@ structure PPContext :=
 (currNamespace : Name := Name.anonymous)
 (openDecls     : List OpenDecl := [])
 
-abbrev PPExprFn := PPContext → Expr → IO Format
+structure PPFns :=
+(ppExpr : PPContext → Expr → IO Format)
+(ppTerm : PPContext → Syntax → IO Format)
 
-/- TODO: delete after we implement the new pretty printer in Lean -/
-@[extern "lean_pp_expr"]
-constant ppOld : Environment → MetavarContext → LocalContext → Options → Expr → Format := arbitrary _
+instance PPFns.inhabited : Inhabited PPFns := ⟨⟨arbitrary _, arbitrary _⟩⟩
 
-def mkPPExprFnRef : IO (IO.Ref PPExprFn) := IO.mkRef (fun ctx e => pure $ ppOld ctx.env ctx.mctx ctx.lctx ctx.opts e)
-@[init mkPPExprFnRef] def ppExprFnRef : IO.Ref PPExprFn := arbitrary _
+def mkPPFnsRef : IO (IO.Ref PPFns) := IO.mkRef {
+  ppExpr := fun ctx e   => pure $ format (toString e),
+  ppTerm := fun ctx stx => pure $ stx.formatStx (getSyntaxMaxDepth ctx.opts),
+}
+@[init mkPPFnsRef] def ppFnsRef : IO.Ref PPFns := arbitrary _
 
-def mkPPExprFnExtension : IO (EnvExtension PPExprFn) :=
-registerEnvExtension $ ppExprFnRef.get
-
-@[init mkPPExprFnExtension]
-constant ppExprExt : EnvExtension PPExprFn := arbitrary _
+def mkPPExt : IO (EnvExtension PPFns) :=
+registerEnvExtension $ ppFnsRef.get
 
+@[init mkPPExt]
+constant ppExt : EnvExtension PPFns := arbitrary _
 def ppExpr (ctx : PPContext) (e : Expr) : IO Format :=
 let e := (ctx.mctx.instantiateMVars e).1;
-if ctx.opts.getBool `ppOld true then
-  (ppExprExt.getState ctx.env) ctx e
-else
+if getPPRaw ctx.opts then
   pure $ format (toString e)
+else
+  (ppExt.getState ctx.env).ppExpr ctx e
 
--- TODO: remove after we remove ppOld
-@[init] def ppOldOption : IO Unit :=
-registerOption `ppOld { defValue := true, group := "", descr := "disable/enable old pretty printer" }
+def ppTerm (ctx : PPContext) (stx : Syntax) : IO Format :=
+if getPPRaw ctx.opts then
+  pure $ stx.formatStx (getSyntaxMaxDepth ctx.opts)
+else
+  (ppExt.getState ctx.env).ppTerm ctx stx
 
 end Lean

tests/lean/run/meta2.lean

@@ -421,10 +421,7 @@ checkM $ do { let b ← isExprMVarAssigned $ m1.mvarId!; pure (!b) };
 checkM $ isExprMVarAssigned $ m3.mvarId!;
 pure ()
 
-section
-set_option ppOld false
 #eval tst26
-end
 
 section
 set_option trace.Meta.isDefEq.step true

tests/lean/run/typeclass_diamond.lean

@@ -28,8 +28,6 @@ class Top (n : Nat) : Type := (u : Unit := ())
 instance Top₁ToTop (n : Nat) [Top₁ n] : Top n := {}
 instance Top₂ToTop (n : Nat) [Top₂ n] : Top n := {}
 
-set_option ppOld false
-
 #synth Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ
 
 def tst : Top Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ :=

tests/lean/run/typeclass_easy.lean

@@ -1,5 +1,4 @@
 new_frontend
-set_option ppOld false
 
 #synth HasToString (Nat × (Nat × Bool))