Leonardo de Moura
56e2ff81b8
chore: ensure all term parsers have precedence >= min
2020-12-22 14:10:07 -08:00
Leonardo de Moura
69d83ecb86
chore: make sure term and tactic parsers have disjoint infix operators
2020-12-22 14:10:07 -08:00
Leonardo de Moura
7b813622c6
chore: increase precedence of |>, <|, $ parsers
...
@Kha Now, all parsers defined by `Init/Std/Lean` packages have
precedence >= `min` and <= `max`.
The only exception is `<|>` since it is an infix operator sharead with
the tactic DSL.
BTW, the meaning of `f $ a <|> b` changed with this commit.
It was `f (a <|> b)`, and now is `(f a) <|> b`. The problem is that
the precedence of the `$` parser is now greater than the `<|>` parser.
I will try another experiment where I make sure we do not "reuse"
term infix operators in the tactic DSL.
2020-12-22 14:10:07 -08:00
Leonardo de Moura
cc34733e52
fix: update builtin precedences for |>. and macroDollarArg
2020-12-22 14:10:06 -08:00
Leonardo de Moura
18aee9de30
fix: precedence issues at tactic DSL
2020-12-22 14:10:06 -08:00
Leonardo de Moura
298bdfdcde
fix: focus behavior
2020-12-22 14:10:06 -08:00
Leonardo de Moura
289ed6485d
feat: eval allGoals
2020-12-22 09:52:54 -08:00
Leonardo de Moura
f638269a71
fix: name resolution at syntax command
...
This commit also cleans up `toParserDescr`+`toParserDescrAux`.
2020-12-22 08:40:00 -08:00
Sebastian Ullrich
93518d4e42
perf: let*-bind syntax match RHSs before duplicating them
2020-12-22 17:25:46 +01:00
Leonardo de Moura
b254aafea0
chore: remove workaround
2020-12-22 07:19:33 -08:00
Leonardo de Moura
7d1e493531
chore: reactivate tactic match and introMatch
2020-12-22 07:15:47 -08:00
Leonardo de Moura
f34bf82e0f
chore: move tactic parsers introMatch and match to Lean/Parser/Tactic
2020-12-22 07:11:06 -08:00
Leonardo de Moura
7fa1430a60
chore: add evalMatchTemp
2020-12-22 06:56:58 -08:00
Leonardo de Moura
a05ca020f4
chore: prepare to move tactic match parser back to Lean/Parser/Tactic
2020-12-22 06:52:41 -08:00
Sebastian Ullrich
1c31240ebb
feat: token antiquotations in macro
2020-12-22 13:11:04 +01:00
Sebastian Ullrich
07c7638fd7
feat: token source info antiquotations tk%$id
...
/cc @leodemoura
2020-12-22 13:11:04 +01:00
Leonardo de Moura
43255a4af3
feat: local and scoped macros
2020-12-21 17:08:25 -08:00
Leonardo de Moura
0642a62848
chore: prepare to add scoped macro and elab commands
2020-12-21 16:50:29 -08:00
Leonardo de Moura
836fd46d90
feat: add OfNat instance for Fin
2020-12-21 16:38:53 -08:00
Leonardo de Moura
227b26636c
chore: increase default depth to 32
2020-12-21 15:03:27 -08:00
Leonardo de Moura
0083e1996a
fix: scoped tokens
...
Tokens introduced by scoped (local) parsers should be scoped (local).
2020-12-21 13:11:09 -08:00
Leonardo de Moura
7723953188
chore: use instance (priority := <prio>)
2020-12-21 10:17:54 -08:00
Leonardo de Moura
4fc06bfcca
feat: add optional (priority := <prio>) to instance command
2020-12-21 10:02:12 -08:00
Leonardo de Moura
c43e77d1a5
chore: fix Notation.lean
2020-12-21 09:47:11 -08:00
Leonardo de Moura
43284cc5fa
feat: improve notation for setting parser names and priorities
2020-12-21 09:11:12 -08:00
Sebastian Ullrich
cf73233dd2
refactor: use quotations & implicit token positions from getRef to clean up a bit
2020-12-21 17:32:36 +01:00
Leonardo de Moura
c524bcf2d3
feat: improve universe level pretty printer
2020-12-21 07:34:48 -08:00
Leonardo de Moura
83ae3b7aaa
fix: bug introduced when moving to new frontend
2020-12-21 07:34:48 -08:00
Sebastian Ullrich
3e77c7cdef
fix: error position
2020-12-21 16:25:01 +01:00
Sebastian Ullrich
756d7643f0
chore: rename syntaxMaxDepth option for consistency and discoverability
...
/cc @leodemoura
2020-12-21 16:25:01 +01:00
Sebastian Ullrich
af89c89c4e
feat: option pp.raw.showInfo
2020-12-21 16:25:01 +01:00
Sebastian Ullrich
cf7f60b470
feat: attach getRef position to symbols from quotations
...
/cc @leodemoura
2020-12-21 16:24:39 +01:00
Sebastian Ullrich
c54f9dd8c8
feat: "slice" patterns [$x, $y, $zs,*, $w] in syntax match
...
/cc @leodemoura
2020-12-21 15:29:46 +01:00
Leonardo de Moura
e8e991064e
chore: remove workaround at expandDoIf?
2020-12-20 17:53:19 -08:00
Leonardo de Moura
340cade575
fix: bug at specialize.cpp
2020-12-20 17:48:46 -08:00
Leonardo de Moura
76eb163a0f
chore: use new pretty printer at specialize trace messages
2020-12-20 16:44:55 -08:00
Leonardo de Moura
2da48e8739
feat: use new pretty printer to trace all compiler steps
2020-12-20 16:44:40 -08:00
Sebastian Ullrich
bc3e9ce961
feat: if let pat ← ...
2020-12-20 23:58:29 +01:00
Sebastian Ullrich
90f747e346
fix: don't change antiquotations semantics in do if
2020-12-20 17:51:37 +01:00
Sebastian Ullrich
a56fd6a8c0
chore: Quotation: minor comments fixes
2020-12-20 16:46:03 +01:00
Sebastian Ullrich
eeb0cad29e
feat: if let
...
/cc @leodemoura
2020-12-20 16:46:03 +01:00
Sebastian Ullrich
fdbec9101f
fix: pattern reordering in syntax match
2020-12-20 13:52:25 +01:00
Leonardo de Moura
91f0e29285
feat: parallel for
2020-12-19 20:01:04 -08:00
Leonardo de Moura
0911936502
feat: parallel for notation
2020-12-19 19:26:53 -08:00
Leonardo de Moura
339a4cf740
chore: remove defaultInstance for ToString
2020-12-19 19:10:42 -08:00
Leonardo de Moura
074259201e
feat: add helper classes for implementing parallel for
...
It is based on an approach suggested by Andrew Kent, and refined by
Sebastian Ullrich.
TODO: expand the the parallel `for`s at `Do.lean`.
2020-12-19 14:15:47 -08:00
Sebastian Ullrich
efc2b79aba
feat: as patterns in syntax match
...
@leodemoura no problem using the new architecture :)
2020-12-19 22:03:37 +01:00
Sebastian Ullrich
5b06e1011f
fix: completely refactor syntax match handling, introduce "undecided" patterns to resolve complex cases
2020-12-19 22:03:37 +01:00
Leonardo de Moura
bbcd2247f2
feat: extend valid set of valid auto bound names
...
@Kha The motivation was Andrew's example :)
Users often use `u₁`, `u1`, `u₂`, ... to name universe variables.
2020-12-19 12:36:19 -08:00
Leonardo de Moura
498dae8fab
chore: add trace messages
2020-12-19 12:26:37 -08:00
