Mario Carneiro
|
e7c7678ab0
|
refactor: line wrapping in parser code
|
2022-10-24 08:37:29 -07:00 |
|
Mario Carneiro
|
583e023314
|
chore: snake-case attributes (part 2)
|
2022-10-19 09:28:08 -07:00 |
|
Mario Carneiro
|
dd5948d641
|
chore: snake-case attributes (part 1)
|
2022-10-19 09:28:08 -07:00 |
|
Gabriel Ebner
|
fb4d90a58b
|
feat: dynamic quotations for categories
|
2022-10-18 14:59:14 -07:00 |
|
Mario Carneiro
|
6392c5b456
|
chore: import reductions
|
2022-09-15 14:02:38 -07:00 |
|
Mario Carneiro
|
a4f1db7aca
|
feat: attributes on {macro,elab}(_rules)
|
2022-08-15 08:40:40 -07:00 |
|
Mario Carneiro
|
3b793b949b
|
feat: attributes on notation
|
2022-08-14 11:18:20 -07:00 |
|
Mario Carneiro
|
c961cd1310
|
feat: doc comments on notation
|
2022-08-13 17:18:14 -07:00 |
|
Mario Carneiro
|
e816424466
|
chore: use Category declarations for builtin cats too (#1400)
|
2022-08-03 18:10:54 -07:00 |
|
Leonardo de Moura
|
1c770ac8d7
|
feat: doc strings for declare_syntax_cat
see #1374
|
2022-07-27 13:40:08 -07:00 |
|
Leonardo de Moura
|
e1fc904786
|
feat: attributes on syntax
closes #1321
|
2022-07-18 23:37:11 -04:00 |
|
Leonardo de Moura
|
e336ff5f93
|
feat: indentation sensitiviy for macro and elab commands
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Command.20terminator/near/257674790
|
2021-10-18 17:16:09 -07:00 |
|
Leonardo de Moura
|
f43ab76641
|
feat: doc string for syntax abbreviations
|
2021-09-12 18:26:36 -07:00 |
|
Leonardo de Moura
|
d67c633ca1
|
feat: allow user to set "behavior" at declare_syntax_cat
|
2021-09-01 13:28:12 -07:00 |
|
Sebastian Ullrich
|
e632c14f3f
|
chore: align stx precedence in syntax to the new one in macro
|
2021-08-24 10:11:12 -07:00 |
|
Sebastian Ullrich
|
20accf5105
|
feat: revise macro parameter syntax
|
2021-08-12 07:48:42 -07:00 |
|
Sebastian Ullrich
|
8637220927
|
fix: make precedence mandatory for mixfix commands
Resolves #577
|
2021-07-19 13:18:58 -07:00 |
|
Sebastian Ullrich
|
3f4ab0a2af
|
feat: implement elab_rules
TODO: infer category from quotation type
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
9101c9d5da
|
feat: support docstrings on syntax/macro/...
|
2021-06-21 10:17:26 -07:00 |
|
tydeu
|
44f45f426c
|
feat: add scoped macro_rules (#432)
|
2021-04-30 09:05:09 +02:00 |
|
Sebastian Ullrich
|
73cf3533a1
|
fix: count quotation depth in parser correctly
|
2021-04-29 13:33:48 +02:00 |
|
Leonardo de Moura
|
09d438ca1d
|
chore: enforce notation parameter naming convention
|
2021-04-19 18:54:09 -07:00 |
|
Leonardo de Moura
|
164577d94e
|
chore: remove parser! and tparser!
The new macros are called "leading_parser` and `trailing_parser`.
cc @Kha
|
2021-03-11 09:36:58 -08:00 |
|
Sebastian Ullrich
|
1c31240ebb
|
feat: token antiquotations in macro
|
2020-12-22 13:11:04 +01:00 |
|
Leonardo de Moura
|
0642a62848
|
chore: prepare to add scoped macro and elab commands
|
2020-12-21 16:50:29 -08:00 |
|
Leonardo de Moura
|
4fc06bfcca
|
feat: add optional (priority := <prio>) to instance command
|
2020-12-21 10:02:12 -08:00 |
|
Leonardo de Moura
|
43284cc5fa
|
feat: improve notation for setting parser names and priorities
|
2020-12-21 09:11:12 -08:00 |
|
Leonardo de Moura
|
97642bd000
|
fix: prio issue
|
2020-12-16 07:44:48 -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
|
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
|
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
|
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
|
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
|
ffefd8db36
|
chore: remove weird syntax sugar from macro command
Before this commit,
```
macro term x:term : term => `($x)
```
would generate the notation
```
syntax "term" term : term
```
|
2020-12-10 08:09:47 -08:00 |
|
Sebastian Ullrich
|
fd1f74c421
|
feat: extend sepBy syntax syntax
|
2020-12-09 17:36:29 +01:00 |
|
Leonardo de Moura
|
bcf4ffdd1a
|
feat: local modifier at @[...]
|
2020-12-05 07:24:55 -08:00 |
|
Leonardo de Moura
|
c6ab0b4d2c
|
feat: allow local modifier at infix, notation, and syntax commands
|
2020-12-05 07:00:06 -08:00 |
|
Leonardo de Moura
|
5a772c6cae
|
feat: expand scoped notation into scoped attribute modifier
|
2020-12-04 11:39:00 -08:00 |
|
Leonardo de Moura
|
4d523e3b8c
|
chore: prepare to add optional "scoped" at syntax, infix, and notation commands
|
2020-12-04 11:20:48 -08:00 |
|
Leonardo de Moura
|
e9069b6965
|
feat: expand optional priority at notation and mixfix commands
|
2020-11-29 08:22:47 -08:00 |
|
Leonardo de Moura
|
ee5679c77c
|
chore: prepare to add optional priorities to the notation and mixfix commands
|
2020-11-29 08:05:26 -08:00 |
|
Leonardo de Moura
|
8751bbe2a8
|
fix: notation for non reserved symbols
|
2020-11-17 11:25:04 -08:00 |
|
Leonardo de Moura
|
af8d616d5a
|
feath: improve unary and binary parsers
|
2020-11-17 08:39:56 -08:00 |
|
Leonardo de Moura
|
360fa1638f
|
chore: rename Parser.try to Parser.atomic
Reason: `try` is a keyword.
cc @Kha
|
2020-11-17 08:25:01 -08:00 |
|
Leonardo de Moura
|
bd76458210
|
feat: add support for nonReservedSymbol at syntax command
|
2020-11-12 07:32:18 -08:00 |
|
Leonardo de Moura
|
6fbaea6563
|
feat: simplify syntax command syntax
|
2020-11-12 07:01:20 -08:00 |
|