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
Sebastian Ullrich
21f4257da5
feat: name resolution during parsing
2020-12-03 17:46:13 +01:00
Leonardo de Moura
f4c9f9579b
chore: update stage0
2020-12-03 08:08:58 -08: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
962cffbaaa
feat: add lean_float_of_decimal using GMP
2020-12-03 06:15:18 -08:00
Leonardo de Moura
e8b58abffc
chore: update stage0
2020-12-02 15:32:17 -08:00
Leonardo de Moura
85c9ab072c
feat: elaborate and delaborate decimals
2020-12-02 15:31:06 -08:00
Leonardo de Moura
983a1e596b
chore: update stage0
2020-12-02 14:57:26 -08:00
Leonardo de Moura
facb28d080
feat: basic support for decimal numbers
2020-12-02 14:54:59 -08:00
Leonardo de Moura
133ecb111b
chore: remove workaround
2020-12-02 13:33:45 -08:00
Leonardo de Moura
6f9d3a1447
chore: update stage0
2020-12-02 13:29:58 -08:00
Leonardo de Moura
469de09280
fix: bug at isDefEq
...
The new test contains a minimal example that triggers the bug.
2020-12-02 13:27:21 -08:00
Leonardo de Moura
3a08dd2771
chore: typo
2020-12-02 13:27:21 -08:00
Sebastian Ullrich
d96393ee47
doc: building Lean packages with Nix
2020-12-02 17:52:57 +01:00
Sebastian Ullrich
2437b1cea1
fix: support single-file packages
2020-12-02 17:29:01 +01:00
Sebastian Ullrich
797bec86f5
chore: Nix: overhaul nix-dev, lift technical restrictions
2020-12-02 16:49:25 +01:00
Sebastian Ullrich
b90f93966d
fix: Nix: add transitive external dependencies to the LEAN_PATH
2020-12-02 13:59:19 +01:00
Leonardo de Moura
c2ea02b7c4
chore: update stage0
2020-12-01 18:42:41 -08:00
