Commit graph

2640 commits

Author SHA1 Message Date
Sebastian Ullrich
cc9577add2 refactor: server: remove SnapshotData 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
dd15c8d5a7 feat: worker: don't abort on import error
to avoid the "crashed" message
2021-04-08 22:10:27 +02:00
Sebastian Ullrich
c3d6f781cf refactor: publishDiagnostics 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
bba8184d3b feat: server: treat import errors as fatal 2021-04-08 22:10:27 +02:00
Sebastian Ullrich
a027b34d58 chore: remove dubious server-only option 2021-04-08 22:10:27 +02:00
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
Sebastian Ullrich
1b1ac393d8 fix: do not try to pretty-print unknown metavariables
Fixes #380
2021-04-08 18:16:05 +02:00
Sebastian Ullrich
d75d7aa0d5 fix: server: ignore unknown implementation-dependent notifications
Fixes #383
2021-04-08 09:54:36 +02:00
Leonardo de Moura
7de9cfeac8 chore: fix StructInst and add mkGroupNode 2021-04-07 22:46:07 -07:00
Leonardo de Moura
578b3b822f fix: do not use nullKind for group combinator
We use `nullKind` for the `group` parser combinator.
When pattern matching `nullKind` nodes, we check their arities.
So, error recovery often fails for parsers that use the `group`
combinator.
For example, we have the parser
```
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
```
If there is syntax error at `letRecDecl`, the node corresponding to
```
group (letRecDecl >> optional ";")
```
will contain only one child, and the pattern matching at
```
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
  match whereDecls with
  | `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
  | _ => Macro.throwUnsupported
