Leonardo de Moura
f600c67bb4
chore: update stage0
2020-08-12 10:24:35 -07:00
Leonardo de Moura
d07796293b
feat: elaborate patterns
...
This is just the first step. I still need to convert them into `DepElim.Pattern`.
2020-08-12 10:22:38 -07:00
Leonardo de Moura
31bbc6ee6d
feat: add primitive for registering syntax node kinds that are not associated with any parser
...
@Kha I added this feature to implement match expressions. The idea is
to be able to create a temporary `Syntax` node using an internal kind that has
no parser associated with it. That is, users cannot create them.
However, we can still associate an elaboration function to this kind.
Without this feature, I would have to create some "arbitrary parser"
for representing this temporary `Syntax` node.
2020-08-12 10:21:37 -07:00
Sebastian Ullrich
1972e04302
test: parenthesizer no longer dependent on importing Lean
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
aefe710caf
feat: close the loop
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
6492fb5d80
chore: update stage0
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
f4e59070c4
feat: support interpreting parenthesizers from ParserDescr
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
1f4cc130b7
feat: precompile parenthesizers instead of interpreting them
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
34e496d606
chore: add stage 1.5 (yes, really)
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
05cb45ca9c
refactor: simplify mkCategoryAntiquotParser
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
91de25ab02
chore: update stage0
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
60e548bf7b
feat: add [combinatorParenthesizer] attribute
2020-08-12 09:15:59 -07:00
Sebastian Ullrich
b2714d36ef
fix: String: take/drop characters, not bytes
2020-08-11 18:24:47 -07:00
Leonardo de Moura
f1c7665a93
feat: validate patterns, and collect pattern variables
2020-08-11 18:19:29 -07:00
Leonardo de Moura
60ebecba15
chore: throw error if namedPattern notation is used in a non pattern
2020-08-11 18:17:57 -07:00
Leonardo de Moura
5a09883cc7
chore: add namedPattern
2020-08-11 15:04:09 -07:00
Leonardo de Moura
167b56c3a7
fix: error message
2020-08-11 13:36:42 -07:00
Leonardo de Moura
c66cb01a4b
feat: listLit and arrayLit as macros
...
Motivation: avoid special support at `Match.lean`.
2020-08-11 13:03:36 -07:00
Leonardo de Moura
d0e07d5608
feat: expand h:t discriminants in match-expressions
2020-08-11 10:43:47 -07:00
Leonardo de Moura
193f8236df
feat: elaborate match discriminants
2020-08-11 09:21:54 -07:00
Leonardo de Moura
f646622bfc
feat: add MatchAltView
2020-08-10 17:30:33 -07:00
Leonardo de Moura
dd5c21bf6f
feat: eagerly expand macros occurring in patterns
2020-08-10 17:15:26 -07:00
Leonardo de Moura
61f8b4ef07
feat: add support for maximum recursion depth checks at MacroM
2020-08-10 16:50:12 -07:00
Leonardo de Moura
fe5927927a
feat: elaborate match type
2020-08-10 13:53:08 -07:00
Leonardo de Moura
25fd5d0a9a
fix: ambiguity at match
...
```lean
match x : t with
| ...
```
Two possible intepretations for `x : t`:
1- The discriminant `t` where `x` is the name for the equality proofs `t = ...` in each alternative.
2- The discriminant `x` with a expected type `t` (aka motive) for the match.
This commit resolves the ambiguity by forcing no space before `:` in
the first interpretation.
cc @Kha
2020-08-10 13:47:09 -07:00
Leonardo de Moura
d1d91b3a50
chore: fix test
2020-08-10 11:19:05 -07:00
Leonardo de Moura
0f719d63db
chore: update stage0
2020-08-10 11:16:31 -07:00
Leonardo de Moura
f974521783
fix: missing node
2020-08-10 11:15:44 -07:00
Leonardo de Moura
e59735bde9
chore: fix test
...
@Kha the tests `Reparen.lean` and `Reformat.lean` are still
broken. Could you please take a look?
They broke because I changed the `match` syntax at 3ce794c58
2020-08-10 10:20:57 -07:00
Leonardo de Moura
9bd4acd9c9
chore: update stage0
2020-08-10 10:13:52 -07:00
Leonardo de Moura
3ce794c58a
feat: allow h : annotation on match discriminants
2020-08-10 10:12:24 -07:00
Leonardo de Moura
c8ab63ea75
feat: mark auxiliary eliminators as [inline]
2020-08-10 09:41:55 -07:00
Leonardo de Moura
e301d57b36
chore: fix comment
2020-08-10 08:39:22 -07:00
Leonardo de Moura
43317d5598
fix: nullary minor premises must be thunks
2020-08-08 16:23:50 -07:00
Leonardo de Moura
d2206dcab2
feat: as-patterns x@pattern
2020-08-08 16:12:44 -07:00
Leonardo de Moura
0ca83699d7
fix: array literal support at DepElim
2020-08-08 15:21:35 -07:00
Leonardo de Moura
0fa404ead2
feat: add support for array literals in the pattern matching compiler
2020-08-07 17:13:15 -07:00
Leonardo de Moura
2e3b158e34
chore: hack for testing array literals in patterns
2020-08-07 16:46:15 -07:00
Leonardo de Moura
e1be008516
feat: add caseArraySizes
...
An auxiliary tactic for pattern matching array literals.
2020-08-07 16:04:57 -07:00
Leonardo de Moura
b624fa78d7
fix: another subst issue
2020-08-07 16:04:01 -07:00
Leonardo de Moura
6b18f486d1
feat: add mkLt and mkLe
2020-08-07 14:47:11 -07:00
Leonardo de Moura
3b0ec1b20a
feat: add mkDecideProof
2020-08-07 13:48:37 -07:00
Leonardo de Moura
77e51306c5
fix: missing substitution
2020-08-07 13:37:38 -07:00
Leonardo de Moura
c59fda4c19
feat: add assertExt
2020-08-07 12:06:53 -07:00
Leonardo de Moura
feda5e746f
chore: improve error message
2020-08-07 11:50:08 -07:00
Leonardo de Moura
aefc9a473f
feat: add auxiliary definitions for compiling array literals in pattern matching expressions
2020-08-07 09:23:33 -07:00
Leonardo de Moura
57ac1751cb
feat: expose mkElimCore
...
`mkElimCore` allows caller to pick the motive.
2020-08-07 06:41:47 -07:00
Leonardo de Moura
251f0cc085
chore: minor tests
2020-08-06 17:00:19 -07:00
Leonardo de Moura
aa972878d8
feat: add processValue
2020-08-06 16:34:37 -07:00
Leonardo de Moura
fd9be5e8ae
feat: add caseValues tactic
...
It is an auxiliary tactic for compiling pattern matching.
2020-08-06 15:37:00 -07:00
