Commit graph

33 commits

Author SHA1 Message Date
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
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
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
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
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