Leonardo de Moura
94ff89bfc4
chore: update stage0
2020-12-05 07:48:37 -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
9389bca624
feat: elaborate attrKind
2020-12-05 07:40:55 -08:00
Leonardo de Moura
6f6e153a85
chore: update stage0
2020-12-05 07:40:35 -08:00
Leonardo de Moura
bcf4ffdd1a
feat: local modifier at @[...]
2020-12-05 07:24:55 -08:00
Leonardo de Moura
ad59ab0d7c
chore: update stage0
2020-12-05 07:01:10 -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
2463371a25
chore: fix test
2020-12-04 18:13:36 -08:00
Leonardo de Moura
b37213e378
chore: remove workaround
2020-12-04 18:11:53 -08:00
Leonardo de Moura
42232609b9
chore: update stage0
2020-12-04 18:08:14 -08:00
Leonardo de Moura
752578a64c
chore: temporary staging workaround
2020-12-04 18:07:09 -08:00
Leonardo de Moura
8f223fb8f2
chore: update stage0
2020-12-04 18:03:44 -08:00
Leonardo de Moura
aad8ea9c76
feat: stable parser names
...
```
syntax term "+" term : term -- generates `term_+_`
syntax "[" sepBy(term, ", ") "]" : term -- generates `term[_,]`
syntax "done" : tactic -- generates `tacticDone`
```
cc @Kha
2020-12-04 18:00:51 -08:00
Leonardo de Moura
8dbbe37d38
chore: fix test
2020-12-04 16:22:45 -08:00
Leonardo de Moura
54723409c3
test: scoped parsers
2020-12-04 16:22:45 -08:00
Leonardo de Moura
c2cfbf2cdd
chore: remove workaround
2020-12-04 16:22:45 -08:00
Leonardo de Moura
ff32de6e7f
chore: update stage0
2020-12-04 16:22:45 -08:00
Leonardo de Moura
2ef84a1b64
chore: temporary staging workaround
...
@Kha It seems the new builtin antiquotation notation you added depends
on the array literal notation that is not builtin. I got the following
error after `update-stage0`
```
Lean/PrettyPrinter/Delaborator/Builtins.lean:455:2: error: elaboration function for '_kind.term._@.Init.Data.Array.Basic._hyg.3391' has not been implemented
```
The base name changed from `_kind.term` to `termKind`. I had to change
it because every parser we were defining was in the artificial (sub-)namespace
`_kind` :)
We didn't notive because we didn't have scoped parsers.
2020-12-04 16:22:44 -08:00
Leonardo de Moura
d6cba5c3c1
chore: update stage0
2020-12-04 16:22:44 -08:00
Leonardo de Moura
0749cb9fa9
fix: avoid artificial hierarchical name at parser declarations
2020-12-04 16:22:43 -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
7266883b41
chore: update stage0
2020-12-04 11:41:33 -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
6c4072cd4a
chore: add keyword "scoped"
2020-12-04 11:28:40 -08:00
Leonardo de Moura
1a90358d5d
chore: update stage0
2020-12-04 11:21:45 -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
a25e6bdd6e
refactor: try out antiquotation scopes
...
current limitations:
* don't work in patterns
* nested antiquotations must be of the form `$id`, not `$(e)`, and at most two of them
* sepBy antiquotation scopes hard-coded to `,`, `;`, `|` (e.g. `$[...],*`)
* unclear whether they can replace the old `$id:kind*` syntax yet
/cc @leodemoura
2020-12-04 19:33:04 +01:00
Sebastian Ullrich
c49d37bba8
chore: update stage0
2020-12-04 19:27:51 +01:00
Sebastian Ullrich
d7f27a140e
feat: antiquotation scopes
2020-12-04 19:24:32 +01:00
Sebastian Ullrich
bdabdd78cf
fix: make "$" ws atomic so it doesn't eat up later antiquotations
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
Sebastian Ullrich
878f32b662
chore: remove obsolete antiquot choice workaround
...
We now parse antiquotations before calling `longestMatch`.
2020-12-04 19:24:32 +01:00
Leonardo de Moura
540f9aa1ea
chore: update stage0
2020-12-04 09:58:33 -08:00
Leonardo de Moura
6f1facd07c
feat: implement ParserExtension using ScopedEnvExtension
2020-12-04 09:57:35 -08:00
Leonardo de Moura
5f5a8010a2
feat: add ScopedEnvExtension
2020-12-03 17:04:16 -08:00
Leonardo de Moura
5064115ff1
feat: trie for hierarchical names
2020-12-03 16:40:00 -08:00
Leonardo de Moura
f896bb27d6
chore: update stage0
2020-12-03 10:46:45 -08:00
Leonardo de Moura
963b0f1270
feat: scoped attributes cont.
2020-12-03 10:46:09 -08:00
Leonardo de Moura
4a879fcd2c
chore: update stage0
2020-12-03 10:40:35 -08:00
Leonardo de Moura
2408b5c6b5
feat: basic support for scoped attributes
2020-12-03 10:39:59 -08:00
Sebastian Ullrich
23b0e6ca5b
fix: Nix: use stage 1 outside of src/
...
Hopefully we can solve this using a src/flake.nix as soon as relative flake inputs are supported
2020-12-03 18:49:29 +01:00
Sebastian Ullrich
58dc7a791f
refactor: more dynamic quot tests
2020-12-03 18:21:16 +01:00
Sebastian Ullrich
e0016662c6
refactor: test dynmaic quotations
...
/cc @leodemoura
2020-12-03 18:05:15 +01:00
Sebastian Ullrich
e74e72a938
chore: update stage0
2020-12-03 17:58:30 +01:00
Sebastian Ullrich
dbf9fc9799
feat: elaborate dynamic quotations
2020-12-03 17:58:30 +01:00
Sebastian Ullrich
07ba3cd171
chore: update stage0
2020-12-03 17:57:40 +01: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
