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
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
Leonardo de Moura
0862df9ade
fix: missing ppSpace at set_option parser
2020-12-13 15:52:03 -08:00
Leonardo de Moura
3b6d65c3c3
chore: use deriving Inhabited
2020-12-13 10:09:20 -08:00
Leonardo de Moura
8fd6870931
fix: optDeriving parser
2020-12-12 18:58:44 -08:00
Leonardo de Moura
01ec581617
chore: update deriving instance syntax
2020-12-12 16:48:12 -08:00
Leonardo de Moura
3743f877f4
feat: add deriving parsers
2020-12-12 15:33:36 -08:00
Sebastian Ullrich
9e06680541
chore: remove old antiquotations splice syntax
2020-12-12 14:57:14 +01:00
Sebastian Ullrich
a13f129312
feat: antiquotation suffix splices such as $x:k,*
...
/cc @leodemoura
2020-12-12 14:57:14 +01:00
Leonardo de Moura
76fb1799fe
chore: goodies for deriving command
2020-12-11 18:08:50 -08:00
Sebastian Ullrich
bf63c4c0d0
feat: make sure dynamic quotations can only be used for parsers of arity 1
2020-12-11 21:34:30 +01:00
Leonardo de Moura
f2ea45e68a
feat: expose doSeq and termBeforeDo parsers
...
Users can use them to extend the `do` DSL.
2020-12-10 19:10:25 -08:00
Leonardo de Moura
1977b66573
feat: proper node for optional .. at structInst
2020-12-10 11:56:37 -08:00
Leonardo de Moura
28feed9c45
feat: proper node for structInstLVal
2020-12-10 11:50:12 -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
Leonardo de Moura
4d79c00846
feat: add double quoted name literal parser
2020-12-09 17:27:45 -08:00
Sebastian Ullrich
4dfa7e1187
feat: use actual separator in sepBy antiquotation scope
2020-12-09 17:48:05 +01:00
Sebastian Ullrich
fd1f74c421
feat: extend sepBy syntax syntax
2020-12-09 17:36:29 +01:00
Sebastian Ullrich
00e167b2f0
feat: match_syntax ~> match
2020-12-08 17:20:36 +01:00
Sebastian Ullrich
32eeac88c8
fix: ensure matchAlts have same shape with and without optionalFirstBar
2020-12-08 17:13:32 +01:00
Leonardo de Moura
ae5aa51712
chore: add explicit discard
2020-12-08 06:18:18 -08:00
Leonardo de Moura
1c0943ad82
feat: add #reduce command parser
2020-12-06 09:32:25 -08:00
Leonardo de Moura
f0372f724c
chore: remove unused attribute
2020-12-05 16:28:58 -08:00
Leonardo de Moura
fdc2c9f281
feat: process local instance ... and scoped instance ... commands
2020-12-05 15:46:25 -08:00
Leonardo de Moura
d27770ea0e
chore: prepare to add scoped and local instances
2020-12-05 15:36:23 -08:00
Leonardo de Moura
1faed06dc1
feat: new attrKind syntax
2020-12-05 13:59:08 -08:00
Leonardo de Moura
f1f8c2482f
feat: prepare to change attrKind parser
...
We want to add a proper node and kind.
2020-12-05 13:49:59 -08:00
Leonardo de Moura
32d5ef8b78
feat: scoped and local unification hints
2020-12-05 13:49:36 -08:00
Leonardo de Moura
10102bf370
chore: remove "local" before attribute command
...
`local` is now part of the `Term.attrInstance` parser.
2020-12-05 07:47:28 -08: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
4d428c8660
feat: add ScopedEnvExtension.addLocalEntry
2020-12-05 06:54:03 -08:00
Leonardo de Moura
0ab368581a
refactor: ScopedEnvExtension
...
1) `ScopedEnvExtension` module now mananges the push/pop/activate
methods. Motivations:
- Easier to add attributes
- One `ScopedEnvExtension` may be shared between multiple
attributes (e.g., parsers)
2) Add `AttributeKind`
2020-12-04 16:22:43 -08:00
Leonardo de Moura
02e13081a9
feat: implement AttributeImpl scoping methods for parsers
2020-12-04 16:22:43 -08:00
Sebastian Ullrich
04f09cc34f
perf: avoid redundant token collections from antiquotation scopes
2020-12-04 22:43:31 +01: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
Sebastian Ullrich
d7f27a140e
feat: antiquotation scopes
2020-12-04 19:24:32 +01:00
Sebastian Ullrich
92cbe27810
refactor: clean up & delay registering parser aliases
2020-12-04 19:24:32 +01:00
Leonardo de Moura
6f1facd07c
feat: implement ParserExtension using ScopedEnvExtension
2020-12-04 09:57:35 -08:00
Leonardo de Moura
963b0f1270
feat: scoped attributes cont.
2020-12-03 10:46:09 -08:00
Leonardo de Moura
2408b5c6b5
feat: basic support for scoped attributes
2020-12-03 10:39:59 -08:00
Sebastian Ullrich
80d4ae82e8
feat: arbitrary quotation kinds via name resolution in the parser and execution in the interpreter
2020-12-03 17:46:13 +01:00
Sebastian Ullrich
21f4257da5
feat: name resolution during parsing
2020-12-03 17:46:13 +01:00
Leonardo de Moura
b95c4788c1
refactor: OfDecimal ==> OfScientific
...
`decimalLit` ==> `scientificLit`
2020-12-03 08:08:19 -08:00
Leonardo de Moura
d1f4d4f57e
feat: scientific notation
2020-12-03 07:49:20 -08:00
Leonardo de Moura
85c9ab072c
feat: elaborate and delaborate decimals
2020-12-02 15:31:06 -08:00
Leonardo de Moura
facb28d080
feat: basic support for decimal numbers
2020-12-02 14:54:59 -08:00
