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

171 commits

Author SHA1 Message Date
Leonardo de Moura
87381e3329 feat: add support for parser priorities in the syntax command 
@Kha Parser priorities are working :)
 2020-09-19 18:47:08 -07:00
Leonardo de Moura
f0ab743ad0 chore: remove temporary workaround 2020-09-19 18:00:45 -07:00
Leonardo de Moura
fe2d3be821 feat: parser priorities 2020-09-19 17:55:17 -07:00
Leonardo de Moura
f679b7d803 feat: add notFollowedBy to syntax 2020-09-19 15:43:44 -07:00
Leonardo de Moura
ee6d723554 feat: add stx.quot 2020-09-19 14:40:17 -07:00
Leonardo de Moura
f876177f26 feat: expand macros in syntax declaration 2020-09-19 14:39:49 -07:00
Leonardo de Moura
17d4117637 chore: remove temporary hacks 2020-09-19 14:21:38 -07:00
Leonardo de Moura
71de0c8eb9 chore: rename category syntax to stx 
Reason: `syntax` is a keywork. So, we can't write `macro "boo" x:syntax`
 2020-09-19 14:11:35 -07:00
Leonardo de Moura
caa624c936 chore: cleanup 2020-09-19 09:24:50 -07:00
Sebastian Ullrich
68568e78d3 feat: formatter: use hard space after opening structure instance brace 2020-09-18 13:15:40 -07:00
Sebastian Ullrich
95007171a8 feat: formatter: group+indent binders and structure instance fields 2020-09-18 13:15:40 -07:00
Leonardo de Moura
8142548237 fix: missing toggleInsideQuot 
cc @Kha
 2020-09-17 13:23:52 -07:00
Leonardo de Moura
d1c3ab3797 feat: many1Unbox and nodeSepBy1Unbox parser combinators 
@Kha I removed the dummy parenthesizer/formatter for `withResultOf`,
and add proper ones for `many1Unbox` and `nodeSepBy1Unbox`.
 2020-09-17 13:17:46 -07:00
Leonardo de Moura
2dafdec000 feat: use withResultOf combinator instead of unboxSingleton parameter 2020-09-17 12:12:12 -07:00
Leonardo de Moura
4265348bed feat: add withResultOf parser combinator and unboxSingleton 2020-09-17 12:03:16 -07:00
Leonardo de Moura
56f8103e66 chore: improve error message for rw [] 2020-09-17 10:55:51 -07:00
Leonardo de Moura
9d1f2b644f chore: rwRuleSeq ; => , 2020-09-17 08:15:58 -07:00
Sebastian Ullrich
0b9e46eee5 chore: universe-+ spacing 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
fad4660135 feat: pretty print space between binders 2020-09-17 08:12:28 -07:00
Sebastian Ullrich
c4761974b7 fix: runParserCategory: ensure EOI 2020-09-17 08:12:28 -07:00
Leonardo de Moura
a2e8a41f33 feat: rewrite tactic parser 2020-09-16 17:43:44 -07:00
Leonardo de Moura
c620a2a59d feat: refine parser location 2020-09-16 17:28:09 -07:00
Leonardo de Moura
0abca5475f refactor: move ppExpr to IO 
@Kha I am also tracking `currNamespace` and `openDecls`.

BTW, I also tried an experiment where I added `currNamespace` and
`openDecls` to `Meta.Context`, but it looked weird. This information
is only needed in the elaborator and pretty printer.
The `PPContext` object should contain everything you need. You
can put `currNamespace` and `openDecls` in the `Delaborator.Context`.
 2020-09-15 18:48:21 -07:00
