Sebastian Ullrich
|
1f447efa54
|
doc: update Lean.Parser.Basic
|
2022-11-11 14:17:21 +01:00 |
|
Sebastian Ullrich
|
7cdd8f81d7
|
refactor: simplify withCacheFn
|
2022-11-11 14:07:15 +01:00 |
|
Sebastian Ullrich
|
43767f8f35
|
fix: uncacheable syntax stack access in doIf
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
4c11743f4b
|
refactor: split paren parser, part 2
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
791fc70dd9
|
refactor: split paren parser
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
30dd28480d
|
fix: suppressInsideQuot inside quotation
|
2022-11-11 13:45:41 +01:00 |
|
Sebastian Ullrich
|
0dea086669
|
fix: reset lhsPrec, errorMsg in withCacheFn
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
22510db004
|
refactor: simplify parser code using withFn
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
e7bf1cd3dc
|
refactor: simplify adaptUncacheableContextFn
compiler.ir.result reports 0 allocations on happy path
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
fb941d0827
|
fix: ensure parser caching is sound re. syntax stack accesses
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
12b267bd8c
|
refactor: categoryParserOfStack is dead
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
17782fba1a
|
fix: replace broken ptrEq cache sanity checks with private ParserContext constructor
The context is now manipulated using `adaptCacheableContext` and `adaptUncacheableContext`
and created using `ParserFn.run`.
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
d5255e94e8
|
perf: improve dynamicQuot caching
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
d3f7d0350f
|
refactor: move parser types into separate file
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
9a4626c495
|
fix: must cache stack of parser evals
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
36189cb51a
|
chore: simplify parser cache key computation, panic on environment/token table divergence
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
ed03ff9d00
|
perf: cache leading_parser and syntax as well
We better hope the `leading_parser`s are closed terms
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
da6efe1bca
|
fix: make parser caching sound (I hope?)
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
35509b5e98
|
refactor: more sensible ordering of declarations in Lean.Parser.Basic
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
246923886a
|
fix: do not create choice nodes for failed parses
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
57320712f0
|
fix: extraneous missing items on parser stack
|
2022-11-11 09:13:02 +01:00 |
|
Sebastian Ullrich
|
7e193a45ce
|
perf: cache category parses
|
2022-11-11 09:13:02 +01:00 |
|
Leonardo de Moura
|
2386c401d2
|
chore: use String.get' and String.next' at Parser/Basic.lean
This commit also cleans up old frontend legacy.
|
2022-11-09 17:06:22 -08:00 |
|
Adrien Champion
|
5849fdc6c9
|
feat: require strict indentation on nested by-s
|
2022-11-08 08:30:42 -08:00 |
|
Mario Carneiro
|
4bf89dfa12
|
feat: allow doSeq in let x <- e | seq
fixes #1804
|
2022-11-08 08:29:21 -08:00 |
|
Mario Carneiro
|
32b6bd0d8b
|
feat: empty type ascription syntax (e :) (part 2)
|
2022-11-07 19:10:56 +01:00 |
|
Mario Carneiro
|
02d8a5d56e
|
feat: empty type ascription syntax (e :)
|
2022-11-07 19:10:56 +01:00 |
|
Sebastian Ullrich
|
5249611d75
|
doc: fix mkAntiquot docstring
|
2022-11-03 10:07:38 +01:00 |
|
Mario Carneiro
|
9b40613207
|
fix: formatting for if let and do if
|
2022-11-01 20:19:39 -07:00 |
|
Sebastian Ullrich
|
7475fd9cbd
|
feat: ignore patternIgnore nodes in syntax patterns
|
2022-10-28 21:25:47 +02:00 |
|
Mario Carneiro
|
29bda62198
|
fix: missed a file from #1771
|
2022-10-27 11:14:13 -07:00 |
|
Leonardo de Moura
|
e369c3beb6
|
fix: disallow . immediately after ..
Rejects the following weird example
```
```
which was being parsed as
```
```
|
2022-10-26 07:13:40 -07:00 |
|
Leonardo de Moura
|
00ca0dde5c
|
feat: add unop% term parser
We not to support unary minus at `BinOp.toTree`
see #1779
|
2022-10-26 06:19:22 -07:00 |
|
Mario Carneiro
|
d7d61bfb55
|
feat: use withoutPosition consistently (part 2)
|
2022-10-24 12:51:32 -07:00 |
|
Mario Carneiro
|
765ebcdbf0
|
feat: use withoutPosition consistently
|
2022-10-24 12:51:32 -07:00 |
|
Mario Carneiro
|
e7c7678ab0
|
refactor: line wrapping in parser code
|
2022-10-24 08:37:29 -07:00 |
|
Mario Carneiro
|
b3ba78aade
|
feat: hovers & name resolution in registerCombinatorAttribute (part 2)
|
2022-10-23 09:30:38 +02: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
|
faa612e7b7
|
chore: remove #resolve_name
|
2022-10-17 14:53:51 -07:00 |
|
Mario Carneiro
|
c06cffa54f
|
refactor: rename isExitCommand -> isTerminalCommand
|
2022-10-12 11:11:31 -07:00 |
|
Mario Carneiro
|
8dfae9eb38
|
feat: import command stub
|
2022-10-12 11:11:31 -07:00 |
|
Gabriel Ebner
|
0d3d05bd3a
|
feat: clear%
|
2022-10-11 17:24:35 -07:00 |
|
Mario Carneiro
|
391aef5cd7
|
feat: automatic extension names
|
2022-10-06 17:19:30 -07:00 |
|
Sebastian Ullrich
|
71e647049f
|
refactor: lexOrd should not be an instance
|
2022-09-28 15:57:01 -07:00 |
|
Sebastian Ullrich
|
d0a002ffff
|
fix: prefer longer parse even if unsuccessful
|
2022-09-28 15:57:01 -07:00 |
|
Mario Carneiro
|
85119ba9d1
|
chore: move Std.* data structures to Lean.*
|
2022-09-26 05:46:04 -07:00 |
|
Gabriel Ebner
|
a351a4be70
|
feat: use colEq in sepByIndent
|
2022-09-19 12:44:43 -07:00 |
|
Gabriel Ebner
|
b1bef71d59
|
feat: colEq parser
|
2022-09-19 12:44:43 -07:00 |
|