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

1026 commits

Author SHA1 Message Date
Leonardo de Moura
53dc8c8c57 test(util/shared_mutex): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 14:03:18 -08:00
Leonardo de Moura
88b2feff6f test(doc/lua): add script for validating examples in the Lua API documentation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 12:49:57 -08:00
Leonardo de Moura
4d1d3d7cc7 fix(build): cygwin also needs the LEAN_WINDOWS flag 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 12:40:02 -08:00
Leonardo de Moura
bfc4023a9e fix(tests/kernel/expr): remove unused function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 10:09:47 -08:00
Leonardo de Moura
80fccc5533 fix(util/realpath): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:55:16 -08:00
Leonardo de Moura
e0c23e5984 fix(kernel/environment): compilation problem on Windows 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:52:47 -08:00
Leonardo de Moura
b2d1acd0b7 test(lua/environment): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:27:46 -08:00
Leonardo de Moura
1315378ebb test(*): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 09:13:34 -08:00
Leonardo de Moura
93b02a6fad fix(lua): fix C++ stack unwinding bug, we should never invoke lua_error from a catch block 
lua_error and luaL_error are based on the longjmp C function. They will not correctly unwind the C++ stack. We should only invoke them after we finished handling the C++ exceptions and unwinding the C++ stack, and invoking the destructors for each object living on the stack.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 06:49:54 -08:00
Leonardo de Moura
2ccd5cc559 fix(lua): workaround memory leak problem with __cxa_thread_atexit code generated by g++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 06:40:32 -08:00
Leonardo de Moura
7976937e4c test(lua/metavar_env): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 19:18:47 -08:00
Leonardo de Moura
69be5f6c94 feat(kernel/environment): track which modules were already imported 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 18:15:44 -08:00
Leonardo de Moura
5254dba195 test(library/update_expr): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 13:36:15 -08:00
Leonardo de Moura
df94e44806 test(lua/expr): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:46:24 -08:00
Leonardo de Moura
f586e58ac3 test(lua/justification): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:13:10 -08:00
Leonardo de Moura
d0bac61e74 fix(lua/numerics): bug in bindings, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:02:44 -08:00
Leonardo de Moura
0e6df0a55b fix(lua): warning message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 19:58:34 -08:00
Leonardo de Moura
926ed0a02d feat(lua): add type_inferer object to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 19:18:15 -08:00
Leonardo de Moura
4ebb3c572a feat(kernel/environment): make the environment throw an exception when weak-ref has expired 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 18:35:17 -08:00
Leonardo de Moura
590b14570f feat(lua): improve error handling in Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 18:21:42 -08:00
Leonardo de Moura
516c5c8fea feat(lua): add metavar_env objects to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 14:44:33 -08:00
Leonardo de Moura
c8fff45319 feat(lua): add justification objects to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-16 11:12:58 -08:00
Leonardo de Moura
9398ea5a59 feat(util/shared_mutex): add support for recursive lock at shared_mutex 
We need support for recursive locks. The main user of this class is
the environment object. This commit adds a test that demonstrates that
the shared_lock of the environment object may be recursively requested.
Before this fix, the Lean was deadlocking in this example.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 22:01:11 -08:00
Leonardo de Moura
209a2d10f7 fix(lua): replace std::mutex with std::recursive_mutex, add test that demonstrates the problem that is being fixed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 21:26:16 -08:00
Leonardo de Moura
8525e8534b feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 16:11:26 -08:00
Leonardo de Moura
d9d9c05e4f refactor(lua/options): remove unnecessary function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 12:53:27 -08:00
Leonardo de Moura
19533c811b feat(library/script_evaluator): add abstract class that exposes only the API needed by frontend objects 
The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua.
This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 12:13:09 -08:00
Leonardo de Moura
1cb0262ec5 chore(memcheck): make the suppression entries for LuaJIT more general 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 11:34:50 -08:00
Leonardo de Moura
e7552d35e0 chore(memcheck): hide another tcmalloc bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 11:33:34 -08:00
Leonardo de Moura
a74412963a chore(build): only execute lua multi-threading tests when on cygwin or linux, and using g++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 09:27:58 -08:00
Leonardo de Moura
782335581b fix(lua/thread): uninitialized memory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 09:07:18 -08:00
Leonardo de Moura
b5dcb93550 feat(lua): communication channels for threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 21:10:46 -08:00
Leonardo de Moura
bd1e9c7548 feat(lua): throw an exception if the user tries to create a thread and Lean was compiled without multi-threading support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 19:06:36 -08:00
Leonardo de Moura
3a924a5fb1 perf(lua/name): improve to_name_ext performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 18:06:09 -08:00
Leonardo de Moura
cd6bd79d63 refactor(lua): cleanup Lua API, improve performance 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 17:33:46 -08:00
Leonardo de Moura
6575566f9f fix(lua): rename lua_ref to lref, lua_ref is a macro in LuaJIT 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 15:50:56 -08:00
Leonardo de Moura
09bed4786c feat(lua): add semantic attachments for builtin arithmetical values to Lua API, improve mk_constant 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 15:15:04 -08:00
Leonardo de Moura
05f254f605 refactor(lua): move lua_ref to separate file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 14:41:54 -08:00
Leonardo de Moura
bdea42b2a9 style(lua): ignore bogus warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 14:13:06 -08:00
Leonardo de Moura
abe93dfec0 fix(lua/splay_tree): for_each method was crashing if the map was updated during for_each 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:48:23 -08:00
Leonardo de Moura
64cce595a5 feat(lua): add splay_maps to the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:35:36 -08:00
Leonardo de Moura
8e56726116 fix(library/expr_lt): fix bug when using hash codes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 13:18:33 -08:00
Leonardo de Moura
b0322787ff feat(lua): add has_metavar method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 10:28:50 -08:00
Leonardo de Moura
9e445d1917 feat(lua): interrupt and sleep Lua APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 10:04:32 -08:00
Leonardo de Moura
691893258d feat(kernel/expr): add hash code based on allocation time 
The new hash code has the property that given expr_cell * c1 and expr_cell * c2,
if c1 != c2 then there is a high propbability that c1->hash_alloc() != c2->hash_alloc().