```
fails, and we can't elaborate the partial syntax tree for
`letRecDecl`, and auto-completion will not work there.

We address this issue by using a new kind for the `group` combinator.
The idea is to pattern match `group` as we pattern match `node`s with
proper syntax node kinds. This change is consistent with the way we
use `group` where it mainly a convenience for saving us the trouble of
defining a new parser definition that is used only once.
2021-04-07 22:30:51 -07:00
Leonardo de Moura
2b9df7d8b9 chore: make it clear that implementation relies on the fact that both branches of the if-then-else generate a node with the same kind
Motivation: we want to change the kind used in the `group` combinator.
2021-04-07 22:02:17 -07:00
Leonardo de Moura
390a476caf fix: incorrect use of unreachable! 2021-04-07 18:11:10 -07:00
Leonardo de Moura
6d361b91b5 Feat: Add getAllParentStructures 2021-04-07 18:06:10 -07:00
Leonardo de Moura
6c0f3c277f fix: ignore syntactically incorrect commands that do not contain any symbol
This kind of broken command does not have a position information, and
was producing a panic message in the server because it makes the
reasonable assumption that every command returned by `parserCommand`
has a position.
2021-04-07 14:46:13 -07:00
Leonardo de Moura
7c8e27b044 chore: minor 2021-04-07 11:14:46 -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
5b5a882da6 fix: watchdog: do not reorder messages while delaying edits 2021-04-07 17:12:37 +02:00
Sebastian Ullrich
43fcf69485 fix: watchdog: mark request as pending even if worker crashed 2021-04-07 16:48:12 +02:00
Leonardo de Moura
ca314f1aa4 refactor: add helper functions for match syntax elaborator 2021-04-06 19:02:03 -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
0717c3d0b2 chore: adding helper parser completion
I am hitting many error recovery problems. This is an attempt to make
auto-completion more robust.
For example, we currently can't auto complete inside of parentheses.
The syntax tree for the syntactically incorrect tern `(s. , 0)` is
```
(Term.paren "(" [(Term.proj `s ".")])
```
The elaborator for `paren` fails to match this partial syntax tree and
returns an error. I considered adding code to the `else` branch of
this elaborator and handle partial trees there. However, we would
still be losing information for the other elements of the tuple.
Example: no hover information for them.
The helper parser makes sure we don't lose information.
2021-04-05 18:44:01 -07:00
Leonardo de Moura
9fa89a73df feat: add helper functions for syntax match
Motivation: improve error recovery.
2021-04-05 18:38:57 -07:00
Leonardo de Moura
f13bdd6869 fix: error recovery at sepBy combinator 2021-04-05 18:38:57 -07:00
Leonardo de Moura
fb38955be2 feat: improve command parser error recovery
After a parser error in a command, we are "swallowing" all command
parsing errors until a command was succesfully parsed.
This was producing counterintuitive behavior in the IDEs.
2021-04-05 12:31:33 -07:00
Leonardo de Moura
d6af843683 chore: remove completion auxiliary parser 2021-04-05 11:26:13 -07:00
Leonardo de Moura
b1b645f5d7 chore: display expected type 2021-04-05 10:29:32 -07:00
Leonardo de Moura
19fcd518bf chore: fix syntax 2021-04-05 07:16:59 -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
98e1baabbd refactor: make trailingNode clean up after itself
Also resolves an issue with emitting both `left` and a partial tree
containing it
2021-04-05 13:51:03 +02:00
Sebastian Ullrich
6dc3e55c54 fix: longestMatchFn: do not discard partial syntax tree of first overload 2021-04-05 10:00:47 +02:00
Sebastian Ullrich
e5be9e7dd4 chore: helpers for parser debugging 2021-04-05 10:00:47 +02:00
Leonardo de Moura
ba3dd181f5 fix: make sure type errors do not break server
We often try to auto-complete code containing errors.
So, the methods `inferType` and `isDefEq` used during completion may
throw exceptions.
2021-04-04 20:29:20 -07:00
Leonardo de Moura
62590b3715 fix: code is reachable 2021-04-04 20:18:49 -07:00
Leonardo de Moura
e8cf38de20 feat: improve auto completion matching 2021-04-04 20:03:13 -07:00
Leonardo de Moura
fb67b49719 fix: missing completion 2021-04-04 18:32:56 -07:00
Leonardo de Moura
f2d81c7389 fix: position information for auto completion
We currently allow spaces between `.` and the "field" name, and this
was creating problems when auto-completing at `f (y.| a b)`
where `|` represents the cursor position
The `InfoTree` had a node for `y. a` and its tail position is after
the cursor position.
2021-04-04 11:25:52 -07:00
Leonardo de Moura
cffef2674f chore: add location 2021-04-04 10:50:30 -07:00
Leonardo de Moura
820495ce7a feat: black list auxiliary match applications 2021-04-04 10:37:13 -07:00
Daniel Fabian
401765f587 test: add test that deriving Ord compiles in various cases. 2021-04-03 21:27:26 -07:00
Daniel Fabian
fb4a119ed7 fix: allow also recursive types in the Ord construction. 2021-04-03 21:27:26 -07:00
Daniel Fabian
a8914380dc feat: add Ord and deriving instance for it.
For many data structures having an ordering is necessary. This one adds the `Ord` type class and a deriving handler for it. The ordering is based on order of constructors followed by lexicographical ordering within a constructor.
2021-04-03 21:27:26 -07:00
Leonardo de Moura
0586fe3200 feat: activate auto completion
There are many pending TODO's, and issues with the error recovery code.
We also need a test suite.
2021-04-03 21:01:17 -07:00
Leonardo de Moura
9d12856432 feat: missing forM 2021-04-03 18:24:31 -07:00
Leonardo de Moura
09ee8bddad feat: tactic name completion 2021-04-03 15:45:44 -07:00
Leonardo de Moura
20f569c033 feat: set_option completion 2021-04-03 15:06:50 -07:00
Leonardo de Moura
0a94aaabc9 feat: use expected type to prioritize completion candidates 2021-04-03 14:12:42 -07:00
Leonardo de Moura
398bbcfce3 feat: save aditional information for id completion, and suppress implicit prefix when reporting completion types 2021-04-03 12:53:32 -07:00