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

816 commits

Author SHA1 Message Date
Leonardo de Moura
f1e0d6ec29 refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:44:26 -07:00
Leonardo de Moura
c1e451151a feat(replace_visitor): add an abstract class for applying transformations on expressions 
I also removed replace_using_ctx since it is subsumed by the new class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:01:37 -07:00
Leonardo de Moura
13531b7d3e refactor(kernel): rename trace to justification 
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:42:17 -07:00
Leonardo de Moura
8e1a75ce1c feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:09:13 -07:00
Leonardo de Moura
172567a2fb feat(elaborator): add support for upper bounds, max constraints, and fix bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:01:39 -07:00
Leonardo de Moura
17b48010b7 fix(unification_constraint): fix printer for max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:00:29 -07:00
Leonardo de Moura
274b11530f feat(metavar): improve apply_local_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 11:59:36 -07:00
Leonardo de Moura
b57f492e2d fix(kernel/printer): improve printer for Type expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 11:58:49 -07:00
Leonardo de Moura
c635c16637 refactor(ho_unifier): remove ho_unifier, it has been subsumed by the elaborator class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:51:54 -07:00
Leonardo de Moura
019f64671b fix(elaborator): add basic support for flex-flex pairs, add more tests, fix bug when enumerating different solutions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:49:37 -07:00
Leonardo de Moura
80a507cf45 refactor(tests/frontends/lean/implicit_args): remove implicit_args unit tests from frontends/lean, all tests were moved to tests/library/elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:42:07 -07:00
Leonardo de Moura
7ad256131e feat(elaborator): add support for constraints of the form ?m[inst, ...] == t, fix bugs, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:39:22 -07:00
Leonardo de Moura
891d22b3de feat(kernel/context): add method for remove context entries at positions [s, s+n). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:52:24 -07:00
Leonardo de Moura
3fa4eac4ef fix(replace_using_ctx_fn): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:46:11 -07:00
Leonardo de Moura
8142726923 fix(type_inferer): bug when inferring the type of free variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:41:22 -07:00
Leonardo de Moura
874f67c605 feat(normalizer): remove normalization rule t == t ==> true 
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:

Theorem Th : a = a := Refl b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 14:02:48 -07:00
Leonardo de Moura
5e61496381 test(elaborator): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:20 -07:00
Leonardo de Moura
a5b4908f71 fix(elaborator): process_simple_ho_match and missing cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:04 -07:00
Leonardo de Moura
cb2c73cf37 feat(elaborator): add higher-order matching support to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 11:22:00 -07:00
Leonardo de Moura
f4592da87f feat(elaborator): solve more unification constraints, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
c3e87f106f fix(kernel/trace): fix typo in depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
dc51d35dc0 feat(library/type_inferer): add support for metavariables at type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
7f96c07a01 refactor(library): rename light_checker to type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
dc0e7a4472 feat(pos_info_provider): add position information provider for expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
8663ac550f feat(kernel/trace): add function depends_on for trace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
42edc4a72d test(set): add set of pointers test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
b1b49e86e7 test(elaborator): add simple test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
1548ffabb1 feat(elaborator): add new elaborator interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
827c65b5e9 feat(kernel): add static_assert for update_metavar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
61ccaf741c fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
7cf83800c0 refactor(metavar): implement metavar_env, and use unification_constraint and trace objects in the type_checker, light_checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
1f0eab7a14 test(type_checker): add new tests for type_checker trace objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
fc288929a2 feat(type_checker): add trace objects to justify constraints created by the type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
5b1b03bafd refactor(is_convertible): move from normalizer to type_checker class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
85bfa45e6a refactor(kernel_exception): delete kernel_exception_formatter, and implement kernel_exception pretty printer as a virtual method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
d843d432d3 refactor(kernel): move printer and formatter objects to the kernel 
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
ddb90d3038 feat(kernel): add unification_constraint and trace objects to the kernel 
Trace objects will be used to justify steps performed by engines such as the elaborator. We use them to implement non-chronological backtracking in the elaborator. They are also use to justify to the user why something did not work.

The unification constraints are in the kernel because the type checker may create them when type checking a term containing metavariables.

