Leonardo de Moura
eeac7fb9f4
feat: declare builtin attr parsers for builtin attributes
...
@Kha I believe this is the minimal set for covering the attributes we
have right now. The parser `simple` covers most of them, and the
dispatch is performed using the identifier.
Otherwise, the dispatch will be based on the node kind.
The `simple` parser is a bit hackish, but it is quite covenient for
simple attributes that do not require complex parameters.
2020-12-15 17:20:28 -08:00
Leonardo de Moura
6100ed9283
feat: add LeadingIdentBehavior type
...
Different strategies for handling the leading identifier in the
`Pratt` parser loop.
2020-12-15 16:45:14 -08:00
Leonardo de Moura
9e3b3b2495
refactor: move attribute related parsers to separate file
2020-12-15 16:13:11 -08:00
Leonardo de Moura
c9f766af5a
feat: we don't want attribute names as keywords
2020-12-15 15:59:48 -08:00
Leonardo de Moura
f4db2f5971
fix: workaround for old frontend
2020-12-15 15:49:45 -08:00
Leonardo de Moura
3ee6aec466
feat: add attr parser category
2020-12-15 15:44:46 -08:00
Leonardo de Moura
195ec0705e
feat: expand macros in attributes eagerly
...
The `AttrM` monad does not have sufficient information for expanding
macros. So, we expand them eagerly before we invoke the attributer
handlers implemented using `AttrM`.
cc @Kha
2020-12-15 15:11:19 -08:00
Leonardo de Moura
7bc630a54d
chore: remove old frontend leftover
2020-12-15 14:58:40 -08:00
Leonardo de Moura
066cae26fb
chore: cleanup
2020-12-15 13:51:03 -08:00
Leonardo de Moura
6985223a55
chore: switch to attrParam
2020-12-14 17:52:28 -08:00
Leonardo de Moura
69e8385f8d
refactor: move prioParser to Term.lean
2020-12-14 17:33:38 -08:00
Leonardo de Moura
0004196977
feat: add attrParam builtin parsers
2020-12-14 17:27:28 -08:00
Leonardo de Moura
a3fe907a28
feat: add attrParam syntax category
...
cc @Kha
2020-12-14 16:45:05 -08:00
Leonardo de Moura
abe7481453
feat: elaborate prio DSL
2020-12-14 16:25:10 -08:00
Leonardo de Moura
acba8d4a4a
chore: cleanup
2020-12-14 16:01:52 -08:00
Leonardo de Moura
fcaf38d566
fix: handle prec DSL at infixl macro
2020-12-14 15:35:37 -08:00
Leonardo de Moura
a46505cb8b
feat: use new precedence syntax
2020-12-14 15:14:03 -08:00
Leonardo de Moura
f95a450894
feat: add builtin prec/prio parsers
2020-12-14 15:05:39 -08:00
Leonardo de Moura
65bb478f7a
feat: expand prec.quot and prio.quot, add helper command macro elabStxQuot!
2020-12-14 13:36:26 -08:00
Leonardo de Moura
216d34e178
feat: add prio parser category
2020-12-14 13:24:56 -08:00
Leonardo de Moura
c5e201bce6
feat: add prec syntax category
2020-12-14 13:09:27 -08:00
Leonardo de Moura
469c9b7bbf
chore: remove TODO
2020-12-14 11:50:22 -08:00
Leonardo de Moura
5a5a49a54a
feat: add class abbrev macro
2020-12-14 10:19:00 -08:00
Leonardo de Moura
f24fff7985
chore: remove temporary workaround
2020-12-14 10:08:29 -08:00
Leonardo de Moura
a0463e8fa8
feat: elaborate new stactic quotations
2020-12-14 09:28:04 -08:00
Leonardo de Moura
ac692bfc79
feat: add new static quotations
...
For users that are writing (not-trivial) macros without `import Lean`.
cc @Kha
2020-12-14 09:21:26 -08:00
Leonardo de Moura
c7a8fa2629
chore: expose a few auxiliary command parsers
2020-12-14 09:15:26 -08:00
Leonardo de Moura
4001407f10
refactor: add MonadError class abbreviation
2020-12-14 09:15:26 -08:00
Sebastian Ullrich
314c5c9d41
feat: run single non-category quotation under interpreter as well
2020-12-14 17:13:59 +01:00
Sebastian Ullrich
a9bdb2f70a
feat: prefer interpreter for running builtin parsers in quotations
2020-12-14 16:45:32 +01:00
Sebastian Ullrich
0316c872b9
feat: macro: use appropriate antiquotation kind dependent on bound syntax
...
/cc @leodemoura
2020-12-14 13:54:34 +01:00
Leonardo de Moura
0d9694d836
chore: user deriving BEq
2020-12-13 16:30:07 -08:00
Leonardo de Moura
bad714f5e9
feat: add deriving BEq
2020-12-13 16:13:27 -08:00
Leonardo de Moura
0862df9ade
fix: missing ppSpace at set_option parser
2020-12-13 15:52:03 -08:00
Leonardo de Moura
15232f51d3
feat: add Expr.constainsFVar
2020-12-13 15:51:48 -08:00
Leonardo de Moura
f5d59ee287
fix: missing eraseMacroScopes at set_option
2020-12-13 15:51:00 -08:00
Leonardo de Moura
ed86e74149
feat: add option match.ignoreUnusedAlts
...
It is useful for macros that generate `match`-expressions
2020-12-13 15:50:24 -08:00
Leonardo de Moura
f345c8c708
feat: add betaReduce
2020-12-13 15:49:22 -08:00
Leonardo de Moura
04a07c15b9
chore: use deriving Inhabited
2020-12-13 11:57:59 -08:00
Leonardo de Moura
3b6d65c3c3
chore: use deriving Inhabited
2020-12-13 10:09:20 -08:00
Leonardo de Moura
0bbc2ca884
feat: elaborate optDeriving
2020-12-13 09:05:03 -08:00
Leonardo de Moura
8fd6870931
fix: optDeriving parser
2020-12-12 18:58:44 -08:00
Leonardo de Moura
ebd8680de8
feat: add Deriving/Inhabited.lean
2020-12-12 18:52:24 -08:00
Leonardo de Moura
2c81d7e91c
feat: add basic deriving instance elaborator
2020-12-12 17:00:49 -08:00
Leonardo de Moura
01ec581617
chore: update deriving instance syntax
2020-12-12 16:48:12 -08:00
Leonardo de Moura
fb175ccab7
feat: add Deriving.lean
2020-12-12 16:08:50 -08:00
Leonardo de Moura
3743f877f4
feat: add deriving parsers
2020-12-12 15:33:36 -08:00
Leonardo de Moura
5249fdc24d
chore: cleanup and style
2020-12-12 10:36:26 -08:00
Sebastian Ullrich
554d0b4d4c
chore: adapt stdlib to new antiquotation splices
2020-12-12 17:20:03 +01:00
Sebastian Ullrich
8dfa588983
feat: introduce SepArray and use it for sepBy antiquotation splices
2020-12-12 16:02:15 +01:00
