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

769 commits

Author SHA1 Message Date
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
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
Soonho Kong
70f383eb82 Add unary minus operator overloadings to mpq & mpfp 2013-08-14 00:01:03 -07:00
Soonho Kong
d51e2e3a25 Add more test to interval 2013-08-13 23:05:00 -07:00
Soonho Kong
e0ffaed41a Fix log/exp in interval 2013-08-13 23:04:55 -07:00
Soonho Kong
60ee5e08fb Add more test to interval 2013-08-13 20:09:06 -07:00
Soonho Kong
548f5f069a Add fmod, sin, cos to interval<T> 2013-08-13 20:09:06 -07:00
Soonho Kong
d5f2d6b26f Fix default constructor of interval<T> to call reset method to assign 0 2013-08-13 20:09:06 -07:00
Soonho Kong
5f143f164e Fix numeric_traits<mpfp>::pi constants 2013-08-13 20:09:06 -07:00
Soonho Kong
8eb87fbeae Fix interval<T>::operator- and interval<T>::operator/ 2013-08-13 20:09:06 -07:00
Soonho Kong
02900e2c83 Add abs/floor/ceil to double/float/mpq/mpfp 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
27b3ac19a7 Fix clang warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-13 07:16:46 -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
b308355426 Add missing tokens 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-13 03:52:08 -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
Leonardo de Moura
ac38937241 Remove parsers directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-13 01:25:42 -07:00
Soonho Kong
c700707f37 Add more tests to interval 2013-08-13 00:35:14 -07:00
Soonho Kong
26d8bd2c12 Add binary operators between interval<T> and T 2013-08-13 00:35:14 -07:00
Soonho Kong
cebe7d415a Fix empty interval 2013-08-13 00:35:14 -07:00
Soonho Kong
e123dd8e58 Use numeric_traits<mpfp>::get_mpfp_rnd() as a default rounding mode in mpfp operations 2013-08-13 00:35:14 -07:00
Soonho Kong
30e34528f6 Use lowercases in src/CMakeLists.txt 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
Leonardo de Moura
68ca5d84e2 Remove unnecessary '--' in status messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-12 15:37:36 -07:00
Leonardo de Moura
fb56869aae Fix cygwin problem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-12 15:22:08 -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
1c9e5226d8 Fix compile-error by adding "defined" to interval_def.h 2013-08-12 14:58:18 -07:00
Soonho Kong
6bbe592e2a Add double/mpfp interval tests 2013-08-12 14:58:18 -07:00
Soonho Kong
71e10a0336 Add missing initialization of numeric_traits<mpfp>::rnd 2013-08-12 14:58:17 -07:00
Soonho Kong
ec233496b6 Fix types of copy/move constructors in interval.h 2013-08-12 14:58:17 -07:00
Leonardo de Moura
7778541422 Send status messages to standard output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-12 14:56:40 -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
2ad9c89684 Fix memory leak in mpfp. Add mpfp finalizer to avoid Valgrind warnings. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-12 11:36:15 -07:00
Soonho Kong
99df36f747 Add missing header <numeric> to format.h 2013-08-12 10:58:07 -07:00
Soonho Kong
2b6d8a4d01 Update CMakeLists.txt to support OSX + Clang 2013-08-12 10:58:07 -07:00
Leonardo de Moura
6cb46d9de7 Remove Flex/Bison requirement, we will not use them. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-11 18:09:47 -07:00
Leonardo de Moura
e07830d0f5 Fix nasty crash that only happens when using cygwin. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-11 14:35:58 -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
3a1514982f Add small optimization. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-10 21:02:45 -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
19440bc103 Fix clang warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-10 16:58:15 -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
3d9f9a12d1 Enable automatic coercion from 'char const *' to hierachical name 
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
Soonho Kong
375bc817cc Add more to mpfp 2013-08-09 22:41:07 -07:00
Soonho Kong
40bdd1a36b Fix typos in format.h (error messages) 2013-08-09 22:41:07 -07:00
Soonho Kong
a1229692b0 Add static_asserts for higher-order functions in kernel/for_each.h and kernel/pp.cpp 2013-08-09 22:41:07 -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
Leonardo de Moura
33e8e4af23 Add initializer list constructor for hierarchical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-08 18:38:18 -07:00
Leonardo de Moura
f18149934b Move sexpr to util directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-08 18:38:18 -07:00
Leonardo de Moura
b50d9df784 Add options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-08 18:38:18 -07:00
Leonardo de Moura
ecf9506abe Add object iterator for environment objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-08 18:38:18 -07:00
Soonho Kong
635407ca4a Fix sexpr_text_length function to handle quotation in string 2013-08-08 12:24:42 -07:00
Soonho Kong
9516d9f88f Restructure format, and fix bugs 2013-08-08 12:24:19 -07:00
Soonho Kong
fe9d2147d2 Improve performance of format by using "space_upto_line_break" instead of "fits" 2013-08-08 10:34:15 -07:00
Leonardo de Moura
2d4caa7450 Mark 'implicit' parameters, and move them to the beginning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 21:53:19 -07:00
Leonardo de Moura
e558edcd52 Use ',' as separator for lambda 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 21:53:19 -07:00
Leonardo de Moura
3fbc506271 Rename Truth to Trivial, and delete Trivial macro 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 21:53:19 -07:00
Leonardo de Moura
bede62e2f7 Fix bug in sexpr operator <<. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 21:53:19 -07:00
Soonho Kong
0f48f73e14 Add constants and transcendental functions to mpfp 2013-08-07 19:32:15 -07:00
Soonho Kong
03dc15868b Add more operator overloadings to mpfp 2013-08-07 19:32:15 -07:00
Soonho Kong
b970c964ff Add transcendental functions to interval (still need to fill more...) 2013-08-07 19:32:15 -07:00
Soonho Kong
8d06185694 Add is_empty & set_empty to interval 2013-08-07 19:32:15 -07:00
Soonho Kong
93b99cf1ec Add constants(Pi, 1/2Pi, 2Pi) to double, float, and mpq 2013-08-07 19:32:03 -07:00
Soonho Kong
3bdfdcc36c Add transcendental functions to interval.h 2013-08-07 19:32:03 -07:00
Soonho Kong
2a8c9e9c06 Reformat mpfp.h 2013-08-07 19:32:03 -07:00
Soonho Kong
ea6b4ddca7 Add more tests to interval 2013-08-07 19:32:03 -07:00
Soonho Kong
d3dbcadf8b Add placeholders for transcendental functions in mpbq & mpq 2013-08-07 19:32:02 -07:00
Leonardo de Moura
2670e94398 Add pretty printer for Lean environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 19:10:12 -07:00
Leonardo de Moura
f8e3563034 Add scoped sets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 13:54:18 -07:00
Leonardo de Moura
84de625ee4 Rename pp functions (that do not use format lib) to print 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 12:10:10 -07:00
Leonardo de Moura
dd21cdcc95 Add more theorems. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 11:23:04 -07:00
Leonardo de Moura
5acedcddbb Remove useless is_* functions. We can use equality for that (more readable and similar performance). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 08:34:50 -07:00
Leonardo de Moura
2d27573e0c Add ImpAntisym axiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 08:29:20 -07:00
Leonardo de Moura
722e2b0ed4 Reformat code (make formating more consistent) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 08:17:33 -07:00
Leonardo de Moura
58fef282c3 Refactor theorems. Add new theorems. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-07 01:16:37 -07:00
Leonardo de Moura
345894d4ed Add => as a primitive. Define Not, And and Or using =>. Add MP and Discharge as axioms. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 20:22:09 -07:00
Soonho Kong
e953032c22 Update interval 2013-08-06 20:01:20 -07:00
Soonho Kong
5efd2fdd6f Update util/numerics/CMakeLists.txt to add mpfp, double, float 2013-08-06 20:01:09 -07:00
Soonho Kong
975730a3fb Add test for mpfp 2013-08-06 20:00:37 -07:00
Soonho Kong
fb41a4f5a3 Add numeric_traits for double and float 2013-08-06 20:00:37 -07:00
Soonho Kong
d22b4bc9f1 Add mpfp, a wrapper for MPFR 2013-08-06 19:59:58 -07:00
Soonho Kong
59ec8357f4 Require GMP version 5.0.5 2013-08-06 19:55:34 -07:00
Leonardo de Moura
d88ff6f8e1 Add more theorems 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 19:10:38 -07:00
Leonardo de Moura
d1388f5e3c Define Lean forall. Prove forall elimination. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 16:44:58 -07:00
Leonardo de Moura
4c28cb933b Fix bug in is_convertible 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 16:44:22 -07:00
Leonardo de Moura
3ff3eb6444 Add Eta axiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 14:47:13 -07:00
Leonardo de Moura
68d092f5ef Prove congr1, congr2 and congr theorems. Add xtrans theorem. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 14:37:30 -07:00
Leonardo de Moura
ab915fb3f0 Add add_theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 12:24:20 -07:00
Leonardo de Moura
9d6b421be9 Add theorems Truth, EqMP and EqTElim 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 12:17:55 -07:00
Leonardo de Moura
84f4a32c0e Change name convention for creating Lean expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 11:27:14 -07:00
Leonardo de Moura
33d2dd2d8b Add subst proof rule. Define symm and trans using subst. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 02:03:22 -07:00
Leonardo de Moura
30513398bb Add basic definitions and axioms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Leonardo de Moura
8aee11e538 Fix test failure when using clang++ and release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Leonardo de Moura
2986f0543e Simplify how universe variable constraints are represented in the kernel. Allow universe variable to be created without an environment. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Leonardo de Moura
7e2d7dcf3d Add more builtin constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Leonardo de Moura
f6057e2b28 Add more environment tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Leonardo de Moura
0c610e0a77 Fix bug in type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Soonho Kong
8dab224137 Fix CMakeLists.txt 2013-08-05 19:16:52 -07:00
Soonho Kong
52232f37cb Add numeric_traits<double> and numeric_traits<float> which are using MPFR 2013-08-05 18:57:09 -07:00
Soonho Kong
a6f825caa5 Add MPFR & restructure cmake directory 2013-08-05 17:58:54 -07:00
Leonardo de Moura
70de591934 Add definitions and facts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 20:52:14 -07:00
Leonardo de Moura
5f77a2367f Allow Boolean expressions (aka propositions) to be used as types. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 18:26:01 -07:00
Leonardo de Moura
4b5d60f2b2 Add get_uvar method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 17:47:54 -07:00
Leonardo de Moura
c97db1f0cf Add children environments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 16:07:37 -07:00
Leonardo de Moura
95447deea3 Add normalization a = b for values (aka semantic attachments) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 14:54:33 -07:00
Leonardo de Moura
f0ccb2a03e Rename eqp --> is_eqp. The name is too similar to heterogeneous equality constructor eq. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 09:41:49 -07:00
Leonardo de Moura
3f789ce2b7 Add let and heterogeneous equality. Add bool_type and bool_value. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-04 09:37:52 -07:00
Leonardo de Moura
b979436c40 Add basic semantic attachments for arithmetic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 19:57:06 -07:00
Leonardo de Moura
15a4152ce8 Fix merge problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:13:56 -07:00
Leonardo de Moura
0a679074f0 Add support for semantic attachments. Remove expr_numeral 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:15 -07:00
Leonardo de Moura
1fec8b0d5b Rename (stack) value to svalue 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:15 -07:00
Leonardo de Moura
0b8fa3b167 Remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:15 -07:00
Leonardo de Moura
cce469119f Flip order of the arguments for instance and abstract. Simplify type_checker. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:15 -07:00
Leonardo de Moura
190855ad1b Add (relaxed) version of instantiate that can substitute terms containing free variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:15 -07:00
Leonardo de Moura
2972bdfec3 Rename abst_type to abst_domain 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:12 -07:00
Leonardo de Moura
e1e3e6b2d6 Add instantiate tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:10:20 -07:00
Leonardo de Moura
b67a92cf10 Add scanner base class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:10:20 -07:00
Soonho Kong
bac75541dc Add static_asserts to template funcs in expr.h & replace.h 2013-08-02 20:00:40 -07:00
Soonho Kong
fd7f0e9658 Update format test 2013-08-02 20:00:40 -07:00
Soonho Kong
83edc38fa1 Change folddoc to fold_right, add static_asserts for template functions 2013-08-02 19:48:11 -07:00
Soonho Kong
5f10d47035 Change operators in format: 
f1 + f2 = f1 <> f2
f1 ^ f2 = f1 <> " " <> f2
 2013-08-02 19:17:29 -07:00
Soonho Kong
bddecd7d9c Roll back to flatten(line) == " " 2013-08-02 19:16:19 -07:00
Soonho Kong
4ebb96d7cd Add static_asserts to sexpr_funcs.h 2013-08-02 18:26:51 -07:00