Leonardo de Moura
c0803d989f
chore: update stage0
2020-01-08 14:25:56 -08:00
Leonardo de Moura
c4ad3a2390
refactor: ParserContextCore and ParserContext
2020-01-08 14:20:53 -08:00
Leonardo de Moura
8484aa08f3
feat: decodeCharLit
2020-01-08 10:50:47 -08:00
Leonardo de Moura
f2958f1f6c
feat: decodeStrLit
2020-01-08 10:47:33 -08:00
Leonardo de Moura
7c7e76defb
fix: missing repr
2020-01-08 08:32:14 -08:00
Leonardo de Moura
0137500c83
fix: missing decodeStrLit and decodeCharLit
...
They are just placeholders.
2020-01-08 08:28:22 -08:00
Leonardo de Moura
b774ed1505
fix: update tokens
2020-01-08 08:28:15 -08:00
Leonardo de Moura
0049cb361e
chore: remove unnecessary instantiateMVars
...
The `MessageData` formatter invokes `instantiateMVars`.
2020-01-07 17:26:28 -08:00
Leonardo de Moura
187897d90d
fix: bug at expandOptType
2020-01-07 17:14:49 -08:00
Leonardo de Moura
abbb9c4848
chore: update stage0
2020-01-07 16:56:53 -08:00
Leonardo de Moura
3de7d6d5c3
fix: remove mvarTypeNotWellFormedInSmallerLCtx
...
We use `check` recursively instead of `isWellFormed`.
@kha This was the last bug for the repro
```
```
This example works now, but I am sure there are many other bugs.
2020-01-07 16:56:10 -08:00
Leonardo de Moura
2ce2610c0a
feat: add compileDecl
...
cc @kha
2020-01-07 16:38:41 -08:00
Leonardo de Moura
69be2148d6
chore: remove buggy optimization
2020-01-07 16:29:59 -08:00
Leonardo de Moura
4b08b1eea3
fix: ?m t =?= ?n
2020-01-07 16:05:17 -08:00
Leonardo de Moura
7caf5051c7
fix: use isDefEq approximations
...
We do the same in the Lean3 elaborator
2020-01-07 13:48:40 -08:00
Leonardo de Moura
de88427fc1
fix: use given type as expectedType
2020-01-07 13:48:23 -08:00
Leonardo de Moura
a99523b4b3
feat: add set_option ppOld false option for disabling ppOld
...
The old pretty printer often sucks.
2020-01-07 13:20:54 -08:00
Leonardo de Moura
d059b7be76
chore: add stuck trace message
2020-01-07 12:56:15 -08:00
Leonardo de Moura
a17ae70be7
feat: elaborate set_option
2020-01-07 12:08:00 -08:00
Leonardo de Moura
62bdbba78d
chore: missing instantiateMVars
2020-01-07 11:34:21 -08:00
Leonardo de Moura
8e7c719ee8
chore: Pi => forall
2020-01-07 11:15:40 -08:00
Leonardo de Moura
070682c4e9
feat: add addContext
2020-01-07 11:04:52 -08:00
Leonardo de Moura
091cc48901
feat: expose old pretty printer in Lean
2020-01-07 10:29:10 -08:00
Leonardo de Moura
477d53f2dd
fix: position information
2020-01-06 21:07:41 -08:00
Leonardo de Moura
4b37c5ad04
test: add new_frontend command test
2020-01-06 21:02:25 -08:00
Leonardo de Moura
e0ae6068d4
chore: set end_pos
2020-01-06 21:00:52 -08:00
Leonardo de Moura
0b2c820e0f
fix: missing levelMVarToParam
2020-01-06 20:52:47 -08:00
Leonardo de Moura
139d6c64e6
feat: add new_frontend command
...
cc @kha
2020-01-06 20:44:53 -08:00
Leonardo de Moura
24f1479758
chore: remove workaround
2020-01-06 16:44:08 -08:00
Leonardo de Moura
20c0a63908
feat: add support for optParam
2020-01-06 16:41:48 -08:00
Leonardo de Moura
fbdf5361d4
chore: update stage0
2020-01-06 15:45:04 -08:00
Leonardo de Moura
bccaaa7af0
fix: bug at lit_type binding
...
cc @kha
2020-01-06 15:44:38 -08:00
Leonardo de Moura
9b29a7bf7e
chore: update stage0
2020-01-06 15:13:46 -08:00
Leonardo de Moura
865ef32e91
feat: add parser! and tparser! elaborators
...
@Kha It is not convenient to use because
1- Coercions have not been implemented
2- Autoparams have not been implemented
3- There is bug the `Expr.lit` type checker
4- The new frontend uses a different mechanism for `export`. So,
`export`s in imported files compiled with the old frontend do not work.
I am working on these issues.
2020-01-06 15:10:35 -08:00
Leonardo de Moura
0afd970e15
feat: add declName? to TermElabM context
2020-01-06 15:10:24 -08:00
Leonardo de Moura
6c474a1eb6
test: add tests/lean/newfrontend
...
cc @Kha
2020-01-06 14:07:22 -08:00
Leonardo de Moura
9f2172e65e
feat: use new frontend when option --new-frontend is provided
2020-01-06 14:02:58 -08:00
Leonardo de Moura
3fb3b34762
chore: disable test
2020-01-06 13:42:29 -08:00
Leonardo de Moura
49d2994dd6
chore: update stage0
2020-01-06 12:12:45 -08:00
Leonardo de Moura
911e9535b9
feat: elabDefLike
2020-01-06 12:10:08 -08:00
Sebastian Ullrich
bc0802d76c
refactor: test quotations in command elab
2020-01-06 10:09:26 -08:00
Sebastian Ullrich
9b6eeacc0f
feat: add macro stack tracking to command elab
2020-01-06 10:09:26 -08:00
Sebastian Ullrich
fd4b9ffcf5
chore: update stage0
2020-01-06 10:09:26 -08:00
Sebastian Ullrich
bece6f7a32
feat: command quotations
2020-01-06 10:09:26 -08:00
Leonardo de Moura
ebd39de20d
feat: add collectFVars
2020-01-06 09:34:00 -08:00
Leonardo de Moura
573877dcdf
chore: cleanup
2020-01-06 09:33:11 -08:00
Leonardo de Moura
5be180910f
test: add applyAttributes test
2020-01-05 16:27:22 -08:00
Leonardo de Moura
af6f7f4bc8
chore: update stage0
2020-01-05 16:27:05 -08:00
Leonardo de Moura
0231841984
feat: applyAttributes
2020-01-05 16:22:46 -08:00
Leonardo de Moura
e344f46e66
chore: allow attributes to parse arguments
2020-01-05 15:58:58 -08:00
