Leonardo de Moura
a0a4b9faec
fix: filter declarations that are not valid dot methods
2021-04-08 11:48:12 -07:00
Sebastian Ullrich
f75ce86f71
fix: server: go to type definition
2021-04-08 18:54:53 +02:00
Leonardo de Moura
2da8e5afa1
chore: add completion test for the group issue
2021-04-07 22:46:08 -07:00
Leonardo de Moura
7de9cfeac8
chore: fix StructInst and add mkGroupNode
2021-04-07 22:46:07 -07:00
Leonardo de Moura
6d361b91b5
Feat: Add getAllParentStructures
2021-04-07 18:06:10 -07:00
Leonardo de Moura
98c6fd1151
fix: another antipattern
2021-04-07 10:42:54 -07:00
Leonardo de Moura
132d6de78d
fix: antipattern
...
We should never assume a `Syntax` node has a specific number of
children because the parser error recovery may produce partial
abstract syntax trees. We should use `stx[i]` instead because
`Syntax.getOp` returns `Syntax.missing` when `i` is out of bounds.
2021-04-07 10:26:05 -07:00
Sebastian Ullrich
0396168c2c
test: make sure the interactive test would have actually failed without the fix
2021-04-07 18:05:48 +02:00
Sebastian Ullrich
5b5a882da6
fix: watchdog: do not reorder messages while delaying edits
2021-04-07 17:12:37 +02:00
Sebastian Ullrich
2de5b141eb
test: interactive: support inserting text
2021-04-07 17:12:37 +02:00
Leonardo de Moura
9b0c054258
test: auto completion
2021-04-05 20:45:04 -07:00
Leonardo de Moura
803161d9fc
fix: propagate expected type
2021-04-05 20:00:05 -07:00
Leonardo de Moura
3ccd992dad
feat: elaborate auxiliary completion node
2021-04-05 19:07:39 -07:00
Leonardo de Moura
f13bdd6869
fix: error recovery at sepBy combinator
2021-04-05 18:38:57 -07:00
Sebastian Ullrich
e863376be1
chore: simplify tests
2021-04-05 22:01:56 +02:00
Leonardo de Moura
fbd6adaf21
chore: fix tests
2021-04-05 12:35:52 -07:00
Leonardo de Moura
383e32937e
test: completion
2021-04-05 12:01:58 -07:00
Leonardo de Moura
e6dec2dd79
feat: don't allow whitespaces between . and field name
2021-04-05 07:11:14 -07:00
Sebastian Ullrich
46be48211e
test: dot completion
2021-04-05 14:00:22 +02:00
Sebastian Ullrich
6dc3e55c54
fix: longestMatchFn: do not discard partial syntax tree of first overload
2021-04-05 10:00:47 +02:00
Leonardo de Moura
5ab3ed5314
chore: fix test
2021-04-04 11:38:35 -07:00
Daniel Fabian
401765f587
test: add test that deriving Ord compiles in various cases.
2021-04-03 21:27:26 -07:00
Leonardo de Moura
750691bd5a
chore: fix tests
2021-04-03 18:24:03 -07:00
Sebastian Ullrich
d0996fb945
chore: improve EOI error message
2021-04-03 11:56:26 +02:00
Leonardo de Moura
f631bd8df9
test: inductive predicate example
2021-04-02 16:21:54 -07:00
Sebastian Ullrich
e20b2c359a
feat: server: show goal state after tactic if cursor not strictly before tactic
2021-04-03 00:23:46 +02:00
Sebastian Ullrich
ac9fee5854
test: add Lean 3-style interactive server tests
...
Fixes #376
2021-04-03 00:23:46 +02:00
Sebastian Ullrich
30062b8988
fix: nomatch with non-fvar terms
2021-04-02 16:04:47 +02:00
Leonardo de Moura
5e66f4c97c
feat: dot completion experiment
...
We still need to use the expected type, fix error recovery, etc. But it
is showing signs of life for very basic examples.
It is disabled for now.
2021-04-01 23:31:38 -07:00
Leonardo de Moura
2837873db5
fix: longestMatch error recovery
...
@kha When replacing an error with a longer one, we were keeping the
message for the longer error, but losing its node.
2021-03-31 20:09:36 -07:00
Leonardo de Moura
2fc775954c
fix: error recovery
...
@kha We have a few parsers that invoke `tokenFn`, and return error
depending of what is on the top of the stack (e.g., `ident`).
These parsers were not restoring the stack size when reporting errord,
and messing up the error recovery. We never notice the problem because
operators such as <|> restore the stack size, and we were not trying
to elaborate syntacticly incorrect terms.
2021-03-31 17:05:34 -07:00
Leonardo de Moura
92193e7d70
chore: fix tests
2021-03-31 17:05:34 -07:00
Sebastian Ullrich
ee55ac5508
chore: fix test
2021-03-31 21:24:28 +02:00
Daniel Fabian
93bb94bfea
test: update playground for Hashable
...
due to new code generation, adjust the playground code
2021-03-30 13:36:52 -07:00
Daniel Fabian
fee3390dd1
feat: add Hashable deriving
...
add support for the `Hashable` deriving by combining structural
hashes over fields
2021-03-30 13:36:52 -07:00
Leonardo de Moura
4ec6804667
fix: issue at expandMatchAlts
2021-03-30 12:55:59 -07:00
Leonardo de Moura
19e0a84817
fix: make the match behavior more uniform
2021-03-30 12:19:31 -07:00
Leonardo de Moura
002f96adc1
test: discriminant refinement
2021-03-28 19:06:06 -07:00
Leonardo de Moura
41539a7725
fix: leftovers in the local context when applying induction
2021-03-27 19:42:22 -07:00
Leonardo de Moura
b32b542a85
chore: fix mkForbiddenSet
2021-03-27 14:59:05 -07:00
Leonardo de Moura
4a0f8bf21a
feat: improve generalizing at induction
2021-03-27 14:28:03 -07:00
Leonardo de Moura
f20fc6328c
fix: better error message when cases fails and there are no alternatives
2021-03-26 16:28:21 -07:00
Leonardo de Moura
6cfc8d0937
fix: ensure discriminants are distinct variables
2021-03-26 16:28:21 -07:00
Sebastian Ullrich
2647cdf813
chore: fix trace.Elab.info position & redundancy
2021-03-26 11:39:44 +01:00
Sebastian Ullrich
170fc62c18
fix: tactic info post state
2021-03-26 11:25:52 +01:00
Leonardo de Moura
a8d672f237
test: add Kevin and Yakov's examples
2021-03-25 17:22:14 -07:00
Leonardo de Moura
c79712becb
chore: fix test
2021-03-25 17:20:58 -07:00
Leonardo de Moura
05022cc80b
fix: disable implicit lambda insertion at _, ?h, and by ...
...
@Kha This commit addresses an issue reported by Kevin. Holes and tactic
blocks represent a discontinuity in the elaboration process.
By introducing inaccessible variables (or "things" as Kevin calls
them), we create error message that are harder to understand (see
affected test), and goals where we didn't allow the user to select the
variable name and/or eagerly unfolded a definition.
BTW, I first considered using "reducible" setting when deciding
whether to insert implicit lambdas or not. This is a bad idea.
See `monotone.lean` test. The decision should not depend on
reducibility status, but whether there is "discontinuity" on the
elaboration process or not. As Kevin pointed out,
"introducing implicits work great if you finish the job".
2021-03-25 16:13:15 -07:00
Sebastian Ullrich
96c8cdfb14
chore: revert test changes
2021-03-25 10:35:22 +01:00
Leonardo de Moura
3176be136c
feat: improve "discriminant refinement"
2021-03-24 21:05:08 -07:00
