feat: strengthen pp* signatures

src/Lean/Elab/InfoTree.lean

@@ -225,7 +225,7 @@ def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPConte
     opts := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls }
 
 def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do
-  ppTerm (info.toPPContext lctx) stx
+  ppTerm (info.toPPContext lctx) ⟨stx⟩  -- HACK: might not be a term
 
 private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format :=
   let pos    := stx.getPos?.getD 0

src/Lean/Message.lean

@@ -119,7 +119,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | _,    _,         ofFormat fmt             => return fmt
   | _,    _,         ofLevel u                => return format u
   | _,    _,         ofName n                 => return format n
-  | nCtx, some ctx,  ofSyntax s               => ppTerm (mkPPContext nCtx ctx) s  -- HACK: might not be a term
+  | nCtx, some ctx,  ofSyntax s               => ppTerm (mkPPContext nCtx ctx) ⟨s⟩  -- HACK: might not be a term
   | _,    none,      ofSyntax s               => return s.formatStx
   | _,    none,      ofExpr e                 => return format (toString e)
   | nCtx, some ctx,  ofExpr e                 => ppExpr (mkPPContext nCtx ctx) e

src/Lean/Parser/Module.lean

@@ -129,14 +129,14 @@ partial def testParseModuleAux (env : Environment) (inputCtx : InputContext) (s
         parse state msgs (stxs.push stx)
   parse s msgs stxs
 
-def testParseModule (env : Environment) (fname contents : String) : IO Syntax := do
+def testParseModule (env : Environment) (fname contents : String) : IO (TSyntax ``Parser.Module.module) := do
   let inputCtx := mkInputContext contents fname
   let (header, state, messages) ← parseHeader inputCtx
   let cmds ← testParseModuleAux env inputCtx state messages #[]
   let stx := mkNode `Lean.Parser.Module.module #[header, mkListNode cmds]
-  pure stx.raw.updateLeading
+  pure ⟨stx.raw.updateLeading⟩
 
-def testParseFile (env : Environment) (fname : System.FilePath) : IO Syntax := do
+def testParseFile (env : Environment) (fname : System.FilePath) : IO (TSyntax ``Parser.Module.module) := do
   let contents ← IO.FS.readFile fname
   testParseModule env fname.toString contents
 

src/Lean/PrettyPrinter.lean

@@ -20,7 +20,7 @@ def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
 
 namespace PrettyPrinter
 
-def ppTerm (stx : Syntax) : CoreM Format := do
+def ppTerm (stx : Term) : CoreM Format := do
   let opts ← getOptions
   let stx := (sanitizeSyntax stx).run' { options := opts }
   parenthesizeTerm stx >>= formatTerm
@@ -50,13 +50,13 @@ def ppConst (e : Expr) : MetaM Format := do
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
   Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
 
-def ppTactic (stx : Syntax) : CoreM Format :=
+def ppTactic (stx : TSyntax `tactic) : CoreM Format :=
   parenthesizeTactic stx >>= formatTactic
 
-def ppCommand (stx : Syntax) : CoreM Format :=
+def ppCommand (stx : Syntax.Command) : CoreM Format :=
   parenthesizeCommand stx >>= formatCommand
 
-def ppModule (stx : Syntax) : CoreM Format := do
+def ppModule (stx : TSyntax ``Parser.Module.module) : CoreM Format := do
   parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
 
 private partial def noContext : MessageData → MessageData

src/Lean/Util/PPExt.lean

@@ -40,14 +40,14 @@ structure PPContext where
 
 structure PPFns where
   ppExpr : PPContext → Expr → IO Format
-  ppTerm : PPContext → Syntax → IO Format
+  ppTerm : PPContext → Term → IO Format
   ppGoal : PPContext → MVarId → IO Format
   deriving Inhabited
 
 builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
     ppExpr := fun _ e => return format (toString e)
