Leonardo de Moura
a61cf4d08b
feat(library/init/meta/interactive): show type information for simp, dsimp arguments
2017-01-22 12:05:51 -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
7a6b9e193c
feat(library/vm, frontends/lean/info_manager): add thread safe vm_obj wrapper, and use it to store arbitrary vm thunks in the info_manager
2017-01-21 22:38:33 -08:00
Leonardo de Moura
a6f120b5e7
fix(frontends/lean/parser): uninitialized variable
2017-01-21 22:38:33 -08:00
Leonardo de Moura
37bc2133ec
fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching
...
fixes #1327
2017-01-21 22:38:17 -08:00
Leonardo de Moura
0913a7e719
feat(library/tactic/dsimplify): add trace msgs for dsimp
2017-01-21 03:12:28 -08:00
Leonardo de Moura
d9528ffad8
chore(library/init/data/nat/lemmas): add comment
2017-01-21 03:11:59 -08:00
Gabriel Ebner
d4879b74cd
chore(tests/lean/run/destruct): fix test
2017-01-21 10:28:46 +01:00
Gabriel Ebner
03e09db70e
refactor(library/data/bitvec,library/data/tuple): use automation
2017-01-21 09:48:35 +01:00
Leonardo de Moura
9c9cad6ae8
test(tests/lean/interactive): add regression test for #1313
2017-01-20 21:48:19 -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
Leonardo de Moura
a357c0cab2
chore(tests/lean): fix tests
2017-01-20 20:35:18 -08:00
Leonardo de Moura
c359eba509
feat(tests/lean): add test to make sure simplifier did not introduce unwanted propext
2017-01-20 20:28:49 -08:00
Leonardo de Moura
e8839cbcdc
feat(library/app_builder): add mk_eq_mpr that removes unnecessary propext
2017-01-20 20:27:41 -08:00
Leonardo de Moura
4de71cadfa
feat(library/init/meta): expose additional app_builder tactics
2017-01-20 20:27:07 -08:00
Leonardo de Moura
f079d05fc2
chore(tests/lean): adjust tests to recent changes
2017-01-20 19:08:41 -08:00
Leonardo de Moura
4e6ad1d34d
fix(library/init/meta/contradiction_tactic): make sure contradiction uses whnf for constructor-eq-constructor case
2017-01-20 18:42:27 -08:00
Leonardo de Moura
c62014df7a
chore(frontends/lean/parser): style
2017-01-20 18:38:58 -08:00
Leonardo de Moura
bbc99d4aa5
feat(library/data/tuple): make sure tuple.nil and tuple.cons can be used in patterns
2017-01-20 18:38:34 -08:00
Leonardo de Moura
9ed9de18bf
feat(frontends/lean/parser): relax pattern validation rules
2017-01-20 18:38:14 -08:00
Leonardo de Moura
0adae9d7c7
chore(library/pp_options): default pp.beta = false
2017-01-20 05:25:28 -08:00
Leonardo de Moura
dae1c9dac2
chore(CMakeLists): make sure we change the version number in a single place
2017-01-19 18:28:51 -08:00
Sebastian Ullrich
3f65690706
feat(emacs/lean-server): print out entire server response on error
2017-01-19 17:50:36 -08:00
Sebastian Ullrich
cc1553d901
fix(emacs/lean-server): dump response before trying to parse it
2017-01-19 17:50:36 -08:00
Sebastian Ullrich
4cba998de3
fix(CMakeLists): minimum g++ version is 4.9
2017-01-19 17:50:36 -08:00
Gabriel Ebner
ecdd17738d
feat(emacs): add toggle for pending task highlight
2017-01-19 17:49:35 -08:00
Leonardo de Moura
e8e483534b
chore(library/init/meta/decl_cmds): remove unused parameter
2017-01-18 19:44:16 -08:00
Leonardo de Moura
0795acaf6a
refactor(library/init/algebra): new transport from multiplicative to additive
...
The motivation is to avoid the problems produced by the "declare as
structure and then tag as class idiom" described in the file ring.lean.
2017-01-18 19:39:53 -08:00
Leonardo de Moura
d0a578c3db
feat(library/init/meta/environment): add is_projection
2017-01-18 18:12:08 -08:00
Leonardo de Moura
0ad053f0f1
feat(library/init/meta/decl_cmds): add command for copying type and value using replacement
2017-01-18 17:52:11 -08:00
Gabriel Ebner
bf20be51d5
chore(emacs/lean-server): put face into lean group for customization
2017-01-18 08:32:53 -08:00
Gabriel Ebner
be6b81db07
chore(emacs): remove lean-flycheck-use option
2017-01-18 08:32:53 -08:00
Gabriel Ebner
9b63ceff91
chore(emacs/lean-project): remove old project file contents
2017-01-18 08:32:53 -08:00
Gabriel Ebner
9530a7db1c
chore(emacs): remove unused options
2017-01-18 08:32:53 -08:00
Leonardo de Moura
b309ef66d7
fix(library/equations_compiler/elim_match): fix #1318
2017-01-18 08:21:53 -08:00
Leonardo de Moura
694e6f47dc
fix(library/init/meta/smt/ematch,library/tactic/simp_lemmas): trick for adding equations of a definition to a simp/hinst lemma set
...
Before this commit, if we declared an equational lemma using 'def',
then it would not be correctly added to the simp/hinst lemma set.
The new test exposes the problem.
2017-01-18 02:05:04 -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
Leonardo de Moura
97b98c58d0
refactor(library): move nat lemmas to library/init/data/nat/lemmas.lean
2017-01-17 17:42:13 -08:00
Joe Hendrix
767ac42dfe
chore(library/data): remove redundent decidable_eq instances
2017-01-17 17:34:10 -08:00
Joe Hendrix
5bc5013f16
chore(library/data/bitvec): remove leftover code
2017-01-17 17:34:05 -08:00
Joe Hendrix
985c3697b9
chore(library/data/list): add back copyright notice
2017-01-17 17:33:59 -08:00
Joe Hendrix
24fc68cef4
feat(library/init/category/combinators.lean): add foldl and when
2017-01-17 17:33:50 -08:00
Joe Hendrix
8e2cf491e5
refactor(library/data/list): move theorems to separate modules per lean2
2017-01-17 17:33:45 -08:00
Joe Hendrix
3de9e722e1
feat(library/data/bitvec): additional definitions
2017-01-17 17:33:37 -08:00
Joe Hendrix
d52c3327ba
feat(library/data/nat/sub): additional theorems
2017-01-17 17:33:32 -08:00
Joe Hendrix
f244c0e70a
feat(library/data/bitvec): add bitvec version of tuple.append
2017-01-17 17:33:24 -08:00
Joe Hendrix
de92ea658a
feat(library/data/tuple): add decidable_eq to tuple
2017-01-17 17:33:17 -08:00
Joe Hendrix
9781a0414c
feat(library/data/list): add has_decidable_eq to list.
2017-01-17 17:33:09 -08:00
Joe Hendrix
18cbc22791
refactor(library/data/nat): migrate data.nat to lean2 structure
2017-01-17 17:24:37 -08:00
Gabriel Ebner
0d949e0da7
chore(library/module_mgr): explain exceptional case
2017-01-17 17:10:37 -08:00
