max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
19793 commits 1 branch 0 tags 5.3 GiB
Commit graph

109 commits

Author SHA1 Message Date
Sebastian Ullrich
8f67db0101 refactor: never implicitly ignore monadic results 
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
 2020-04-23 11:09:59 -07:00
Sebastian Ullrich
ed14375dad feat: sort and deduplicate "expected" tokens in parser error messages 2020-03-19 17:17:08 -07:00
Leonardo de Moura
bb0bfb5742 fix: sepBy 
If parser consumed something, keep error.
 2020-02-21 11:43:45 -08:00
Sebastian Ullrich
86d2b82c29 refactor: get rid of antiquotExpr hack 2020-02-18 10:57:27 -08:00
Sebastian Ullrich
25f764daad feat: antiquotation escapes 2020-02-18 10:57:12 -08:00
Leonardo de Moura
3c235c3613 chore: naming convention 2020-02-09 17:10:20 -08:00
Leonardo de Moura
7e959f8393 chore: try to control code explosion 
@Kha We got 100k extra lines of code in the last update stage0
 2020-02-06 10:10:10 -08:00
Leonardo de Moura
9270fa5ad8 chore: add [inline] to make sure we do not allocate a closure 
cc @kha
 2020-02-06 08:15:39 -08:00
Sebastian Ullrich
933ff6dc88 perf: short-circuit all antiquotation parsers 2020-02-06 08:12:08 -08:00
Leonardo de Moura
9169a975f8 perf: improve peekToken performance 
`peekToken` is invoked 3 times in sequence whenever we use
`categoryParser`.

1- `currLbp` at `prattParser`
2- check `$` at `leadingParser`
3- `indexed`

@Kha It improved the performance by 10% on my machine.
 2020-02-05 09:58:34 -08:00
Leonardo de Moura
3a9f6e4133 perf: avoid closure allocations and orelse when next token is not "$" 2020-02-04 10:45:41 -08:00
Sebastian Ullrich
52a0a0937e feat: check precedence of leading parsers as well 2020-02-04 07:49:33 -08:00
Leonardo de Moura
d75cd49ea2 fix: app parser 
cc @kha
 2020-02-03 20:13:38 -08:00
Leonardo de Moura
2138a11480 feat: use custom error messages at checkRBPGreater 2020-02-03 18:30:22 -08:00
Leonardo de Moura
99f7aff491 fix: liftMethod notation 2020-02-03 17:12:44 -08:00
Sebastian Ullrich
4279df4170 perf: special-case antiquotation syntax in Pratt parser to avoid choice nodes 
fixes #99
 2020-02-03 09:43:41 -08:00
Leonardo de Moura
21618361b7 refactor: remove ParserKind 2020-01-30 20:56:46 -08:00
Leonardo de Moura
6b1e64d7ea chore: prepare for refactoring 2020-01-30 20:41:10 -08:00
Leonardo de Moura
31ebccea58 chore: remove ParserDescr.pushLeading 2020-01-30 19:04:07 -08:00
Leonardo de Moura
410d295429 refactor: remove unnecessary pushLeading, add ParserDescr.trailingNode 2020-01-30 18:32:28 -08:00
Leonardo de Moura
72ff3da6cd refactor: preparing to remove ParserKind 2020-01-30 17:31:53 -08:00
Sebastian Ullrich
470e1623de chore: hide "expected '$'" 2020-01-30 08:56:14 -08:00
Leonardo de Moura
8525584a78 refactor: naming consistency ensure List and Array have similar find* methods 
`find?`     -> takes predicate
`findSome?` -> takes a function (A -> Option B)
 2020-01-26 15:13:05 -08:00
Leonardo de Moura
74bac15c6f chore: make sure letDecl is a node 
This is useful when defining notation such as `where`.
Moreover, it allows us to write `$d:letDecl`, but `$d` never matches
a `letDecl`
 2020-01-25 19:56:53 -08:00
