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

166 commits

Author SHA1 Message Date
Leonardo de Moura
3daac17ea8 feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 15:30:16 -08:00
Leonardo de Moura
f67b5c4d00 test(tests/lua): more to_ceqs tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 13:50:35 -08:00
Leonardo de Moura
c651d3ea2d feat(library/simplifier): filter out propositions that cannot be used as conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 12:06:27 -08:00
Leonardo de Moura
94fa987814 fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool 
The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 11:02:52 -08:00
Leonardo de Moura
97d9765992 fix(tests/lua/threads): increase timeout to make sure it passes the test on slow machines 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-15 08:46:14 -08:00
Leonardo de Moura
c8e1ec87d2 feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 18:30:19 -08:00
Leonardo de Moura
7c2a4211a8 feat(kernel): expose imported predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 16:41:40 -08:00
Leonardo de Moura
8217a544cc fix(library/hop_match): bugs in the higher-order matching procedure, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 14:37:28 -08:00
Leonardo de Moura
485ca842c9 test(tests/lua): extra tests for Lua hierachical name API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-14 11:38:10 -08:00
Leonardo de Moura
4595c50f7e fix(library/hop_match): in locally bound variable management 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-13 16:54:21 -08:00
Leonardo de Moura
84f017f127 chore(tests/lua): use default environment instead of creating a new one 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 18:24:04 -08:00
Leonardo de Moura
35bacf95fc feat(shell): provide the default environment when parsing Lua files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 18:21:14 -08:00
Leonardo de Moura
7f818ecd92 feat(library): match procedure for higher-order patterns 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-12 17:45:24 -08:00
Leonardo de Moura
411f14415d feat(builtin): automatically generate Lean/C++ interface for builtin theories 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 18:09:53 -08:00
Leonardo de Moura
a339a53f50 feat(util/options): 'verbose' as a system option, add -q (quiet) option 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 15:31:58 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 08:33:52 -08:00
Leonardo de Moura
5fe8c32da9 feat(kernel): use new universe contraints in the environment, allow new constraints to be added 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 16:46:11 -08:00
Leonardo de Moura
8c956280d9 chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-06 11:41:03 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 19:21:44 -08:00
Leonardo de Moura
4ba097a141 feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 13:06:36 -08:00
Leonardo de Moura
9f08156a73 feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 11:03:35 -08:00
Leonardo de Moura
028a9bd9bd feat(frontends/lean/scanner): use Lua style comments in Lean 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-05 08:53:27 -08:00
Leonardo de Moura
7726ccad28 chore(builtin): rename nat, int and real modules to Nat, Int and Real. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-01 13:52:25 -08:00
Leonardo de Moura
08718e33dc refactor(builtin): only load the kernel and natural numbers by default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-30 13:35:37 -08:00
Leonardo de Moura
3f0279b88c refactor(frontends/lua): replace lean.lua.h with util.lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 19:49:26 -08:00
Leonardo de Moura
40eca048e0 feat(extra): replace parse_lean_tpl with improved parse_template, that is based on macros 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-26 19:28:02 -08:00
Leonardo de Moura
4229e498d2 refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-22 11:51:38 -08:00
Leonardo de Moura
7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque 
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-20 12:47:47 -08:00
Leonardo de Moura
dd72269b13 feat(frontends/lean): rename command Set to SetOption 
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-18 21:18:48 -08:00
Leonardo de Moura
0eaa98221b fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-09 12:25:19 -08:00
Leonardo de Moura
3ea09daf44 fix(frontends/lean/frontend): is_coercion for environment objects that have parents 
Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:47:00 -08:00
Leonardo de Moura
2a80807fef refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 17:33:18 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-08 14:37:38 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression 
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 23:21:10 -08:00
Leonardo de Moura
0c059a9917 feat(library/tactic): use _tac suffix instead of _tactic like Isabelle 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-05 20:06:32 -08:00
Leonardo de Moura
8e53643b61 feat(library/fo_unify): first order unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-03 12:21:21 -08:00
Leonardo de Moura
70e06f8e86 feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-01 10:27:27 -08:00
Leonardo de Moura
7ed78815e0 fix(tests/lua): incorrect assertion 
The assertion got violated after a bug was fixed in the to_goal procedure.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:53:57 -08:00
Leonardo de Moura
662fb71d59 chore(tests/lua/threads): fix type in file name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:12:54 -08:00
Leonardo de Moura
ce674d2d43 feat(library/tactic): execute Lua tactics using coroutines 
This is very important when several Lua tactics are implemented in the
same Lua State object.  In this case, even if we use the par
combinator, a Lua tactic will block the other Lua tactics running in
the same Lua State object.

With this commit, a Lua tactic can use yield to allow other tactics
in the same State object to execute.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:09:33 -08:00
Leonardo de Moura
09bc7ddf91 feat(library/tactic): add support for migratic tactic framework object between Lua states 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 08:03:05 -08:00
Leonardo de Moura
3dc7a856f0 refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 18:11:46 -08:00
Leonardo de Moura
b4a8418d38 feat(library/tactic): expose tactics in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 17:47:29 -08:00
Leonardo de Moura
0934d7b2f4 fix(frontends/lua): make sure Lua 'sleep' function support interruption 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 13:25:06 -08:00
Leonardo de Moura
99a811a586 feat(bindings/lua): expose io_state object in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 12:54:47 -08:00
Leonardo de Moura
861be072d8 feat(bindings/lua): add proof_state to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:58 -08:00
Leonardo de Moura
fd3b9e39f6 feat(bindings/lua): add cex_builder to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 09:17:57 -08:00
Leonardo de Moura
4d9075bdfd feat(bindings/lua): add proof_map, assignment and proof_builder to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 08:37:37 -08:00
Leonardo de Moura
3ebc099ec5 feat(bindings/lua/options): improve options Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 21:05:05 -08:00
Leonardo de Moura
feeb6d9105 feat(bindings/lua): add goal object to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 20:51:47 -08:00
Leonardo de Moura
7b8bd97699 feat(lua/expr): add method for extracting semantic attachment data 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 19:06:47 -08:00
Leonardo de Moura
a98fdd9be6 refactor(shell): combine lean and leanlua executables in a single executable 
The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files.
Example:
        ./lean extension1.lua extension2.lua file.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-19 16:48:21 -08:00
Leonardo de Moura
87775cbc07 chore(build): include incorrect output in the logs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-18 15:39:55 -08:00
Soonho Kong
20756c382c test(*): split leantests, leanslowtests, leanluatests, leanluadocs into singletons 2013-11-18 18:27:11 -05: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
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
5f651d46e6 tests(lua/frontend_lean): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 13:48:29 -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
e693c2de01 test(lua/name): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:25:21 -08:00
Leonardo de Moura
8a13df3ce1 test(lua/type_inferer): add missing tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-17 11:17:32 -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
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
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
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
5e170ce5fe chore(tests/lua): move examples that use threads to tests/lua/threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-15 09:11:58 -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
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
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
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
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
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
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
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
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
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
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
2ac594a159 test(lua): add a new example showing how to create nested State objects and threads 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 18:27:09 -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
bdc23fba32 test(lua): add tests for expr object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 13:11:31 -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
c2db18a003 test(lua): add tests for sexpr object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 09:51:07 -08:00
Leonardo de Moura
6c7be28807 test(lua): add tests for options object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-11 09:42:50 -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
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
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
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