Leonardo de Moura
7a8fb1b66c
chore: remove workaround
...
`elabAppArgsAux` has been improved in the previous commit.
2020-10-11 15:08:12 -07:00
Leonardo de Moura
fda1d7b213
refactor: elabAppArgsAux
...
It also adds better support for opt/auto params and named arguments.
2020-10-11 15:08:12 -07:00
Leonardo de Moura
cd20e2ef8d
chore: use interpolated string
2020-10-11 15:08:12 -07:00
Leonardo de Moura
a53ab799d9
chore: remove workaround
2020-10-10 16:20:44 -07:00
Leonardo de Moura
c5e3da89e8
fix: (try to) postpone when discriminant type is not known
2020-10-10 16:16:22 -07:00
Leonardo de Moura
7fec9587db
fix: dollarProj notation bug
2020-10-10 13:38:07 -07:00
Leonardo de Moura
069faf0a0a
chore: move ResolveName to new frontend
2020-10-10 13:03:46 -07:00
Leonardo de Moura
f84fa47566
fix: use resolveGlobalConstNoOverload at implementedBy attribute handler
2020-10-10 11:40:32 -07:00
Leonardo de Moura
89eebc9534
fix: use resolveGlobalConstNoOverload at init attribute handler
2020-10-10 11:37:37 -07:00
Leonardo de Moura
fa6b7b6393
feat: add MonadResolveName type class
...
`AttrM` can now resolve names.
2020-10-10 11:33:52 -07:00
Leonardo de Moura
eacf3ed6c7
refactor: move ResolveName to Lean directory
2020-10-10 11:07:14 -07:00
Leonardo de Moura
b93c5b47ec
chore: remove Alias.lean
2020-10-10 11:00:16 -07:00
Leonardo de Moura
fa338c1885
refactor: move resolveGlobalName to Lean namespace
2020-10-10 10:58:44 -07:00
Leonardo de Moura
63edecf106
feat: expand initialize macro
2020-10-10 08:23:49 -07:00
Leonardo de Moura
736b2bf8ed
chore: remove kind
2020-10-10 07:53:52 -07:00
Leonardo de Moura
446b7dc690
chore: remove workaround
2020-10-10 07:47:28 -07:00
Leonardo de Moura
698c3db655
chore: take doSeq at initialize
2020-10-10 07:41:44 -07:00
Leonardo de Moura
58b0da222f
feat: add coercion A => Thunk A
2020-10-10 07:39:02 -07:00
Leonardo de Moura
3e4bfe9a85
fix: missing coercion for new frontend
2020-10-10 07:07:14 -07:00
Leonardo de Moura
fb2fea2744
fix: explicit syntax kind in macro_rules
2020-10-10 06:42:45 -07:00
Leonardo de Moura
9538772c1c
chore: do not use string interpolation by default at dbgTrace!
...
It is nice to be able to write `dbgTrace! x` instead of `dbgTrace! "{x}"`
2020-10-09 20:49:39 -07:00
Leonardo de Moura
be252743b3
feat: add string interpolation for MessageData
2020-10-09 20:43:26 -07:00
Leonardo de Moura
2151052b79
chore: move Log.lean to new frontend
2020-10-09 17:38:35 -07:00
Leonardo de Moura
719f384d69
chore: move DefView to new frontend
2020-10-09 17:26:54 -07:00
Leonardo de Moura
bca81714fe
feat: println! and dbgTrace! macros with string interpolation
2020-10-09 17:19:04 -07:00
Leonardo de Moura
51dc10dd93
feat: array slicing notation
2020-10-09 16:40:18 -07:00
Leonardo de Moura
3bd75d51d5
feat: add ParserDescr.noWs
2020-10-09 16:26:49 -07:00
Leonardo de Moura
e021a7d011
chore: remove symbolNoWs
...
@Kha This is a leftover from the time precedence was associated with
tokens instead of parsers.
2020-10-09 16:17:56 -07:00
Leonardo de Moura
5a40d9eb13
feat: add Subarray
2020-10-09 16:06:24 -07:00
Leonardo de Moura
ec5aa511a4
chore: move Level.lean to new frontend
2020-10-09 14:57:14 -07:00
Leonardo de Moura
a621256b10
fix: unintended overload
2020-10-09 14:56:11 -07:00
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
