Rewrite the Rewriter

[JasonGross]

I don't think the rewriter is suitable for wider adoption. It's very, very, very much a research prototype, and I don't see it becoming not a research prototype without going through a complete rewriting. Almost all of it is either a pile of hacks or proofs which are made very painful by inline CPS and dependent types. It's going to be hard to maintain, too, in it's current form. I think the ideas are good, but the implementation is just good enough to work for fiat-crypto. (Recall that the prior state-of-the-art was writing the pattern matches on PHOASTs by hand.) An incomplete list of things that I think need to be rewritten from scratch:

1. The code for creating the rewriter is currently a messy mixture of a bit of OCaml plugin code for adding inductives and setting the strategy of things (this should be replaced by something like coq-elpi or MetaCoq), and a large amount of exremely hacky Ltac code that should be replaced by something more maintainable
2. Generation of the various necessary properties of the syntax languages should be streamlined and made more efficient, so that we incur less overhead when creating the language in the first place.
3. The code for reducing the rewriter early is currently a mess, because it was developed organically. It should be rewritten with an eye on what can be unfolded early and what needs to remain folded from the very start, possibly with some sort of type-driven separation of them. (There might be interesting research to do here.)
4. The proofs of the rewriter are not really maintainable, and are severely complicated by the use of CPS + dependent types. I think the way to go moving forward is to separate out two implementations of the rewriter, to be kept in sync: one that is CPS'd and fit for early reduction, and one that is not CPS'd and is clean to prove things about, but which ultimately can be proven equal to the CPS'd one.
5. Proving the side-conditions of reifying rewrite rules is currently a mess, because the rewriter was initially written without any intent to reify the rewrite rules, and instead was intended to have them proven by hand. The rewrite of the rewriter should follow the standard proof-by-reflection methodology, where the reification can be proven equal to the denotation via reflexivity, and then the only side-condition needed on the reified AST is a well-formedness predicate. (Then we can simply ask for a proof of the denotation of the reified rewrite rule.) All further transformations should happen reflectively rather than during the reification process, and the rewriter should be built around the presumption that this is where rules will be coming from. (This will incidentally simplify some of the dependent types, which were present only to make hand-writing rewrite rules nicer.)
6. There are a number of restrictions that should be lifted, the chief among them being the requirement that matching is linear on non-constants. (@achlipala, does there exist somewhere a treatment of PHOAS transformations which are allowed to query equality of variable nodes? The only way I can think of to do this is to instantiate var with symbol * outvar where I have a splittable infinite stream of symbols available and symbol has decidable equality, manually generating new symbols at each lambda node, and maintaining proof state about equality of outvars matching equality of symbols. It seems like there's a lot of overhead here, and I'm wondering if this can actually be done nicely.)
7. The code should be set up from the get-go to support generalization to arbitrary container types (I believe the main blocker for this, theoretically-speaking, is knowing how to thread the let-binding monad with arbitrary container-eliminator types).
8. The fact that pattern matching compilation naturally operates on raw syntax while NbE naturally operates on intrinsically-typed syntax is an ugly wart that I'm not sure how to fix. The current rewriter code glues them together with ugly code and painful proofs, but I'd like to see an elegant treatment of fusing pattern-matching compilation with NbE. (This would require new research. But even without this, in a rewrite of the rewriter, the glue should be accounted for so that its impact can be localized.)

Originally posted by @JasonGross in mit-plv/fiat-crypto#833 (comment)