Leonardo de Moura
00d46e4a7d
chore: preparing to refactor DepElim
2020-08-14 19:02:20 -07:00
Leonardo de Moura
55d9689a7b
fix: finalizePatternDecls
2020-08-14 13:55:43 -07:00
Leonardo de Moura
c5316d5cf3
fix: missing withMVarContext
2020-08-14 12:52:51 -07:00
Leonardo de Moura
50abd28f6e
feat: generalize "constructor transition"
2020-08-14 12:38:43 -07:00
Leonardo de Moura
e2109ceab6
fix: missing substitution
...
We should include the `majorFVarId -> ctor-application` substitution
in each subgoal.
2020-08-14 12:38:00 -07:00
Leonardo de Moura
b3894200f0
feat: expose constructorApp? and isConstructorApp?
2020-08-14 12:37:34 -07:00
Leonardo de Moura
d85a41a4d7
chore: reduce number of dependencies
...
@Kha Please try to avoid importing `Lean.Meta`, it is huge, and any
change there was forcing a bunch of files to be recompiled since
`Parser.Extension` depends on `Parenthesizer`
2020-08-14 10:59:00 -07:00
Leonardo de Moura
8e81c19162
fix: combine "complete" and constructor transitions
2020-08-14 10:50:48 -07:00
Leonardo de Moura
54f6517ca3
fix: condition for using simple casesOn
2020-08-14 10:50:48 -07:00
Sebastian Ullrich
0df6445be6
fix: relax [builtinParenthesizer] check
2020-08-14 19:05:02 +02:00
Sebastian Ullrich
92162ffb7f
feat: check parenthesizer attribute arguments
2020-08-14 19:05:02 +02:00
Sebastian Ullrich
72310a4aee
fix: parenthesizer: ParserDescr.parsers should not be assumed to be a registered parser, or even one with a kind
2020-08-14 19:05:02 +02:00
Sebastian Ullrich
e9473722b1
feat: elaborate new quotation kinds, make macro_rules elaborator work with them
2020-08-14 17:44:29 +02:00
Sebastian Ullrich
129b60022d
refactor: use distinct syntax kinds for quotations
2020-08-14 17:18:09 +02:00
Sebastian Ullrich
64631609cc
feat: use [categoryParenthesizer] to parenthesize syntax parsers correctly
2020-08-14 14:42:44 +02:00
Sebastian Ullrich
3a28761e86
chore: make sure syntax parsers' names and kinds coincide
2020-08-14 14:33:51 +02:00
Sebastian Ullrich
09c70320ef
feat: add [categoryParenthesizer]
2020-08-14 11:00:18 +02: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
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
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
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
5103040063
chore: fix parameter
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
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
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
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