Remark: a minimalistic kernel does not need to include metavariables, unification constraints, nor trace objects. We include these objects in our kernel to minimize code duplication.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
e741cc29ef test(metavar): encode two of the bad examples as unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
59914a36f3 refactor(metavar): reorganize and simplify metavariables 
- Use hierarchical names instead of unsigned integers to identify metavariables.
- Associate type with metavariable.
- Replace metavar_env with substitution.
- Rename meta_ctx --> local_ctx
- Rename meta_entry --> local_entry
- Disable old elaborator
- Rename unification_problems to unification_constraints
- Add metavar_generator
- Fix metavar unit tests
- Modify type checker to use metavar_generator
- Fix placeholder module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
3387c300a0 feat(polynomial): add multivariate polynomials 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:22:14 -07:00
Leonardo de Moura
93d4466d06 refactor(interval): move interval unit tests to tests/util/interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:17:34 -07:00
Leonardo de Moura
f18d35555e refactor(interval): organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 18:15:27 -07:00
Leonardo de Moura
e208309abd refactor(numerics): rename power operator to pow, the idea is to follow the C/C++ name convention for the power operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-21 17:23:56 -07:00
Leonardo de Moura
f1d9312521 feat(numerics/zpz): add numeric_traits for zpz numerals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-18 14:41:18 -07:00
Leonardo de Moura
1429cc9df2 feat(numerics): add finite field Z/pZ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-18 13:27:28 -07:00
Leonardo de Moura
bdade0e638 fix(numerics): problem with gcd tests on OSX 
Now, we only test gcd(a, b) for a != b && a != 0 && b != 0.
When one of these conditions do not hold, the result is implementation dependent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-17 10:38:02 -07:00
Leonardo de Moura
cf2c0f8ebb feat(numerics): add gcd and extended gcd templates (for primitive types) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 18:18:20 -07:00
Leonardo de Moura
39f68ed0d6 feat(numerics): add is_prime function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 17:25:08 -07:00
Leonardo de Moura
1097bbfb22 fix(style): fix warnings produced by cpplint.py, disable sizeof(type) warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 17:04:39 -07:00
Leonardo de Moura
105f55c68b feat(numerics): add zero() method to all numeric_traits 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 16:55:17 -07:00
Leonardo de Moura
ff04c5a2e2 test(numerics): add test to make sure that zeros of different precision mpfp numbers are the equal. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 16:54:43 -07:00
Leonardo de Moura
467eff4662 add(numerics): add prime number generator/iterator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-16 16:05:45 -07:00
Leonardo de Moura
0783805671 feat(kernel): add weight to kernel definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-15 14:50:08 -07:00
Leonardo de Moura
5bd6ba37d0 fix(light_checker): fix inconsistent cache bug in light_checker, add tests that expose the problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-01 19:25:58 -07:00
Leonardo de Moura
aa5be3262f fix(type_checker): fix inconsistent cache bug in type_checker, add tests that expose the problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-01 19:23:55 -07:00
Leonardo de Moura
2089d12bd0 fix(replace_using_ctx): fix inconsistent cache bug in replace_using_ctx, and add tests that expose the problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-01 18:52:18 -07:00
Soonho Kong
760f2e15ce feat(library/replace_using_ctx): add static_assert 2013-10-01 16:47:49 -07:00
Soonho Kong
e3b762e909 feat(kernel): add static_assert to expr,expr_eq,replace 2013-10-01 16:47:36 -07:00
Soonho Kong
b823c7d779 feat(util): add static_assert to {scoped,splay}_{map,set} 2013-10-01 16:47:28 -07:00
Soonho Kong
a726f5fbb7 feat(util/list): add static_asserts for map/for_each/compare 2013-10-01 09:05:53 -07:00
Soonho Kong
3381df0150 fix(util/list_fn): rename iter to for_each 2013-10-01 09:03:07 -07:00
Soonho Kong
c50bc13be0 test(library/rewriter): add more tests 2013-10-01 00:30:38 -07:00
Soonho Kong
7c0b56ad0d feat(library/rewriter): implement repeat/app/lambda/pi/try rewriter 
- refactor to use rewriter_cell
 - implement display and operator<< for debugging
 2013-10-01 00:30:31 -07:00
