Commit graph

249 commits

Author SHA1 Message Date
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
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
02b72acc2f Add implicit arguments unit tests 2013-08-24 18:23:39 -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
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
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
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
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
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
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
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
d82c60a314 Add test normalizer interrupt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-20 20:16:02 -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
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
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
676ebcca3d Add parse_arrow
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-18 15:44:39 -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
843253355b Improve parser
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
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
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
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
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
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
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
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
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
Soonho Kong
c5db989e38 Add csc, sec, cot to interval & add tests for them 2013-08-15 17:44:11 -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
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
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
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
338ce88ea0 Add occurs function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-14 18:17:17 -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
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
d51e2e3a25 Add more test to interval 2013-08-13 23:05:00 -07:00
Soonho Kong
60ee5e08fb Add more test to interval 2013-08-13 20:09:06 -07:00
Leonardo de Moura
2dad1e0e33 Fix type mismatch error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 19:24:11 -07:00
Leonardo de Moura
392b347f53 Add expr_formatter and expr_locator. Add better error messages. Improve simple printer.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 19:16:40 -07:00
Leonardo de Moura
3bcbdf7c7b Add options to customize formatter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 16:19:30 -07:00
Leonardo de Moura
11a9cac5d6 Refactor kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 15:13:54 -07:00
Leonardo de Moura
00c06839a4 Fix scanner. Add scanner tests. Add itera to list::iterator. Add parser_exce.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 10:55:41 -07:00
Leonardo de Moura
0a4e03efc5 Remove option name::separator, it can't be configured during runtime
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 08:18:01 -07:00
Leonardo de Moura
963afa4861 Add missing files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 07:07:14 -07:00
Leonardo de Moura
2ea7479ee9 Move sexpr/format/options to util/sexpr (reason: circular dependency between util and numerics lib), now numerics depend on util, and sexpr depends on numerics and util. Add scanner to frontend.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-13 03:40:51 -07:00
Soonho Kong
c700707f37 Add more tests to interval 2013-08-13 00:35:14 -07:00
Leonardo de Moura
8142317983 Fix typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 19:15:12 -07:00
Leonardo de Moura
50cf3e42f1 Add operator_info
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 19:12:44 -07:00
Soonho Kong
916e348dec Disable thread-related tests on OSX due to the bug on gcc-4.8.1 2013-08-12 14:58:18 -07:00
Soonho Kong
6bbe592e2a Add double/mpfp interval tests 2013-08-12 14:58:18 -07:00
Leonardo de Moura
ca4c37528f Fix cygwin compilation error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 14:50:48 -07:00
Leonardo de Moura
276240748e Add simple thread example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-12 14:10:21 -07:00
Leonardo de Moura
4eeb72b0ee Fix performance problem in has_free_var. Add new test at src/tests/kernel/free_vars.cpp that exposes the problem.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-11 11:19:59 -07:00
Leonardo de Moura
6d9a342f17 Add regression test to expose bug fixed in previous commit.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 22:14:27 -07:00
Leonardo de Moura
5c6ee647a9 Fix bug in has_free_vars_fn. Add optimization to type_checker.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 22:05:04 -07:00
Leonardo de Moura
7ebaac62a8 Add scoped_map. Cache type checker results.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 19:27:56 -07:00
Leonardo de Moura
f79c0d3546 Add support for cygwin
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
03461df55e Add frontend object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
9fbe99bf58 Rename define_uv -> add_uvar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
c6d0afcc40 Rename sexpr eqp to is_eqp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-10 14:21:13 -07:00
Leonardo de Moura
e5fe016a44 Add pretty printer for s-expressions and options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-08 18:38:18 -07:00