Leonardo de Moura
487bcaaf2b
chore: remove dead coe
2021-04-06 19:11:59 -07:00
Leonardo de Moura
ca314f1aa4
refactor: add helper functions for match syntax elaborator
2021-04-06 19:02:03 -07:00
Sebastian Ullrich
3438f425f1
feat: leanpkg init: emit lean_version
2021-04-06 14:38:17 +02:00
Sebastian Ullrich
11e2243c9a
fix: leanpkg version warning
2021-04-06 14:20:37 +02: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
5c838c57f1
chore: disable special support for Syntax.missing at isNodeOf'
...
It didn't help with the problem I was having, but we talked about
customizing this behavior in the past. So, I will leave the function
here because it is convenient for trying experiments without having to
modify `Quotation.lean` and `update-stage0`
2021-04-05 18:38:58 -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
François G. Dorais
9949aa653e
feat: add missing simp lemmas for <->
2021-04-05 06:41:39 -07:00
Sebastian Ullrich
5644cee2d6
chore: reset prefer_native
2021-04-05 13:58:15 +02: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
Leonardo de Moura
a6a008ec5b
feat: use user provided name if available
2021-04-03 12:52:25 -07:00
Leonardo de Moura
ac35b543bf
feat: add addional CompletionInfo
2021-04-03 11:17:51 -07:00
Sebastian Ullrich
d0996fb945
chore: improve EOI error message
2021-04-03 11:56:26 +02:00
Sebastian Ullrich
46ec999a71
fix: don't leak thread-local stream objects
...
Fixes #245
2021-04-03 10:00:17 +02:00
Leonardo de Moura
ff1d27370c
feat: add CompletionInfo
2021-04-02 20:44:57 -07:00
Leonardo de Moura
d26aa5e1ab
feat: black list other auxiliary constructions
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
334320fd40
fix: lean --run
2021-04-03 00:23:46 +02:00
Sebastian Ullrich
8f67921221
feat: Json.setObjVal!
2021-04-03 00:23:46 +02:00
Sebastian Ullrich
8440097e87
chore: server: repr-print invalid header
2021-04-03 00:23:45 +02:00
Leonardo de Moura
ed4504929d
refactor: add Server/Completion.lean
...
Add environment extension for black listing declaritions for completion.
2021-04-02 11:10:06 -07:00
Leonardo de Moura
9815d626f5
feat: hide auxiliary constructions when generating completion candidates
2021-04-02 11:10:06 -07:00
Leonardo de Moura
bc44ad65ae
feat: only consider dot completion info occurring in the hover line
2021-04-02 11:10:06 -07:00
