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

402 commits

Author SHA1 Message Date
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
Leonardo de Moura
15c1c97873 Refactor frontend pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Leonardo de Moura
93ab18df71 Add context_to_lambda hack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Leonardo de Moura
0fbfef8eb0 Remove sanitize_names from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Leonardo de Moura
e792e079e2 Add formatter API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Leonardo de Moura
cbff5ea856 Cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Leonardo de Moura
111cdd4e62 Remove pretty printer from kernel. Add basic printing capability to exprlib module. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Leonardo de Moura
519a290f32 Refactor kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 20:40:39 -07:00
Soonho Kong
c5cc5d1739 Optimize interval functions to reduce rounding-mode switches 2013-08-16 19:58:56 -07:00
Soonho Kong
93475ac2eb Clean up interval check function 2013-08-16 19:58:56 -07:00
Soonho Kong
3d8eda2239 Fix src/tests/interval/CMakeLists.txt to have different test names 2013-08-16 19:58:56 -07:00
Leonardo de Moura
c41b3dc4d8 Add kernel_exceptions. The idea is to avoid expression formatting in the kernel. It also allows different frontends to display the error messages is a different way. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 12:51:12 -07:00
Leonardo de Moura
1038f7346e Refine initialization order. Polish Universe command pretty printer. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 09:30:08 -07:00
Leonardo de Moura
4560527058 Conjunction and Disjunction are right associative. Add notation for implication. Use Isabelle precendence levels. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 09:26:05 -07:00
Leonardo de Moura
abab4b667a Define implies using ite operator. Rename mk_bin_op to mk_bin_rop (it is using right associativity). Add mk_bin_lop (for left assoc). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 09:04:59 -07:00
Leonardo de Moura
1c30c68d2d Refine toplevel API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 09:02:45 -07:00
Leonardo de Moura
d002074419 Fix uninitialized variables bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-16 09:02:07 -07:00
Leonardo de Moura
07946f9e32 Fix bug in pretty printer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 20:10:00 -07:00
Leonardo de Moura
efbf3a434d Highlight assignment keyword 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 20:00:12 -07:00
Leonardo de Moura
43fa55723a Pretty print condensed definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:56:29 -07:00
Leonardo de Moura
5ec2780321 Extend formatter with support for definitions and postulates. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:26:58 -07:00
Leonardo de Moura
790d4a4447 Move pretty printer to frontend. Add support for mixfix pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
5395ced0e5 Improve comments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
e9106f7512 Delete obsolete function continue_on_violation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
d6d221b992 Move auxiliary files away from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
99219f998b Rename files sets.h and maps.h to expr_sets.h and expr_maps.h 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
013fa866fa Add iterator for traversing local objects (i.e., ignores objects defined in ancestor environments) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
2b7834c5fc Add methods for creating infix, prefix, postfix operators in the frontend object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Leonardo de Moura
577256fedc Add highlight_keyword, highlight_builtin, highlight_command for consistent formatting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-15 19:02:28 -07:00
Soonho Kong
c5db989e38 Add csc, sec, cot to interval & add tests for them 2013-08-15 17:44:11 -07:00
Soonho Kong
a6f3122146 Fix cygwin error caused by the use of thread_local in numerics/float class 2013-08-15 13:49:15 -07:00
Soonho Kong
25bfb58f17 Update interval tests to reduce compile-time 2013-08-15 11:32:27 -07:00
Soonho Kong
7059836e21 Add more tests for float and double interval 2013-08-14 23:49:27 -07:00
Soonho Kong
f87b4394d3 Fix precision problem in interval<T>::cos 2013-08-14 23:49:27 -07:00
Soonho Kong
eb29a67395 Fix mpfp::operator^= to resolve operator overloading problem 2013-08-14 23:49:26 -07:00
Leonardo de Moura
2d74ff5fe0 Cache results of the normalizer. Add example that demonstrates the exponential performance improvement. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 23:18:50 -07:00
Leonardo de Moura
984c4149fa Add helper functions for creating Let expressions. Add simple type checking test for Let expressions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 22:30:12 -07:00
Soonho Kong
da764aec14 Add more test to interval, to check inclusion property of the results 2013-08-14 19:55:47 -07:00
Soonho Kong
0a2ac88dd1 Fix interval<T>::cosh 2013-08-14 19:55:47 -07:00
Soonho Kong
cd71218a68 Fix interval::sin and interval<tan> to pass inclusion property check 2013-08-14 19:55:47 -07:00
Soonho Kong
ce74c62226 Change interval<T>::contains to take const argument 2013-08-14 19:53:07 -07:00
Soonho Kong
a56bfe3397 Fix interval<T>::power(n) to round downward/upward when n is odd number 2013-08-14 19:53:07 -07:00
Leonardo de Moura
b0f2ee6de0 Add notation support to frontend object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
f604be760d Add helper function for maps. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
913fd14549 Add operator== to list 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
5bfb074eaf Create objects for universe variable declarations. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
285c8dafdc Display context_entry body when pretty printing contexts. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
d71c36ed60 Improve sanitizer test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
23d245bb2e Sanitize context names before generating error messages. Add [[ noreturn ]] attribute to functions that always throw exceptions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
a6f0a69186 Avoid head and tail when manipulating contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:18 -07:00
Leonardo de Moura
56305e4672 Add sanitize_names for (local) contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:17 -07:00
Leonardo de Moura
e5b8c45b3f Rename type to domain in contexts (aka telescopes). Reason: make name convention consistent with the one used for abstractions (lambdas and pis). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:17 -07:00
Leonardo de Moura
338ce88ea0 Add occurs function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 18:17:17 -07:00
Soonho Kong
38a3dfdd85 Fix interval<T>::cosh 2013-08-14 15:06:02 -07:00
Soonho Kong
eaa531bc02 Add asinh, acosh, atanh to interval 2013-08-14 15:06:02 -07:00
Soonho Kong
43b25a0231 Add operator<(mpq, double) to mpq 2013-08-14 13:45:29 -07:00
Soonho Kong
5a38480cf7 Remove "continue_on_violation(true);" from tests 2013-08-14 13:24:18 -07:00
Soonho Kong
49b8bde67c Add asin, acos, atan, sinh, cosh, tanh to interval 2013-08-14 12:08:24 -07:00
Soonho Kong
56f4050932 Add {float,double,mpfp}_interval.cpp in tests/interval 2013-08-14 10:56:05 -07:00
Soonho Kong
840403db42 Add more test 2013-08-14 00:01:29 -07:00
Soonho Kong
8ce6bc8050 Add tan to interval 2013-08-14 00:01:23 -07:00