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

49 commits

Author SHA1 Message Date
Leonardo de Moura
c4c548dc5d feat(*): simplify interrupt propagation 
Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.

The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:

    try-for (T1 ORELSE T2) 5

It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 21:45:48 -08:00
Leonardo de Moura
a9b2be0b9c feat(frontends/lean): add support for embedded Lua scripts in Lean files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-07 13:56:04 -08:00
Leonardo de Moura
40fde1a69c test(lua): invoke Lua binding tests from ctest 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-05 13:17:10 -08:00
Leonardo de Moura
f13a97397f feat(lua): expose s-expressions in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 19:58:32 -08:00
Leonardo de Moura
0579970fc5 feat(lua): expose options object in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 14:38:49 -08:00
Leonardo de Moura
543aea65c9 chore(lua): rename init_* functions to open_* 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-04 13:54:51 -08:00
Leonardo de Moura
fd7e85f0bb feat(lua): add safe_function template that catches Lean and C++ exceptions and convert them into Lua errors 
I'm using the approach described at:
http://stackoverflow.com/questions/4615890/how-to-handle-c-exceptions-when-calling-functions-from-lua

BTW, in some Lua versions, the C++ exceptions are correctly propagated.
I think we should not rely on features of particular implementations.
For example, LuaJIT does not propagate C++ exceptions.
Whenever an exception is thrown from C++ code invoked from LuaJit, LuaJit interrupts the execution and converts it to an error "C++ exception".
On the other hand, Lua 5.2 PUC-Rio interpreter (for Ubuntu) seem to propagate the C++ exceptions.
The template safe_function solves the issue. It will also produce a Lua error whenever the function being wrapped throws an exception. The error message is based on the "what()" method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 14:42:57 -08:00
Leonardo de Moura
1a734979b4 fix(shell/lua): catch lean exceptions in the leanlua frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 13:46:15 -08:00
Leonardo de Moura
e2da8c1f4d feat(lua/numerics): expose mpz and mpq numbers in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-03 12:05:54 -08:00
Soonho Kong
88ebdbcfb6 fix(shell/lua): move "#include<iostream>" 2013-11-03 13:25:33 -05:00
Leonardo de Moura
dbf2d56c77 feat(lua/name): expose hierarchical names in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-02 20:49:42 -07:00
Leonardo de Moura
d843d432d3 refactor(kernel): move printer and formatter objects to the kernel 
The printer and formatter objects are not trusted code.
We moved them to the kernel to be able to provide them as an argument to the trace objects.
Another motivation is to eliminate the kernel_exception_formatter hack.
With the formatter in the kernel, we can implement the pretty printer for kernel exceptions as a virtual method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Soonho Kong
ab6ca82e6f Update to suppress unused-parameter warnings 2013-09-19 22:40:34 -07:00
Soonho Kong
bc60b47295 Apply coding style 2013-09-13 18:48:09 -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
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
9f34f96b08 Add another example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-04 05:40:28 -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
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
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
03a5b5dbd0 Add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-31 14:25:27 -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
4ef4655183 Add homogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-30 14:26:12 -07:00
Leonardo de Moura
8dacd97801 Remove obsolete commands. 2013-08-27 16:03:45 -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
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
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
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
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
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
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
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
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
c82a704302 Add Lean default application. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-18 11:02:29 -07:00
Leonardo de Moura
c581990f67 Clean white-spaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-19 10:29:33 -07:00
Leonardo de Moura
e559bf73a9 Add basic testing infrastructure using CTest 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-18 09:12:07 -07:00
Leonardo de Moura
4ccf770b64 Move mpz, mpq and mpbq to numerics directory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 14:33:00 -07:00
Leonardo de Moura
d028041135 Add methods to mpz, mpq, mpbq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 14:24:35 -07:00
Leonardo de Moura
88b49ec21f Add thread_local test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 12:43:28 -07:00
Leonardo de Moura
c0f9f06d70 Set clang++ as default compiler. Add -pthread as a linker flag 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-17 12:41:28 -07:00
Leonardo de Moura
501f63e27d Add build instructions. Improve build. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-16 22:32:21 -07:00
Leonardo de Moura
139f4f2a7f Add simple build system based on cmake 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-16 22:10:51 -07:00