Leonardo de Moura
80d0b8d5f5
chore(library,shell): fix style
2017-01-10 09:00:17 -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
2b374cd517
fix(emacs/lean-company): do not highlight prefix of non-prefix match
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
481a217722
feat(shell/completion): prefer exact prefix matches for all completion modes
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
cc3126e944
feat(frontends/lean,library/scoped_ext,shell): complete namespaces
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
fb294f4415
chore(shell/server): info: skip "record" output field if null
2017-01-10 12:25:33 +01:00
Sebastian Ullrich
3c89a79144
feat(shell/completion): sort completions alphabetically (secondary)
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
Sebastian Ullrich
7ef1bd1a15
chore(tests/lean/interactive): simplify input format and test full completion output
2017-01-10 12:25:33 +01:00
Leonardo de Moura
c726f19d32
fix(library/tactic/smt/ematch): warning
2017-01-09 19:28:36 -08:00
Leonardo de Moura
3acdcaef2c
fix(library/tactic/smt/smt_state): ematch_using should not fail when a ground fact was added but no instance
2017-01-09 19:24:13 -08:00
Leonardo de Moura
5d750ba0a4
fix(library/tactic/tactic_state): closes #1293
2017-01-09 16:23:02 -08: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
b526e30c55
fix(library/compiler/cse): common subexpressions inside common subexpressions were not being eliminated
2017-01-09 11:11:55 -08:00
Leonardo de Moura
694bb5c7b8
feat(library/tactic/smt/ematch): skeleton for AC support
2017-01-08 23:53:57 -08:00
Leonardo de Moura
0a6a09fb3a
fix(library/tactic/smt/hinst_lemmas): pattern normalization issue
2017-01-08 23:35:39 -08:00
Leonardo de Moura
5ba414700f
fix(library/tactic/smt/smt_state): canonize at intros
2017-01-08 19:31:04 -08:00
Leonardo de Moura
7ff91ec1ef
feat(library/defeq_canonizer): add trace.defeq_canonizer
2017-01-08 19:31:04 -08:00
Leonardo de Moura
26949db4f1
fix(library/tactic/smt/smt_state): remove auxiliary hypotheses added by the equation compiler
2017-01-08 10:36:38 -08:00
Leonardo de Moura
9d273d924f
fix(library/tactic/smt/congruence_closure): must check whether constructors have the same type or not
2017-01-08 00:36:57 -08:00
Leonardo de Moura
8a12c834ca
fix(library/tactic/smt/ematch): ematch should not use app_builder since its type_context is already in tmp_mode
2017-01-07 17:06:12 -08:00
Leonardo de Moura
de60233ef1
fix(library/tactic/smt/congruence_closure): subsingleton propagation was introducing non canonical instances
2017-01-07 16:16:36 -08:00
Leonardo de Moura
0c4c41ae54
feat(library/init/meta): produce nicer error message for overloaded simp/ematch lemma
2017-01-07 14:13:46 -08:00
Leonardo de Moura
8e315c61e3
fix(library/util): is_eq was returning true for partially applied terms
...
This commit also cleanups many of the is_* predicates
2017-01-07 13:35:53 -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
8069872861
fix(library/tactic/backward/backward_chaining): bug in back_chaining tactic
2017-01-07 11:19:03 -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
da945e34de
perf(library/equations_compiler/util, library/local_context): preserve instance fingerprint and avoid flushing the cache
2017-01-07 00:17:09 -08:00
Leonardo de Moura
ff455d3ec9
chore(library/vm/vm): warning
2017-01-06 21:22:27 -08:00
Leonardo de Moura
8c652600dd
feat(library/tactic/smt/smt_state): ematch tactics fail if no instance is produced
...
The goal is to avoid nontermination of (repeat {ematch}) when the goal
is not provable. Of course, if there is a matching loop, it will still loop.
2017-01-06 21:20:01 -08:00
Leonardo de Moura
d81acfc44a
feat(library/tactic/smt/smt_state): use eta reduction in the smt preprocessor
2017-01-06 20:23:41 -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
36453b894d
fix(library/print): avoid numerical internal names in the pretty printer
2017-01-06 19:27:31 -08:00
Leonardo de Moura
de8ba72a86
feat(library/vm/vm): suppress snapshots when printing profiling information
2017-01-06 19:22:07 -08:00
Leonardo de Moura
93c8e69313
chore(frontends/lean, library): cleanup anonymous instance management
2017-01-06 14:37:44 -08:00
Leonardo de Moura
b86aef1ff0
feat(shell/completion): do not show internal declarations
2017-01-06 14:14:43 -08:00
Leonardo de Moura
44ef2f4eeb
feat(shell/completion): only filter class projections
2017-01-06 14:06:17 -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
Gabriel Ebner
7770e87f69
fix(emacs/lean-server): disable undo and hide process buffers
2017-01-06 14:01:50 -08:00
Leonardo de Moura
5e3f26ec95
feat(library/tactic/smt/congruence_closure): propagate not_exists
2017-01-06 14:00:36 -08:00
Leonardo de Moura
d5da18299b
feat(library/private): make sure the private prefix is an internal name
2017-01-06 11:48:05 -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
Gabriel Ebner
6f8ccb5873
fix(CMakeLists): emscripten: pass compiler flags to gmp and mpfr as well
2017-01-06 01:04:36 -08:00
Gabriel Ebner
70e41305e5
fix(module_mgr): produce olean files with correct mtimes
2017-01-06 01:04:18 -08:00
Leonardo de Moura
15eaf30192
feat(library/tactic/smt/smt_state): allow user to provide a function ("to be unfolded") in the ematch_using tactic
2017-01-06 00:33:58 -08:00
