Leonardo de Moura
76a8f17c4b
chore: update stage0
2020-10-06 08:28:41 -07:00
Leonardo de Moura
786b1a952c
chore: update stage0
2020-10-06 08:28:41 -07:00
Leonardo de Moura
c3b0e9936c
chore: group many elements
2020-10-06 08:28:40 -07:00
Leonardo de Moura
5c74c408ae
chore: remove nodeSepBy1Unbox combinator
2020-10-06 08:28:40 -07:00
Leonardo de Moura
e635196f32
chore: fix test
...
I added a temporary workaround. I will remove it later.
2020-10-06 08:28:13 -07:00
Leonardo de Moura
a71cc58d70
chore: update stage0
2020-10-06 07:28:21 -07:00
Leonardo de Moura
54bfc1e168
chore: add elabTacticQuotSeq
2020-10-06 07:27:31 -07:00
Leonardo de Moura
de161aba96
chore: update stage0
2020-10-06 07:23:30 -07:00
Leonardo de Moura
93dc94b3b0
chore: remove nodeSepBy1Unbox hack
2020-10-06 07:22:28 -07:00
Leonardo de Moura
0447966b72
chore: adjust elaborator to new syntax
2020-10-06 06:53:12 -07:00
Leonardo de Moura
fda85f6a71
chore: update stage0
2020-10-06 06:45:13 -07:00
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
5f28f2badc
test: add another do notation test
2020-10-05 19:19:18 -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
ac16393ae9
chore: add break and continue keywords
2020-10-05 15:37:01 -07:00
Leonardo de Moura
98dbe45ab8
chore: remove Monad List instance
...
@Kha The new `do` notation works for pure code too.
It automatically inserts `Id` if the expected type is not a monad.
This works great when we are not conflating data and control.
After deleting `Monad List`, we will be able to write functions such as
```lean
def mapWhen (p : Nat → Bool) (f : Nat → Nat) (xs : List Nat) : List Nat := do
for x in xs do
if p x then
x := f x
```
without adding `Id.run` before the `do`.
2020-10-05 13:27:18 -07:00
Leonardo de Moura
7a0cbdbe04
test: shadowing in do blocks
2020-10-05 11:51:17 -07:00
Leonardo de Moura
60edde82b0
fix: special support for Id
2020-10-05 11:50:07 -07:00
Leonardo de Moura
a6063a5560
chore: fix tests
2020-10-05 11:28:52 -07:00
Leonardo de Moura
fb83e8e79b
feat: allow any variable to be reassigned
2020-10-05 11:25:19 -07:00
Leonardo de Moura
5adb04b10e
chore: add helper instance
2020-10-05 11:24:35 -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
d7d7e16f96
chore: Id missing instances
2020-10-05 09:55:19 -07:00
Leonardo de Moura
ebc166585a
chore: update stage0
2020-10-05 09:46:42 -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
666398bf96
chore: update stage0
2020-10-05 09:37:21 -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
4a2a2758ec
chore: adjust test
2020-10-04 16:19:50 -07:00
Leonardo de Moura
9810b405d9
feat: add CodeBlock to Syntax converter
2020-10-04 16:19:09 -07:00
Leonardo de Moura
b4289d5c5d
feat: add DoResult
2020-10-03 15:38:30 -07:00
Leonardo de Moura
e47e9c8be3
chore: remove unnecessary withNewVars
2020-10-03 15:24:35 -07:00
Leonardo de Moura
21d90afa43
feat: add ForInStep type
2020-10-03 15:16:45 -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
ef741d343d
chore: update stage0
2020-10-03 08:36:08 -07:00
Leonardo de Moura
4e7fd4b4bf
chore: add doSeqIndent kind
2020-10-03 08:22:02 -07:00
Leonardo de Moura
ee830ec293
chore: update stage0
2020-10-03 07:35:03 -07:00
Leonardo de Moura
a5daaee3ed
chore: do syntax adjustments
2020-10-03 07:33:18 -07:00
Leonardo de Moura
3caa683626
chore: add unless to keyword list
2020-10-02 19:16:14 -07:00
