Documentation

Lean.PrettyPrinter.Delaborator.Basic

The delaborator is the first stage of the pretty printer, and the inverse of the elaborator: it turns fully elaborated Expr core terms back into surface-level Syntax, omitting some implicit information again and using higher-level syntax abstractions like notations where possible. The exact behavior can be customized using pretty printer options; activating pp.all should guarantee that the delaborator is injective and that re-elaborating the resulting Syntax round-trips.

Pretty printer options can be given not only for the whole term, but also specific subterms. This is used both when automatically refining pp options until round-trip and when interactively selecting pp options for a subterm (both TBD). The association of options to subterms is done by assigning a unique, synthetic Nat position to each subterm derived from its position in the full term. This position is added to the corresponding Syntax object so that elaboration errors and interactions with the pretty printer output can be traced back to the subterm.

The delaborator is extensible via the [delab] attribute.

structure Lean.PrettyPrinter.Delaborator.Context:

Type

defaultOptions : Lean.Options
optionsPerPos : Lean.PrettyPrinter.Delaborator.OptionsPerPos
currNamespace : Lean.Name
openDecls : List Lean.OpenDecl
inPattern : Bool
subExpr : Lean.SubExpr

structure Lean.PrettyPrinter.Delaborator.State:

Type

We attach Elab.Info at various locations in the Syntax output in order to convey its semantics. While the elaborator emits InfoTrees, here we have no real text location tree to traverse, so we use a flattened map.
infos : Std.RBMap Lean.SubExpr.Pos Lean.Elab.Info compare
See SubExpr.nextExtraPos.
holeIter : Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator

opaque Lean.PrettyPrinter.Delaborator.delabFailureId:

Lean.InternalExceptionId

@[inline]

abbrev Lean.PrettyPrinter.Delaborator.DelabM (α : Type) :

Type

Equations

