Leonardo de Moura
146eaf5281
fix(library/tactic/tactic_state): has_to_format universe changed
...
see #1341
2017-01-30 11:54:00 -08:00
Leonardo de Moura
c8542bd77c
fix(library/norm_num): bug when creating eq.refl
...
The universe parameter was missing.
see #1341
2017-01-30 11:54:00 -08:00
Leonardo de Moura
a6f26f0b74
chore(library): poly_unit ==> punit
...
psum, pprod and punit are used internally.
see #1341
2017-01-30 11:54:00 -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
Leonardo de Moura
0e3a8758dc
fix(library/equations_compiler/structural_rec): bug when synthesizing equational lemmas
2017-01-30 11:51:07 -08:00
Gabriel Ebner
952f444710
feat(init/meta/task): allow task creation from VM
2017-01-28 08:27:23 +01: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
9107439bce
feat(frontends/lean/elaborator): default parameter prototype
...
See #1340
2017-01-27 16:32:22 -08: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
6f502b9afd
fix(library/vm): make sure vm_rb_map objects can be stored in ts_vm_obj
...
See discussion at #1337
2017-01-26 15:58:11 -08:00
Leonardo de Moura
4e625b35ad
fix(library/vm/vm): memory leak at operator=
2017-01-26 13:32:44 -08:00
Leonardo de Moura
89daecb568
fix(library/type_context): assertion violation
...
fixes #1335
2017-01-25 16:05:23 -08:00
Leonardo de Moura
552ca66e9e
feat(library/init/meta/pexpr): expose low level function mk_placeholder
2017-01-25 15:32:50 -08:00
Leonardo de Moura
258fb522d3
feat(library/tactic/smt): add generation heuristic to control matching loops
2017-01-24 22:46:45 -08:00
Leonardo de Moura
477ffd1bc7
fix(library/tactic/smt): make sure a partially applied terms can be used to ematch terms with "more arguments"
2017-01-24 19:25:00 -08:00
Leonardo de Moura
434ada7dcc
chore(library/vm,library/tactic): add missing override
2017-01-24 16:19:36 -08:00
Leonardo de Moura
ac6bfce01c
feat(library/tactic/smt/congruence_closure): improve propagation for beta reduction in the congruence closure module
2017-01-24 12:09:37 -08:00
Leonardo de Moura
28ce1e6d2b
fix(library/tactic/simplify): make sure a partially applied lhs can be used to rewrite terms with "more arguments" in simp
...
See discussion at issue #1331
2017-01-23 19:53:49 -08:00
Leonardo de Moura
f60bbb5fcb
fix(library/tactic/simp_lemmas): refl_lemma_rewrite, make sure a partially applied lhs can be used rewrite terms with "more arguments"
2017-01-23 19:37:35 -08:00
Leonardo de Moura
418d62ff48
fix(library/tactic/rewrite_tactic): fixes #1277
2017-01-23 16:34:07 -08:00
Leonardo de Moura
2ca2920284
fix(library/tactic/simplify): relax test
...
We only need to check whether the resulting expression does not contain
temporary metavariables introduced by the simplifier.
It is ok if it contains regular metavariables that were already in the goal.
This fixes the issue reported at
https://groups.google.com/forum/#!topic/lean-user/3qzchWkut0g
2017-01-23 09:59:06 -08:00
Gabriel Ebner
b0c67abb2f
feat(library/vm/vm_aux): add vm code for sorry
2017-01-22 14:18:38 -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
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
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
0adae9d7c7
chore(library/pp_options): default pp.beta = false
2017-01-20 05:25:28 -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
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
Gabriel Ebner
0d949e0da7
chore(library/module_mgr): explain exceptional case
2017-01-17 17:10:37 -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
Leonardo de Moura
3178f41cce
fix(library/compiler/inliner): applications of definitions marked as [inline] are inlined even if they are not fully applied
...
see #1316
2017-01-17 16:33:19 -08:00
Gabriel Ebner
b4774e9ed1
fix(library/vm/vm): fix segfault in call_stack_fn
2017-01-17 16:00:01 -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
7a210a9b62
chore(library/util): style
2017-01-16 22:59:17 -08:00
Leonardo de Moura
fc00275636
fix(library/compiler/elim_recursors): it was assuming that recursive arguments occur after non recursive ones
2017-01-16 22:59:17 -08:00
Leonardo de Moura
70b7a35cfe
fix(library/constructions/has_sizeof): it was assuming that recursive arguments occur after non recursive ones
2017-01-16 22:59:17 -08:00
Leonardo de Moura
29b7001bff
fix(library/equations_compiler/elim_match): avoid nasty inferred types in auxiliary declarations produced by the equation compiler
2017-01-16 22:55:12 -08:00
Leonardo de Moura
cce6e4d58c
fix(library/equations_compiler/compiler): fix #1315
2017-01-16 20:01:25 -08:00
Leonardo de Moura
eabbc5bb68
chore(library/module_mgr): comment unreachable_code assertion
...
@gebner, could you please take a look a check whether there is a better fix.
2017-01-15 23:18:44 +01:00
Leonardo de Moura
67226269b4
feat(library/tactic/simp_lemmas): convenient way of adding equational lemmas of a definition to a simp set
2017-01-14 22:16:16 -08:00
Leonardo de Moura
6a5d3ed0e5
feat(library/vm/vm_string): use check_system to avoid stack overflow
2017-01-13 17:06:24 -08:00
Leonardo de Moura
05d86e49ca
feat(library/init/meta/smt): add intros variants for smt_tactic
2017-01-13 16:13:37 -08:00
Leonardo de Moura
db646dda89
fix(library/tactic/smt/smt_state): forgot to set zeta option
2017-01-13 13:33:47 -08:00
Scott Morrison
6f8fc0fe06
fix(library/scoped_ext): typo in error message
2017-01-13 11:33:17 -08:00
Sebastian Ullrich
b180c54c0e
feat(shell): move lean.js to server mode
2017-01-13 07:34:54 -08:00
Leonardo de Moura
c1ecaf4edd
feat(library/tactic/smt/smt_state): do not apply intros automatically in begin[smt]...end blocks
2017-01-12 21:49:17 -08:00
