feat(frontends/lean): change 'proof-qed' semantics: no backtracking

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-12 16:49:21 -07:00
parent b32d801116
commit 2869d9059f
3 changed files with 8 additions and 3 deletions

View file

@ -149,10 +149,11 @@ static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &
auto pos = p.pos();
expr tac = p.parse_expr();
if (use_exact)
tac = p.save_pos(mk_app(get_exact_tac_fn(), tac), pos);
tac = p.mk_app(get_exact_tac_fn(), tac, pos);
if (pre_tac)
tac = p.save_pos(mk_app(get_and_then_tac_fn(), *pre_tac, tac), pos);
r = r ? p.save_pos(mk_app(get_and_then_tac_fn(), *r, tac), pos) : tac;
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
tac = p.mk_app(get_determ_tac_fn(), tac, pos);
r = r ? p.mk_app({get_and_then_tac_fn(), *r, tac}, pos) : tac;
if (p.curr_is_token(g_qed)) {
auto pos = p.pos();
p.next();

View file

@ -29,12 +29,15 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) {
static name g_tac("tactic"), g_tac_name(g_tac, "tactic"), g_builtin_tac_name(g_tac, "builtin_tactic");
static name g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then");
static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat"), g_fixpoint_name(g_tac, "fixpoint");
static name g_determ_tac_name(g_tac, "determ");
static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name));
static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name));
static expr g_determ_tac_fn(Const(g_determ_tac_name));
static expr g_tac_type(Const(g_tac_name)), g_builtin_tac(Const(g_builtin_tac_name)), g_fixpoint_tac(Const(g_fixpoint_name));
expr const & get_exact_tac_fn() { return g_exact_tac_fn; }
expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; }
expr const & get_or_else_tac_fn() { return g_or_else_tac_fn; }
expr const & get_determ_tac_fn() { return g_determ_tac_fn; }
expr const & get_repeat_tac_fn() { return g_repeat_tac_fn; }
expr const & get_tactic_type() { return g_tac_type; }

View file

@ -45,6 +45,7 @@ expr const & get_exact_tac_fn();
expr const & get_and_then_tac_fn();
expr const & get_or_else_tac_fn();
expr const & get_repeat_tac_fn();
expr const & get_determ_tac_fn();
/** \brief Exception used to report a problem when an expression is being converted into a tactic. */
class expr_to_tactic_exception : public tactic_exception {