Leonardo de Moura
3fa7e61b26 feat: add done and admit syntax 2020-09-15 10:46:40 -07:00
Leonardo de Moura
e66f6cdd6c feat: using indentation 2020-09-14 16:12:23 -07:00
Leonardo de Moura
c49ccda46a feat: add antiquotation for indentedNonEmptySeq 2020-09-14 14:57:38 -07:00
Leonardo de Moura
05e6a779ba fix: can't use maxPrec at by 
If `by` uses `maxPrec`, then `have A by B ...` is parsed as
`have (A by B) ...` :(

cc @Kha
 2020-09-14 14:57:14 -07:00
Leonardo de Moura
f95675dc22 feat: add have-by and show-by syntax 2020-09-14 14:25:35 -07:00
Leonardo de Moura
fc4ab139b5 feat: indented by 
@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
  have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
  Eq.trans this (by assumption)
```
 2020-09-14 14:20:02 -07:00
Leonardo de Moura
4c6a589e6c feat: indented do blocks 
@Kha it is soooooo much nicer :)
 2020-09-14 13:44:51 -07:00
Leonardo de Moura
3c2044f06b chore: add coercion for new frontend 2020-09-13 10:12:25 -07:00
Leonardo de Moura
151012cb39 feat: remove emptyc elaboration hack 
@Kha I removed the hack. We know get a nice error message.
 2020-09-11 14:41:44 -07:00
Leonardo de Moura
ba4fdce508 feat: expand helper macros 2020-09-10 14:25:07 -07:00
Leonardo de Moura
d77dc5efb8 feat: add helper syntax 2020-09-10 13:31:45 -07:00
Leonardo de Moura
232fe8cadd doc: document parser trick 2020-09-10 11:20:09 -07:00
Leonardo de Moura
20152c1192 chore: change by precedence 
@Kha it now uses the same precedence of `fun`.
The main motivation is to allow us to write `@by { ... }` instead of
`@(by { ... })`.

BTW, I am considering disabling implicit lambdas for `by ...` expressions.
It is automatically "intro"ducing the implicit variables without
giving an opportunity for users to pick their names.
 2020-09-10 11:17:42 -07:00
Leonardo de Moura
b24d1c2d90 feat: add .. syntax for pattern applications 2020-09-09 09:55:29 -07:00
Leonardo de Moura
cf944e32cf chore: add back support for Lean3 mixfix/reserve syntax 
We have tests that rely on them :(
 2020-09-07 16:40:12 -07:00
Leonardo de Moura
804ebcec16 feat: adjust mixfix syntax 2020-09-07 15:55:02 -07:00
Leonardo de Moura
7dc1b461fa chore: give a proper node to matchAlts 2020-09-04 18:42:09 -07:00
Leonardo de Moura
70c42456b9 feat: expand intro+matchAlts macro 2020-09-04 18:22:56 -07:00
Leonardo de Moura
a88b2be72a feat: add intro + funMatchAlts syntax 2020-09-04 16:32:53 -07:00
Leonardo de Moura
ef64e1c25a feat: fun+match macro 
Example:
```
fun
  | 0 => true
  | _ => false
```
 2020-09-04 16:23:01 -07:00
Leonardo de Moura
0883f96da0 chore: remove optional partial from 'let rec' 
It will inherit the parent declaration annotation.
 2020-09-02 17:02:22 -07:00
Leonardo de Moura
bda85f287c feat: in trailing command 2020-09-02 09:52:54 -07:00
Leonardo de Moura
095e07d52d chore: letrec => let rec 
cc @Kha
 2020-09-01 13:27:41 -07:00
Leonardo de Moura
b192293b8a feat: allow arbitrary commands (except end) in a mutual block 
This is useful, for example, for having a mutual command with macros
that expand into definitions.
 2020-08-31 15:37:41 -07:00
Leonardo de Moura
2563d03ae2 feat: add notFollowedBy 2020-08-31 15:37:41 -07:00
Sebastian Ullrich
75b2dc1baf refactor: simplify ppModule using new module parser 2020-08-31 15:44:58 +02:00
Sebastian Ullrich
2418d851fc feat: declarative module parser 
/cc @leodemoura
 2020-08-31 14:45:21 +02:00