Leonardo de Moura
cebadf9efd
chore: group many elements
...
TODO: the parser combinators `many` and `sepBy` should do it.
2020-10-06 06:43:19 -07:00
Leonardo de Moura
83f5329aa3
chore: make missing case explicit
2020-10-05 19:13:15 -07:00
Leonardo de Moura
eac3ca9286
feat: let rec in do notation
2020-10-05 19:10:06 -07:00
Leonardo de Moura
802dd9056c
fix: missing braces
2020-10-05 19:09:41 -07:00
Leonardo de Moura
520a5f566a
fix: local name resolution
...
Local name resolution was incorrect when identifier had macro scopes
and projections were used.
cc @Kha
2020-10-05 17:32:46 -07:00
Leonardo de Moura
954f38d4c2
chore: remove leftover
2020-10-05 17:00:50 -07:00
Leonardo de Moura
43ce35985b
chore: fix test
2020-10-05 16:47:34 -07:00
Leonardo de Moura
54e10776d4
feat: improve error messages for do notation
...
@Kha we are getting better error message, but we need to figure out a
way to suppress error messages that come from the "plumbing".
For example, in the following example.
```
def f4 (b : Bool) (n : Nat) (v : Vector Nat n) : Vector Nat (n+1) := do
if b then
v := Vector.cons 1 v
Vector.cons 1 v
```
We get the nice "invalid reassignment" error at `v := ...`, but
we also get the nasty
```
error: application type mismatch
jp✝ v
argument
v
has type
Vector Nat (n + 1)
but is expected to have type
Vector Nat n
failed to synthesize instance
CoeT (Vector Nat (n + 1)) v (Vector Nat n)
```
Where `jp✝` is a joinpoint created by the do-notation macro expander.
I thought about using `withoutErrToSorry` when elaborating the expanded
`do` term.
We may also try to add more helper hints such as `ensureTypeOf!` and
use them around "plumbing" code (e.g., "joinpoint goto"s)
2020-10-05 16:33:59 -07:00
Leonardo de Moura
eafd9bc0ad
feat: expand for x in xs notation
2020-10-05 15:37:34 -07:00
Leonardo de Moura
60edde82b0
fix: special support for Id
2020-10-05 11:50:07 -07:00
Leonardo de Moura
fb83e8e79b
feat: allow any variable to be reassigned
2020-10-05 11:25:19 -07:00
Leonardo de Moura
82e11c401d
fix: #eval was not capturing dbgTrace! output in pure code
...
In the following example, the output produced by `dbgTrace!` was not
being captured. It could break the lean server. At least, it broke the lean4-mode.
```lean
def f (x : Nat) : Nat :=
dbgTrace! ">>> " ++ toString x;
x + 1
eval f 10
```
cc @Kha
2020-10-05 10:22:04 -07:00
Leonardo de Moura
7325dcd630
feat: use do at for-in and unless notations
2020-10-05 09:43:11 -07:00
Leonardo de Moura
9a551d9219
feat: add withForbidden and withoutForbidden parser combinators
2020-10-05 09:36:28 -07:00
Leonardo de Moura
fa4d6d24eb
feat: use toString at dbgTrace!
2020-10-05 09:27:42 -07:00
Leonardo de Moura
6e7a883b21
fix: make sure all joinpoints have at least 1 argument
2020-10-04 18:07:00 -07:00
Leonardo de Moura
d8c2d0b551
fix: CodeBlock concatenation
2020-10-04 17:59:56 -07:00
Leonardo de Moura
0caa17889f
feat: remove old elabDo
...
Remark: we still have a few WIP
2020-10-04 17:14:36 -07:00
Leonardo de Moura
9810b405d9
feat: add CodeBlock to Syntax converter
2020-10-04 16:19:09 -07:00
Leonardo de Moura
e47e9c8be3
chore: remove unnecessary withNewVars
2020-10-03 15:24:35 -07:00
Leonardo de Moura
251ac73df4
feat: add missing code to new elabDo
...
WIP
2020-10-03 14:59:28 -07:00
Leonardo de Moura
a84b3ac8de
chore: fix old elabDo and test
2020-10-03 08:36:22 -07:00
Leonardo de Moura
4e7fd4b4bf
chore: add doSeqIndent kind
2020-10-03 08:22:02 -07:00
Leonardo de Moura
a5daaee3ed
chore: do syntax adjustments
2020-10-03 07:33:18 -07:00
Leonardo de Moura
d3d245c711
feat: ToCodeBlock skeleton
2020-10-02 19:02:47 -07:00
Leonardo de Moura
96f5c51a3e
fix: doElem issues
2020-10-02 18:58:43 -07:00
Leonardo de Moura
c40ec0128d
fix: return value is optional
2020-10-02 18:09:42 -07:00
Leonardo de Moura
137b9efd42
chore: remove leftover
2020-10-02 15:51:03 -07:00
Leonardo de Moura
35e401e915
chore: naming consistency
2020-10-02 15:47:12 -07:00
Leonardo de Moura
40640b85bd
fix: doSeqBracketed parser
...
It was failing to parse
```
def f2 (x : Nat) : IO Nat := do {
let y := 1;
if x > 0 then
y := y + 1;
IO.println y
}
```
cc @Kha
2020-10-02 15:05:22 -07:00
Leonardo de Moura
379e34a910
feat: do reassignment parsers
2020-10-02 13:16:55 -07:00
Leonardo de Moura
703adc9a0a
chore: remove leftover
2020-10-01 18:47:35 -07:00
Leonardo de Moura
299bc54af0
chore: improve error message
2020-10-01 18:47:22 -07:00
Leonardo de Moura
946f5537ee
fix: pullExitPoints
2020-10-01 16:12:58 -07:00
Leonardo de Moura
4a57eace89
chore: remove expandDo builtin macro
2020-10-01 16:12:19 -07:00
Leonardo de Moura
4b6d308bc2
feat: add elabTypeOf and elabEnsureTypeOf
2020-10-01 14:56:46 -07:00
Leonardo de Moura
6db45891e2
feat: add typeOf! and ensureTypeOf! parsers
2020-10-01 14:33:04 -07:00
Leonardo de Moura
d0ade7ff08
feat: extend doBlock expander
...
- Add support for `if h:c then t else e`, `h` may shadow reassignable
variables
- Pattern variables in `match` alternatives may shadow reassignable
variables
- A single declaration/reassignment in a `do` block may
declare/reassign multiple variables. Example: `let (x, y) := t`
2020-10-01 10:40:55 -07:00
Leonardo de Moura
4e72530ce7
chore: let rec in do blocks
2020-10-01 10:40:11 -07:00
Leonardo de Moura
94c7945bd3
feat: do code blocks
...
WIP
2020-09-30 19:20:16 -07:00
Leonardo de Moura
a3218dd063
refactor: export Core.mkFreshUserName to Lean namespace
2020-09-30 11:21:46 -07:00
Leonardo de Moura
75cb42d8be
chore: improve try parser
2020-09-30 07:12:04 -07:00
Leonardo de Moura
0911b9bc80
feat: add missing features to do notation parser
2020-09-30 06:51:25 -07:00
Leonardo de Moura
0fe705f3a1
feat: improve error messages for unassigned metavariables
...
cc @Kha
2020-09-29 17:18:03 -07:00
Sebastian Ullrich
19dcbdcec9
fix: do not format Syntax in Messages eagerly
2020-09-29 07:59:22 -07:00
Sebastian Ullrich
d51101b884
feat: sanitize Syntax in messages
...
Fixes #182
2020-09-29 07:59:22 -07:00
Sebastian Ullrich
b4ea61e79d
fix: NameSet.insert return type
2020-09-29 07:59:22 -07:00
Sebastian Ullrich
af8dc5eeab
feat: pretty print Syntax in messages
2020-09-29 07:59:22 -07:00
Sebastian Ullrich
2d8c7e4fd0
fix: MetaM.run'
2020-09-29 07:59:22 -07:00
Sebastian Ullrich
6ad47878ef
chore: improve error message using (<- ...) outside of do
2020-09-29 07:59:22 -07:00