Soonho Kong
e6c76fbe76 refactor(library/rewriter/fo_match): add more lean_trace for debugging 2013-10-01 00:20:12 -07:00
Soonho Kong
a832173f5f feat(kernel/expr): add expr::operator() which takes 8 args 2013-10-01 00:19:30 -07:00
Soonho Kong
1a3ea26032 feat(util/list_fn): add iter function 2013-10-01 00:18:55 -07:00
Leonardo de Moura
15979ab991 fix(lean): fix warnings produced by cppcheck 
Fix (relevant) warnings produced by http://cppcheck.sourceforge.net.
Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-30 21:38:55 -07:00
Leonardo de Moura
30089aa4f8 test(type_checker): add example showing how to use the kernel exception formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-30 16:39:29 -07:00
Soonho Kong
54f4c4d9bc test(library/rewriter/fo_match): clean up enable_trace 2013-09-29 18:36:01 -07:00
Leonardo de Moura
8d3ae665e7 fix(splay_map): fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:30:08 -07:00
Leonardo de Moura
21f9699661 test(splay_tree): add missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:28:10 -07:00
Leonardo de Moura
790c2a72d5 test(safe_arith): add unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:20:32 -07:00
Leonardo de Moura
1179b6b52b test(hash): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:20:32 -07:00
Leonardo de Moura
57b6148bbb test(buffer): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 17:20:32 -07:00
Leonardo de Moura
02f621aa45 test(lazy_list): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 14:38:35 -07:00
Leonardo de Moura
3c8dff9085 feat(lazy_list): implement ML-like lazy lists 
We will use lazy lists to represent the set of solutions produced by the elaborator. The elaborator plugins will also use lazy lists.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-29 12:35:26 -07:00
Soonho Kong
841a1fb20c fix(debug): print type in lean_assert, print bool correctly 
- use typeinfo to print out a type of value when an assertion fails.
   need to use "c++filt --types" to demangle names for non-basic types.
 - use std::boolalpha and std::noboolalpha to control the printed values
   for "true" and "false"
 2013-09-28 23:38:21 -07:00
Soonho Kong
4602dfd209 test(util/numerics): more tests to improve coverage 2013-09-28 23:38:17 -07:00
Soonho Kong
fb3635a9ef test(util/numerics/mpbp): add more tests for improving coverage 2013-09-28 01:01:52 -07:00
Soonho Kong
6519d4bb0f chore(memcheck.supp): generalize TCmalloc_Bug2 pattern 
to suppress a warning from MSR 32bit build
[skip-ci]
 2013-09-27 19:16:02 -07:00
Soonho Kong
0065d69e0a chore(build): put --coverage CXX_FLAGS for TESTCOV build 2013-09-27 10:24:31 -07:00
Leonardo de Moura
d2667d56c0 test(lean/parser): add more tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-27 09:59:50 -07:00
Leonardo de Moura
0ff69d28f3 test(lean/scanner): add more tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-27 09:59:50 -07:00
Leonardo de Moura
6fc177056e refactor(tests/frontends/lean): use consistent name convention for file names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-27 09:59:50 -07:00
Soonho Kong
6a0d211d54 test(fo_match): add more unittests 
[skip ci]
 2013-09-27 01:53:42 -07:00
Soonho Kong
285495313b refactor(rewrite): use scoped_map as a type of substitution 2013-09-27 01:45:22 -07:00
Soonho Kong
1d4a1b68f5 refactor(fo_match): use scoped_map 2013-09-27 01:44:05 -07:00
Soonho Kong
6307beedc9 feat(scoped_map): add operator<< to scoped_map for debugging 2013-09-27 01:42:11 -07:00
Soonho Kong
a05b6b476e fix(testcov): install lcov and include testcov only when it's on 2013-09-26 22:24:24 -07:00
Soonho Kong
6abb7bf2ff chore(testcov): add missing CodeCoverage.cmake 2013-09-26 21:26:52 -07:00
Soonho Kong
3a5a565594 feat(splay_map): add operator<< to splay_map for debugging 2013-09-26 20:44:20 -07:00
Soonho Kong
5e5087b0a3 chore(testcov): add compile target "cov" to run code-coverage locally 
- need to run cmake with "-DTESTCOV=ON" and "-DCMAKE_BUILD_TYPE=Debug"
 - type "make/ninja cov"
 - open "coverage/index.html" to check the code coverage
 2013-09-26 20:28:52 -07:00
Leonardo de Moura
9d8ff0eadb test(mpz): add unit tests for mpz 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 20:01:39 -07:00
Leonardo de Moura
5cce74d116 test(library): add tests for improving coverage 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 19:43:10 -07:00
Soonho Kong
60157aa92a fix(splay_map): add 'const' to coersion operator of ref class 
[skip ci]
 2013-09-26 19:09:37 -07:00
Leonardo de Moura
54e63fd4de feat(splay_tree): add fold and for_each templates for splay_tree and splay_map 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:20 -07:00
Leonardo de Moura
1aca1d2d77 refactor(list): improve append function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:20 -07:00
Leonardo de Moura
24c173a519 feat(debug): add assert_ne (not equal) macro 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-26 18:18:20 -07:00