The structural hash code hash() does not have this property because we may have
c1 != c2, but c1 and c2 are structurally equal.

The new hash code is only compatible with pointer equality.
By compatible we mean, if c1 == c2, then c1->hash_alloc() == c2->hash_alloc().
This property is obvious because hash_alloc() does not have side-effects.

The test tests/lua/big.lua exposes the problem fixed by this commit.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-14 02:43:11 -08:00
Leonardo de Moura
ae7ea99b56 fix(lua): copy_values and add tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 21:31:27 -08:00
Leonardo de Moura
c759fc93f7 test(lua): object Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 20:59:28 -08:00
Leonardo de Moura
6e0fc0ca9b chore(build): include dl.so when compiling on Linux 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 18:44:28 -08:00
Leonardo de Moura
6964e374c0 fix(lua): luajit incompatibility 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 18:08:00 -08:00
Leonardo de Moura
cbc4254ff5 feat(lua): add occurs method to expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 17:10:09 -08:00
Leonardo de Moura
ad1180c5b4 fix(kernel/occurs): typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 17:04:56 -08:00
Leonardo de Moura
351ef867d2 feat(lua): add abstract, instantiate, has_free_vars, lift/lower free_vars to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 17:02:49 -08:00
Leonardo de Moura
ed3cf8152b feat(lua): add for_each to expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 16:30:59 -08:00
Leonardo de Moura
eacd60de9c feat(frontends/lean): return the operator associated with constant expressions that are names of builtin values 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 16:08:21 -08:00
Leonardo de Moura
1bf6051866 test(lua): expr LUA API test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 15:29:31 -08:00
Leonardo de Moura
9a22702383 feat(lua): make objects() and localobjects() methods return iterators in the environment LUA API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 14:26:01 -08:00
Leonardo de Moura
8c52d47692 chore(lua): rename env() to get_env() 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 13:58:51 -08:00
Leonardo de Moura
ba0889265e refactor(lua): cleanup Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 13:55:05 -08:00
Leonardo de Moura
b5f0185729 fix(lua): replace lua_pushfstring with lua_pushstring 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 12:14:55 -08:00
Leonardo de Moura
a80adae1c3 feat(lua): add fields method to sexpr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 12:10:24 -08:00
Leonardo de Moura
e2efce6b62 style(util/sexpr): name convetion for enumeration types 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 11:50:12 -08:00
Leonardo de Moura
450128e28b refactor(lua): cleanup Lua bindings, and add accessor/tester to expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-13 11:46:09 -08:00
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
b31233e8c2 feat(util/interrupt): restore interrupt module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 21:16:10 -08:00
Leonardo de Moura
126c45626c chore(memcheck.supp): add suppressions for LuaJIT bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 18:52:03 -08:00
Leonardo de Moura
be093ecf90 feat(lua): use formatter available in the state object to convert Lean objects into strings in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 16:56:30 -08:00
Leonardo de Moura
9a5f86fce6 feat(lua): use (** ... **) instead of {{ ... }} for nested Lua scripts 
The token }} is a bad delimiter for blocks of Lua script code nested in Lean files.
The problem is that the sequence }} occurs very often in Lua code because Lua uses { and } to build tables/lists/arrays.
Here is an example of Lua code that contains the sequence }}
     t = {{1, 2}, {2, 3}, {3, 4}}

