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

4013 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 17:39:12 -08:00
Leonardo de Moura
1da4294793 refactor(builtin): more theorems, fix iff notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 09:26:50 -08:00
Leonardo de Moura
7d6cd514d1 doc(examples/lean): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 05:01:34 -08:00
Leonardo de Moura
fd8a1266d0 doc(examples/lean): update notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 04:52:45 -08:00
Leonardo de Moura
2ce245d68e doc(examples/lean): transitive closure example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 04:37:36 -08:00
Leonardo de Moura
398d83b6d5 chore(builtin/Nat): use iff 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 02:06:53 -08:00
Leonardo de Moura
4dc98bc73b refactor(builtin/kernel): use iff instead of = for Booleans 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 02:05:09 -08:00
Leonardo de Moura
5453a8f2f1 test(tests/lua): hop_match experiment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 00:15:31 -08:00
Leonardo de Moura
d063828ff9 feat(library/kernel_bindings): expose abst_name, abst_domain and abst_body in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 00:03:16 -08:00
Leonardo de Moura
8d73fb5699 fix(library/hop_match): Lua bindings gotcha 
See http://www.luafaq.org/gotchas.html#T6.4

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 23:51:26 -08:00
Leonardo de Moura
14c6218bdc chore(kernel): file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 20:06:29 -08:00
Leonardo de Moura
3238c7e2a0 feat(library/simplifier): add is_permutation_ceq predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 19:53:52 -08:00
Leonardo de Moura
7fb0aa4800 chore(kernel/expr): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:24:31 -08:00
Leonardo de Moura
2368c936d3 test(tests/lua): exercise fields method for semantic attachments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:24:18 -08:00
Leonardo de Moura
438fa8251b test(kernel/expr): check if the serializer works for metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:15:56 -08:00
Leonardo de Moura
5058e403b5 test(kernel/expr): check if the serializer works for applications with many argumets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:09:46 -08:00
Leonardo de Moura
c096eec1d6 chore(kernel/expr): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 17:09:04 -08:00
Leonardo de Moura
57e58c598c fix(tests/lean): adjust tests to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 16:35:33 -08:00
Leonardo de Moura
8c2f78a756 feat(builtin): minimize use of heterogenous equality in the kernel, add simpler version of congruence theorems for non-dependent types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 16:34:23 -08:00
Leonardo de Moura
c73398a0b8 refactor(library/simplifier): relax rule for conditional equalities 
The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:

theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 16:06:00 -08:00
Leonardo de Moura
3daac17ea8 feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 15:30:16 -08:00
Leonardo de Moura
1176093afa refactor(library/simplifier): simplifier should only use homogeneous equalities 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 14:58:32 -08:00
Leonardo de Moura
f177c8d1ec fix(library/elaborator): missing condition 
The elaborator was failing in the following higher-order constraint

   ctx |- (?M a) = (?M b)

This constraint has solution, but the missing condition was making the elaborator to reduce this problem to

   ctx |- a = b

That does not have a solution.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 14:11:36 -08:00
Leonardo de Moura
f67b5c4d00 test(tests/lua): more to_ceqs tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 13:50:35 -08:00
Leonardo de Moura
c651d3ea2d feat(library/simplifier): filter out propositions that cannot be used as conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 12:06:27 -08:00
Leonardo de Moura
94fa987814 fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool 
The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 11:02:52 -08:00
Leonardo de Moura
91e1f9fc02 fix(tests/lean): adjust test to reflect recent changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 10:20:35 -08:00
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
97d9765992 fix(tests/lua/threads): increase timeout to make sure it passes the test on slow machines 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 08:46:14 -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
485ca842c9 test(tests/lua): extra tests for Lua hierachical name API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 11:38:10 -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
d83a13d044 doc(doc/lean/tutorial): update tutorial 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 21:56:08 -08:00
Leonardo de Moura
84f017f127 chore(tests/lua): use default environment instead of creating a new one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 18:24:04 -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