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

752 commits

Author SHA1 Message Date
Leonardo de Moura
87e749cd12 test(trace): add unit test for trace module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:30:05 -07:00
Leonardo de Moura
e16f45854b refactor(deep_copy): simplify deep_copy implementation, and move unit test to separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:25:24 -07:00
Leonardo de Moura
037ebfd1d4 refactor(util): make 'util/test.h' the first include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 20:13:05 -07:00
Soonho Kong
ad62f9762b fix(tests/util): use lean_assert_eq 2013-09-25 19:22:36 -07:00
Soonho Kong
475338080f fix(tests/interval): use new lean_assert and lean_assert_eq 2013-09-25 18:40:45 -07:00
Leonardo de Moura
9f0dab1add fix(kernel): add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel 
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.
We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include
'library/printer.h', but contains

    expr a;
    ...
    std::cout << a << "\n";
    ...

The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
 2013-09-25 17:45:54 -07:00
Leonardo de Moura
1452e9319e feat(debug): improve lean_assert macro 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-25 17:29:00 -07:00
Soonho Kong
1d8b7dc193 Update 'orelse' and 'then' rewriter to take a list of rewriters 2013-09-25 16:46:39 -07:00
Soonho Kong
a50f5f92b8 Rename 'rewrite' to 'Rewriter', change type of rewriter::operator() 2013-09-25 15:38:16 -07:00
Soonho Kong
573ca92a08 Fix typo in CTestConfig.cmake 2013-09-24 21:46:51 -07:00
Soonho Kong
6d10e978dc Add "--gen-suppressions=all" to valgrind option 2013-09-24 21:36:03 -07:00
Soonho Kong
0ef633a3c5 Fix to be compiled by clang++-3.4 
Clang++-3.4 is starting to enforce the following item of C++11 standard,
thus it's making lean not compiling:

It's illegal in C++11: §8.3.6.4 [dcl.fct.default]
"If a friend declaration specifies a default argument expression, that
declaration shall be a definition and shall be the only declaration of
the function or function template in the translation unit."
 2013-09-24 21:30:56 -07:00
