leanprover
feat: light-weight basic quotation macro
Description:
I finally got annoyed enough at the lack of Qq, that I figured we can just roll our own basic version to get 80% of the benefits. So, I implemented a very basic ql(..) macro. Crucially, we only attempt to deal with closed terms, so we avoid a lot of the complexity that QQ has to deal with anti-quotations. Similarly, we avoid the performance problems of QQ because we don't attempt to deal with expression matching either.
To implement the macro, we had to take the ToExpr Expr instance from Mathlib, which meant pulling in the ToExpr derive handler (which isn't a bad thing, that derive handler will be generally useful). That is, DeriveToExpr.lean, ToExpr.lean and ToLevel.lean are taken from Mathlib, with only very slight modifications to eliminate any further Mathlib dependencies to do with pretty-printing.
Then, Tactics/QuoteLight.lean is actually new code. The implementation of the ql(..) macro is quite simple, only about 50 lines of meta-code. The rest of the file consists of a few basic tests.
Even with this limited scope, the macro will be useful to simplify a bunch of our meta-code, removing some of the tedium involved and improving readability. For example, we currently have mkApp (.const ``List.nil [0]) (mkConst ``StateField) somewhere in the code, with the macro we can simplify this to ql(@List.nil StateField).
Testing:
What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine? Yes
License:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
