Sebastian Ullrich
0948742da1
perf: fix formatting info tree unconditionally
2021-06-22 10:22:08 +02:00
Sebastian Ullrich
30a0954424
refactor: revert MonadRef changes
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
65f2874d86
chore: address reviews
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
eb1e285e26
chore: style
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
a86efc4796
fix: info tree context of command macros
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
652097e184
fix: separate ElabInfo from MacroExpansionInfo, always emit the former before the latter
...
This way all hover info is contained in the former info node kinds
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
da4c46370d
feat: store elaborator declaration name in info tree
2021-06-21 10:17:26 -07:00
Sebastian Ullrich
b4e9ba1500
perf: specialize more monad instances
2021-06-17 11:25:58 +02:00
Sebastian Ullrich
b82b90a687
feat: KeyedDeclAttribute: expose declaration names
2021-06-06 15:32:58 +02:00
Leonardo de Moura
164b26bf01
fix: make sure the resulting array size is equal to the number of binders
...
The following code relies on this property
```lean
for uid in scope.varUIds, x in xs do
sectionFVars := sectionFVars.insert uid x
```
2021-05-04 19:46:14 -07:00
Leonardo de Moura
5c6b13ef9a
feat: MonadTrace instance for CommandElabM
2021-04-23 18:49:56 -07:00
Sebastian Ullrich
ccb873cea2
fix: panic on variable :
2021-04-23 09:24:35 +02:00
Sebastian Ullrich
60f2faefb7
feat: display placeholder & goal errors even on parse error
2021-04-17 23:46:15 +02:00
Sebastian Ullrich
e96a21631b
refactor: move elaboration error filtering into Elab.Command
...
Also make it dependent on presence of `missing` instead of parse error,
which means that messages from complete commands that are immediately followed
by parse errors are not filtered out anymore
2021-04-17 23:44:57 +02:00
Leonardo de Moura
dbc84c502c
chore: make sure we don't lift methods over binders
2021-04-15 12:06:46 -07:00
Leonardo de Moura
ac35b543bf
feat: add addional CompletionInfo
2021-04-03 11:17:51 -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
Sebastian Ullrich
3557d521d5
fix: don't unconditionally format InfoTrees in the server
2021-03-25 14:45:42 +01:00
Sebastian Ullrich
7b9ee8611c
fix: trace.Elab.Info in the server
2021-03-25 14:36:30 +01:00
Leonardo de Moura
99cd4fa720
feat: refine auto bound implicit locals
2021-03-23 17:33:15 -07:00
Sebastian Ullrich
c86f41a42b
feat: command-level info trees
2021-03-20 08:28:18 -07:00
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
1112ab6eff
chore: use new notation
2021-03-11 11:19:33 -08:00
Leonardo de Moura
ad68c5cbaa
refactor: polymorphic elabSetOption
2021-03-06 15:33:01 -08:00
Leonardo de Moura
8249620c9e
refactor: add polymorphic elabOpenDecl method
2021-03-06 15:32:59 -08:00
Leonardo de Moura
b6c388780f
chore: cleanup
2021-03-06 15:32:59 -08:00
Sebastian Ullrich
10bcd0bc9e
fix: #check_failure
2021-02-11 11:30:37 +01:00
Leonardo de Moura
6c119a1921
chore: use register_builtin_option
2021-01-26 18:24:56 -08:00
Leonardo de Moura
f53e83b182
feat: add options maxHeartbeats and synthInstance.maxHeartbeats
2021-01-24 17:45:50 -08:00
Sebastian Ullrich
446f953461
feat: allow hygienic capture of section variables in quotations
2021-01-24 11:46:04 -08:00
Sebastian Ullrich
8a02dfec4f
feat: subsume variables under variable
...
/cc @leodemoura
2021-01-22 14:36:05 +01:00
Leonardo de Moura
ea0fda39bc
chore: Declaration.lean naming convention
...
`Declaration.lean` was one of the first Lean 4 files, and was still
using an old naming convention.
cc @Kha
2021-01-20 17:07:02 -08:00
Sebastian Ullrich
a9f96ace3e
chore: naming
2021-01-20 16:48:50 +01:00
Leonardo de Moura
25c9727a92
feat: add TermInfo for LVal
...
@Vtec234 Added the missing info.
Given
```lean
def f3 (s : Nat × Array (Array Nat)) : Array Nat :=
s.2[1].push s.1
```
We produce the following `InfoTree` for the body (originally at line 30)
```
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨30, 2⟩-⟨30, 17⟩
s : Nat × Array (Array Nat) @ ⟨30, 2⟩-⟨30, 3⟩
Prod.snd : {α β : Type} → α × β → β @ ⟨30, 4⟩-⟨30, 5⟩
Array.getOp : {α : Type} → [inst : Inhabited α] → Array α → Nat → α @ ⟨30, 5⟩-⟨30, 6⟩
1 : Nat @ ⟨30, 6⟩-⟨30, 7⟩
Array.push : {α : Type} → Array α → α → Array α @ ⟨30, 9⟩-⟨30, 13⟩
s.fst : Nat @ ⟨30, 14⟩-⟨30, 17⟩
s : Nat × Array (Array Nat) @ ⟨30, 14⟩-⟨30, 15⟩
Prod.fst : {α β : Type} → α × β → α @ ⟨30, 16⟩-⟨30, 17⟩
```
2021-01-14 12:19:21 -08:00
Leonardo de Moura
873634be7e
feat: hierarchical InfoTree
2021-01-09 14:10:11 -08:00
Wojciech Nawrocki
238f5c1d70
feat: type info
2021-01-09 14:10:11 -08:00
Leonardo de Moura
43f258af3f
chore: cleanup
2021-01-05 17:23:50 -08:00
Leonardo de Moura
f0ac477d2e
feat: add sanity checks
2021-01-01 18:31:28 -08:00
Sebastian Ullrich
550d352bdc
feat: log output of #... auxiliary commands at command token
2020-12-27 14:33:02 +01:00
Leonardo de Moura
619885e745
feat: add throwMVarError!
2020-12-25 10:03:42 -08:00
Leonardo de Moura
9a8de1774c
chore: minor cleanup
2020-12-17 17:30:23 -08:00
Leonardo de Moura
f5d59ee287
fix: missing eraseMacroScopes at set_option
2020-12-13 15:51:00 -08:00
Leonardo de Moura
3b6d65c3c3
chore: use deriving Inhabited
2020-12-13 10:09:20 -08:00
Leonardo de Moura
5249fdc24d
chore: cleanup and style
2020-12-12 10:36:26 -08:00
Leonardo de Moura
0b8edeeadc
chore: use double quoted literals
2020-12-09 17:51:01 -08:00
Leonardo de Moura
e899b63def
feat: suppress "synthetic sorry" at #check
...
@Kha The message `sorryAx ?m : ?m` is content free.
2020-12-09 14:17:16 -08:00
Sebastian Ullrich
e6493755e9
chore: stdlib: match_syntax ~> match
2020-12-08 17:32:02 +01:00
Leonardo de Moura
d25f520143
feat: elaborate #reduce command
2020-12-06 10:54:57 -08:00
Leonardo de Moura
f15986a25d
fix: use levelMVarToParam at #check command
2020-12-06 09:28:41 -08:00
