michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic): expose 'trace' tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-02 10:52:45 -07:00
parent e1d909455c
commit 6ab46396d8
4 changed files with 41 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/standard/tactic.lean
View file

@ -1,7 +1,8 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import logic
import logic string
using string
namespace tactic
-- This is just a trick to embed the 'tactic language' as a
@ -26,7 +27,7 @@ definition id : tactic := tactic_value
definition beta : tactic := tactic_value
definition apply {B : Type} (b : B) : tactic := tactic_value
definition unfold {B : Type} (b : B) : tactic := tactic_value
definition trace (s : string) : tactic := tactic_value
infixl `;`:200 := and_then
infixl `|`:100 := or_else
notation `!`:max t:max := repeat t

52
src/library/tactic/expr_to_tactic.cpp
View file

@ -7,6 +7,8 @@ Author: Leonardo de Moura
#include <unordered_map>
#include <string>
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "library/string.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/apply_tactic.h"
@ -21,35 +23,36 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) {
get_expr_to_tactic_map().insert(mk_pair(n, fn));
}
tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const * p) {
expr const & f = get_app_fn(e);
tactic expr_to_tactic(type_checker & tc, expr const & e, pos_info_provider const * p) {
expr const & f = get_app_fn(tc.whnf(e));
if (is_constant(f)) {
auto const & map = get_expr_to_tactic_map();
auto it = map.find(const_name(f));
if (it != map.end()) {
return it->second(env, e, p);
} else if (auto it = env.find(const_name(f))) {
return it->second(tc, e, p);
} else if (auto it = tc.env().find(const_name(f))) {
if (it->is_definition()) {
buffer<expr> locals;
get_app_rev_args(e, locals);
expr v = it->get_value();
v = instantiate_univ_params(v, it->get_univ_params(), const_levels(f));
v = apply_beta(v, locals.size(), locals.data());
return expr_to_tactic(env, v, p);
return expr_to_tactic(tc, v, p);
}
}
throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
} else if (is_lambda(f)) {
buffer<expr> locals;
get_app_rev_args(e, locals);
return expr_to_tactic(env, apply_beta(f, locals.size(), locals.data()), p);
} else {
throw expr_to_tactic_exception(e, "failed to convert expression into tactic");
}
}
tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const * p) {
type_checker tc(env);
return expr_to_tactic(tc, e, p);
}
register_simple_tac::register_simple_tac(name const & n, std::function<tactic()> f) {
register_expr_to_tactic(n, [=](environment const &, expr const & e, pos_info_provider const *) {
register_expr_to_tactic(n, [=](type_checker &, expr const & e, pos_info_provider const *) {
if (!is_constant(e))
throw expr_to_tactic_exception(e, "invalid constant tactic");
return f();
@ -57,23 +60,23 @@ register_simple_tac::register_simple_tac(name const & n, std::function<tactic()>
}
register_bin_tac::register_bin_tac(name const & n, std::function<tactic(tactic const &, tactic const &)> f) {
register_expr_to_tactic(n, [=](environment const & env, expr const & e, pos_info_provider const * p) {
register_expr_to_tactic(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 2)
throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments");
return f(expr_to_tactic(env, args[0], p),
expr_to_tactic(env, args[1], p));
return f(expr_to_tactic(tc, args[0], p),
expr_to_tactic(tc, args[1], p));
});
}
register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tactic const &)> f) {
register_expr_to_tactic(n, [=](environment const & env, expr const & e, pos_info_provider const * p) {
register_expr_to_tactic(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 1)
throw expr_to_tactic_exception(e, "invalid unary tactic, it must have one argument");
return f(expr_to_tactic(env, args[0], p));
return f(expr_to_tactic(tc, args[0], p));
});
}
@ -86,16 +89,28 @@ static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tact
static register_bin_tac reg_then(name(g_tac, "and_then"), [](tactic const & t1, tactic const & t2) { return then(t1, t2); });
static register_bin_tac reg_orelse(name(g_tac, "or_else"), [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); });
static register_unary_tac reg_repeat(name(g_tac, "repeat"), [](tactic const & t1) { return repeat(t1); });
static register_tac reg_state(name(g_tac, "state"), [](environment const &, expr const & e, pos_info_provider const * p) {
static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) {
if (p)
return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e));
else
return trace_state_tactic("unknown", mk_pair(0, 0));
});
static register_tac reg_apply(name(g_tac, "apply"), [](environment const &, expr const & e, pos_info_provider const *) {
static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr const & e, pos_info_provider const *) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() != 1)
throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected");
if (auto str = to_string(args[0]))
return trace_tactic(*str);
else if (auto str = to_string(tc.whnf(args[0])))
return trace_tactic(*str);
else
throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected");
});
static register_tac reg_apply(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) {
return apply_tactic(app_arg(e));
});
static register_tac reg_unfold(name(g_tac, "unfold"), [](environment const &, expr const & e, pos_info_provider const *) {
static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) {
expr id = get_app_fn(app_arg(e));
if (!is_constant(id))
return fail_tactic();
@ -103,6 +118,7 @@ static register_tac reg_unfold(name(g_tac, "unfold"), [](environment const &, ex
return unfold_tactic(const_name(id));
});
// We encode the 'by' expression that is used to trigger tactic execution.
// This is a trick to avoid creating a new kind of expression.
// 'by' macros are temporary objects used by the elaborator,

2
src/library/tactic/expr_to_tactic.h
View file

@ -16,7 +16,7 @@ public:
expr const & get_expr() const { return m_expr; }
};
typedef std::function<tactic(environment const & env, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
typedef std::function<tactic(type_checker & tc, expr const & e, pos_info_provider const *)> expr_to_tactic_fn;
void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn);
struct register_tac {
register_tac(name const & n, expr_to_tactic_fn fn) { register_expr_to_tactic(n, fn); }

6
tests/lean/run/tactic3.lean
View file

@ -2,8 +2,8 @@ import standard
using tactic
theorem tst {A B : Bool} (H1 : A) (H2 : B) : A
:= by state; now |
state; fail |
exact
:= by trace "first"; state; now |
trace "second"; state; fail |
trace "third"; exact
check tst