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

862 commits

Author SHA1 Message Date
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
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 10:06:26 -07:00
Leonardo de Moura
6da194334e Move 'slow' test files to different subdir. Modify CTestCustom.cmake.in to run leantests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 08:48:12 -07:00
Leonardo de Moura
6f3b0c30fb Add 'Variables' command. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 08:48:12 -07:00
Leonardo de Moura
3dc55c452c Parse decimal values 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 08:48:12 -07:00
Leonardo de Moura
b3a095b068 Fix pretty printer for evaluator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 18:57:29 -07:00
Leonardo de Moura
c22bd8b6ed Clean elaborator_exception pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 10:15:52 -07:00
Leonardo de Moura
eb96e6441f Moved kernel exception formatting to kernel_exception_formatter.cpp. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-05 10:15:43 -07:00
Soonho Kong
974b99b424 Update CTestCustom.cmake.in 
Exclude "threads" test from valgrind targets
[skip ci]
 2013-09-04 16:41:04 -07:00
Leonardo de Moura
87d3961158 Improve elaborator error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 16:36:58 -07:00
Leonardo de Moura
613d83cdf4 Improve application type mismatch errors. We also show the implicit arguments (not just their types) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 16:36:58 -07:00
Leonardo de Moura
408005b730 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 16:36:57 -07:00
Soonho Kong
30e5ac7004 Fix OSX linker warning issue 2013-09-04 15:35:07 -07:00
Leonardo de Moura
be7fa0932a Add unicode name for the types: Nat, Int and Real 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 09:03:41 -07:00
Leonardo de Moura
d41160f8a5 Modify environment. Now, when a builtin value is declared, if it has a unicode alternative representation, then we add it as a definition. Now, everything that occurs in the environment has been 'declared'. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 08:53:00 -07:00
Leonardo de Moura
e955c054ca Modify type checker. Now, it only accepts builtin values that have been declared in the environment. The idea is to be able to track which classes of builtin values have been used in a given environment. We want to be able to quantify the size of the trusted code base for a particular development. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 08:30:04 -07:00
Leonardo de Moura
9f34f96b08 Add another example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 05:40:28 -07:00
Soonho Kong
a8c16bc127 Fix test coverage problem by forcing to use gcov-4.8 2013-09-04 08:07:24 -04:00
Soonho Kong
5e603dbf9f Use cdash on cmacslab2 machine due to 10-build per day restriction 2013-09-04 04:46:37 -07:00
Leonardo de Moura
9f64e2b14b Fix another cdash warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 04:43:55 -07:00
Leonardo de Moura
00bee9c96e Fix warning produced by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 04:40:43 -07:00
Leonardo de Moura
57c0c69872 Fix bug reported by Valgrind. Reason: m_metavars is a vector of metavar_info; each metavar_info has a context; when we invoke mk_metavar the vector can grow in size, and the context is moved to a new location. The previous location is invalidated. To avoid the problem we have to save ctx in a local variable. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 04:29:03 -07:00
Soonho Kong
bbbd584b45 Use my.cdash.org to store results of unittests, coverage, and valgrind 2013-09-04 00:51:20 -07:00
Leonardo de Moura
887f696f66 Factor duplicate code. Add more comments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 23:27:58 -07:00
Leonardo de Moura
0c071d43af Move examples to lean examples subdir. We should have an example subdirectory for each frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 20:42:20 -07:00
Leonardo de Moura
fc9e395818 Define absolute value function and notation for it. Add new example. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 20:39:54 -07:00
Leonardo de Moura
3992c4b8f9 Define divides, and add examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 20:18:20 -07:00
Leonardo de Moura
8e7c657cf7 Use expected type of a definition in the elaborator. Improve elaborator solver. Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 18:04:42 -07:00
Leonardo de Moura
4a75e2d965 Fix bug when pretty printing function applications where the head is a meta-variable. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 17:51:56 -07:00
Leonardo de Moura
51422fe654 Modify the parser for accepting expressions such as: 'fun a b, f a b', 'forall a, f a > 0', etc. This is just syntax sugar for 'fun (a : _) (b : _), f a b' and 'forall a : _, f a > 0' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 17:24:05 -07:00
Leonardo de Moura
6f3fa63ccb Add missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 14:51:34 -07:00
Leonardo de Moura
a154f4e439 Modify Set command in the default lean frontend. Now, the lean prefix (for lean default frontend specific options) is optional when we are in the lean front-end. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 11:07:28 -07:00
Leonardo de Moura
a341643335 Fix unit tests for Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 10:44:51 -07:00
Leonardo de Moura
2d97bc3861 Make pp::unicode false by default in Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 10:26:12 -07:00
Leonardo de Moura
544229e5d3 Create pp::unicode option. The idea is to be able to disable unicode characters, but still be able to use mixfix notation. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-03 10:11:45 -07:00
Leonardo de Moura
e031d7bc10 Improve error messages when overloads+coercions do not work 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 20:05:47 -07:00
Leonardo de Moura
fd44ec8d79 Improve application type mismatch error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 18:28:12 -07:00
Leonardo de Moura
72188691de Add hyperbolic functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 17:28:43 -07:00
Leonardo de Moura
4eaba93591 Add trigonometric functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 17:03:02 -07:00
Leonardo de Moura
395513258e Define mod and unary minus 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 16:31:44 -07:00
Leonardo de Moura
b483d0dc45 Replace Int::sub and Real::sub with definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 16:31:30 -07:00
Leonardo de Moura
abc939382b Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 13:20:00 -07:00
Leonardo de Moura
e218b92a9d Modify verbose message for Set command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 12:29:21 -07:00
Leonardo de Moura
0a67679afb Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 12:24:29 -07:00
Leonardo de Moura
7acf438bf4 Metavariables will not be part of the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 09:36:04 -07:00
Leonardo de Moura
990f428a81 Remove virtual method kind from value class and subclasses. We can use dynamic_cast to achieve the same goal 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 09:35:10 -07:00
Leonardo de Moura
81d0203ee0 Replace macros TypeM, TypeU, Int, Bool, True and False with constant global expressions. The macros were producing counterintuitive behavior. For example, we had an enumeration type with an element called Int. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 09:11:53 -07:00
Leonardo de Moura
db88920f81 Rename normalize and type_check to normalizer and type_checker (using a consistent naming convention) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-02 08:43:38 -07:00
Leonardo de Moura
c97e669f0c Add coercion support in the elaborator and pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 19:09:07 -07:00
Leonardo de Moura
e8c09015ad Move elaborator to lean default frontend. It is getting too specific 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 18:22:24 -07:00
Leonardo de Moura
42be7a4989 Add coercion declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 18:11:28 -07:00
Leonardo de Moura
75f4ec5092 Add functions for 'updating expressions'. The new functions are used to simplify the elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 15:37:30 -07:00
Leonardo de Moura
61a8fd16db Remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 14:57:08 -07:00
Leonardo de Moura
d27680d7fc Add support for overloads in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 14:54:02 -07:00
Leonardo de Moura
598daa40bc Refactor elaborator for supporting overloads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 10:24:10 -07:00
Leonardo de Moura
b2924bba99 Fix typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-01 10:03:15 -07:00
Leonardo de Moura
e54338f4a8 Add a real example. Fix bug in the parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 19:32:08 -07:00
Leonardo de Moura
51640ecff8 Move files in examples directory to tests directory. They are not real examples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 19:16:30 -07:00
Leonardo de Moura
389f23f356 Add test script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 18:31:39 -07:00
Leonardo de Moura
9d9f9797e4 Improve elaborator interface. Now, the metavariables are created inside the elaborator. The elaborator-user only needs to create placeholders. Motivaton: the placeholders are meaningful independently of the elaborator. On the other hand, the metavariables depend on the elaborator state. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 17:11:06 -07:00
Leonardo de Moura
71b8b6408e Handle (and pretty print) elaborator error messages in the lean default frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 16:46:41 -07:00
Leonardo de Moura
03a5b5dbd0 Add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 14:25:27 -07:00
Leonardo de Moura
64788320f2 Fix elaborator for let-expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 14:24:07 -07:00
Leonardo de Moura
4a28a64685 Fix type checker for let expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 14:19:24 -07:00
Leonardo de Moura
793468072b Fix nontermination problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 12:32:16 -07:00
Leonardo de Moura
4c27530930 Fix missing case in the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 17:07:45 -07:00
Leonardo de Moura
4b7d4cf0d1 Add latest example to regression suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 16:39:31 -07:00
Leonardo de Moura
dadbf15e70 Change how the (auxiliary) explicit definitions are encoded in the system. The previous encoding was confusing the pretty printer, and the definition looked recursive. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 16:37:21 -07:00
Leonardo de Moura
1b6d51b0aa Mark implicit arguments of builtin symbols 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 15:56:04 -07:00
Leonardo de Moura
4ef4655183 Add homogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 14:26:12 -07:00
Leonardo de Moura
1e370023b1 Attach elaborator the lean default parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 13:25:30 -07:00
Leonardo de Moura
45d89ace65 Fix name clash problem when pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 13:25:12 -07:00
Leonardo de Moura
6efb6c6e83 Fix clang++ compilation problem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 09:04:11 -07:00
Leonardo de Moura
2aac94f2e6 Refactor elaborator using new metavar library. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 01:25:06 -07:00
Leonardo de Moura
682df7699d Fix is_convertible propositions => type 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 01:24:06 -07:00
Leonardo de Moura
1f6943e3a4 Add head_reduce_mmv (reduction function modulo metavariables) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-29 14:15:17 -07:00
Leonardo de Moura
2cf9ca9345 Add metavariable utilities. They will be used to refactor the elaborator. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-29 13:49:22 -07:00
Leonardo de Moura
01e4b4b7fe Add postprocessor functional object to the replace_fn template. Add unit-test that demonstrates how to build a replacer that builds a trace. The trace associates new expressions with the old ones that were used to create it. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-28 10:47:19 -07:00
Leonardo de Moura
cdab19b88c Simplify the elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-27 20:39:38 -07:00
Leonardo de Moura
8dacd97801 Remove obsolete commands. 2013-08-27 16:03:45 -07:00
Leonardo de Moura
a9c6088d11 Uniform notation declarations. 2013-08-27 15:59:13 -07:00
Leonardo de Moura
5aae838e1c Add missing mixfix notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-27 10:09:46 -07:00
Leonardo de Moura
85daaea8ce Rename get_exs in oper to get_deno 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-27 09:49:48 -07:00
Leonardo de Moura
206c7fa203 Implement support for notation + implicit arguments. Cleanup pretty printer code for handling implicit arguments. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-27 09:45:00 -07:00
Leonardo de Moura
76c968a5b8 Add basic support for hiding implicit arguments when pretty printing. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-26 20:35:10 -07:00
Leonardo de Moura
fc6cc17925 Improve lean pretty printer support for implicit argument annotations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-26 19:19:56 -07:00
Leonardo de Moura
7bca3705ca Add implicit argument declarations to lean parser. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-26 10:16:29 -07:00
Leonardo de Moura
7003f85213 Add implicit argument management to lean frontend. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-26 10:16:29 -07:00
Leonardo de Moura
0a34959716 Fix a bug. Add another test. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 20:43:50 -07:00
Leonardo de Moura
3721577700 Fix bugs in elaborator. Cleanup tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 18:46:33 -07:00
Leonardo de Moura
8f4a844598 Fix unit tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:42:36 -07:00
Leonardo de Moura
7e130ac47f Propagate interrupt to normalizer in the lean frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:34:46 -07:00
Leonardo de Moura
b42e04297d Add support for creating meta-variables in the parser. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:18:19 -07:00
Leonardo de Moura
25e47a8a2f Add check_interrupted 'macro' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:03:09 -07:00
Leonardo de Moura
ece6e6ca6a Add interrupt to parser. Add elaborator to parser. Add placeholder support in the scanner. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-25 11:02:34 -07:00
Leonardo de Moura
02b72acc2f Add implicit arguments unit tests 2013-08-24 18:23:39 -07:00
Leonardo de Moura
ac1267bef3 Add expression elaborator to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 18:14:09 -07:00
Leonardo de Moura
68e1a1a24a Add metavar_env to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 17:51:53 -07:00
Leonardo de Moura
dc91a7adb8 Add Ctrl-C support for interrupting Lean shell. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 16:11:35 -07:00
Leonardo de Moura
f0edf2b4a3 Pretty print kernel exceptions. Improve default lean frontend error messages. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 13:16:43 -07:00
Leonardo de Moura
0b112b6637 Add sstream to simplify the generation of exception messages. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 11:55:17 -07:00
Leonardo de Moura
48ba655bd5 Store position at parser_error. It produces better error messages. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 11:30:54 -07:00
Leonardo de Moura
55eaef1a44 Save position information when parsing expression in the lean default fronted. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-24 09:56:07 -07:00
Leonardo de Moura
bf608a38aa Add head_reduce 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 19:35:33 -07:00
Leonardo de Moura
be1ea2ddc7 Add name_set typedef 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 19:34:10 -07:00
Leonardo de Moura
e95a0c2559 Modify basic printer for contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 12:11:16 -07:00
Leonardo de Moura
18a195029b Refactor expression equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
f08c06d582 Add head_beta tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
e7487a1fec Add head_beta function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
670dc5ad55 Add option to control maximum recursion depth in the expression normalizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

