Leonardo de Moura
6020e6682a
feat: process interpolatedStr in the elaborator
2020-10-09 14:18:45 -07:00
Leonardo de Moura
70ec458fde
test: new frontend
2020-10-09 13:20:04 -07:00
Leonardo de Moura
650bd95ab9
feat: add efficient Array.forIn
2020-10-09 13:07:20 -07:00
Leonardo de Moura
0b81ffb569
refactor: factor out nested do term support and document code
...
We currently use the nested `do` terms for two combinators: `catch`
and `finally`. We may want to support more in the future.
2020-10-09 11:59:14 -07:00
Leonardo de Moura
f6fffc9532
test: monad stack with multiple ExceptT
...
cc @Kha :)
2020-10-08 19:53:12 -07:00
Leonardo de Moura
8a6cb1842f
feat: expand doTry
...
@Kha I did not implement support for reassignments and `continue`,
`break`, `return` inside the `finally` clause. It is doable, but it
feels like unnecessary complexity. We currently don't have any
instance in our code base where this would be useful.
2020-10-08 19:39:36 -07:00
Leonardo de Moura
c005a9375a
chore: remove workarounds
2020-10-08 16:50:59 -07:00
Leonardo de Moura
a31595bda5
feat: add doElem.quot elaboration function
2020-10-08 13:50:25 -07:00
Leonardo de Moura
a3a5190004
feat: expand doElem macros
2020-10-08 13:42:56 -07:00
Leonardo de Moura
608de7b592
feat: expand doReassignArrow
2020-10-08 13:31:27 -07:00
Leonardo de Moura
3694936b7d
test: doHave test
2020-10-08 12:11:07 -07:00
Leonardo de Moura
09dcf718c1
feat: expand doHave
2020-10-08 11:56:03 -07:00
Leonardo de Moura
d7ec398b28
test: new do notation
2020-10-07 17:55:38 -07:00
Leonardo de Moura
d9d8e95987
feat: elaborate doElems at doLetArrow
...
@Kha The Rust `let+return` example works in Lean too :)
The Rust function
```rust
fn f (x : i32) -> i32 {
let y = if x == 0 { println!("x is zero"); return 100 } else { x + 1 };
println!("y: {}", y)
y
}
```
The Lean version is
```lean
def f (x : Nat) : IO Nat := do
let y ← if x == 0 then IO.println "x is zero"; return 100 else pure (x + 1)
IO.println ("y: " ++ toString y)
return y
```
The main missing feature now is the `try-catch-finally` `do` element.
2020-10-07 17:30:25 -07:00
Leonardo de Moura
ac07999e95
chore: cleanup do expander, and make sure it can handle the "easy" doLetArrows
2020-10-07 17:00:07 -07:00
Leonardo de Moura
5b76155318
feat: new return semantics
...
`return e` is not equivalent to `pure e` anymore.
Now, `return e` means "return value `e` as the result of the root `do` block".
2020-10-07 14:07:58 -07:00
Leonardo de Moura
e70dd03340
chore: remove forInMap
2020-10-07 10:01:04 -07:00
Leonardo de Moura
ac1c0714a1
fix: expand macros in patterns before retrieving pattern variables
2020-10-07 09:15:05 -07:00
Sebastian Ullrich
6c25717377
test: can finally reparse pretty-printed Core.lean
2020-10-07 09:46:47 +02:00
Leonardo de Moura
294a750110
feat: expand doMatch
2020-10-06 19:07:47 -07:00
Leonardo de Moura
f4ccb78014
feat: improve tryPureCoe? and document its limitations
2020-10-06 17:41:45 -07:00
Leonardo de Moura
3a426d96e7
feat: custom error message header at elabTermEnsuringType
...
This commit also improves `ensureTypeOf!` primitive.
2020-10-06 09:27:13 -07:00
Leonardo de Moura
653f1406d6
chore: remove workaround
2020-10-06 08:28:41 -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
5f28f2badc
test: add another do notation test
2020-10-05 19:19:18 -07:00
Leonardo de Moura
eac3ca9286
feat: let rec in do notation
2020-10-05 19:10:06 -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
43ce35985b
chore: fix test
2020-10-05 16:47:34 -07:00
Leonardo de Moura
eafd9bc0ad
feat: expand for x in xs notation
2020-10-05 15:37:34 -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
fb83e8e79b
feat: allow any variable to be reassigned
2020-10-05 11:25:19 -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
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
946f5537ee
fix: pullExitPoints
2020-10-01 16:12:58 -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
94c7945bd3
feat: do code blocks
...
WIP
2020-09-30 19:20:16 -07:00
Leonardo de Moura
c10e92b348
chore: add temporary workarounds
2020-09-30 07:05:46 -07:00
Leonardo de Moura
72f969e9dd
test: new frontend
2020-09-29 18:22:34 -07:00
Sebastian Ullrich
af8dc5eeab
feat: pretty print Syntax in messages
2020-09-29 07:59:22 -07:00
Leonardo de Moura
49c5c5c08a
fix: horrible error message due to constApprox := true
...
The new test `typeMismatch.lean` contains two examples where the error
message was dreadful.
2020-09-29 07:54:48 -07:00
Leonardo de Moura
d6db541366
chore: cleanup
2020-09-28 19:05:48 -07:00
Leonardo de Moura
4fae8588fd
test: optional ';'
2020-09-28 17:11:00 -07:00
Leonardo de Moura
e10edde5cd
feat: optional ; in terms
2020-09-28 17:10:59 -07:00
Leonardo de Moura
d4c1432574
fix: tacticSeqBracketed
2020-09-28 17:10:59 -07:00
Leonardo de Moura
2755972447
fix: missing checkColGt and tests
2020-09-28 17:10:59 -07:00
Leonardo de Moura
765a8ac984
test: do with optional ;
2020-09-28 17:10:57 -07:00
Leonardo de Moura
39f8fd8eb9
fix: trailing ';' at end of input
2020-09-27 16:58:23 -07:00