Leonardo de Moura
9f816277fc feat: make sure letSimpleDecl and letPatDecl have the same #args 2020-01-25 19:08:16 -08:00
Leonardo de Moura
7b6caba457 feat: add `ident as a valid elaboration kind 2020-01-25 14:55:32 -08:00
Leonardo de Moura
6d5de9f965 feat: handle raw identifiers as binders in fun 
@Kha I am adding this kind of feature to improve the user experience.
For example, the macro
```
syntax "[" ident "↦" term "]" : term
macro_rules
| `([$x ↦ $v]) => `(fun $x => $v)
```
is accepted and looks perfectly reasonable.
However, before this commit, we would get a nasty error when
elaborating
```lean
check [x ↦ x + 1]
```
 2020-01-25 14:55:21 -08:00
Leonardo de Moura
364bb7bdf7 fix: proper Name literals 
cc @kha
 2020-01-24 12:38:15 -08:00
Leonardo de Moura
954c69de35 feat: use macroscopes for creating fresh kinds 2020-01-23 12:38:31 -08:00
Leonardo de Moura
764b854742 fix: bug at longestMatchStep 
@Kha I found the bug by accident when I was playing with the
bigop.lean
 2020-01-22 17:31:54 -08:00
Leonardo de Moura
3f24b31286 chore: remove leftover 2020-01-22 16:50:05 -08:00
Leonardo de Moura
a5bcebb07f feat: add antiquotation support for strLit, numLit and charLit 2020-01-22 12:57:28 -08:00
Leonardo de Moura
0be31c14ec fix: workaround for term parser antiquotation issue 
@Kha this is a temporary workaround. We should discuss how to cleanup
in the next Dev meeting.
 2020-01-22 12:05:12 -08:00
Leonardo de Moura
642850efb2 fix: antiquotation for all categories 2020-01-22 11:52:08 -08:00
Leonardo de Moura
e8c54ad1bf fix: use nonReservedSymbol when defining tactic new syntax 2020-01-21 14:37:29 -08:00
Leonardo de Moura
8fb710c31e chore: remove simple parser kind 
Now, the previous commit makes sure pratt's parsers subsume simple parsers
 2020-01-21 09:16:38 -08:00
Leonardo de Moura
f3c1928d2d feat: improve prattParser tables 
We can delete the simple category after this change

cc @Kha
 2020-01-21 09:16:38 -08:00
Leonardo de Moura
b279433236 feat: improve checkNoWsBefore (skip None nodes) 2020-01-20 22:24:01 -08:00
Leonardo de Moura
47c85cc351 fix: bug at ParserDescr.ident 2020-01-20 21:55:16 -08:00
Leonardo de Moura
1dbfc4b337 fix: add checkNoWsBefore before option * in mkAntiquot 
@kha we need it, otherwise we can't process rules such as
```
| `(FOO $t >>> $r) => `($t * $r)
```
without adding parenthesis at `(($t) * $r)
 2020-01-20 21:48:40 -08:00
Leonardo de Moura
98033f298f feat: add support for simple category 2020-01-20 20:55:54 -08:00
Leonardo de Moura
4ff001fa04 feat: add new kind of parser category 2020-01-20 20:06:04 -08:00
Leonardo de Moura
4d57790cc5 fix: add workaround for setting correct LBP for $ in antiquotations 2020-01-20 10:42:58 -08:00
Leonardo de Moura
f20d4aaa83 fix: avoid termParser at mkAntiquot 
@kha `mkAntiquot` is used in all categories. I removed
`termParser (appPrec + 1)` to avoid nasty interactions between
`termParser` and the surrounding category.
This commity ensures the antiquotation prefix is one of the following
forms `$<id>` or `$(<term>)`.
I made the two cases look like term syntax because I didn't want to
change your expander. We should fix this next week.
 2020-01-20 10:19:16 -08:00
Sebastian Ullrich
15bed7c95c chore: support old notation syntax 2020-01-19 18:45:08 +01:00
Leonardo de Moura
58b21fe0c9 feat: mark literals as valid kinds 2020-01-18 19:41:40 -08:00
Leonardo de Moura
98d9022321 chore: cleanup and new test 2020-01-17 18:07:58 -08:00
Sebastian Ullrich
ec8227cfd4 fix: antiquotation kinds :term should not be new tokens 2020-01-17 09:42:34 -08:00
Leonardo de Moura
f2231ebbc0 feat: improve macro command parser 2020-01-17 09:37:36 -08:00
Leonardo de Moura
14ae1166b1 feat: add unboxSingleton trick to sepBy1 2020-01-16 20:57:18 -08:00