Soonho Kong
8e9bd9ee67 Add Repeat/Success/Fail to rewrite (skeleton) 2013-09-24 20:04:08 -07:00
Soonho Kong
ac0eafa1b6 Fix style-warning 2013-09-24 19:34:58 -07:00
Soonho Kong
57e9e2c658 Re-implement rewrite module using rewrite_cell 2013-09-24 19:11:09 -07:00
Leonardo de Moura
ba0528c298 Implement total order on expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 12:16:32 -07:00
Leonardo de Moura
e23813f15d Add support for creating unique internal names. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 11:01:30 -07:00
Leonardo de Moura
1779b29355 Implement map using splay_trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 01:44:46 -07:00
Soonho Kong
71fb150333 Fix type of rewrite() to take an env. Add skeletons for other rewriters 2013-09-24 01:20:45 -07:00
Soonho Kong
81c9de229b Add then and orelse rewrite combinators and tests 2013-09-24 01:19:03 -07:00
Soonho Kong
9ba6068858 Update fo_match 2013-09-24 01:19:03 -07:00
Soonho Kong
f89ededddc Add rewrite and first-order pattern matching skeletal 2013-09-24 01:19:03 -07:00
Leonardo de Moura
b78b2e0585 Add remaining splay tree methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-24 01:04:02 -07:00
Soonho Kong
01f5fa59b1 Update src/memcheck.supp to suppress warnings caused by tcmalloc 2013-09-24 03:58:13 -04:00
Leonardo de Moura
d31f3facac Implement splay trees 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-23 22:31:18 -07:00
Soonho Kong
c1b12eae99 Update memcheck.supp to suppress a valgrind warning caused by a bug in tcmalloc-2.0 2013-09-23 19:57:16 -07:00
Leonardo de Moura
46d6c41835 Fix bug in the type checker (when type checking terms with meta-variables). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-22 19:12:19 -07:00
Leonardo de Moura
1647e44510 Fix memory corruption bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-22 18:53:58 -07:00
Leonardo de Moura
16a6a54df1 Fix abuse of operator-> overload 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-22 16:41:51 -07:00
Leonardo de Moura
c847d27763 Improve higher order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-21 00:41:49 -07:00
Soonho Kong
80581a76bb Update Find{MSize,MallocSize,MallocUsableSize}.cmake to handle the case where find_path fails 2013-09-21 00:10:25 -07:00
Soonho Kong
48318511f2 Undo the previous change which caused compile-errors 2013-09-21 00:04:23 -07:00
Soonho Kong
66ba1a20d7 Suppress cmake warning for OSX build 2013-09-20 23:49:09 -07:00
Leonardo de Moura
d29ec9ab6f Add tests for memory.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 22:37:13 -07:00
Leonardo de Moura
7ac94ee976 Add max_sharing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 22:01:40 -07:00
Leonardo de Moura
d34cfe3f8a Add simple formatter tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 21:46:32 -07:00
Soonho Kong
bef44899c8 Suppress style warning on util/memory.cpp 2013-09-20 18:07:12 -07:00
Soonho Kong
9226c46358 Add support OSX's malloc_size 2013-09-20 17:48:55 -07:00
Soonho Kong
8dc31dae4d Fix Check{MSize,MallocUsableSize}.cc and FindMSize.cmake to consider cross-compilation 2013-09-20 16:10:00 -07:00
Leonardo de Moura
3971265bcb Add support for _msize 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 14:14:57 -07:00
Leonardo de Moura
dae654e4c6 Track memory usage. Add new CMake option TRACK_MEMORY_USAGE (It is ON by default). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-20 12:32:12 -07:00
Leonardo de Moura
9d1266c972 Fix bugs in Tcmalloc detection. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 23:52:50 -07:00
Leonardo de Moura
a7a5426ff5 Fix wrong message in tcmalloc detection code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 23:36:57 -07:00
Leonardo de Moura
16dc056abc Remove invalid use of register 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 22:59:39 -07:00
Soonho Kong
49e87ccbb1 Enable "-Wextra" compiler option and fix code to remove warnings 
"-Wextra" option turns on the following warnings:
 -Wclobbered
 -Wempty-body
 -Wignored-qualifiers
 -Wmissing-field-initializers
 -Wmissing-parameter-type (C only)
 -Wold-style-declaration (C only)
 -Woverride-init
 -Wsign-compare
 -Wtype-limits
 -Wuninitialized
 -Wunused-parameter (only with -Wunused or -Wall)
 -Wunused-but-set-parameter (only with -Wunused or -Wall)
 2013-09-19 22:52:52 -07:00
Leonardo de Moura
651c5d6751 Fix warnings and bugs related to unused variables. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 22:41:07 -07:00
Soonho Kong
2b72c5f681 Update cpplint.py, disable "All parameters should be named in a function" 2013-09-19 22:41:07 -07:00
Soonho Kong
ab6ca82e6f Update to suppress unused-parameter warnings 2013-09-19 22:40:34 -07:00
Leonardo de Moura
80a1b96925 Remove duplicate solutions in the higher order matching module. Simplify solutions when higher-order matching is used, and we don't have a residue. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 18:59:28 -07:00
Leonardo de Moura
ffef055e34 Add options to ho_unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 18:19:25 -07:00
Leonardo de Moura
8c5c17ee12 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:30:37 -07:00
Leonardo de Moura
42482622f6 Add imitation for lambdas and Pis 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Leonardo de Moura
4afeb1a400 Add imitation step for equalities. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Leonardo de Moura
b3aa8b37f3 Remove cleanup_subst. The residue may still reference auxiliary variable. So, it is not safe to remove then from the resultant partial substitution. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Leonardo de Moura
d7cc5d2404 Fix bug in ho_unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-19 16:28:23 -07:00
Soonho Kong
0005d22bd1 Update memcheck.supp, add a new suppression rule for 32bit ubuntu 
[skip ci]
 2013-09-19 11:46:47 -07:00
