Sebastian Ullrich
e10cf4cf33
fix: Nix: leanpkg outside flake
2021-04-05 10:50:21 +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
9f708ece44
chore: update stage0
2021-04-04 20:32:35 -07: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
41dda0f624
chore: update stage0
2021-04-04 20:04:37 -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
dbbb7bf9f6
chore: update stage0
2021-04-04 11:39:31 -07:00
Leonardo de Moura
5ab3ed5314
chore: fix test
2021-04-04 11:38:35 -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
ab4ec76a25
chore: update stage0
2021-04-03 21:02:46 -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
750691bd5a
chore: fix tests
2021-04-03 18:24:03 -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
f631bd8df9
test: inductive predicate example
2021-04-02 16:21:54 -07:00
Leonardo de Moura
8cd6b573d6
chore: update stage0
2021-04-02 16:21:54 -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
90f2438cfd
chore: update stage0
2021-04-02 11:13:40 -07: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
Leonardo de Moura
8c2ba16f74
feat: store expected type at DotCompletionInfo
2021-04-02 11:10:06 -07:00
Leonardo de Moura
a22d8dd924
fix: the code is reachable
2021-04-02 11:10:06 -07: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
c9f4359045
feat: add DotCompletionInfo
2021-04-01 23:31:38 -07:00
Leonardo de Moura
447e57ee99
chore: update-stage0
2021-04-01 23:31:38 -07:00
Leonardo de Moura
caae7952cd
feat: add helper parsers for auto-completion
2021-04-01 23:31:38 -07:00
Leonardo de Moura
8d00a06d97
feat: add helper functions for completion
2021-04-01 23:31:38 -07:00
