michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
1837 commits 3 branches 0 tags 28 MiB
Commit graph

1585 commits

Author SHA1 Message Date
Leonardo de Moura
3ab2d2a441 fix(frontends/lean/parser): memory leak due to g++ bug 
g++ implementation of std::initializer_list has bug.
http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html

This commit memory leaks triggered by this bug.
It also adds minimal tests to expose three different instances of the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 10:15:04 -08:00
Leonardo de Moura
83efa644d1 fix(frontends/lean/parser): uninitialized var error reported by valgrind 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 08:43:43 -08:00
Leonardo de Moura
28eb980484 fix(build): C++ module dependency problem, and style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 18:30:31 -08:00
Leonardo de Moura
c8e1ec87d2 feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 18:30:19 -08:00
Leonardo de Moura
7c2a4211a8 feat(kernel): expose imported predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 16:41:40 -08:00
Leonardo de Moura
07059b0531 feat(library): add if_then_else Lean/C++ interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 16:10:49 -08:00
Leonardo de Moura
8217a544cc fix(library/hop_match): bugs in the higher-order matching procedure, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 14:37:28 -08:00
Leonardo de Moura
acfb11e290 fix(kernel/instantiate): relax apply_beta pre-condition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 14:36:51 -08:00
Leonardo de Moura
a968a43487 fix(kernel/free_vars): make sure has_free_var does not return incorrect result due to arithmetic overflows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 14:36:14 -08:00
Leonardo de Moura
f8eaae7218 feat(builtin/kernel): add new useful theorems for the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 18:21:22 -08:00
Leonardo de Moura
4595c50f7e fix(library/hop_match): in locally bound variable management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 16:54:21 -08:00
Leonardo de Moura
55aa4cbfa3 feat(frontends/lean): improve error message for expressions containing unsolved metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 13:21:44 -08:00
Leonardo de Moura
12451e4a35 feat(frontends/lean/pp): display implicit arguments when expression contains metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 12:42:05 -08:00
Leonardo de Moura
35bacf95fc feat(shell): provide the default environment when parsing Lua files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 18:21:14 -08:00
Leonardo de Moura
7f818ecd92 feat(library): match procedure for higher-order patterns 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:45:24 -08:00
Leonardo de Moura
e6c322d97f feat(kernel/free_vars): make free_vars module functions more robust 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:44:28 -08:00
Leonardo de Moura
29fec3fecc fix(builtin/util): bug incorrect encoding of \t and \n in regular expression, and missing local 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:40:41 -08:00
Leonardo de Moura
915644f3b3 fix(util/debug): avoid infinite loop when Ctrl-D is pressed after an assertion violation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:20:35 -08:00
Leonardo de Moura
5d9a95addd refactor(kernel/free_vars): replace max_free_var with relaxed free_var_range 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:06:57 -08:00
Leonardo de Moura
582569b793 feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 16:46:53 -08:00
Leonardo de Moura
4d9eb4ac6c feat(kernel): add max_free_var function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 16:45:34 -08:00
Leonardo de Moura
6508e63a17 feat(builtin/macros): add assume/take macros for making proof scripts more readable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 18:36:37 -08:00
Leonardo de Moura
781720a26a feat(builtin/kernel): add left_comm theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 18:08:08 -08:00
Leonardo de Moura
a1a467a65f refactor(builtin): move congruence theorems to kernel/if_then_else modules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 13:48:28 -08:00
Leonardo de Moura
a0a92f11b7 feat(builtin/congr): add congruence theorems for contextual simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 13:37:36 -08:00
Leonardo de Moura
53537d0684 feat(builtin/kernel): 'implication' simplification theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 13:35:20 -08:00
Leonardo de Moura
50f281b430 feat(builtin/kernel): add eqf_intro and eqf_elim theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 11:13:54 -08:00
Leonardo de Moura
4057f0d2fe feat(emacs): minor improvements to emacs mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-11 11:13:20 -08:00
Leonardo de Moura
745c702ffb fix(build): dependency problem on some platforms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-10 19:06:15 -08:00
Leonardo de Moura
d4a7d796a5 feat(builtin): prove strong induction theorem, add < theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-10 18:46:33 -08:00
Leonardo de Moura
5fb718c03a fix(build): broken dependencies between lean executable and .olean, *_decls.cpp and *_decls.h files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-10 10:58:35 -08:00
Leonardo de Moura
9e8b083673 feat(emacs): more highlighting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 20:44:01 -08:00
Leonardo de Moura
3008cad151 feat(emacs): highlight tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 20:10:57 -08:00
Leonardo de Moura
2cf73fc4d2 feat(emacs): useful abbreviations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 19:57:00 -08:00
Leonardo de Moura
65bdb9c7e0 fix(frontends/lean): unprotected call to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 19:56:20 -08:00
Leonardo de Moura
411f14415d feat(builtin): automatically generate Lean/C++ interface for builtin theories 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 18:09:53 -08:00
Leonardo de Moura
a339a53f50 feat(util/options): 'verbose' as a system option, add -q (quiet) option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 15:31:58 -08:00
Leonardo de Moura
8c41b4e899 feat(build): run tests using -t 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 14:12:32 -08:00
Leonardo de Moura
2179e57db3 refactor(builtin): move if_then_else to its own module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 14:08:39 -08:00
Leonardo de Moura
fdeb457a81 feat(kernel/pos_info_provider): add support for file names in pos_info_provider 
The idea is to include the file name when displaying justification objects.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 12:19:30 -08:00
Leonardo de Moura
dff0b9011b chore(builtin/cast): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 12:06:22 -08:00
Leonardo de Moura
3e18cdfeec feat(util/format): do not use colors by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:56:58 -08:00
Leonardo de Moura
6fe362ef07 feat(emacs): include lean-mode Emacs files in the distribution 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:50:07 -08:00
Leonardo de Moura
84e211b81b fix(frontends/lean): missing ':' in error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:01:27 -08:00
Leonardo de Moura
87b238efcd chore(builtin/kernel): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 09:00:05 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 08:33:52 -08:00
Leonardo de Moura
25086947fa fix(builtin/kernel): incorrect comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 19:14:11 -08:00
Leonardo de Moura
e42b616438 fix(kernel/normalizer): equality between semantic attachments 
Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-08 19:10:30 -08:00