Pretty printing projection notation #

This module contains the @[pp_dot] attribute, which is used to configure functions to pretty print using projection notation (i.e., like x.f y rather than C.f x y).

Core's projection delaborator collapses chains of ancestor projections. For example, to turn x.toFoo.toBar into x.toBar. The pp_dot attribute works together with this delaborator to completely collapse such chains.

source

def Mathlib.ProjectionNotation.mkExtendedFieldNotationUnexpander (f : Lean.Name) :

Lean.Elab.Command.CommandElabM Unit

Given a function f that is either a true projection or a generalized projection (i.e., a function that works using extended field notation, a.k.a. "dot notation"), generates an app_unexpander for it to get it to pretty print using dot notation.

See also the docstring of the pp_dot attribute.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Mathlib.ProjectionNotation.ppDotAttr :

Lean.ParserDescr

Adding the @[pp_dot] attribute defines an app_unexpander for the given function to support pretty printing the function using extended field notation ("dot notation"). This particular attribute is only for functions whose first explicit argument is the receiver of the generalized field notation. That is to say, it is only meant for transforming C.f c x y z ... to c.f x y z ... for c : C.

It can be used to help get projection notation to work for function-valued structure fields, since the built-in projection delaborator cannot handle excess arguments.

Example for generalized field notation:

structure A where
  n : Nat

@[pp_dot]
def A.foo (a : A) (m : Nat) : Nat := a.n + m

Now, A.foo x m pretty prints as x.foo m. If A is a structure, it also adds a rule that A.foo x.toA m pretty prints as x.foo m. This rule is meant to combine with core's the projection collapse delaborator, where together A.foo x.toB.toA m will pretty print as x.foo m.

Since the mentioned rule is a purely syntactic transformation, it might lead to output that does not round trip, though this can only occur if there exists an A-valued toA function that is not a parent projection that happens to be pretty printable using dot notation.

Here is an example to illustrate the round tripping issue:

import Mathlib.Tactic.ProjectionNotation

structure A where n : Int

@[pp_dot]
def A.inc (a : A) (k : Int) : Int := a.n + k

structure B where n : Nat

def B.toA (b : B) : A := ⟨b.n⟩

variable (b : B)

#check A.inc b.toA 1
-- (B.toA b).inc 1 : Int

attribute [pp_dot] B.toA
#check A.inc b.toA 1
-- b.inc 1 : Int

#check b.inc 1
-- invalid field 'inc', the environment does not contain 'B.inc'

To avoid this, don't use pp_dot for coercion functions such as B.toA.

Equations

Mathlib.ProjectionNotation.ppDotAttr = Lean.ParserDescr.node `Mathlib.ProjectionNotation.ppDotAttr 1024 (Lean.ParserDescr.nonReservedSymbol "pp_dot" false)

Instances For