From cd7f55b6c92b6d20fb2a0428abc097fa8be421b3 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 23 Feb 2026 20:30:26 -0800 Subject: [PATCH] feat: `pp.mdata` (#12606) This PR adds the pretty printer option `pp.mdata`, which causes the pretty printer to annotate terms with any metadata that is present. For example, ```lean set_option pp.mdata true /-- info: [mdata noindex:true] 2 : Nat -/ #guard_msgs in #check no_index 2 ``` The `[mdata ...] e` syntax is only for pretty printing. Thanks to @Rob23oba for an initial version. Closes #10929 --- src/Lean/Parser/Term.lean | 8 +++ .../PrettyPrinter/Delaborator/Builtins.lean | 54 ++++++++++++---- .../PrettyPrinter/Delaborator/Options.lean | 5 ++ tests/lean/run/ppMData.lean | 64 +++++++++++++++++++ 4 files changed, 119 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/ppMData.lean diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 9bfda1d349..68e908c836 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -1028,6 +1028,14 @@ string or a `MessageData` term. @[builtin_term_parser] def logNamedWarningAtMacro := leading_parser "logNamedWarningAt " >> termParser maxPrec >> ppSpace >> identWithPartialTrailingDot >> ppSpace >> (interpolatedStr termParser <|> termParser maxPrec) +/-- +Representation of an expression with metadata used during pretty printing for the `pp.mdata` option. +-/ +@[run_builtin_parser_attribute_hooks] +def mdataDiagnostic := leading_parser + group ("[" >> "mdata" >> many (group <| ppSpace >> ident >> optional (":" >> termParser)) >> "]") >> + ppSpace >> termParser + end Term @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 3bb8b5bc81..4099b37220 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -296,7 +296,10 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in let insertExplicit := needsExplicit ((← getExpr).getBoundedAppFn numArgs) numArgs paramKinds let fieldNotation ← pure (fieldNotation && !insertExplicit) <&&> getPPOption getPPFieldNotation <&&> not <$> getPPOption getPPAnalysisNoDot - <&&> withBoundedAppFn numArgs do pure (← getExpr).consumeMData.isConst <&&> not <$> withMDatasOptions (getPPOption getPPAnalysisBlockImplicit <|> getPPOption getPPUniverses) + <&&> withBoundedAppFn numArgs do + pure (← getExpr).consumeMData.isConst + <&&> not <$> (pure (← getExpr).isMData <&&> getPPOption getPPMData) + <&&> not <$> withMDatasOptions (getPPOption getPPAnalysisBlockImplicit <|> getPPOption getPPUniverses) let field? ← if fieldNotation then appFieldNotationCandidate? else pure none let (fnStx, _, argStxs) ← withBoundedAppFnArgs numArgs (do return (← delabHead insertExplicit, paramKinds.toList, Array.mkEmpty numArgs)) @@ -357,7 +360,10 @@ Assumes `numArgs ≤ paramKinds.size`. -/ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) : Delab := do let unexpand ← pure unexpand - <&&> withBoundedAppFn numArgs do pure (← getExpr).consumeMData.isConst <&&> not <$> withMDatasOptions (getPPOption getPPUniverses) + <&&> withBoundedAppFn numArgs do + pure (← getExpr).consumeMData.isConst + <&&> not <$> (pure (← getExpr).isMData <&&> getPPOption getPPMData) + <&&> not <$> withMDatasOptions (getPPOption getPPUniverses) let field? ← if ← pure unexpand <&&> getPPOption getPPFieldNotation <&&> not <$> getPPOption getPPAnalysisNoDot then appFieldNotationCandidate? @@ -522,7 +528,12 @@ Default delaborator for applications. @[builtin_delab app] def delabApp : Delab := do let delabAppFn (insertExplicit : Bool) : Delab := do - let stx ← if (← getExpr).consumeMData.isConst then withMDatasOptions delabConst else delab + let e ← getExpr + let stx ← + if ← pure e.consumeMData.isConst <&&> not <$> (pure e.isMData <&&> getPPOption getPPMData) then + withMDatasOptions delabConst + else + delab if insertExplicit && !stx.raw.isOfKind ``Lean.Parser.Term.explicit then `(@$stx) else pure stx delabAppCore (← getExpr).getAppNumArgs delabAppFn (unexpand := true) @@ -843,18 +854,37 @@ where else x +private def reflectDataValue (t : DataValue) : Term := Unhygienic.run do + match t with + | .ofBool b => return mkIdent (if b then `true else `false) + | .ofNat n => return quote n + | .ofInt n => if n ≥ 0 then return quote n.toNat else `(-$(quote n.natAbs)) + | .ofString s => return quote s + | .ofName n => return mkIdent n + | .ofSyntax _ => `(_) + @[builtin_delab mdata] def delabMData : Delab := do - if let some _ := inaccessible? (← getExpr) then - let s ← withMDataExpr delab - if (← read).inPattern then - `(.($s)) -- We only include the inaccessible annotation when we are delaborating patterns - else - return s - else if let some _ := isLHSGoal? (← getExpr) then - withMDataExpr <| withAppFn <| withAppArg <| delab + if ← getPPOption getPPMData then + let .mdata d _ ← getExpr | unreachable! + let (keys, vals?) ← d.entries.foldlM (init := (#[], #[])) + fun ((keys : Array Ident), (vals : Array (Option Term))) (k, v) => do + return (keys.push (mkIdent k), vals.push (some <| reflectDataValue v)) + let e ← withMDataOptions delab + -- Annotate to prevent overwriting the terminfo for `e`, which is + -- already inserted at the current position. + annotateCurPos =<< `(mdataDiagnostic| [mdata $[$keys $[:$vals?]?]*] $e) else - withMDataOptions delab + if let some _ := inaccessible? (← getExpr) then + let s ← withMDataExpr delab + if (← read).inPattern then + `(.($s)) -- We only include the inaccessible annotation when we are delaborating patterns + else + return s + else if let some _ := isLHSGoal? (← getExpr) then + withMDataExpr <| withAppFn <| withAppArg <| delab + else + withMDataOptions delab /-- Return `true` iff current binder should be merged with the nested diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 1668c09883..0c54b1ed04 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -98,6 +98,10 @@ register_builtin_option pp.numericTypes : Bool := { defValue := false descr := "(pretty printer) display types of numeric literals" } +register_builtin_option pp.mdata : Bool := { + defValue := false + descr := "(pretty printer) displays a representation of mdata annotations" +} register_builtin_option pp.instantiateMVars : Bool := { defValue := true descr := "(pretty printer) instantiate mvars before delaborating" @@ -260,6 +264,7 @@ def getPPTagAppFns (o : Options) : Bool := o.get pp.tagAppFns.name (getPPAll o) def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o) def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o) def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o) +def getPPMData (o : Options) : Bool := o.get pp.mdata.name pp.mdata.defValue def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue def getPPMVars (o : Options) : Bool := o.get pp.mvars.name pp.mvars.defValue def getPPMVarsAnonymous (o : Options) : Bool := o.get pp.mvars.anonymous.name (pp.mvars.anonymous.defValue && getPPMVars o) diff --git a/tests/lean/run/ppMData.lean b/tests/lean/run/ppMData.lean new file mode 100644 index 0000000000..c26e5b1e5c --- /dev/null +++ b/tests/lean/run/ppMData.lean @@ -0,0 +1,64 @@ +import Lean.Meta.Basic +/-! +# Tests of `pp.mdata` +-/ + +open Lean + +set_option pp.mdata true + +/-! +Having mdata on the head constant, partially applied, and fully applied. +-/ +/-- +info: ([mdata n:1 z:-1 b:true s:"str" x:_ m:foo.bar] @id) 3 +--- +info: ([mdata n:1 z:-1 b:true s:"str" x:_ m:foo.bar] id) 3 +--- +info: [mdata n:1 z:-1 b:true s:"str" x:_ m:foo.bar] id 3 +-/ +#guard_msgs in +run_meta + let d : KVMap := KVMap.empty + |>.insert `n (1 : Nat) + |>.insert `z (-1 : Int) + |>.insert `b true + |>.insert `s "str" + |>.insert `x (Unhygienic.run `(1+1)) + |>.insert `m `foo.bar + Lean.logInfo <| mkApp2 (.mdata d <| .const ``id [1]) (mkConst ``Nat) (.lit (.natVal 3)) + Lean.logInfo <| Expr.app (.mdata d <| Expr.app (.const ``id [1]) (mkConst ``Nat)) (.lit (.natVal 3)) + Lean.logInfo <| Expr.mdata d <| mkApp2 (.const ``id [1]) (mkConst ``Nat) (.lit (.natVal 3)) + +/-! +`noindex` +-/ +/-- info: [mdata noindex:true] 2 : Nat -/ +#guard_msgs in #check no_index 2 + +/-! +Metadata blocks unexpanders +-/ +/-- info: ([mdata noindex:true] HAdd.hAdd) 2 3 : Nat -/ +#guard_msgs in #check (no_index HAdd.hAdd) 2 3 +/-- info: 2 + 3 : Nat -/ +#guard_msgs in #check HAdd.hAdd 2 3 + +/-! +Metadata blocks dot notation, both in implicit and explicit mode +-/ +/-- info: ([mdata noindex:true] Nat.add) x y : Nat -/ +#guard_msgs in variable (x y : Nat) in #check (no_index Nat.add) x y +/-- info: x.add y : Nat -/ +#guard_msgs in variable (x y : Nat) in #check Nat.add x y +/-- info: [mdata noindex:true] x.add y : Nat -/ +#guard_msgs in variable (x y : Nat) in #check no_index (Nat.add x y) +section +set_option pp.explicit true +/-- info: ([mdata noindex:true] Nat.add) x y : Nat -/ +#guard_msgs in variable (x y : Nat) in #check (no_index Nat.add) x y +/-- info: x.add y : Nat -/ +#guard_msgs in variable (x y : Nat) in #check Nat.add x y +/-- info: [mdata noindex:true] x.add y : Nat -/ +#guard_msgs in variable (x y : Nat) in #check no_index (Nat.add x y) +end