Sebastian Ullrich
d66503f7a8
chore: update stage0
2020-08-14 11:03:35 +02:00
Sebastian Ullrich
09c70320ef
feat: add [categoryParenthesizer]
2020-08-14 11:00:18 +02:00
Leonardo de Moura
17770ee479
chore: update stage0
2020-08-13 16:56:01 -07:00
Leonardo de Moura
94689ca91f
chore: fix test
2020-08-13 16:55:03 -07:00
Leonardo de Moura
69ee44d68e
feat: match-expressions showing signs of life
2020-08-13 16:51:31 -07:00
Leonardo de Moura
0a54391eba
chore: add helper
2020-08-13 16:20:25 -07:00
Leonardo de Moura
2ba4f02de9
chore: move code to testing part
2020-08-13 16:01:52 -07:00
Leonardo de Moura
24025b96c5
feat: elaborate equation RHS
2020-08-13 15:19:40 -07:00
Leonardo de Moura
f31d16496d
feat: generate AltLHS
2020-08-13 15:05:38 -07:00
Leonardo de Moura
a670de93cd
chore: fix test
2020-08-13 14:59:37 -07:00
Leonardo de Moura
8b0a100e21
chore: field name
2020-08-13 14:59:28 -07:00
Leonardo de Moura
4cab743932
feat: mark implicit fields as inaccessible
2020-08-13 14:56:22 -07:00
Leonardo de Moura
81ae6a734b
feat: mark List.toArray with [matchPattern]
2020-08-13 14:25:47 -07:00
Leonardo de Moura
9deab00941
feat: add toDepElimPattern
2020-08-13 14:20:56 -07:00
Leonardo de Moura
aaf5034ba2
chore: add helper
2020-08-13 14:14:21 -07:00
Leonardo de Moura
08f1c2310b
chore: enforce naming convention
2020-08-13 14:09:00 -07:00
Leonardo de Moura
5b1b11ffe0
feat: add isCharLit
2020-08-13 13:15:15 -07:00
Leonardo de Moura
145a3dddca
chore: remove ref from patterns
...
We don't use them to report errors. We only need `ref` at `Alt`
2020-08-13 12:31:32 -07:00
Leonardo de Moura
a6b22728ca
chore: reduce stack space requirements in test
2020-08-13 12:13:38 -07:00
Leonardo de Moura
71be882039
chore: update stage0
2020-08-13 10:42:52 -07:00
Leonardo de Moura
5ba9aad7a3
refactor: eliminate ref plumbing
2020-08-13 10:37:53 -07:00
Sebastian Ullrich
46f5670ba3
chore: Lean.Parser.Parser ~> Lean.Parser.Basic
2020-08-13 18:44:13 +02:00
Sebastian Ullrich
a0f825f67f
refactor: move Lean.PrettyPrinter.Parenthesizer in between Lean.Parser.Parser and Lean.Parser.Extension
2020-08-13 18:44:13 +02:00
Sebastian Ullrich
f7e004b44a
refactor: split Lean.Parser.Parser
2020-08-13 18:44:13 +02:00
Leonardo de Moura
6c234daad7
chore: MonadExceptCore => MonadExceptOf
2020-08-13 09:28:23 -07:00
Wojciech Nawrocki
9c7d91c67f
fix: don't normalize line endings but still diff
2020-08-13 09:21:35 -07:00
Wojciech Nawrocki
55655869b7
feat: default to binary file mode on Windows
2020-08-13 09:21:35 -07:00
Leonardo de Moura
5103040063
chore: fix parameter
2020-08-13 09:19:26 -07:00
Leonardo de Moura
c24ff8fe16
chore: update stage0
2020-08-13 09:19:26 -07:00
Leonardo de Moura
3ad0871dd4
chore: increase class.instance_max_depth
2020-08-13 09:19:26 -07:00
Leonardo de Moura
d7add53229
feat: add MonadExceptCore
2020-08-13 09:19:26 -07:00
Sebastian Ullrich
baadfca817
fix: commit missing file...
2020-08-13 17:39:43 +02:00
Sebastian Ullrich
541d77da8b
refactor: custom implementation for [combinatorParenthesizer], revert KeyedDeclsAttribute changes
...
/cc @leodemoura
2020-08-13 15:32:16 +02:00
Sebastian Ullrich
61a706d8cd
chore: adjust parenthesizer docs
...
/cc @leodemoura
2020-08-13 12:27:25 +02:00
Leonardo de Moura
02b81e263e
chore: update stage0
2020-08-12 20:24:19 -07:00
Leonardo de Moura
bd7a7ed623
refactor: reduce ref plumbing
...
TODO: reduce `ref` plumbing at `CommandElabM`
2020-08-12 20:23:02 -07:00
Leonardo de Moura
e2df2d5a7c
fix: metavariable type scope
2020-08-12 17:43:55 -07:00
Leonardo de Moura
a23b640cbc
fix: equality orientation
2020-08-12 17:15:07 -07:00
Leonardo de Moura
f40811e0c1
feat: convert patternVars into LocalDecl
2020-08-12 17:13:25 -07:00
Leonardo de Moura
f924b481c2
chore: simplify mkElim interface
2020-08-12 16:34:43 -07:00
Leonardo de Moura
2e3587872c
feat: add withSynthesize
2020-08-12 16:18:22 -07:00
Leonardo de Moura
f955552d5b
feat: elaborate .(t)
2020-08-12 14:07:43 -07:00
Leonardo de Moura
fcf4df2f5c
fix: do not use named holes for representing _ in patterns
2020-08-12 13:58:27 -07:00
Leonardo de Moura
174acc82e4
chore: update stage0
2020-08-12 10:45:46 -07:00
Leonardo de Moura
f487b88024
feat: register auxiliary Syntax node kind
2020-08-12 10:45:07 -07:00
Leonardo de Moura
0e0754346b
chore: fix method name
2020-08-12 10:43:26 -07:00
Leonardo de Moura
57533726f6
feat: add mkFreshExprMVarWithId
2020-08-12 10:35:38 -07:00
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
