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

2003 commits

Author SHA1 Message Date
Leonardo de Moura
813eba6b3a chore(build): add Lua thread tests to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:53:36 -07:00
Leonardo de Moura
9676f48470 feat(library/kernel_bindings): add list of certified_definitions in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:51:34 -07:00
Leonardo de Moura
bc1a91496a feat(util/lua_list): allow Lua list objects to be moved between states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:49:27 -07:00
Leonardo de Moura
fca65a9d69 fix(kernel/environment): is_descendant optimization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:48:25 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:08:32 -07:00
Leonardo de Moura
5a7f181efc feat(util/name_set): improve name_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 17:17:00 -07:00
Leonardo de Moura
95262fb68d feat(library/kernel_bindings): add remaining type_checker constructors in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 17:13:06 -07:00
Leonardo de Moura
3aa1afdf51 refactor(util): file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 14:15:28 -07:00
Leonardo de Moura
1e4c5f1761 feat(util/lua_named_param): add new functions for handling named parameters in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 14:12:15 -07:00
Leonardo de Moura
bf57f951ea refactor(util): move Lua named parameter support to a different file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 13:20:37 -07:00
Leonardo de Moura
f3c7bc948a feat(library/kernel_bindings): type_checker Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 19:04:15 -07:00
Leonardo de Moura
1a8d75c4f0 feat(util): name_set Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 18:32:53 -07:00
Leonardo de Moura
7fe61bc69c feat(util): name_generator Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:28:11 -07:00
Leonardo de Moura
62db010ba3 feat(library/kernel_bindings): add optional arguments to empty_environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:06:27 -07:00
Leonardo de Moura
4c5f88e63b feat(library/kernel_bindings): global level constructor/accessor/recognizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:22:45 -07:00
Leonardo de Moura
db39458c30 fix(kernel/level): predicate is_param_core 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:22:08 -07:00
Leonardo de Moura
8ae0e46e9d feat(library/kernel_bindings): add new global level methods to environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:17:04 -07:00
Leonardo de Moura
9c760132e2 feat(kernel): add global levels to environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:07:31 -07:00
Leonardo de Moura
208384b5b6 fix(util/rb_tree): missing const 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 14:07:15 -07:00
Leonardo de Moura
2424cf7ece fix(kernel/expr): old comment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 13:07:17 -07:00
Leonardo de Moura
503d8dfa9e feat(kernel): add global universe level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-06 16:13:29 -07:00
Leonardo de Moura
8095783c36 refactor(library/kernel_bindings): use new functions for simulating python-like named arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:42:16 -07:00
Leonardo de Moura
f568ed97b8 feat(util/lua): add functions for simulating python-like named arguments using Lua tables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:41:33 -07:00
Leonardo de Moura
850ec69538 feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:09:17 -07:00
Leonardo de Moura
10d8840cac feat(library/kernel_bindings): add environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:53:32 -07:00
Leonardo de Moura
4f3fad5d65 feat(library/kernel_bindings): add certified_definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:46:59 -07:00
Leonardo de Moura
8f5491447a feat(library/kernel_bindings): add environment_id Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:42:27 -07:00
Leonardo de Moura
fc2d5f1595 feat(library/kernel_bindings): add definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:00:59 -07:00
Leonardo de Moura
b928f313d3 feat(util): add macro for exposing the type std::pair<T1, T2> in Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 16:30:17 -07:00
Leonardo de Moura
b83410f042 fix(library/kernel_bindings): g++ compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 14:34:56 -07:00
Leonardo de Moura
dc627c9965 test(lua): add constraint API tests, and fix minor bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:37:46 -07:00
Leonardo de Moura
91069c5f7f feat(util/list_lua): add length method to list Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:37:15 -07:00
Leonardo de Moura
107f139764 fix(util/list_lua): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:33:49 -07:00
Leonardo de Moura
6ef161824d feat(library/kernel_bindings): constraint Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:17:00 -07:00
Leonardo de Moura
802edd77d1 feat(kernel/justification): add is_eqp predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:15:29 -07:00
Leonardo de Moura
e4f69bd780 fix(kernel/justification): bug in depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:15:01 -07:00
Leonardo de Moura
94ca82ec85 fix(library/kernel_bindings): incorrect use of pushinteger, and improve justification Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:03:43 -07:00
Leonardo de Moura
50089dc64e feat(kernel/error_msgs): expose pp_indent_expr 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:03:12 -07:00
Soonho Kong
468abb72b8 tests(util/rb_tree): wrap tst6 with #if !defined 2014-05-02 01:39:13 -04:00
Leonardo de Moura
a5229e5283 chore(util/lua): name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:40:18 -07:00
Leonardo de Moura
7cd892464f feat(library/definition): macro definition and application Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:29:34 -07:00
Leonardo de Moura
65486b2dec refactor(kernel/expr): add macro_definition smart pointer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:05:46 -07:00
Leonardo de Moura
9f5122b4c7 feat(library/kernel_bindings): justification Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 16:04:30 -07:00
Leonardo de Moura
340c0e0945 feat(library/kernel_bindings): substitution Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:30:30 -07:00
Leonardo de Moura
0bc101ac28 fix(kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:28:34 -07:00
Leonardo de Moura
739f98b642 fix(util/script_state): deadlock 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 14:10:57 -07:00
Leonardo de Moura
ddd980aa63 fix(kernel/level): warning messages when compiling in release mode 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 13:06:00 -07:00
Leonardo de Moura
120c24319e fix(tests/kernel/metavar): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:58:09 -07:00
Leonardo de Moura
027614cebb fix(kernel/metavar): wierd memory leak that only happens when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:55:55 -07:00
Leonardo de Moura
9452d164ec feat(util/script_state): use recursive_mutex instead of mutex 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:27:12 -07:00