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

204 commits

Author SHA1 Message Date
Leonardo de Moura
67def8da21 fix(library/type_inferer): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:47:29 -08:00
Leonardo de Moura
dae86c2ffa feat(frontends/lean/parser): add basic tactic support in the frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 21:08:12 -08:00
Leonardo de Moura
73bbf67702 refactor(library/elaborator): simplify synthesizer interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 19:00:48 -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
d36a91e145 feat(library/tactic): expose COND and WHEN tacticals in Lua, add HOL-like tactical names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 17:57:24 -08:00
Leonardo de Moura
ff052d41ee chore(*): fix cygwin compilation errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-28 13:49:18 -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
f7e8545e97 refactor(frontends/lua): rename leanlua_state to script_state, and move it to util 
This commit also minimizes the dependencies of script_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 14:57:36 -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
a6f6f49b5f refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular 
copy_values is not a big if-then-else anymore.
Before this change, whenever we added a new kind of userdata, we would have to update copy_values.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-27 10:32:19 -08:00
Leonardo de Moura
956f203a55 refactor(bindings/lua): move Lua bindings to the file associated with them 
The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 19:15:56 -08:00
Leonardo de Moura
4e66a2e14a fix(library/tactic/goal): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:58 -08:00
Leonardo de Moura
b41789d085 feat(kernel): add is_bool predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-26 11:34:50 -08:00
Leonardo de Moura
c22f863114 refactor(library/tactic): improve solve method 
Now, it produces the following outcomes:
1- A proof
2- A counterexample
3- A list of (unsolved) final states

Remark: the solve method does not check whether the proof or counterexample is correct.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 13:04:12 -08:00
Leonardo de Moura
9a8ea0c735 feat(library/tactic): add precision and counterexample builder to proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 11:43:16 -08:00
Leonardo de Moura
ccaa272f9a refactor(library/tactic): simplify proof_builder API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:50:33 -08:00
Leonardo de Moura
500ed7a05b refactor(library/tactic): remove dead code, make proof_state a smart pointer, cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 10:39:40 -08:00
Leonardo de Moura
2c65fdb346 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-25 01:06:34 -08:00
Leonardo de Moura
9dcfa03dd2 feat(library/tactic): add conj_hyp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 21:00:38 -08:00
Leonardo de Moura
d75bd2ae98 feat(library/tactic/proof_state): remove goal name when pretty printing the proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 20:22:47 -08:00
Leonardo de Moura
48d7afb0e8 feat(library/tactic): add trace_state_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:44:02 -08:00
Leonardo de Moura
6f05276acd refactor(library/tactic): remove unnecessary tactic_exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:31:49 -08:00
Leonardo de Moura
9c42a05b08 feat(library/tactic): add conj_tactic and imp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 16:29:04 -08:00
Leonardo de Moura
1c607f3350 feat(library/tactic): add cond and when tacticals. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 12:04:32 -08:00
Leonardo de Moura
40d612eca0 feat(library/tactic): add repeat1 and determ tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:38:51 -08:00
Leonardo de Moura
cb7a5288c5 refactor(library/tactic): minimize the amount of copying in the tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:27:06 -08:00
Leonardo de Moura
22c49146ae feat(library/tactic): refine repeat and repeat_at_most tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 11:18:32 -08:00
Leonardo de Moura
e839787b74 refactor(library/tactic): cleanup 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-24 00:38:52 -08:00
Leonardo de Moura
40a2f0a588 refactor(util/lazy_list): polish lazy_list API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:45:01 -08:00
Leonardo de Moura
9da95dc6e6 style(library/tactic): missing include 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:06:00 -08:00
Leonardo de Moura
16cf60a04b refactor(library/tactic): modify par and try_for tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 17:03:59 -08:00
Leonardo de Moura
d1adfd52e6 feat(library/tactic): add mk_simple_tactic template 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:53:45 -08:00
Leonardo de Moura
f19944cf09 refactor(util/lazy_list): 'lazier' lazy_lists 
In the new implementation, even the head of the lazy list is computed on demand.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-23 15:33:30 -08:00
Leonardo de Moura
18d114416f feat(library/tactic): add take and force tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 17:05:18 -08:00
Leonardo de Moura
d258a4b7b8 feat(library/tactic): add repeat and repeat_at_most tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 16:39:25 -08:00
Leonardo de Moura
8bece1b53d feat(library/tactic): add append, interleave and par tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 16:15:03 -08:00
Leonardo de Moura
df96068caa fix(library/tactic): clean up try_for 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 15:51:17 -08:00
Leonardo de Moura
9fd594533d refactor(library/tactic): simplify tactic framework, add orelse and try_for combinators/tacticals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-22 15:46:43 -08:00
Leonardo de Moura
796fb3c3bf refactor(library/tactic): remove justification_builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
41062fdf9f feat(library/tactic): add pretty printer for goal and proof_state objects, add solve method for tactics, add trivial example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
5346b67651 refactor(library/state): rename Lean state object to io_state 
The idea is to make it clear that io_state is distinguish it from proof_state, and from leanlua_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
680ec8abba refactor(library/tactic): reorganize tactic API, add assumption_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
63bbf07f64 feat(library/tactic): add 'idtac' tactic and 'then' tactical 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
a03841c18b feat(tactic): refine tactic API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 17:29:06 -08:00
Leonardo de Moura
367108edfa fix(library/tactic): compilation problem reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-21 08:53:37 -08:00
Leonardo de Moura
f6d1f4db60 chore(library/tactic): remove trash 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-11-20 17:25:00 -08:00