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
Leonardo de Moura
7f5b454382
chore: improve for type mismatch error message
2020-10-06 10:50:03 -07:00
Leonardo de Moura
5cabc917f5
chore: improve error message
2020-10-06 10:45:12 -07:00
Leonardo de Moura
74e5bf2539
feat: add elabEnsureExpectedType
2020-10-06 09:39:16 -07:00
Leonardo de Moura
ef2d9b4d59
feat: add ensureExpectedType! parser
2020-10-06 09:31:21 -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
10fc908463
chore: use Tactic.seq1 instead of Tactic.tacticSeq1Indented
...
Reason: antiquotations.
2020-10-06 08:28:41 -07:00
Leonardo de Moura
71e6ab2a06
fix: evalTacticSeqBracketed and evalSeq1
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
54bfc1e168
chore: add elabTacticQuotSeq
2020-10-06 07:27:31 -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
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
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
60edde82b0
fix: special support for Id
2020-10-05 11:50:07 -07:00
Leonardo de Moura
fb83e8e79b
feat: allow any variable to be reassigned
2020-10-05 11:25:19 -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
7325dcd630
feat: use do at for-in and unless notations
2020-10-05 09:43:11 -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
9810b405d9
feat: add CodeBlock to Syntax converter
2020-10-04 16:19:09 -07:00
Leonardo de Moura
e47e9c8be3
chore: remove unnecessary withNewVars
2020-10-03 15:24:35 -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
4e7fd4b4bf
chore: add doSeqIndent kind
2020-10-03 08:22:02 -07:00
