Leonardo de Moura
cd4ec6313e
chore: try macros first
2020-02-01 00:53:49 -08:00
Leonardo de Moura
ca919c2021
refactor: move instance to LeanInit
2020-02-01 00:52:52 -08:00
Leonardo de Moura
3dfc93550a
feat: add liftMacroM
...
We implement `expandDoElems` using `MacroM`.
2020-02-01 00:26:42 -08:00
Leonardo de Moura
b332d5e74d
feat: add proper withFreshMacroScope to MacroM
...
This is useful, for example, for users that want to write recursive
procedural macros.
2020-02-01 00:12:13 -08:00
Leonardo de Moura
d8c738bef8
feat: elaborate do notation
2020-01-31 20:11:06 -08:00
Leonardo de Moura
4b0284778c
feat: expand ^(...) notation
2020-01-31 18:21:28 -08:00
Leonardo de Moura
34a6029a28
feat: expand do elements
2020-01-31 17:39:32 -08:00
Leonardo de Moura
adc8b7f447
chore: missing attribute
2020-01-31 17:39:20 -08:00
Leonardo de Moura
9a505a0900
chore: name instance
2020-01-31 17:39:00 -08:00
Leonardo de Moura
398aa32f4d
refactor: move elabDo to its own file
2020-01-31 14:40:58 -08:00
Leonardo de Moura
b604eb997a
feat: add lift notation
...
@Kha The motivation is to avoid conflicts with the power operator.
I am assuming users will write `2^n` and `2^(n+1)`. So, we can't use
the space sensitiviy trick nor the token `^(`. So, I am using `(^` for
now.
2020-01-31 14:37:39 -08:00
Leonardo de Moura
61f5bdf09b
feat: MutQuot basic definition
2020-01-31 10:56:15 -08:00
Leonardo de Moura
3d0bfcd36a
fix: assertion violation
2020-01-31 08:25:59 -08:00
Leonardo de Moura
21618361b7
refactor: remove ParserKind
2020-01-30 20:56:46 -08:00
Leonardo de Moura
6b1e64d7ea
chore: prepare for refactoring
2020-01-30 20:41:10 -08:00
Leonardo de Moura
54bdddb98f
fix: toParserDescrAux
2020-01-30 20:38:14 -08:00
Leonardo de Moura
31ebccea58
chore: remove ParserDescr.pushLeading
2020-01-30 19:04:07 -08:00
Leonardo de Moura
410d295429
refactor: remove unnecessary pushLeading, add ParserDescr.trailingNode
2020-01-30 18:32:28 -08:00
Leonardo de Moura
72ff3da6cd
refactor: preparing to remove ParserKind
2020-01-30 17:31:53 -08:00
Leonardo de Moura
3f32d9eb0b
fix: closes #111
2020-01-30 14:09:47 -08:00
Leonardo de Moura
50327205c9
chore: erase macro scopes
...
cc @Kha
2020-01-30 12:22:27 -08:00
Leonardo de Moura
2f0ac98b51
feat: extend scope of cdot notation
2020-01-30 11:42:37 -08:00
Leonardo de Moura
fe6502493b
chore: use macros instead of elab
...
@Kha The motivation is to avoid code duplication. The `match`
elaborator will need a `elabPattern`. We can use the macros for
`elabTerm` and `elabPattern`.
2020-01-30 10:58:23 -08:00
Leonardo de Moura
5d3db23d4b
chore: remove hack
2020-01-30 10:10:46 -08:00
Leonardo de Moura
38cfa1dcb6
feat: add elabMatch skeleton
2020-01-30 10:02:15 -08:00
Leonardo de Moura
018891b168
fix: subgoal order at hasMonadLiftTTrans
2020-01-30 09:58:21 -08:00
Leonardo de Moura
d11c2321c8
chore: precedence of nested parsers
2020-01-30 08:58:49 -08:00
Sebastian Ullrich
470e1623de
chore: hide "expected '$'"
2020-01-30 08:56:14 -08:00
Sebastian Ullrich
b818994bbe
fix: do not swallow errors from parser interpreter
...
@leodemoura I think we should only use `throwUnsupportedSyntax` in the
top level `match_syntax` of a transformer/elaborator
2020-01-30 08:56:14 -08:00
Sebastian Ullrich
9160c561c1
feat: postfix syntax for optional syntax parser
2020-01-30 08:56:14 -08:00
Leonardo de Moura
0c4030137f
feat: simplify Coe again
...
Users may add the expensive instances if they want.
The goal is to make sure the default configuration is solid, and
covers all examples we really want to support.
cc @kha @dselsam
2020-01-29 22:08:42 -08:00
Leonardo de Moura
812c47d463
feat: simplify CoeFun and CoeSort
...
The main issue is nontermination for problems that do not have
solution. When using dependent coercions, we keep creating goals of
the form `CoeSort ... (coe (coe (coe ...))) ...`. Same for `CoeFun`.
I am considering simplifying it even further, and making sure
`CoeDep` can be used at most once in a sequence of coercions `CoeTC`.
Another option is to use a very small amount of fuel to
guarantee termination when solving coercion TC problems.
cc @Kha @dselsam
2020-01-29 21:56:26 -08:00
Leonardo de Moura
755e22c0ef
doc: document propagateExpectedType
2020-01-29 20:49:18 -08:00
Leonardo de Moura
f29a13323a
fix: forget to update
2020-01-29 20:08:03 -08:00
Leonardo de Moura
6793559896
fix: missing ensureHasType at elabLetDeclAux
2020-01-29 19:20:55 -08:00
Leonardo de Moura
8c0cc7b33b
fix: "function expected" error message
2020-01-29 19:17:44 -08:00
Leonardo de Moura
a656096c4b
feat: expected type propagation
2020-01-29 19:00:56 -08:00
Leonardo de Moura
dc567708a6
fix: prevent macroStack from appearing more than once in error messages
2020-01-29 18:09:41 -08:00
Leonardo de Moura
5c6e24be18
chore: better position for this kind of error
2020-01-29 16:30:02 -08:00
Leonardo de Moura
b00c04c491
fix: missing ensureHasType
2020-01-29 16:29:48 -08:00
Leonardo de Moura
29320145b9
fix: missing withMacroExpansion
2020-01-29 15:51:58 -08:00
Leonardo de Moura
81e363b13e
feat: add withPtrEq and withPtrAddr
2020-01-29 04:31:10 -08:00
Leonardo de Moura
db8eaad410
fix: propagate only
2020-01-29 03:50:21 -08:00
Leonardo de Moura
1eb6abdc15
chore: use CoeT
2020-01-29 03:49:02 -08:00
Leonardo de Moura
c048a3f573
fix: Level.normalize
2020-01-29 03:38:35 -08:00
Leonardo de Moura
9bc07254a1
feat: add support for CoeSort
2020-01-29 02:34:35 -08:00
Leonardo de Moura
6a046a11c2
chore: remove coeSortBool
...
It is interacting with new `Coe`.
We can add it back at `Coe.lean` after we remove `HasCoe.lean`
2020-01-28 19:07:02 -08:00
Leonardo de Moura
c33cd11be1
feat: add CoeHead and CoeTail to minimize nontermination
...
The adventure continues.
cc @Kha @dselsam
2020-01-28 18:20:58 -08:00
Leonardo de Moura
55bb0805b2
feat: handle attribute inferTCGoalsLR
2020-01-28 18:01:35 -08:00
Leonardo de Moura
f2a32e5985
feat: tag coeFunTrans and coeSortTrans with [inferTCGoalsLR]
2020-01-28 17:19:21 -08:00
