feat: typed syntax as the target of doc elaboration

[robsimmons]

This PR allows block elaboration to target a typed concrete representation of blocks instead of producing Term objects. It is directly modeled off of #453, which retargeted block elaboration from Term to Expr. Unlike in that PR, here the goal is not to reduce build times, it is to make document elaboration less metaprogramming-ful, and to move towards being able to serialize much of the structure of an elaborated document as JSON or something similar.

The first critical change is in Verso.Doc.Elab.Basic: the FinishedPart type, which is already a concrete representation of the result of elaborating a document, is renamed to Elab.Part, and corresponding Elab.Block and Elab.Inline types are added to represent the concrete representations of the result of elaborating a block and of elaborating inline syntax. (Elab.Inline is just an alias for Term, since we're not retargeting term elaboration in this PR.)

The second critical change is in Verso.Doc.Elab.Monad, where a new block_elab decorator is added to parallel the block_expander decorator, and in Verso.Doc.Elab.Block, where the new family of decorators are queried. This is a relatively isolated change: the interesting changes happen when elaborators are introduced that parallel the code_block_expander and directive_expander decorators.

[leanprover-radar]

Benchmark results for 052dcb4 against 41cc5c3 are in! @robsimmons

No significant changes detected.

[david-christiansen]

Why are these Term, rather than a parallel structure to Target.Block? Has it just not yet been done, or is there an underlying reason?

[robsimmons]

Just hasn't been done — was demonstrating a block-only incremental adoption.

[david-christiansen]

This looks like it could be implemented without the repetition as:

inductive InlineExt where
  | other (container : Term)
  | stx (stx : Term)
inductive BlockExt where
  | other (container : Term)
  | stx (stx : Term)
abbrev Inline := Lean.Doc.Inline InlineExt
abbrev Block := Lean.Doc.Block InlineExt BlockExt

That would give the same expressive power, from what I can see, while allowing a lot more shared code.

[david-christiansen]

Or, alternately,

inductive InlineExt where
  | other (container : Term)
  | stx (stx : Term)

inductive BlockExt where
  | other (container : Term)
  | stx (stx : Term)

def Target : Genre where
  Inline := InlineExt
  Block := BlockExt
  PartMetadata := Empty
  TraverseContext := Empty
  TraverseState := Empty

but I think that's a bit less straightforward.

[david-christiansen]

This whole mutual block strikes me as code that should be Quote instances. That wouldn't let the code use quotations, but this kind of thing isn't so hard to build directly. Is it because there were issues propagating the genre via unification?

[david-christiansen]

Oh wait, these are converting from Target.Block. The fact that I stumbled here is evidence that at least a comment would be useful!

[david-christiansen]

Having this in two stages says that all expanders take precedence over all elaborators. I think the current code follows the usual Lean practice, where more-recently-defined expanders take precedence. I say "I think" because this feature is used in only a few places so it's not fresh in my mind.

I think this is OK, but it should be a deliberate and documented decision rather than an artifact of the implementation. To make them use the same precedence rules, the expander/elab extension could be one extension that contains a sum type instead of two separate ones.

[david-christiansen]

I think this is a nice direction to go in with a lot of potential to make it much easier to implement Verso extensions.

Given that the Verso AST is "closed" (the concrete syntax is fixed), I think this same approach could be put earlier in the pipeline. Instead of passing TSyntax block to the elaborators, what if they got Source.Block as parameters? This would be an inductive type of Verso concrete syntax, with all the source positions and such.