Commit graph

1232 commits

Author SHA1 Message Date
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
1e12ddc7a9 refactor(lua): add goodies for accessing Lean values on the Lua stack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 19:45:15 -08:00
Leonardo de Moura
47c289a24b refactor(lua/name): improve name bindings for Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 18:48:21 -08:00
Leonardo de Moura
3c475e890d refactor(lua/options): improve options bindings for Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 18:46:58 -08:00
Leonardo de Moura
7b77863507 refactor(lua/name): improve name bindings for Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 18:44:20 -08:00
Leonardo de Moura
f488e6bbfc fix(lua): safe_function_wrapper
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 18:12:53 -08:00
Leonardo de Moura
92b2591a6f style(lua): add missing include
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 16:29:47 -08:00
Leonardo de Moura
32d3990fc7 fix(lua): problem when compiling with clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-04 15:05:04 -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
6f2183fafe feat(FindLua.cmake): search also for LuaJit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-03 13:45:23 -08:00
Leonardo de Moura
9884c056ce feat(lua): allow Lean to be compiled with Lua 5.1 and LuaJit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-03 12:40:44 -08:00
Leonardo de Moura
df7dbe17b5 feat(lua/util): remove dependency on luaL_setfuncs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-03 12:16:23 -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
Soonho Kong
a9d55bf036 fix(lua): use updated FindLua and check version 5.2 2013-11-03 13:24:46 -05:00
Soonho Kong
044813615e fix: add '#include <tuple>' 2013-11-03 13:00:42 -05:00
Soonho Kong
0d0d0cd533 chore(cmake): add gmp/mpfr include paths to cmakelists.txt 2013-11-03 13:00:42 -05:00
Leonardo de Moura
ccd95a9b66 fix(lua/name): fix memory leak
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-02 20:57:41 -07: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
1b9cf816c4 fix(lua): mark package as optional
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-02 11:43:23 -07:00
Leonardo de Moura
36fe8e5c5f feat(lua): install Lua at travis VM
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-02 11:21:30 -07:00
Leonardo de Moura
ac08e244a6 feat(lua): add Lua support to build
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-02 11:16:30 -07:00
Leonardo de Moura
bf998d8661 feat(frontends/lean/parser): allow 'typeless' definitions, the type is inferred by the system
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-01 08:51:49 -07:00
Leonardo de Moura
fdea8aba10 feat(frontends/lean/scanner): allow '#' to be used in class B identifiers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-01 08:42:25 -07:00
Leonardo de Moura
96dcd003c6 fix(frontends/lean/parser): associated position with 'type' placeholder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-31 16:27:36 -07:00
Leonardo de Moura
aa99ac6618 feat(kernel/value): allow semantic attachments to use coercions when being pretty printed
For example, this feature is useful when displaying the integer value 10 with coercions enabled. In this case, we want to display "nat_to_int 10" instead of "10".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 11:42:26 -07:00
Leonardo de Moura
032f5cd7b3 feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-30 10:45:43 -07:00
Leonardo de Moura
bc92671ae4 fix(frontends/lean/notation): adjust the implicit arguments of TransExt, and add new test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:12:50 -07:00
Leonardo de Moura
7fc87faa8f feat(kernel): heterogeneous transitivity axiom, we need this axiom to be able to generate modular proofs in the rewriting engine module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:07:30 -07:00
Leonardo de Moura
a57ca284ec fix(tests/library/elaborator): replace eq with my_eq because eq is now a builtin symbol
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 17:06:32 -07:00
Leonardo de Moura
e3228b1f5c test(frontends/lean): add 'l = nil' test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:30:03 -07:00
Leonardo de Moura
4dd6cead83 refactor(equality): make homogeneous equality the default equality
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.

- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
     l = nil
will not propagate the type (List Int) to nil.

- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.

Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:20:06 -07:00
Leonardo de Moura
d0009d0242 feat(frontends/lean): make the first argument of if-expression implicit, add support for marking implicit arguments on builtin symbols (aka semantic attachments)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 15:53:50 -07:00
Leonardo de Moura
2d88922543 feat(frontends/lean/elaborator): solve easy overloads at preprocessing time
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 10:07:15 -07:00
Leonardo de Moura
577ca128a1 fix(library/elaborator): add missing conflict justification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 03:01:17 -07:00
Leonardo de Moura
521fa1ddb8 style(kernel/metavar): add missing includes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 03:00:43 -07:00
Leonardo de Moura
7c8daf8974 fix(kernel/metavar): make sure the justification and substitution are always matching each other
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:39:52 -07:00
Leonardo de Moura
2c6d4d2225 fix(kernel/normalizer): do not apply substitutions in the normalizer
It is incorrect to apply substitutions during normalization.
The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 02:14:48 -07:00
Soonho Kong
7944db2f18 doc(coding_style): add how to organize template source code
[skip ci]
2013-10-28 11:31:46 -04:00
Leonardo de Moura
5f11392fcc test(numerics/numeric_traits): add missing test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:50:33 -07:00
Leonardo de Moura
1d18f60dd5 fix(numerics): add missing numeric_traits<float>::zero()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:47:23 -07:00
Leonardo de Moura
b16a64f44b fix(library/elaborator): missing normalization step for semantic attachments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-28 07:42:14 -07:00
Leonardo de Moura
4564bfa1d3 feat(library/elaborator): improve simple_ho_match
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:17:03 -07:00
Leonardo de Moura
dbefc91151 fix(kernel/metavar): add normalize assignment justification
We need that when we normalize the assignment in a metavariable environment.
That is, we replace metavariable in a substitution with other assignments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 11:02:34 -07:00
Leonardo de Moura
92f5a31976 feat(kernel/expr): add new mk_app template for creating applications using a collection
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 08:53:58 -07:00
Leonardo de Moura
eaccdcb558 refactor(assumption_justification): move to the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-26 14:21:29 -07:00
Leonardo de Moura
4bed9f85b0 feat(kernel/for_each): add option for disabling cache of atomic expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 15:25:17 -07:00