mit-plv / rewriter

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Other
22 stars 20 forks source link

Add profiling for cbn #141

Closed JasonGross closed 10 months ago

JasonGross commented 10 months ago

Seems to be responsible for 23.0% of the cost of rewrite rules in https://github.com/mit-plv/fiat-crypto/pull/1778, with a single call taking 168.429s.

Should not add much overhead (just a branch) when not enabled.