In Lean, (* ... *) is used to create comments. Thus, (** ... **) code blocks will not affect
valid Lean files. It also looks reasonably good.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 16:05:49 -08:00
Leonardo de Moura
8190d4fed5 feat(lua): allow Lua scripts to update 'global' options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 15:38:00 -08:00
Leonardo de Moura
0a6f622aec chore(build): remove CheckLuaObjlen, it is easier to check the Lua version 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 12:58:22 -08:00
Leonardo de Moura
b986af09ed feat(lua): add support for copying closures between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 12:54:34 -08:00
Leonardo de Moura
c46edcf370 feat(lua): expose formatter in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 11:19:15 -08:00
Leonardo de Moura
2af2a69fc6 feat(lua): expose kernel objects in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-12 09:40:29 -08:00
Leonardo de Moura
d257156b88 fix(lua): memory leaks, we should not use luaL_error because it does not unwind C++ stack 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 21:45:13 -08:00
Leonardo de Moura
a30e02d862 fix(lua): redefine Lua 'print' function, and make sure it is thread safe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 21:15:21 -08:00
Leonardo de Moura
eb9d0f0552 test(lua): add example showing how to access/update an environment object using multiple threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:53:23 -08:00
Leonardo de Moura
0af8f17834 feat(lua): allow Booleans to be copied between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:39:46 -08:00
Leonardo de Moura
7cb15cdac5 feat(lua): allow environment object references to be moved between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:32:36 -08:00
Leonardo de Moura
ac6c18321a fix(lua): make sure environment objects can be safely accessed/updated from current threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:29:53 -08:00
Leonardo de Moura
596e4aeb57 feat(util/shared_mutex): add shared_mutex object, this is a temporary replacement for std::shared_mutex that will be available in C++11 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 20:00:21 -08:00
Leonardo de Moura
cc7b5b7e50 fix(lua): disable custom allocation for Lua, it is crashing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 18:20:52 -08:00
Leonardo de Moura
7d49df3985 style(lua): fix cpplint.py warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 17:46:39 -08:00
Leonardo de Moura
69b41eae70 feat(lua): add support for multiple execution threads in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 16:25:17 -08:00
Leonardo de Moura
95785c7aaa feat(lua): add State objects, it allows us to create several Lua State objects in a lua script 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 15:05:50 -08:00
Leonardo de Moura
f158b0b311 fix(util/memory): make sure realloc behaves like free when sz == 0 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:42:22 -08:00
Leonardo de Moura
7cc6c35eee feat(lua/name): add hash method to name objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:32:56 -08:00
Leonardo de Moura
8dd85ebc15 fix(lua): typos and a bug in the expr Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:11:06 -08:00
Leonardo de Moura
b227775a07 test(lua): add tests for format object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 12:58:47 -08:00
Leonardo de Moura
31abc00db8 chore(*): add LCOV_EXCL_LINE to lean_unreachable statements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 09:19:38 -08:00
Leonardo de Moura
dbdb9a41af style(lua): use C++-style cast 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
7683188ab0 chore(emplace_back): use emplace_back when appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
8c140ff86f feat(lua): allow lua scripts (embedded in Lean files) to access the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
3078923ea4 fix(kernel/type_checker): add missing test, and kernel_exception has_no_type_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
9d61fcf85b feat(lua): expose environment objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
119e0ba5e6 feat(lua): add to_nonnull_expr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Leonardo de Moura
8dd62e76be feat(lua): add mk_metavar to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-10 11:14:04 -08:00
Soonho Kong
1cf037f11e chore(cmake): do not delete coverage.info.cleaned which will be used for coveralls.io 2013-11-09 22:19:08 -05:00
Leonardo de Moura
6b71fb346c fix(lua): add missing files for local_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-09 12:47:52 -08:00
Leonardo de Moura
554defe89d feat(lua): expose local_context objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-09 12:18:46 -08:00
Leonardo de Moura
183080294b fix(cmake/Modules/CheckLuaNewstate.cc): compilation problem on cygwin 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-09 12:18:20 -08:00
Leonardo de Moura
ad2de3b53c feat(lua): expose level objects in the Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-08 17:08:24 -08:00