Leonardo de Moura
7325dcd630
feat: use do at for-in and unless notations
2020-10-05 09:43:11 -07:00
Leonardo de Moura
9a551d9219
feat: add withForbidden and withoutForbidden parser combinators
2020-10-05 09:36:28 -07:00
Leonardo de Moura
4e7fd4b4bf
chore: add doSeqIndent kind
2020-10-03 08:22:02 -07:00
Leonardo de Moura
a5daaee3ed
chore: do syntax adjustments
2020-10-03 07:33:18 -07:00
Leonardo de Moura
96f5c51a3e
fix: doElem issues
2020-10-02 18:58:43 -07:00
Leonardo de Moura
c40ec0128d
fix: return value is optional
2020-10-02 18:09:42 -07:00
Leonardo de Moura
35e401e915
chore: naming consistency
2020-10-02 15:47:12 -07:00
Leonardo de Moura
40640b85bd
fix: doSeqBracketed parser
...
It was failing to parse
```
def f2 (x : Nat) : IO Nat := do {
let y := 1;
if x > 0 then
y := y + 1;
IO.println y
}
```
cc @Kha
2020-10-02 15:05:22 -07:00
Leonardo de Moura
379e34a910
feat: do reassignment parsers
2020-10-02 13:16:55 -07:00
Leonardo de Moura
6db45891e2
feat: add typeOf! and ensureTypeOf! parsers
2020-10-01 14:33:04 -07:00
Leonardo de Moura
4e72530ce7
chore: let rec in do blocks
2020-10-01 10:40:11 -07:00
Leonardo de Moura
75cb42d8be
chore: improve try parser
2020-09-30 07:12:04 -07:00
Leonardo de Moura
0911b9bc80
feat: add missing features to do notation parser
2020-09-30 06:51:25 -07:00
Leonardo de Moura
e1ad5a948b
feat: add focus tactic parser
2020-09-28 17:11:00 -07:00
Leonardo de Moura
e10edde5cd
feat: optional ; in terms
2020-09-28 17:10:59 -07:00
Leonardo de Moura
d4c1432574
fix: tacticSeqBracketed
2020-09-28 17:10:59 -07:00
Leonardo de Moura
2755972447
fix: missing checkColGt and tests
2020-09-28 17:10:59 -07:00
Leonardo de Moura
f45fa34cba
feat: optional ; at tacticSeq1Indented
2020-09-28 17:10:59 -07:00
Leonardo de Moura
7f9013e496
fix: seq1Unbox
2020-09-28 17:10:59 -07:00
Leonardo de Moura
85d8c4fa85
chore: add proper kind for tacticSeq1Indented
2020-09-28 17:10:59 -07:00
Leonardo de Moura
aa410283c6
fix: we don't want antiquotation for seq1
2020-09-28 17:10:59 -07:00
Leonardo de Moura
cb55ffae94
chore: add new tactic syntax kind
2020-09-28 17:10:58 -07:00
Leonardo de Moura
861fd11a57
chore: add tacticSeq node
...
We use `$tac:tacticSeq` in many places, and we want them to match
the bracketed and indented cases.
2020-09-28 17:10:58 -07:00
Leonardo de Moura
6f211d3449
chore: adjust tactic parser
2020-09-28 17:10:57 -07:00
Leonardo de Moura
93090baa82
chore: cleanup tactic syntax
2020-09-28 17:10:57 -07:00
Leonardo de Moura
96a0fb41be
feat: optional ; in do notation
2020-09-28 17:10:57 -07:00
Leonardo de Moura
08d54b6043
feat: add checkColGt at app
...
@Kha Only one example broke :)
2020-09-28 17:10:57 -07:00
Leonardo de Moura
1fcdbaf223
feat: add withoutPosition combinator
2020-09-28 17:10:57 -07:00
Leonardo de Moura
6ddec22763
refactor: simplify withPosition combinator
...
Add `checkColGt`
2020-09-28 17:10:56 -07:00
Leonardo de Moura
39f8fd8eb9
fix: trailing ';' at end of input
2020-09-27 16:58:23 -07:00
Leonardo de Moura
453ce9b3b8
feat: add eoi parser
2020-09-27 16:54:19 -07:00
Leonardo de Moura
7dcd011be0
chore: improve notFollowedBy at doExpr
...
cc @Kha
2020-09-27 06:59:43 -07:00
Leonardo de Moura
2d4b7e7952
feat: add doMatch parser
2020-09-27 06:29:21 -07:00
Leonardo de Moura
8f27848d82
chore: preparing for "reassignment" notation
2020-09-26 18:16:35 -07:00
Leonardo de Moura
5fa8d9105e
feat: add if and for for do blocks
2020-09-26 18:03:53 -07:00
Leonardo de Moura
0275d23ad7
fix: ignore $ at notFollowedByCategoryToken when inside quotations
2020-09-26 17:57:26 -07:00
Leonardo de Moura
ee4dc452ac
chore: remove leftover
2020-09-26 16:10:29 -07:00
Leonardo de Moura
6892a957d6
feat: trailing ; in indented "do" sequences
...
cc @Kha
2020-09-26 16:08:30 -07:00
Leonardo de Moura
3d6cc2de08
feat: add notFollowedByCategoryToken parser
2020-09-26 15:53:23 -07:00
Leonardo de Moura
3f4499be08
feat: allow trailing ; at doSeqBracketed
2020-09-26 14:20:47 -07:00
Leonardo de Moura
e31fd665f0
feat: add checkLineLe parser
2020-09-26 14:03:28 -07:00
Leonardo de Moura
13ded3f964
chore: use doElem category
2020-09-26 12:51:24 -07:00
Leonardo de Moura
a1579f3123
fix: notFollowedBy info
2020-09-26 12:33:11 -07:00
Leonardo de Moura
2d8506b7c6
feat: add doElem parser category
2020-09-26 06:18:44 -07:00
Leonardo de Moura
dc9626ceab
feat: try to improve weird error message
...
@Kha Before this commit, we were producing the error "expected command" at the `let` token
```lean
check id let x := 1; x
```
The new error is "expected command, but found term; this error may be
due to parsing precedence levels, consider parenthesizing the term".
The example above looks artificial, but it will happen all the time as
users start to define their own notation.
2020-09-21 18:29:01 -07:00
Leonardo de Moura
b0564a32b9
feat: add AttrM
...
We are going to use `AttrM` to implement solution 2 described at https://github.com/leanprover/lean4/issues/175
2020-09-21 16:44:20 -07:00
Leonardo de Moura
cab56d1e1b
chore: do not invoke the hooks from addImported
...
@Kha I am working on issue
https://github.com/leanprover/lean4/issues/175
I am using solution 2 described there. The hooks will be at `AttrM`
instead of `CoreM`.
AFAICT code deleted by this commit is not necessary.
2020-09-21 16:28:07 -07:00
Sebastian Ullrich
f693e910b1
fix: skip minimum amount of tokens during parser recovery
...
Fixes #186
2020-09-21 11:37:50 +02:00
Leonardo de Moura
9eb978946c
chore: add quotedCharCoreFn
2020-09-20 17:05:47 -07:00
Leonardo de Moura
03a361edf4
feat: add initialize command parser
2020-09-20 13:42:50 -07:00