Conflicts:
	src/tests/kernel/normalize.cpp
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
198fd46fc2 Track recursion depth at normalizer. Add fluid let template. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
d30c6b2c9d Fix spaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
42a7094ca2 Fix bug in display_decimal. Add more mpq tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Leonardo de Moura
218b6ac8b7 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-23 09:42:49 -07:00
Soonho Kong
ca779265e5 Update src/CMakeLists.txt to increase stack size for windows build 
[skip ci]
 2013-08-22 21:16:57 -07:00
Leonardo de Moura
f1462dc51e Change lean frontend specific options. Now, frontend specific options must begin with the frontend name. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 10:55:55 -07:00
Leonardo de Moura
0f6a7e4a95 Rename exprlib to library. Name was misleading, it is more than a library for manipulating expressions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 10:26:52 -07:00
Leonardo de Moura
60fdcf0011 Add option_declaration tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 08:59:39 -07:00
Leonardo de Moura
5d813c30d0 Add missing option test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 08:51:33 -07:00
Leonardo de Moura
fbd25cac9f Add hierarchical names tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 08:48:52 -07:00
Leonardo de Moura
1b5fcb80ee Add sexpr tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 08:30:52 -07:00
Leonardo de Moura
6272408f12 Add format tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 08:20:42 -07:00
Leonardo de Moura
3c5f993191 Fix bugs in options module. Add more tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-22 08:08:55 -07:00
Leonardo de Moura
eb4315baab Add small trick to improve pretty printer performance. Now, deep.lean takes 0.140secs to be processed. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 22:54:58 -07:00
Leonardo de Moura
56d2d2a112 Improve pretty printer performance for deep formulas and formats with long lines. Add example that demonstrates performance problem (before: 13 secs, after: 1 sec). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 22:45:48 -07:00
Leonardo de Moura
aceae7a1b2 Change policy for adding input to readline history. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 19:43:47 -07:00
Leonardo de Moura
bd3b422158 Add support for READLINE. Remark: it is not enabled by default. Rename tcmalloc option to TCMALLOC (using consistent name convention for cmake parameters). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 19:08:44 -07:00
Leonardo de Moura
59e63c0421 Add prompt when in interactive mode. Fix Show Environment [num] 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 18:24:26 -07:00
Leonardo de Moura
0ffa76aa5e Fix unused variable warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 17:02:09 -07:00
Leonardo de Moura
31460aa5b8 Add option declarations. Add Help. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 17:02:09 -07:00
Leonardo de Moura
65898f6d5b Add Import command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 17:02:09 -07:00
Leonardo de Moura
90678566b4 Improve lambda/pi formatting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 17:02:09 -07:00
Soonho Kong
5f1c12feb8 Fix interval<T>::mul to suppress clang warnings 2013-08-21 14:35:46 -07:00
Soonho Kong
c9b6be829e Doxygen: exclude src/tests directory 2013-08-21 14:35:46 -07:00
Soonho Kong
3f40953efc Add comments for unicode symbols, fix a typo 2013-08-21 14:35:45 -07:00
Leonardo de Moura
ce470f57db Add set options to lean_parser. Add support for disabling unicode output. Use channels in lean_parser. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 12:42:55 -07:00
Leonardo de Moura
6534142fb9 Fix annoying problem when an integer occurs in the end of a command. Example 'Show 1.' was being parsed as 'Show 1.0'. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 11:57:22 -07:00
Leonardo de Moura
d750469667 Move frontend to frontends/lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-21 09:04:49 -07:00
Leonardo de Moura
6f36611010 Fix clang++ error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
7778ae0ade Fix cyclic reference: frontend -> state -> pp_formatter -> frontend. Now pp_formatter is only valid while frontend is still alive. This should not be problem in practice. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
3f5a2a83cc Add methods for setting options. Add string output channel. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
4fa2468a85 Add output_channel and state abstractions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
73262e9786 Add Echo command. Allow '\' 'n' escape sequence in strings. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
57b9a4f2b3 Allow square brackets to be used in operator names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
fbb021386c Add minor improvement to pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Leonardo de Moura
d82c60a314 Add test normalizer interrupt 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-20 20:16:02 -07:00
Soonho Kong
fce26a824e Implement dependencies on interval arithmetic functions (+,-,*,/,inv,power), fix problems on trigonometric functions 2013-08-20 19:49:50 -07:00
Soonho Kong
176b1fccf7 Implement dependencies on interval functions (exp, log, and trigonometric functions) 2013-08-20 02:03:24 -07:00
Leonardo de Moura
b2ba0618c9 Use normalizer object in type checker. The idea is to make sure the interruption is propagated to normalizer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Leonardo de Moura
88cc3dc20d Add interrupt to normalizer. Fix tests (they were not using the basic printer). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Leonardo de Moura
f6ea9fca7d Remove interrupt.cpp. We changed the way we will handle interruptions in Lean. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Leonardo de Moura
b964edfb3e Add interrupt method to type checker. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Leonardo de Moura
eba4172a0c Remove verbosity.cpp, verbosity message channel should not be a global. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Leonardo de Moura
f5e0150db3 Allow notation to be associated with arbitrary expression (instead of only constants). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Leonardo de Moura
f0b5ec8dfa Fix bug in parse_arrow 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 20:05:56 -07:00
Soonho Kong
db8322e6e8 Fix interval::sin to suppress a warning 2013-08-19 16:46:36 -07:00
Leonardo de Moura
754227fc89 Pretty print forall/exists expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 15:48:31 -07:00
Leonardo de Moura
986d9635e1 Add syntax sugar for forall/exists expressions. Fix problem when pretty printing nested equalities. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 15:48:07 -07:00
Leonardo de Moura
de80db3985 Add support for pretty printing Dags. Find unused prefix for naming shared expressions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 12:04:40 -07:00
Leonardo de Moura
90ad0ba3b3 Add is_prefix_of for hierarchical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 11:43:46 -07:00
Leonardo de Moura
b2c877b0c3 Add comments to parser.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-19 09:39:46 -07:00
Leonardo de Moura
ce43c1cbae Fix cup symbol. In Emacs, the unicode characters cup and cap are assigned incorrectly. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 18:43:31 -07:00
Leonardo de Moura
a46bf357b0 Fix bug in level.cpp. Add new example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 18:37:47 -07:00
Leonardo de Moura
95cfac426d Add parse_level. Fix bug at environment::is_ge 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 18:25:34 -07:00
Leonardo de Moura
5d609928af Add support for reading input files from the command line. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 16:23:29 -07:00
Leonardo de Moura
aa49eb4b0f Run examples during testing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 15:51:27 -07:00
Leonardo de Moura
676ebcca3d Add parse_arrow 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 15:44:39 -07:00
Leonardo de Moura
4d5b65fe87 Fix bug in parser. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 15:25:20 -07:00
Leonardo de Moura
afd62ced87 Add parse_let 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 15:25:20 -07:00
Leonardo de Moura
7a9319b72e Pretty print let expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 15:25:20 -07:00
Leonardo de Moura
ae523e33b4 Add parse_theorem and parse_definition 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 12:48:42 -07:00
Leonardo de Moura
5d2027d889 Add parse_lambda and parse_pi 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 12:34:00 -07:00
Leonardo de Moura
843253355b Improve parser 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
cdccca9316 Rename builtin operator if-then-else 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
51280864cf Move '\' character to class b 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
7ec7b4dce8 Fix bug in pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
18f319d00f Add more notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
823fe6df07 Move test from lean.cpp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
c82a704302 Add Lean default application. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Soonho Kong
ec83fd8093 Fix interval::acosh and add more tests on interval to improve code coverage 2013-08-18 01:20:16 -07:00
Leonardo de Moura
65b4845fbc Add more tests to improve coverage. Fix bug in mpz. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 00:28:50 -07:00
Soonho Kong
3b0a7a2d96 Update src/CMakeLists.txt to include 'TESTCOV' build 2013-08-17 20:58:05 -07:00
Leonardo de Moura
06f1b2a7db Add parse_expr. Add more tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 18:35:50 -07:00
Leonardo de Moura
685aeae43a Add parser skeleton 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 18:13:55 -07:00
Leonardo de Moura
f1961ab33f Add another pp example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 12:38:32 -07:00
Leonardo de Moura
80ec48c93d Make sure formatter can be used even when associated frontend is not in scope. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 12:33:19 -07:00
Leonardo de Moura
6edae938b7 Improve list iterator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 11:31:36 -07:00
Leonardo de Moura
a6f36ba546 Improve formatter usage. Fix bug in object printer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 11:29:43 -07:00
Leonardo de Moura
0f3af23778 Fix crash when trying to format an object created by a different frontend. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 11:04:22 -07:00
Leonardo de Moura
b633c866e6 Expose environment API in the frontend object. Add support for formatting objects. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-17 10:55:42 -07:00
Leonardo de Moura
c6226c6951 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:51:11 -07:00