Commit graph

96 commits

Author SHA1 Message Date
Leonardo de Moura
b3f87e2e4f feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 22:11:07 -08:00
Leonardo de Moura
5dfb3b8b56 feat(frontends/lean/parse): allow script-code blocks to be used in the apply command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 21:48:30 -08:00
Leonardo de Moura
c6b05bcfcb feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 18:23:38 -08:00
Leonardo de Moura
e3f3ec5553 feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 18:17:15 -08:00
Leonardo de Moura
d87ad9eb7e refactor(util/lua): propagate C++ Lean exceptions in Lua
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 12:25:29 -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
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
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
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
390f7eaec8 test(kernel/typechecker): type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 15:01:39 -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
45858d54ae test(frontends/lean): add missing expected output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 15:51:47 -08:00
Leonardo de Moura
6b30ebab5e test(lua): use simplified Const creation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 15:17:00 -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
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
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
3dea7ae0d6 test(frontends/lean): example mixing Lean and Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-13 16:07:15 -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
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
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
57b9657bf0 feat(lua): add lua_exception for wrapping lua errors, and improve Lua error messages in the Lean frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 15:19:26 -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
9c60eed93c refactor(kernel/metavar): avoid using unique names for default metavariable prefix
The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file.
Avoiding unique name feature in the default metavariable prefix avoids this problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-07 10:16:25 -08: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
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
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
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
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
cb06d0a959 test(frontends/lean): add example showing higher order matching is working, and is useful
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:18:48 -07:00
Leonardo de Moura
02c22e509d fix(tests/lean): remove obsolete comments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:16:02 -07:00
Leonardo de Moura
250cf70410 test(frontends/lean): all 'bad' examples can be solved
Move them to the main test directory

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:12:58 -07:00
Leonardo de Moura
c1c1af4b98 fix(tests/lean): add parenthesis
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 20:04:50 -07:00
Leonardo de Moura
a5c3829d1b feat(kernel): add unexpected_metavar_occurrence exception
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:56:44 -07:00
Leonardo de Moura
46b9b2114a fix(tests/lean): adjust error messages in the expected output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 19:27:26 -07:00
Leonardo de Moura
e55fb4f165 fix(tests/lean): adjust expected results, the new result is also acceptable
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 17:54:09 -07:00
Leonardo de Moura
d2f9c24d3c fix(tests/lean): adjust tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:42:17 -07:00
Leonardo de Moura
a7f94b55db fix(frontends/lean/elaborator): fix bugs and adjust tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-24 15:29:56 -07:00
Leonardo de Moura
29ad71f9fc test(conversion): add more conversion tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-15 15:35:08 -07:00