Leonardo de Moura
9ed9de18bf
feat(frontends/lean/parser): relax pattern validation rules
2017-01-20 18:38:14 -08:00
Leonardo de Moura
c52be7e8c5
feat(frontends/lean,shell): autocompletion for ^.
...
@kha, I added autocompletion for ^. I try to elaborate the expression
before ^. using the local context provided by the parser.
The autocompletion only works if the type for the expression before ^. can be
inferred. This is a big limitation because this information cannot be
obtained in many cases. Here are examples that do not work:
meta def proof_for (e : expr) : smt_tactic expr :=
do cc ← to_cc_state, cc^.proof_for e
--^ does not work here
If we annotate cc with its type, it works:
meta def proof_for (e : expr) : smt_tactic expr :=
do cc : cc_state ← to_cc_state, cc^.proof_for e
--^ works
We don't have typing information on the equation lhs at
autocompletion time. So, the following will not work
private meta def mk_smt_goals_for (cfg : smt_config)
: list expr → list smt_goal → list expr → tactic (list smt_goal × list expr)
| [] sr tr := return (sr^.reverse, tr^.reverse)
--^ does not work since
| (tg::tgs) sr tr := ...
2017-01-17 19:27:59 -08:00
Gabriel Ebner
a230c47178
feat(util/task_queue,emacs,*): highlight running tasks with different background color
2017-01-17 17:10:37 -08:00
Sebastian Ullrich
484bb67d44
fix(frontends/lean/tactic_notation): report state after tactic execution on ,
2017-01-17 16:38:00 -08:00
Sebastian Ullrich
6acc2cf8b7
fix(frontends/lean/notation_cmd): some position fixes
2017-01-17 16:38:00 -08:00
Gabriel Ebner
1a6629ce3b
feat(frontends/lean/parser): keep list of tasks that have to succeed
2017-01-17 15:31:17 -08:00
Leonardo de Moura
bfa48ff0c7
fix(frontends/lean/parser): position info when error is inside notation
2017-01-16 10:29:00 -08:00
Sebastian Ullrich
222952d5b8
chore(frontends/lean/scanner): another CLion fix
2017-01-13 07:34:54 -08:00
Leonardo de Moura
30cea2dceb
fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions.
...
The new test exposes the problem.
2017-01-12 18:38:31 -08:00
Gabriel Ebner
b5ac381a5e
chore(frontends/lean/print_cmd): update print command to keyword changes
2017-01-12 12:04:37 -08:00
Leonardo de Moura
7e1db95c79
fix(frontends/lean): doc strings after constants and axioms
2017-01-12 00:22:37 -08:00
Gabriel Ebner
db81e4b5b8
feat(frontends/lean/parser): gracefully handle scanner exceptions in imports
2017-01-11 23:49:44 -08:00
Leonardo de Moura
df91ae3738
fix(library/string,library/init/data/to_string): handle ASCII control characters
2017-01-11 23:44:33 -08:00
Leonardo de Moura
acef1efb86
fix(frontends/lean/pp,library/equations_compiler,library/tactic/smt/congruence_closure): bug at to_char function
2017-01-11 23:44:25 -08:00
Leonardo de Moura
ae56c6d322
feat(frontends/lean/builtin_cmds): improve error message when import is used in the middle of the file
2017-01-11 11:15:29 -08:00
Sebastian Ullrich
83bddce900
feat(frontends/lean/info_manager,shell/server,emacs/lean-type): info: provide more metadata
...
* docs: attributes, options, identifiers
* location: attributes, imports
2017-01-11 15:29:14 +01:00
Leonardo de Moura
19e20f7e1a
fix(frontends/lean/elaborator): universe elaboration issue
2017-01-10 22:35:12 -08:00
Sebastian Ullrich
e0ebe9f4a8
fix(frontends/lean/tactic_evaluator): show VM errors on tactic
2017-01-10 14:42:48 -08:00
Sebastian Ullrich
ed4275ae17
fix(frontends/lean/builtin_cmds): do not complete after namespace
...
Most identifiers used with the command are not namespaces yet
2017-01-10 14:42:48 -08:00
Sebastian Ullrich
8eb39bb982
fix(frontends/lean/parser): catch exceptions thrown by sync_command
2017-01-10 14:42:48 -08:00
Leonardo de Moura
00c89f209c
fix(frontends/lean/definition_cmds): fix #1299
2017-01-10 14:38:46 -08:00
Sebastian Ullrich
3ae4d0fbee
feat(shell/completion,emacs/lean-company): provide doc string and location with completion candidate
2017-01-10 16:19:32 +01:00
Sebastian Ullrich
cc3126e944
feat(frontends/lean,library/scoped_ext,shell): complete namespaces
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
b04df04120
feat(frontends/lean): rework and simplify completion parsing, enabling completion of empty prefixes
2017-01-10 12:25:33 +01:00
Leonardo de Moura
7a150b41b9
fix(frontends/lean): fixes #1292
2017-01-09 15:53:37 -08:00
Leonardo de Moura
7d540b6d02
fix(frontends/lean/parser): fixes #1290
2017-01-09 15:35:25 -08:00
Leonardo de Moura
299751982b
fix(frontends/lean/tactic_evaluator): 'begin [smt] ... end' block nested in regular one
2017-01-07 13:35:43 -08:00
Leonardo de Moura
94f16d1e44
refactor(library/tactic): move defeq_canonizer::state to tactic_state
...
It was being stored in the environment before. This was very hackish,
and it was producing a series of unnecessary environment updates, and
thread local caches invalidations.
The new test tests/lean/run/heap.lean is 5x-6x faster after this commit.
2017-01-07 10:17:51 -08:00
Leonardo de Moura
93c8e69313
chore(frontends/lean, library): cleanup anonymous instance management
2017-01-06 14:37:44 -08:00
Sebastian Ullrich
26e2aeec7a
feat(frontends/lean,shell): complete attributes
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
2816d3a036
feat(frontends/lean,shell): complete interactive tactics
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
7040844f9a
feat(frontends/lean/parser,shell): complete imports
2017-01-06 14:02:31 -08:00
Sebastian Ullrich
3136f36ed6
fix(frontends/lean/parser): complete after periods trailing identifiers
2017-01-06 14:02:31 -08:00
Leonardo de Moura
db70c78704
feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names
2017-01-06 11:40:34 -08:00
Leonardo de Moura
31a0d7d520
feat(frontends/lean/elaborator): catch exception at is_def_eq
...
@semorrison this commit improves the bad error message you have
reported at lean-user. It is not perfect since the user has to
remember the position of the structure field in the constructor.
2017-01-06 08:16:51 -08:00
Leonardo de Moura
7ba889b5cf
feat(frontends/lean/tactic_notation): try/repeat for smt_tactic in interactive mode
2017-01-05 18:31:57 -08:00
Gabriel Ebner
063130ee18
feat(kernel/environment): add function that checks whether all proofs are correct
2017-01-05 18:09:28 -08:00
Gabriel Ebner
90ab29d7a3
chore(CMakeLists): rename misleading LEAN_SERVER option
2017-01-05 18:08:59 -08:00
Leonardo de Moura
82f8eeb280
feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler
2017-01-05 18:02:14 -08:00
Leonardo de Moura
eeab242595
feat(frontends/lean/elaborator): catch error early
2017-01-05 13:37:55 -08:00
Leonardo de Moura
b0de6723ec
feat(frontends/lean/tactic_evaluator): better error message
2017-01-05 13:32:59 -08:00
Gabriel Ebner
9435762643
fix(compiler/vm_compiler): only compile computable non-builtin definitions
2017-01-04 16:30:22 -08:00
Leonardo de Moura
eeb8237b04
feat(frontends/lean): 'begin [smt] ... end' blocks nested inside regular 'begin ... end' blocks
2017-01-04 15:35:46 -08:00
Leonardo de Moura
2e15304f05
feat(frontends/lean): add support for smt_state in the info_manager
2017-01-04 14:23:48 -08:00
Leonardo de Moura
5f2b247af9
feat(frontends/lean/tactic_evaluator): step-by-step evaluation for 'begin [smt] ... end' blocks
2017-01-04 14:06:44 -08:00
Leonardo de Moura
d53215a2fb
feat(frontends/lean/tactic_notation, library/init/meta/smt): add by_cases and by_contradiction smt_tactics, support for classical reasoning, add support for 'begin [smt] with config, ... end'
2017-01-04 12:03:45 -08:00
Leonardo de Moura
59f3c9775a
feat(frontends/lean/tactic_notation): add support for begin [smt] ... end blocks
...
TODO: add support for inspecting intermediate states.
2017-01-04 11:13:00 -08:00
Leonardo de Moura
3a62ca0581
refactor(library/init/meta): move smt tactics to library/init/meta/smt, and add interactive definitions
2017-01-04 09:36:50 -08:00
Leonardo de Moura
d6ab3739ff
refactor(frontends/lean/elaborator): move tactic executation code to tactic_evaluator
2017-01-04 08:42:59 -08:00
Leonardo de Moura
0319fd5728
refactor(frontends/lean/elaborator): move pos_string_for
2017-01-04 07:32:44 -08:00
