rewriter
rewriter copied to clipboard
mit-plv
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Of the time spent in the new rewrite rule reification, 82.7% is spent in [`replace_type_try_transport`](https://github.com/mit-plv/rewriter/blob/03889802d6ddb8dcaeb922206f07c3836d0a7b49/src/Rewriter/Rewriter/Reify.v#L597-L636) (236.006s max for a single call), which is basically "`match context[@type.try_transport ?base_type ?try_make_transport_base_type_cps ?p ?t...
Currently, we cannot handle rewrite rules such as ```coq forall x, '(S x) = pred '(S (S x)) ``` because we end up generating a pattern like `forall x1 x2,...
It's quite painful to figure out why rewriter rules aren't matching. It should be possible, using a combination of [reduction-effects](https://github.com/coq-community/reduction-effects) for `cbv` (alas, no support for `native_compute` / `vm_compute`, yet;...
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...
The file https://github.com/mit-plv/rewriter/blob/master/src/Rewriter/Demo.v should be fleshed out and completed. Perhaps ideally in time for the POPL submission.