-    ppTerm := fun ctx stx => return stx.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
+    ppTerm := fun ctx stx => return stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
     ppGoal := fun _ _ => return "goal"
   }
 
@@ -67,8 +67,8 @@ def ppExpr (ctx : PPContext) (e : Expr) : IO Format := do
       else
         pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)"
 
-def ppTerm (ctx : PPContext) (stx : Syntax) : IO Format :=
-  let fmtRaw := fun () => stx.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
+def ppTerm (ctx : PPContext) (stx : Term) : IO Format :=
+  let fmtRaw := fun () => stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
   if pp.raw.get ctx.opts then
     return fmtRaw ()
   else

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -83,7 +83,7 @@ where
   | _,    _,         ofFormat fmt             => withIgnoreTags (pure fmt)
   | _,    _,         ofLevel u                => return format u
   | _,    _,         ofName n                 => return format n
-  | nCtx, some ctx,  ofSyntax s               => withIgnoreTags (ppTerm (mkPPContext nCtx ctx) s) -- HACK: might not be a term
+  | nCtx, some ctx,  ofSyntax s               => withIgnoreTags (ppTerm (mkPPContext nCtx ctx) ⟨s⟩) -- HACK: might not be a term
   | _,    none,      ofSyntax s               => withIgnoreTags (pure s.formatStx)
   | _,    none,      ofExpr e                 => return format (toString e)
   | nCtx, some ctx,  ofExpr e                 => do

tests/lean/Reformat.lean

@@ -17,8 +17,8 @@ let (f, _) ← (tryFinally (PrettyPrinter.ppModule stx) printTraces).toIO { opti
 IO.print f
 let stx' ← Lean.Parser.testParseModule env args.head! (toString f)
 if stx' != stx then
-  let stx := stx.getArg 1
-  let stx' := stx'.getArg 1
+  let stx := stx.raw.getArg 1
+  let stx' := stx'.raw.getArg 1
   stx.getArgs.size.forM fun i => do
     if stx.getArg i != stx'.getArg i then
       throw $ IO.userError s!"reparsing failed:\n{stx.getArg i}\n{stx'.getArg i}"

tests/lean/ppSyntax.lean

@@ -2,7 +2,7 @@ import Lean
 
 open Lean
 
-def test (stx : Unhygienic Syntax) : MetaM Unit := do
+def test (stx : Unhygienic Term) : MetaM Unit := do
   IO.println (← PrettyPrinter.ppTerm stx.run)
 
 -- test imported `ParserDescr`

tests/lean/run/PPTopDownAnalyze.lean

@@ -9,7 +9,7 @@ import Std
 open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.Elab.Command
 open Lean.PrettyPrinter
 
-def checkDelab (e : Expr) (tgt? : Option Syntax) (name? : Option Name := none) : TermElabM Unit := do
+def checkDelab (e : Expr) (tgt? : Option Term) (name? : Option Name := none) : TermElabM Unit := do
   let pfix := "[checkDelab" ++ (match name? with | some n => ("." ++ toString n) | none => "") ++ "]"
   if e.hasMVar then throwError "{pfix} original term has mvars, {e}"
   let stx ← delab e

tests/lean/run/Reparen.lean

@@ -26,10 +26,10 @@ let (debug, f) : Bool × String := match args with
   | _         => panic! "usage: file [-d]";
 let env ← mkEmptyEnvironment;
 let stx ← Lean.Parser.testParseFile env args.head!;
-let header := stx.getArg 0;
+let header := stx.raw.getArg 0;
 let some s ← pure header.reprint | throw $ IO.userError "header reprint failed";
 IO.print s;
-let cmds := (stx.getArg 1).getArgs;
+let cmds := (stx.raw.getArg 1).getArgs;
 cmds.forM $ fun cmd => do
   let cmd := unparen cmd;
   let (cmd, _) ← (tryFinally (PrettyPrinter.parenthesizeCommand cmd) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.parenthesize debug, fileName := "", fileMap := default } { env := env };