Specifying which expressions `Expr` presenters apply to

[Vtec234]

In Lean, a delaborator (see the metaprogramming book) is a metaprogram which can take low-level kernel Expressions to Syntax, pretty-printing them as human-readable, structured syntax trees. In ProofWidgets, an Expr presenter (defined here) is a sort of generalized delaborator which outputs interactive HTML trees instead of ASTs. For example, an Expr of type RBTree can be presented as a 2D red-black tree diagram:

Similarly to delaborators, when registering a presenter we need some way to specify which Expressions it applies to (e.g. just the constructors of type RBTree). The current design (which I am about to remove) is that each ExprPresenter comes with an isApplicable : Expr → MetaM Bool field. This is super expressive but inefficient -- every time we want to present something, we have to run isApplicable on all the known presenters.

In contrast, delaborators are registered with reference to a constant name, and are executed on any expression whose head is that constant:

@[delab app.foo]
def delabfoo2 : Delab := do
  `(2)

#check foo -- 2 : Nat → Nat

A better mechanism for registering presenters would be analogous -- we use @[expr_presenter app.foo]. This is reasonably efficient as we can store them in a name-indexed environment extension and achieve amortized constant-time lookup (assuming a bounded amount of presenters for any given constant name). However, our design constraints are not exactly the same: the assumption with delaborators is that the first one that applies to a given Expr is the canonical choice. With widgets, we can give the user a choice of which presenter to use in the UI, for example to choose LaTeX in one case and a diagram in another. So there will have to be something to account for that.

If we wanted a higher degree of control than just the head constant name, a different possible design would have every presenter register itself with some global data structure. For example, registerSelf : DiscrTree ExprPresenter → DiscrTree ExprPresenter which stores the presenter at all patterns that it cares about (e.g. foo and foo *). My intuition is that this overcomplicates things and the simple delaborator-like design is better.

[Vtec234]

Experience now shows that going purely off the head constant name is not generally sufficient, for example because there are many, many ways to display an equality. Instead the plan is to attempt a slightly more general pattern syntax, for example something like @[expr_presenter (_ + _ = _ + _)]. It would be implemented with a DiscrTree in the environment extension. For cases when a pattern is not enough to disambiguate, we will use precedence levels, leading to the full syntax @[expr_presenter (_ + _ = _ + _):4].