Lean.PrettyPrinter.Delaborator.DelabM = ReaderT Lean.PrettyPrinter.Delaborator.Context (StateRefT' IO.RealWorld Lean.PrettyPrinter.Delaborator.State Lean.MetaM)

@[inline]

abbrev Lean.PrettyPrinter.Delaborator.Delab:

Type

Equations

Lean.PrettyPrinter.Delaborator.Delab = Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

instance Lean.PrettyPrinter.Delaborator.instInhabitedDelabM {α : Type} :

Inhabited (Lean.PrettyPrinter.Delaborator.DelabM α)

Equations

Lean.PrettyPrinter.Delaborator.instInhabitedDelabM = { default := throw default }

@[inline]

def Lean.PrettyPrinter.Delaborator.orElse {α : Type} (d₁ : Lean.PrettyPrinter.Delaborator.DelabM α) (d₂ : Unit → Lean.PrettyPrinter.Delaborator.DelabM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

Lean.PrettyPrinter.Delaborator.orElse d₁ d₂ = Lean.catchInternalId Lean.PrettyPrinter.Delaborator.delabFailureId d₁ fun x => d₂ ()

def Lean.PrettyPrinter.Delaborator.failure {α : Type} :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

Lean.PrettyPrinter.Delaborator.failure = throw (Lean.Exception.internal Lean.PrettyPrinter.Delaborator.delabFailureId)

instance Lean.PrettyPrinter.Delaborator.instAlternativeDelabM:

Alternative Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instAlternativeDelabM = Alternative.mk (fun {α} => Lean.PrettyPrinter.Delaborator.failure) fun {α} => Lean.PrettyPrinter.Delaborator.orElse

instance Lean.PrettyPrinter.Delaborator.instOrElseDelabM {α : Type} :

OrElse (Lean.PrettyPrinter.Delaborator.DelabM α)

Equations

Lean.PrettyPrinter.Delaborator.instOrElseDelabM = { orElse := Lean.PrettyPrinter.Delaborator.orElse }

instance Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM:

MonadReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM = { read := Lean.PrettyPrinter.Delaborator.Context.subExpr <$> read }

instance Lean.PrettyPrinter.Delaborator.instMonadWithReaderOfSubExprDelabM:

MonadWithReaderOf Lean.SubExpr Lean.PrettyPrinter.Delaborator.DelabM

Equations

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

instance Lean.PrettyPrinter.Delaborator.instMonadStateOfHoleIteratorDelabM:

MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator Lean.PrettyPrinter.Delaborator.DelabM

Equations

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

instance Lean.PrettyPrinter.Delaborator.instMonadQuotationDelabM:

Lean.MonadQuotation Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instMonadQuotationDelabM = Lean.MonadQuotation.mk (pure default) (pure default) fun {α} x => x

unsafe def Lean.PrettyPrinter.Delaborator.mkDelabAttribute:

IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Delaborator.Delab)

Equations

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

opaque Lean.PrettyPrinter.Delaborator.delabAttribute:

Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Delaborator.Delab

def Lean.PrettyPrinter.Delaborator.getExprKind:

Lean.PrettyPrinter.Delaborator.DelabM Lean.Name

Equations

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

def Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos:

Lean.PrettyPrinter.Delaborator.DelabM Lean.Options

Equations

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

def Lean.PrettyPrinter.Delaborator.getPPOption (opt : Lean.Options → Bool) :

Lean.PrettyPrinter.Delaborator.DelabM Bool

Evaluate option accessor, using subterm-specific options if set.

Equations

Lean.PrettyPrinter.Delaborator.getPPOption opt = do let a ← Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos pure (opt a)

def Lean.PrettyPrinter.Delaborator.whenPPOption (opt : Lean.Options → Bool) (d : Lean.PrettyPrinter.Delaborator.Delab) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.whenPPOption opt d = do let b ← Lean.PrettyPrinter.Delaborator.getPPOption opt if b = true then d else failure

def Lean.PrettyPrinter.Delaborator.whenNotPPOption (opt : Lean.Options → Bool) (d : Lean.PrettyPrinter.Delaborator.Delab) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.whenNotPPOption opt d = do let b ← Lean.PrettyPrinter.Delaborator.getPPOption opt if b = true then failure else d

def Lean.PrettyPrinter.Delaborator.withOptionAtCurrPos {α : Type} (k : Lean.Name) (v : Lean.DataValue) (x : Lean.PrettyPrinter.Delaborator.DelabM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Set the given option at the current position and execute x in this context.

Equations

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

def Lean.PrettyPrinter.Delaborator.annotatePos (pos : Lean.SubExpr.Pos) (stx : Lean.Term) :

Equations

Lean.PrettyPrinter.Delaborator.annotatePos pos stx = { raw := Lean.Syntax.setInfo (Lean.SourceInfo.synthetic { byteIdx := pos } { byteIdx := pos }) stx.raw }

def Lean.PrettyPrinter.Delaborator.annotateCurPos (stx : Lean.Term) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.annotateCurPos stx = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos pure (Lean.PrettyPrinter.Delaborator.annotatePos a stx)

def Lean.PrettyPrinter.Delaborator.getUnusedName (suggestion : Lean.Name) (body : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Name

Equations

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

def Lean.PrettyPrinter.Delaborator.getUnusedName.bodyUsesSuggestion (body : Lean.Expr) (lctx : Lean.LocalContext) (suggestion' : Lean.Name) :

Equations

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

def Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName {α : Type} (d : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

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

@[inline]

def Lean.PrettyPrinter.Delaborator.liftMetaM {α : Type} (x : Lean.MetaM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

Lean.PrettyPrinter.Delaborator.liftMetaM x = liftM x

def Lean.PrettyPrinter.Delaborator.addTermInfo (pos : Lean.SubExpr.Pos) (stx : Lean.Syntax) (e : Lean.Expr) (isBinder : optParam Bool false) :

Lean.PrettyPrinter.Delaborator.DelabM Unit

Equations

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

def Lean.PrettyPrinter.Delaborator.addTermInfo.mkTermInfo (stx : Lean.Syntax) (e : Lean.Expr) (isBinder : optParam Bool false) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Elab.Info

Equations

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

def Lean.PrettyPrinter.Delaborator.addFieldInfo (pos : Lean.SubExpr.Pos) (projName : Lean.Name) (fieldName : Lean.Name) (stx : Lean.Syntax) (val : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.DelabM Unit

Equations

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

def Lean.PrettyPrinter.Delaborator.addFieldInfo.mkFieldInfo (projName : Lean.Name) (fieldName : Lean.Name) (stx : Lean.Syntax) (val : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Elab.Info

Equations

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

partial def Lean.PrettyPrinter.Delaborator.delabFor:

Lean.Name → Lean.PrettyPrinter.Delaborator.Delab

partial def Lean.PrettyPrinter.Delaborator.delab:

Lean.PrettyPrinter.Delaborator.Delab

unsafe def Lean.PrettyPrinter.Delaborator.mkAppUnexpanderAttribute:

IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Unexpander)

Equations

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

opaque Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute:

Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Unexpander

def Lean.PrettyPrinter.delabCore (e : Lean.Expr) (optionsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅) (delab : optParam Lean.PrettyPrinter.Delaborator.Delab Lean.PrettyPrinter.Delaborator.delab) :

Lean.MetaM (Lean.Term × Std.RBMap Lean.SubExpr.Pos Lean.Elab.Info compare)

Equations

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

def Lean.PrettyPrinter.delab (e : Lean.Expr) (optionsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅) :

Lean.MetaM Lean.Term

"Delaborate" the given term into surface-level syntax using the default and given subterm-specific options.

Equations

Lean.PrettyPrinter.delab e optionsPerPos = do let discr ← Lean.PrettyPrinter.delabCore e optionsPerPos Lean.PrettyPrinter.Delaborator.delab match discr with | (stx, snd) => pure stx