Leonardo de Moura
552a185e6a
feat(frontends/lean): 'let' in 'do' blocks
2017-02-24 09:10:36 -08:00
Sebastian Ullrich
dd379e5b34
refactor(library/equations_compiler/elim_match): simplify is_complete_transition
2017-02-23 01:52:14 +01:00
Sebastian Ullrich
dfe1874365
refactor(frontends/lean/{parser,util}): extract quote functions
...
Also fixes ``f when f is private
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
1c7ca3f20a
feat(frontends/lean/parser): ignore implicit arguments in expr patterns
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
44b27a9a44
chore(library/vm/vm): fix comment
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
908a7bd9f3
feat(frontends/lean/parser): expr patterns
2017-02-23 01:52:13 +01:00
Sebastian Ullrich
3aa9e32c5f
fix(library/equations_compiler/elim_match): always prefer value transitions over complete transitions
2017-02-23 01:21:14 +01:00
Leonardo de Moura
6b76b65881
feat(library/equations_compiler/elim_match): change default max number of steps to 2048
2017-02-21 21:33:10 -08:00
Leonardo de Moura
d9307413b9
feat(library/compiler): skip bytecode optimization for interactive tactics
...
This is just overhead for begin...end blocks.
Moreover, "live variable analysis" is currently a recursive
procedure, and Lean will run of stack space when processing big begin
end blocks (> 1000 tactics).
2017-02-21 21:23:58 -08:00
Leonardo de Moura
ca31ad0107
perf(library/metavar_util): quadratic behavior when assembling the final proof
...
The peformance problem was affecting theorems that contain many `intro`
tactic applications.
@gebner After this optimization, the GAPT benchmark elaboration time went from
1.6 secs to 0.6 secs.
2017-02-21 21:02:43 -08:00
Leonardo de Moura
321105099f
feat(library/type_context): add compilation flag for disabling type inference cache
2017-02-21 20:17:25 -08:00
Leonardo de Moura
09819cb159
feat(library/type_context): add compilation flag for disabling type class resolution flag
2017-02-21 20:04:43 -08:00
Leonardo de Moura
7c57d23b46
feat(kernel): add compilation flags for disabling has_local optimization and abstraction cache
2017-02-21 19:46:31 -08:00
Leonardo de Moura
1c959f6790
feat(kernel): add compilation flag for disabling "free var range" optimization
2017-02-21 19:40:56 -08:00
Leonardo de Moura
622e9a6035
feat(library/type_context): use m_unfold_pred to decide whether macros should be unfolded or not
...
see #1394
2017-02-21 18:07:39 -08:00
Leonardo de Moura
074574be0a
feat(library/vm/vm_array): add native array.iterate and array.foreach
2017-02-21 16:22:25 -08:00
Leonardo de Moura
d9dcb4461e
perf(library/vm/vm_array): minor optimization
2017-02-21 15:43:48 -08:00
Leonardo de Moura
3f87fd15eb
feat(library/vm): add liveness analysis, and support destructive updates for lean arrays
2017-02-21 15:09:37 -08:00
Leonardo de Moura
19cf5e916b
chore(script/gen_constants_cpp): generates a warning if automatically generated C++ function is not used in the source code
2017-02-21 12:05:41 -08:00
Sebastian Ullrich
a053175714
refactor(init/meta,library/vm): use structure for position information
2017-02-21 11:06:39 -08:00
Sebastian Ullrich
bea34eb936
fix(emacs/lean-debug): disable undo in lean-debug buffer
2017-02-21 10:55:15 -08:00
Gabriel Ebner
61c380b534
fix(shell/lean): catch all exceptions
...
Fixes #1386 .
2017-02-21 10:54:46 -08:00
Gabriel Ebner
4ae9312a5f
fix(emacs/lean-input): remove overloading of \b abbreviation
2017-02-21 10:54:19 -08:00
Leonardo de Moura
613a4d6e45
chore(shell/CMakeFiles): enable SMT2 tests
2017-02-21 10:53:03 -08:00
Leonardo de Moura
d1d5428808
feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes
2017-02-21 10:45:31 -08:00
Leonardo de Moura
9863755ae1
feat(shell/lean,library/smt): fix SMT2 frontend
2017-02-21 09:28:21 -08:00
Leonardo de Moura
04fd50e4e8
chore(*): fix tests and style
2017-02-20 23:53:44 -08:00
Leonardo de Moura
87eaedc580
feat(library/vm): shrink VM stack eagerly
...
TODO: liveness analysis objects on the VM stack
2017-02-20 23:10:50 -08:00
Leonardo de Moura
e9a98362d3
feat(library): functional arrays
2017-02-20 22:00:02 -08:00
Leonardo de Moura
2e1221b1b4
chore(CMakeLists): bump version number
2017-02-20 18:06:18 -08:00
Leonardo de Moura
61254847fb
fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a sorry expression)
2017-02-20 14:51:59 -08:00
Leonardo de Moura
ddee94b831
fix(frontends/lean/elaborator): incorrect invariant due to error recovery
...
We cannot assume both source and target are binding expressions.
The source has already been elaborated, and it may be a `sorry` because
of error recovery code.
2017-02-20 14:30:10 -08:00
Leonardo de Moura
296d4b0f09
refactor(library/tactic, library/init/meta): simplify_config => simp_config
2017-02-19 13:10:36 -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
Leonardo de Moura
203a0ac932
feat(library/tactic/smt/smt_state): more restrictive default intros
2017-02-18 22:48:34 -08:00
Leonardo de Moura
0a99910c52
feat(library/init/meta): add exception set to rsimp attributes, use iff lemmas
2017-02-18 19:43:21 -08:00
Leonardo de Moura
0626835530
feat(library/init/meta): add native name_set
2017-02-18 19:07:50 -08:00
Leonardo de Moura
bed3e6c2fd
feat(library/tactic/smt): add get_config and use it to implement slift
...
smt_tactic.slift was losing the configuration.
2017-02-18 17:52:45 -08:00
Leonardo de Moura
c065faaf1f
feat(frontends/lean/elaborator): improve ^. notation
2017-02-18 16:20:21 -08:00
Leonardo de Moura
74f7bc0473
feat(frontends/lean): improve notation for converting infix notation into functions
2017-02-17 23:11:22 -08:00
Leonardo de Moura
077176b82f
feat(frontends/lean): add Haskell-like for converting infix notation into functions
...
Examples:
qsort (<) [20, 5, 10, 3, 2, 14, 1]
foldl (+) 0 [1, 2, 3]
2017-02-17 22:51:50 -08:00
Leonardo de Moura
10c881266b
refactor(frontends/lean): add parse_lparen
2017-02-17 21:46:39 -08:00
diakopter
554e6bad90
chore(library): fix warning
2017-02-17 21:09:23 -08:00
Leonardo de Moura
7eef501ae1
chore(*): remove mpfr dependency
...
closes #1380
2017-02-17 20:36:53 -08:00
Johannes Hölzl
bb4920fcbc
feat(library/vm/vm_expr): export instantiate_univ_params
2017-02-17 20:08:18 -08:00
Johannes Hölzl
3db0ebdcf0
feat(library/tactic/match_tactic): return also assignments for universe meta-variables
2017-02-17 20:08:09 -08:00
diakopter
19606fd197
chore(util,kernel,library): clang warnings
2017-02-17 20:01:34 -08:00
Sebastian Ullrich
b9424975b3
refactor(init/meta): replace dynamically-checked quotes where possible
2017-02-17 19:59:57 -08:00
Gabriel Ebner
0c2878e509
fix(frontends/lean/definition_cmds): copy position for equation in meta definitions
...
Fixes #1377 .
2017-02-17 19:57:49 -08:00
Leonardo de Moura
d3c340a30c
feat(library/init/meta): improve induction tactic interface
...
It uses .rec recursor when it is not specified
2017-02-17 10:58:51 -08:00
