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
Leonardo de Moura
8e81db0d2b
chore: add temporary workaround to tests
...
We will remove it after we implement `doMatch`
2020-09-27 06:58:10 -07:00
Leonardo de Moura
a0a724ddbd
fix: tests and elabDo
2020-09-26 19:12:01 -07:00
Leonardo de Moura
ef9b661c8d
chore: add temporary workarounds until we implement new elabDo
2020-09-26 18:11:46 -07:00
Leonardo de Moura
5fa8d9105e
feat: add if and for for do blocks
2020-09-26 18:03:53 -07:00
Leonardo de Moura
6892a957d6
feat: trailing ; in indented "do" sequences
...
cc @Kha
2020-09-26 16:08:30 -07:00
Leonardo de Moura
3f4499be08
feat: allow trailing ; at doSeqBracketed
2020-09-26 14:20:47 -07:00
Leonardo de Moura
8e159f004c
fix: missing synthesizeSyntheticMVarsNoPostponing at elabMatch
2020-09-25 18:48:23 -07:00
Leonardo de Moura
b71e5b4648
test: cdot tests
2020-09-25 18:48:23 -07:00
Leonardo de Moura
240680db1a
feat: add binductionOn support
2020-09-25 07:18:14 -07:00
Leonardo de Moura
d17c20be25
test: add old Lean3 tests
2020-09-25 06:48:51 -07:00
Leonardo de Moura
1775d9b04b
fix: visit types
...
See new test `tests/lean/run/def14.lean`
2020-09-25 06:48:51 -07:00
Leonardo de Moura
0e16bd60dc
fix: missing case
2020-09-25 06:48:51 -07:00
Leonardo de Moura
afa2f9b74c
test: add old Lean3 tests
2020-09-25 06:48:51 -07:00
Leonardo de Moura
e4f492d68a
feat: add support for reflexive inductive datatypes
2020-09-24 20:30:12 -07:00
Leonardo de Moura
66d35cdd76
fix: the generated matcher must be able to eliminate into different universe levels
2020-09-24 19:34:14 -07:00
Leonardo de Moura
bdf412bf49
test: add old Lean3 tests
2020-09-24 18:01:23 -07:00
Leonardo de Moura
3256a24813
fix: bug at toBelow
2020-09-24 17:38:51 -07:00
Leonardo de Moura
bdefe91fbf
test: add old Lean3 tests
2020-09-24 17:32:47 -07:00
Leonardo de Moura
7edc52682b
fix: processNonVariable
2020-09-24 17:16:50 -07:00
Leonardo de Moura
8383177c96
fix: nonoptimal specialization
...
@Kha Here is the fix for the problem I told you this morning.
Please, take a look at `specialize.cpp` and see whether it makes sense.
2020-09-24 12:40:28 -07:00
Leonardo de Moura
6fe8a0e179
test: issue 29
...
New frontend fixed this issue.
closes #29
2020-09-23 18:30:28 -07:00
Leonardo de Moura
e22d2f6cb1
test: new tests for structural recursion
...
@Kha The structural recursion is working :)
It is so much more powerful than the one in Lean3.
I added examples with `let rec`, nested and multiple
`match`-expressions.
I will keep testing and adding missing features tomorrow, and
will hopefully start porting stdlib to new frontend before the end of
the week.
2020-09-23 18:24:56 -07:00
Leonardo de Moura
6a51ec8427
fix: missing case (kernel projection) at isExprDefEqAuxImpl
2020-09-23 18:24:56 -07:00
Leonardo de Moura
c46e64b089
feat: add Array.zipWith and Array.zip
2020-09-23 18:24:56 -07:00
Leonardo de Moura
d66b6738ee
chore: fix test
2020-09-22 19:07:46 -07:00
Leonardo de Moura
0511b73d80
feat: add replaceFVars
2020-09-22 14:24:03 -07:00
Leonardo de Moura
f4b5ec710f
fix: fixes #175
2020-09-21 17:12:07 -07:00
Leonardo de Moura
6a90fbf855
test: String interpolation
...
@Kha I wrote this extended test using the new frontend. The new
frontend worked great. I only had a minor issue with `#exit`.
The example uses `let rec`, parsers, macros, lift-method notation, etc.
It implements the new parser `strInterpolant p` for string
interpolation. The parser `p` is used to process the elements inside
`{...}`. Then, I use this parser to implement the macro `toString!`.
Example: `toString! "1+2 = {1+2}"` produces `"1+2 = 3"`.
Even the new "lift-method" notation works inside the string interpolant.
```lean
def g (x : Nat) : StateRefT Nat IO Nat := do
modify (· + x);
get
def ex : StateRefT Nat IO Unit := do
IO.println $ toString! ">> hello {(<- g 1)}";
IO.println $ toString! ">> world {(<- g 1)}";
pure ()
```
2020-09-20 18:11:19 -07:00
Leonardo de Moura
ac2a9539f9
fix: old&new frontend interference
...
The new test was not working because new frontend was using old
frontend function.
2020-09-20 08:25:45 -07:00
Leonardo de Moura
c43450f027
feat: macros for the syntax category
...
This is the last of a series of commits for adding this feature.
2020-09-19 15:00:41 -07:00
Leonardo de Moura
052e67d1af
feat: rewrite tactic
2020-09-18 16:13:14 -07:00
Sebastian Ullrich
f1386672c8
chore: disable format-reparse test until hard linebreaks are working
2020-09-18 13:15:40 -07:00
