Leonardo de Moura
c0e6314f14
fix(library/init/meta,library/tactic/elaborate): bad error position when to_expr is used outside of interactive mode
2017-02-09 18:44:50 -08:00
Leonardo de Moura
5e397795cf
fix(library/init/meta): focus tactic
...
This commit also add the interactive tactic 'focus'
2017-02-09 10:02:19 -08:00
Leonardo de Moura
32e6442d0a
feat(frontends/lean): no global universes in the frontend
2017-02-08 17:23:04 -08:00
Leonardo de Moura
c5dc8e651a
chore(library/init/meta): cleanup
2017-02-08 15:33:25 -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
a28d6a94fd
feat(library/init/meta): add any_goals tactic
2017-02-06 16:23:29 -08:00
Leonardo de Moura
ae06844f57
chore(library/init/meta): remove unnecessarily '| failed' annotations
...
tactic and smt_tactic are instaces of monad_fail
2017-02-05 20:12:42 -08:00
Leonardo de Moura
8b662d19ac
feat(library/init/category/monad_fail): add monad_fail type class
2017-02-05 18:46:29 -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
30a1876fc8
feat(library/init/meta): add add_aux_decl and abstract tactics
2017-02-05 16:00:47 -08:00
Gabriel Ebner
95068e4e79
feat(library/sorry): make sorry a macro
2017-02-05 14:01:03 +01:00
Rob Lewis
d18a47b588
feat(tactic): add tactic_format instances
2017-02-04 15:30:55 -08:00
Leonardo de Moura
b28ed2453e
feat(frontends/lean/definition_cmds): allow meta recursive definitions without recursive equations
2017-02-04 13:44:05 -08:00
Leonardo de Moura
aff5a2dd37
fix(library/init/meta): bug introduced 9bee8ce36d
2017-02-03 17:01:46 -08:00
Leonardo de Moura
bb9a0c79f4
feat(frontends/lean/builtin_exprs): better syntax for quoted terms with type ascription
2017-02-01 12:49:38 -08:00
Leonardo de Moura
6e7929252f
feat(frontends/lean, library/init): add 'thunk' gadget
...
We can now write
trace "hello" t
instead of
trace "hello" (fun _, t)
2017-01-31 18:41:59 -08:00
Leonardo de Moura
5da8b205b9
feat(library/type_context, frontends/lean/elaborator): type classes with output parameters
2017-01-30 18:32:54 -08:00
Leonardo de Moura
bf9f7560f7
feat(frontends/lean): (Type u) can't be a proposition
...
(Type u) is the old (Type (u+1))
(PType u) is the old (Type u)
Type* is the old (Type (_+1))
PType* is the old Type*
The stdlib can be compiled, but we still have > 70 broken tests
See discussion at #1341
2017-01-30 11:54:00 -08:00
Gabriel Ebner
5fdc737dfc
feat(library/tactic): store name of current declaration in tactic_state
2017-01-28 08:27:19 +01:00
Leonardo de Moura
b1d097e63a
feat(library/init/meta): add 'delta' tactic for applying delta reduction
...
closes #1331
2017-01-26 19:04:07 -08:00
Leonardo de Moura
b913ba3336
feat(library/init/meta): add type information for the arguments of the smt tactics: ematch_using and add_lemmas
2017-01-22 12:12:31 -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
4de71cadfa
feat(library/init/meta): expose additional app_builder tactics
2017-01-20 20:27:07 -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
Gabriel Ebner
fcc559a7f0
feat(library/init/util): add trace_call_stack function
2017-01-12 21:47:46 +01:00
Leonardo de Moura
d5c3736609
feat(library/init/meta/tactic): add helper tactic
2017-01-11 17:08:03 -08:00
Leonardo de Moura
e256022746
chore(library/init/meta/tactic): avoid the weird 'command' type when auto completing tactics
2017-01-10 14:59:10 -08:00
Leonardo de Moura
e96bbaee3f
fix(library/type_context): fix #1295
2017-01-10 11:54:38 -08:00
Leonardo de Moura
c29a2bdac9
feat(library/init/meta/tactic): add eta reduction tactic
2017-01-06 19:56:10 -08:00
Leonardo de Moura
d333c444cd
test(tests/lean/run): add tactic examples
2017-01-06 18:48:03 -08:00
Leonardo de Moura
858ce76e73
feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas
2017-01-04 20:31:38 -08:00
Leonardo de Moura
3adcf30d2f
feat(library/init/meta/smt_tactic): add assert/assertv/define/definev/pose/note for smt_tactic
2017-01-03 17:12:00 -08:00
Leonardo de Moura
35cc334b10
feat(library/init/meta): smt_tactic skeleton
2016-12-31 18:22:23 -08:00
Leonardo de Moura
b86494f0d4
feat(library/tactic): add destruct tactic that is similar to cases, but does not use revert/intro/clear
...
This tactic is useful for building more complex tactics using ematch and
cc because it does not invalidate cc_state nor ematch_state.
2016-12-30 17:05:24 -08:00
Leonardo de Moura
a0e9d38241
feat(library/init/meta/congruence_tactics): allow user to configure congruence_closure module
2016-12-30 12:42:10 -08:00
Leonardo de Moura
f3f1ec268b
chore(library/init/meta/tactic): make all arguments in id_locked explicit.
2016-12-26 18:22:37 -08:00
Leonardo de Moura
cc077554b5
fix(library/tactic/change_tactic): use id_locked in the change tactic to create checkpoint
...
closes #1260
2016-12-21 11:29:03 -08:00
Leonardo de Moura
b65c774f5b
chore(library/init/meta): opened_namespaces ==> open_namespaces
2016-12-18 23:55:45 -08:00
Leonardo de Moura
7d5b866503
feat(library/init/meta/tactic): add is_prop and is_proof tactics
2016-12-17 11:53:21 -08:00
Gabriel Ebner
6b15f6cef9
feat(library/tools/super): add super prover
2016-12-16 18:18:13 -08:00
Daniel Selsam
317989bf9e
feat(tactic/exact_tactic): exact_core that takes transparency
2016-12-13 08:27:21 -08:00
Leonardo de Moura
9f6e71b374
feat(library/tactic): add "approximate" parameter to apply_core and rewrite_core
...
If this parameter is set to true, then approximate unification is
used.
closes #1208
2016-12-10 10:24:05 -08:00
Jeremy Avigad
6f64244f2a
refactor(library/init/meta/tactic): switch 'pose' and 'note'
2016-12-08 13:17:42 -08:00
Leonardo de Moura
6577cc87a3
feat(library): add pre_monad
...
closes #1235
2016-12-08 12:48:55 -08:00
Leonardo de Moura
ed97ab486f
refactor(library/init): timeit, trace ==> util
2016-12-02 16:19:15 -08:00
Leonardo de Moura
00f5a807af
refactor(library/init): create init.category folder
2016-12-02 15:52:49 -08:00
Leonardo de Moura
e11fd8820a
refactor(library/init): create init.data folder
2016-12-02 14:23:06 -08:00
Leonardo de Moura
94c882f4d5
feat(library/documentation, frontends/lean): add /-! -/ doc string module block
2016-11-27 12:23:53 -08:00
Leonardo de Moura
6978906a78
chore(frontends/lean): remove namespace documentation
...
We will add module level doc strings /-! -/
2016-11-27 11:57:03 -08:00
