Sebastian Ullrich
421a6d6f01
feat(frontends/lean/interactive,emacs): highlight current tactic parameter
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
24e7e87f7d
feat(frontends/lean/tactic_notation): fall back to tactic info when hovering over/between parameters
2017-03-17 18:20:44 -07:00
Sebastian Ullrich
16558bf082
refactor(library,library): rename pre_monad to has_bind
2017-03-09 20:32:25 -08:00
Sebastian Ullrich
5d68938a9c
feat(frontends/lean): expr literals ```(...)
2017-03-05 08:37:16 -08:00
Sebastian Ullrich
a053175714
refactor(init/meta,library/vm): use structure for position information
2017-02-21 11:06:39 -08:00
Leonardo de Moura
0d22410e2e
feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode
2017-02-19 12:11:22 -08:00
Sebastian Ullrich
4d41b03168
chore(frontends/lean,library/tactic): remove old tactic_state functions
2017-02-17 15:41:58 +01:00
Sebastian Ullrich
9d8c84713c
refactor(*): reduce exception context info from expr to pos_info
2017-02-17 13:45:57 +01:00
Sebastian Ullrich
d15591a2d8
feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters
2017-02-17 13:45:56 +01:00
Leonardo de Moura
9210e45da0
feat(frontends/lean): add notation for ';' and '<|>' in the tactic interactive mode
2017-02-10 22:53:30 -08:00
Leonardo de Moura
6334ff24eb
fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...]
...
See new test for understanding the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2017-02-09 19:06:56 -08:00
Leonardo de Moura
54f7bf9391
fix(frontends/lean, library/tactic): remove redundant error messages, and fix position of error messages
...
Summary:
We minimize the number of "'sorry' used warning messages". We also
re-target the error to the main declaration. Example: foo._main ==> foo
We do not report for auxiliary declarations such as "_example" and
"foo.equations._eqn_1"
Get rid of the redundant error message "error : failed" for tactics.
We added "silent failures" in the tactic framework.
We do not store line/col information for tactics nested in notation
declarations. Before this commit, we would have tactics such
as (tactic.save_info line col) nested inside of notation declarations.
2017-02-07 20:25:28 -08:00
Leonardo de Moura
797b26f402
fix(frontends/lean/tactic_notation): trace messages in nested blocks were not being displayed in the correct place
2017-02-05 18:20:10 -08:00
Leonardo de Moura
d34386fef7
perf(frontends/lean/tactic_notation): closes #1345
...
We can now elaborate
https://gist.github.com/gebner/439273deee592603190d4f8b4447295b
in 1.6 secs and using less than 500Kb of stack space.
It was takins 44 secs and 5Mb before this commit.
Two modifications:
1) Use pre_monad.seq instead of pre_monad.and_then.
They have the same implementation, but seq is not marked as [inline].
2) Modify how we concatenate the tactics in a begin...end block.
Before: (((a_1 ++ a_2) ++ a_3) ++ a_4)
After: ((a_1 ++ a_2) ++ (a_3 ++ a_4))
2017-01-30 14:13:53 -08:00
Leonardo de Moura
cce88c6190
refactor(frontends/lean): interactive tactic support
...
After this commit, new interactice tactic classes can be added without
writing C++ code (see example: tests/lean/run/my_tac_class.lean).
The tactic_evaluator was simplified, and all the complexity has been
moved to tactic_notation, and lean code.
We can now inspect the intermediate states produced by the rewrite
tactic.
The function (@scope_trace _ line col thunk) can be used to position trace
messages produced by thunk. If line/col are not provided (i.e., we
just write (scope_trace thunk)), then line/col are filled with the
position of this term by the elaborator.
We can visualize the intermediate tactic states inside nested blocks
such as (try { ... })
The new infrastructure can be used to implement custom tactic_state
pretty printers.
2017-01-21 22:38:47 -08:00
Leonardo de Moura
e2bf4fcddb
fix(frontends/lean/tactic_notation): add skip tactic to save intermediate result
...
@kha, this commit fixes the issue: comma before a `{}` block will show the state inside the block.
2017-01-20 20:58:05 -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
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
Sebastian Ullrich
2816d3a036
feat(frontends/lean,shell): complete interactive tactics
2017-01-06 14:02:31 -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
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
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
d24577c57c
fix(frontends/lean/tactic_notation): remove problematic code for get_begin_end_block_elements
2017-01-03 22:38:03 -08:00
Leonardo de Moura
e6f6c6bb3a
fix(frontends/lean/tactic_notation): typo
2017-01-03 22:15:22 -08:00
Leonardo de Moura
493be76afe
feat(frontends/lean/tactic_notation): add support for other tactic types
...
TODO: we still need to add support in the elaborator.
2017-01-03 22:11:45 -08:00
Leonardo de Moura
46a3aacc17
fix(frontends/lean): begin...end block scope
2017-01-03 21:01:14 -08:00
Leonardo de Moura
5d825483c4
refactor(library/init/meta/interactive): tactic.interactive.types ==> interactive.types
...
Motivation: we will use auto-quotation for other tactic monads
2016-12-30 18:06:41 -08:00
Sebastian Ullrich
daf839e0d5
feat(frontends/lean,shell/server): report current goal anywhere within begin-end/by
2016-12-27 10:07:34 -08:00
Leonardo de Moura
ffc9c75824
fix(frontends/lean/parser): do not clear local universes when switching to tactic mode and/or quoting
2016-12-19 09:21:54 -08:00
Leonardo de Moura
6577cc87a3
feat(library): add pre_monad
...
closes #1235
2016-12-08 12:48:55 -08:00
Leonardo de Moura
e237109434
fix(frontends/lean/tactic_notation): do not store position information for auxiliary terms introduced by the interactive mode
...
The idea is to prevent unwanted type information at lean-mode.
For example, before this commit, we would get "list.nil : ..." type
info whenever we hovered over the "end" of a "begin...end" block.
2016-12-02 09:53:24 -08:00
Leonardo de Moura
e1a90fbe89
fix(frontends/lean/tactic_notation): fixes #1207
2016-12-01 17:16:22 -08:00
Leonardo de Moura
2309e35296
fix(frontends/lean): position information for by tac
...
Now, Ctrl-c-Ctrl-g also works when hovering the beginning of the tactic
instead of the beginning of the `by` token.
The idea is to make the behavior consistent with `begin...end` blocks.
2016-11-29 17:08:10 -08:00
Leonardo de Moura
ed2a507dd9
fix(frontends/lean/tactic_notation): assertion violation
2016-11-18 17:39:25 -08:00
Leonardo de Moura
88d2f07567
feat(frontends/lean/tactic_notation): switch to proof-term mode when calc/suppose/assume/have/show occurs in a tactic block
2016-11-18 16:57:31 -08:00
Leonardo de Moura
29e5464e42
fix(frontends/lean/tactic_notation): fix minor problem for info at position
...
See comment for details.
2016-11-10 13:48:35 -08:00
Leonardo de Moura
c0022253a7
feat(frontends/lean/tactic_notation): allow lemmas to be removed
2016-09-30 19:53:51 -07:00
Leonardo de Moura
fd6dc8154a
feat(library/init/meta/interactive): add interactive tactics
2016-09-30 19:02:45 -07:00
Leonardo de Moura
d627011786
feat(frontends/lean/tactic_notation): do is tactic unit in begin end blocks.
2016-09-30 16:35:45 -07:00
Leonardo de Moura
051b6bd026
feat(frontends/lean/tactic_notation): add notation for entering auto-quotation mode
2016-09-30 16:18:52 -07:00
Leonardo de Moura
9ea858e6fe
feat(frontends/lean/tactic_notation): nested interactive tactics
2016-09-30 14:53:07 -07:00
Leonardo de Moura
23ce2b0587
feat(frontends/lean/tactic_notation, library/init/meta/interactive): add "interactive" versions of define/assert/definev/assertv/note tactics
2016-09-29 18:48:32 -07:00
Leonardo de Moura
c8a720212b
feat(frontends/lean): 'by' is now also using interactive mode syntax
2016-09-29 01:57:40 -07:00