Leonardo de Moura
2f29ff70d7 Implement higher-order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-18 20:46:00 -07:00
Leonardo de Moura
ad901ce087 Use consistent naming conventions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 14:43:07 -07:00
Leonardo de Moura
22949051f1 Higher-order unifier skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 14:43:07 -07:00
Soonho Kong
27d5ae13d7 Move src/interval to src/util/interval 2013-09-17 14:10:53 -07:00
Leonardo de Moura
df054477eb Remove unnecessary TODOs. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 13:33:52 -07:00
Leonardo de Moura
3df6149daa Add support for metavariables in the type checker. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 11:09:59 -07:00
Leonardo de Moura
9f9dcf9a29 Fix bug in the creation of children environments. Remove unnecessary function. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 07:37:33 -07:00
Leonardo de Moura
30b19c314a Add basic support for metavariables at is_convertible. Swap is_convertible arguments to make it more intuitive. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 07:15:47 -07:00
Leonardo de Moura
a26c7d47f2 Add simplification to add_lift 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 03:14:02 -07:00
Leonardo de Moura
99e8d2feae Add simplification rule to add_inst 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 02:57:28 -07:00
Leonardo de Moura
21c7a45f67 Relax definition of identity_stack. Fix printer for metavariable contexts. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 02:09:45 -07:00
Leonardo de Moura
d3bce584f4 Add support for new metavariable representation in the normalizer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-17 01:57:21 -07:00
Leonardo de Moura
da09e7217a Cleanup meta_entry code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
99a163f11d Simplify metavariable context. Now, we have only 'lift' and 'inst' instead of 'subst', 'lift' and 'lower' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
cad562a448 Add support for metavariables in the normalizer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Leonardo de Moura
1be2a30c8c Fix bug in normalizer. We must create a scope whenever we extend the value stack. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-16 19:32:28 -07:00
Soonho Kong
01339a93a3 Fix cpplint warning in util/safe_arith.cpp 2013-09-16 19:12:12 -07:00
Soonho Kong
13401d534c Add static assertion to util/safe_arith.cpp 2013-09-16 18:17:05 -07:00
Soonho Kong
6ee14bf17f Use unsigned short for the type of interval::bound_deps 2013-09-16 18:15:32 -07:00
Soonho Kong
ef18759e77 Update src/CmakeLists.txt - only check style over files starting with [A-z] 2013-09-16 16:23:20 -07:00
Leonardo de Moura
f79f046294 Add partial support for metavariables in the normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 21:23:50 -07:00
Soonho Kong
58c8c1a5ec Add EXCLUDE_PATTERNS to src/Doxyfile 
- */src/cmake/*
- GTAGS GPATH GRTAGS
- memcheck.supp
- *.cmake *.cmake.in
-  *.txt
 2013-09-15 20:31:15 -07:00
Leonardo de Moura
2800292947 Add timestamp to metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:50:48 -07:00
Leonardo de Moura
5a4bc331d2 Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 19:38:36 -07:00
Leonardo de Moura
63e102055e Move metavariables to the kernel. This is the first step for implementing the new elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-15 12:09:01 -07:00
Soonho Kong
e4b327bbaa Use C++11's <random> in pdeque/pvector tests (cygwin doesn't support rand_r) 2013-09-15 01:38:57 -07:00
Soonho Kong
dcc917a6b4 Use "sprintf" instead of "snprintf" because cygwin doesn't support "snprintf" 2013-09-15 01:38:21 -07:00
Soonho Kong
b553521578 Attempt to suppress valgrind warnings on Travis 
- don't understand why cmake on travis doesn't pick up the memcheck.supp
file. It works on my local machine.
 2013-09-15 01:17:05 -07:00
Soonho Kong
30f4b2de5f Update memcheck.supp 
[skip ci]
 2013-09-14 19:33:47 -07:00
Soonho Kong
ce05345129 Update CTestConfig.cmake to fix memcheck.supp 2013-09-14 20:22:05 -04:00
Soonho Kong
60903d3cea Fix cygwin build which was failed due to snprintf 2013-09-14 17:11:37 -07:00
Soonho Kong
c96a6982a0 Add <ctime> header for time() in pdeque/pvector tests 2013-09-13 20:42:49 -07:00
Soonho Kong
5266e22f05 Remove debug code from cpplint.py 2013-09-13 20:37:31 -07:00
Soonho Kong
eda25e77a4 Use time(0) as an initial seed for rand_r() in pvector/pdeque tests 2013-09-13 20:28:15 -07:00
Soonho Kong
f8c0c02cb0 Exclude 'style_check' from MemCheck list 2013-09-13 20:27:35 -07:00
Soonho Kong
0905529720 Add "style_check" test 2013-09-13 20:00:55 -07:00
Soonho Kong
0c450b5c23 Add StyleCheck.cmake 2013-09-13 19:21:02 -07:00
Soonho Kong
f620f54b32 Add target "style" to run cpplint.py 
- try "ninja style"
 2013-09-13 19:15:38 -07:00
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -07:00
Leonardo de Moura
99eaff0b4f Extract private and static, and add treeview to documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 17:55:37 -07:00
Leonardo de Moura
bcc3827a99 Modify Doxygen file to extract all elements even the undocumented ones. Disable warnings for undocumented entities. Add extra comments. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 13:46:22 -07:00
Leonardo de Moura
d54834279e Use consistent coding style for if-then-else 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:57:40 -07:00
Leonardo de Moura
8c735f1daa Use consistent coding style for spaces after ',' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:49:03 -07:00
Leonardo de Moura
2c68117adf Tag TODOs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 12:25:21 -07:00
Leonardo de Moura
18f9378f97 Rename numtype.h to num_type.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 09:07:44 -07:00
Leonardo de Moura
573ec5ccc2 Rename import_all. The idea is to use consistent name for library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 09:06:46 -07:00
Leonardo de Moura
0c09e4524a Use consistent names for import functions, and library files. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:58:34 -07:00
Leonardo de Moura
070c87bef0 Rename arith library files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-13 08:55:09 -07:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -07:00
Leonardo de Moura
4c19cc6957 Rename lean frontend files. The prefix lean_ is not necessary anymore. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:09:35 -07:00
Leonardo de Moura
26097475fd Use fullpath in #include directives. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 20:04:10 -07:00
Leonardo de Moura
c655e9fe7b Move sexpr_funcs to sexpr_fn. Using consistent file name conventions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 18:27:46 -07:00
Leonardo de Moura
2e990ef7d3 Fix warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 14:02:40 -07:00
Leonardo de Moura
bc69e7803f Add support for writing a[i] = v instead of a.set(i, v) in the pdeque class. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:18:26 -07:00
Leonardo de Moura
74b8a4f0ac Add support for writing a[i] = v instead of a.set(i, v) in the pvector class. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:12:02 -07:00
Leonardo de Moura
f972cc9aae Fix bugs in pvector. Improve test driver 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 11:01:40 -07:00
Leonardo de Moura
55ff49d2d5 Replace queue.h with pdeque.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 10:09:54 -07:00
Leonardo de Moura
cd5e45bae2 Reduce pvector delta_cell quota on reads. Add example that demonstrates why this is needed. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-12 08:28:24 -07:00
Soonho Kong
5858c9d5e0 Update tests/util/list.cpp to suppress a g++ warning 2013-09-12 01:39:04 -07:00
Leonardo de Moura
f7196e05ff Add 'persistent' vectors. We should use the same approach for queues. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:55 -07:00
Leonardo de Moura
ef0e0ad382 Add (optional) performance tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:55 -07:00
Leonardo de Moura
572c7ced2a Add #include<atomic> to expr.h. We need it when #define LEAN_THREAD_UNSAFE_REF_COUNT is used 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:55 -07:00
Leonardo de Moura
ed15a2df9b Use split_reverse_second instead of split and then reverse in queue 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:55 -07:00
Leonardo de Moura
37498f9fb8 Add persistent queues 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:54 -07:00
Leonardo de Moura
3657320edb Add basic list functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-11 19:48:54 -07:00
Soonho Kong
7a6032dd86 Update memcheck.supp to ignore bash memroy leak on Fedora19 2013-09-10 22:44:24 -04:00
Soonho Kong
9e3583a04a Update memcheck.supp to match the thread bug patterns we get by using clang++-3.3 2013-09-10 17:37:22 -07:00
Soonho Kong
a993424165 Use "--gen-suppressions=all" in valgrind 2013-09-10 17:09:39 -07:00
Soonho Kong
6569406fb9 Update memcheck.supp 
add reference for the suppression stuff
[skip ci]
 2013-09-10 15:47:47 -07:00
Soonho Kong
3505ed8adb Use suppressions file to ignore certain valgrind warnings 2013-09-10 15:37:09 -07:00
Soonho Kong
9113f824bd Use '--track-origins=yes' option in valgrind 2013-09-10 14:31:30 -07:00
Leonardo de Moura
6fe86ffefd Fix initialized memory error reported by Valgrind. Disable 2 tests that produce memory leaks due to a bug in g++. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-10 13:51:02 -07:00
Soonho Kong
fae6c29237 Fix memory leaks in mpfp.h 2013-09-10 13:26:14 -07:00
Soonho Kong
8ce18a1508 Use "--leak-check=full" option in valgrind 2013-09-10 13:12:22 -07:00
Soonho Kong
f4edbba325 Turn off '--show-reachable=yes' valgrind option 2013-09-10 12:34:33 -07:00
Soonho Kong
b04bdae763 Use "--trace-children=yes" option for MemCheck(valgrind) to handle 
leantests shell script
 2013-09-10 10:47:04 -07:00
Leonardo de Moura
4c67721d32 Fix test error on Cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-09 18:35:11 -07:00
Leonardo de Moura
adfbba6447 Fix problem reported by Soonho 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 23:10:33 -07:00
Leonardo de Moura
2ca30571b4 Display the input term in the output of the Check command. It is useful to see the fully elaborated term. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 22:55:21 -07:00
Leonardo de Moura
a8ba50531b Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 20:38:11 -07:00
Leonardo de Moura
59a589037e Keep expanded form when pretty printings variable declarations with implicit marks (i.e., curly braces) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 11:23:46 -07:00
Leonardo de Moura
df116f88e0 Improve pretty printer for Pi's 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-08 11:04:07 -07:00
Leonardo de Moura
1cee392483 Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-07 22:33:18 -07:00
Leonardo de Moura
33c4b44b2b Encapsulate context implementation. The current implementantion based on lists may be a performance problem in the future, and we should be able to change it without affecting the whole code base. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-07 11:15:11 -07:00
Leonardo de Moura
bab11b57ad Move Symm and Trans back to basic_thms.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:49:35 -07:00
Leonardo de Moura
c674bb3790 Add castlib as an independent library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:40:47 -07:00
Leonardo de Moura
7a9d53d0d7 Refactor arith libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 23:19:47 -07:00
Leonardo de Moura
b92bbeb83b Add casting propagation and normalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 20:45:26 -07:00
Leonardo de Moura
7eab229114 Improve check_pi in lean elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 18:58:33 -07:00
Leonardo de Moura
c0c2f52087 Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 18:32:15 -07:00
Leonardo de Moura
b62816cc25 Fix problem with pretty printer. Add another test for elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 18:01:11 -07:00
Leonardo de Moura
edafd519e1 Add missing case to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 17:43:08 -07:00
Leonardo de Moura
26bf7bcaac Fix bug in the elaborator. Move character ' to class A 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 17:12:35 -07:00
Leonardo de Moura
8840b37258 Fix type checker and elaborator for let expressions. Fix get_coercions (we need to pass the context). Fix pretty printer for def_type_mismatch_exception. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 11:02:00 -07:00