Leonardo de Moura
6020e6682a
feat: process interpolatedStr in the elaborator
2020-10-09 14:18:45 -07:00
Leonardo de Moura
7013ea4098
feat: add interpolatedStr to ParserDescr and Syntax
2020-10-09 14:04:53 -07:00
Leonardo de Moura
36696d726d
feat: add String Interpolation
2020-10-09 13:40:35 -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
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
9ec583e808
chore: use (doElem| ...) quotation instead of auxDo idiom
2020-10-08 13:54:49 -07:00
Leonardo de Moura
a31595bda5
feat: add doElem.quot elaboration function
2020-10-08 13:50:25 -07:00
Leonardo de Moura
7f5af84660
chore: add doElem quotation parser
2020-10-08 13:45:53 -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
c1469643ca
chore: cleanup doLetArrowToCode
2020-10-08 13:00:27 -07:00
Leonardo de Moura
09dcf718c1
feat: expand doHave
2020-10-08 11:56:03 -07:00
Leonardo de Moura
426f139ea3
chore: remove unnecessary [inline]
2020-10-08 11:29:56 -07:00
Leonardo de Moura
91aaab9e0d
fix: error message location
2020-10-07 17:43:23 -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
5d8764dd92
feat: take doElem at doLetArrow and doReassignArrow
2020-10-07 16:49:28 -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
a841842de1
chore: Code.action => Code.seq
2020-10-07 10:19:04 -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
be7a3b76eb
feat: Format.fill
2020-10-07 15:30:36 +02:00
Sebastian Ullrich
df16221013
fix: Format.be: properly re-evaluate flattening after hard line break
2020-10-07 11:03:44 +02:00
Sebastian Ullrich
1fc1c55ed2
refactor: Format.be: explicit WorkItem structure
2020-10-07 10:09:05 +02:00
Sebastian Ullrich
f0dad079ad
fix: checkWsBefore.formatter
2020-10-07 10:01:17 +02:00
Sebastian Ullrich
064c9b2e0b
chore: binder spacing
2020-10-07 09:46:47 +02:00
Sebastian Ullrich
69fe4c7338
fix: formatter: must backtrack on symbols as well
2020-10-07 09:46:47 +02:00
Sebastian Ullrich
21f1a66ceb
feat: add & use ppDedent parser combinator
2020-10-07 09:46:47 +02:00
Sebastian Ullrich
b1e35d6ca9
fix: ppGroup
2020-10-07 09:44:05 +02:00
Sebastian Ullrich
88164a5e91
feat: more pp tweaks
2020-10-07 09:44:05 +02:00
Sebastian Ullrich
e777478aa1
fix: Formatter.pushLine
2020-10-07 09:44:05 +02:00
Sebastian Ullrich
3030c1ef7a
fix: Format.merge
2020-10-07 09:44:04 +02:00
Sebastian Ullrich
02001971c6
feat: Format: allow negative indentation to cancel out undesired automatic indentation
2020-10-07 09:44:04 +02:00
Sebastian Ullrich
5d76a981b0
chore: adjust pp spacing
2020-10-07 09:44:04 +02:00
Sebastian Ullrich
bdff53fdf5
feat: use ppLine
2020-10-07 09:43:05 +02:00
Sebastian Ullrich
98b3251fd3
feat: Format.pretty: support hard line breaks
2020-10-07 09:43:05 +02:00
Sebastian Ullrich
c3ebb6ad1f
fix: Format.group ignored preceding content on line
2020-10-07 09:43:05 +02:00
Sebastian Ullrich
31a2761bec
perf: make Format.group a constructor, flatten on the fly
2020-10-07 09:43:05 +02:00
Sebastian Ullrich
7154c2380b
refactor: simplify Format.SpaceResult
2020-10-07 09:43:05 +02:00
Leonardo de Moura
2fda7f4f9f
chore: add TODO
2020-10-06 19:12:08 -07: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
cda4de474b
fix: weird error message in do notation
...
cc @Kha
2020-10-06 15:12:55 -07:00
Leonardo de Moura
db1b110f7e
fix: use let* to avoid bad error messages in do notation
...
cc @Kha
2020-10-06 15:01:05 -07:00
Leonardo de Moura
d124718b05
feat: elaborate let*
2020-10-06 14:48:46 -07:00
Leonardo de Moura
db5fdd15c4
feat: add let* parser and add some support for it at Binders.lean
2020-10-06 14:42:47 -07:00
Leonardo de Moura
82dad3c86f
feat: add Code.returnAction
2020-10-06 13:19:55 -07:00
Leonardo de Moura
5110b1212d
test: do notation error messages
2020-10-06 11:35:44 -07:00
Leonardo de Moura
13591e59d5
chore: improve regular 'for' error message
2020-10-06 11:30:14 -07:00
Leonardo de Moura
760b658d19
chore: suppress extraMsg in type mismatch errors
2020-10-06 10:58:50 -07:00
