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

feat(frontends/lean): add support for empty match-with expressions

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-26 16:04:36 -08:00
parent d00c013ad8
commit 5b736a2268
4 changed files with 67 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/frontends/lean/decl_cmds.cpp
View file

@ -603,11 +603,18 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
/** \brief Use equations compiler infrastructure to implement match-with */
expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
expr t = p.parse_expr();
p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
if (is_eqn_prefix(p))
p.next();
buffer<expr> eqns;
p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
if (p.curr_is_token(get_end_tk())) {
p.next();
// empty match-with
eqns.push_back(Fun(fn, mk_no_equation()));
expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
return p.mk_app(f, t, pos);
}
if (is_eqn_prefix(p))
p.next(); // optional '|' in the first case
while (true) {
expr lhs;
unsigned prev_num_undef_ids = p.get_num_undef_ids();

47
src/library/definitional/equations.cpp
View file

@ -29,11 +29,13 @@ Author: Leonardo de Moura
namespace lean {
static name * g_equations_name = nullptr;
static name * g_equation_name = nullptr;
static name * g_no_equation_name = nullptr;
static name * g_decreasing_name = nullptr;
static name * g_inaccessible_name = nullptr;
static name * g_equations_result_name = nullptr;
static std::string * g_equations_opcode = nullptr;
static std::string * g_equation_opcode = nullptr;
static std::string * g_no_equation_opcode = nullptr;
static std::string * g_decreasing_opcode = nullptr;
static std::string * g_equations_result_opcode = nullptr;
@ -50,9 +52,8 @@ public:
unsigned get_num_fns() const { return m_num_fns; }
};
class equation_macro_cell : public macro_definition_cell {
class equation_base_macro_cell : public macro_definition_cell {
public:
virtual name get_name() const { return *g_equation_name; }
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const {
expr dummy = mk_Prop();
return mk_pair(dummy, constraint_seq());
@ -61,9 +62,21 @@ public:
expr dummy = mk_Type();
return some_expr(dummy);
}
};
class equation_macro_cell : public equation_base_macro_cell {
public:
virtual name get_name() const { return *g_equation_name; }
virtual void write(serializer & s) const { s.write_string(*g_equation_opcode); }
};
// This is just a placeholder to indicate no equations were provided
class no_equation_macro_cell : public equation_base_macro_cell {
public:
virtual name get_name() const { return *g_no_equation_name; }
virtual void write(serializer & s) const { s.write_string(*g_no_equation_opcode); }
};
class decreasing_macro_cell : public macro_definition_cell {
void check_macro(expr const & m) const {
if (!is_macro(m) || macro_num_args(m) != 2)
@ -84,6 +97,7 @@ public:
};
static macro_definition * g_equation = nullptr;
static macro_definition * g_no_equation = nullptr;
static macro_definition * g_decreasing = nullptr;
bool is_equation(expr const & e) { return is_macro(e) && macro_def(e) == *g_equation; }
@ -101,6 +115,15 @@ expr mk_equation(expr const & lhs, expr const & rhs) {
expr args[2] = { lhs, rhs };
return mk_macro(*g_equation, 2, args);
}
expr mk_no_equation() { return mk_macro(*g_no_equation); }
bool is_no_equation(expr const & e) { return is_macro(e) && macro_def(e) == *g_no_equation; }
bool is_lambda_no_equation(expr const & e) {
if (is_lambda(e))
return is_lambda_no_equation(binding_body(e));
else
return is_no_equation(e);
}
bool is_decreasing(expr const & e) { return is_macro(e) && macro_def(e) == *g_decreasing; }
expr const & decreasing_app(expr const & e) { lean_assert(is_decreasing(e)); return macro_arg(e, 0); }
@ -144,7 +167,9 @@ void to_equations(expr const & e, buffer<expr> & eqns) {
expr mk_equations(unsigned num_fns, unsigned num_eqs, expr const * eqs) {
lean_assert(num_fns > 0);
lean_assert(num_eqs > 0);
lean_assert(std::all_of(eqs, eqs+num_eqs, is_lambda_equation));
lean_assert(std::all_of(eqs, eqs+num_eqs, [](expr const & e) {
return is_lambda_equation(e) || is_lambda_no_equation(e);
}));
macro_definition def(new equations_macro_cell(num_fns));
return mk_macro(def, num_eqs, eqs);
}
@ -201,14 +226,17 @@ expr const & get_equations_result(expr const & e, unsigned i) { return macro_arg
void initialize_equations() {
g_equations_name = new name("equations");
g_equation_name = new name("equation");
g_no_equation_name = new name("no_equation");
g_decreasing_name = new name("decreasing");
g_inaccessible_name = new name("innaccessible");
g_equations_result_name = new name("equations_result");
g_equation = new macro_definition(new equation_macro_cell());
g_no_equation = new macro_definition(new no_equation_macro_cell());
g_decreasing = new macro_definition(new decreasing_macro_cell());
g_equations_result = new macro_definition(new equations_result_macro_cell());
g_equations_opcode = new std::string("Eqns");
g_equation_opcode = new std::string("Eqn");
g_no_equation_opcode = new std::string("NEqn");
g_decreasing_opcode = new std::string("Decr");
g_equations_result_opcode = new std::string("EqnR");
register_annotation(*g_inaccessible_name);
@ -218,7 +246,7 @@ void initialize_equations() {
d >> num_fns;
if (num == 0 || num_fns == 0)
throw corrupted_stream_exception();
if (!is_lambda_equation(args[num-1])) {
if (!is_lambda_equation(args[num-1]) && !is_lambda_no_equation(args[num-1])) {
if (num <= 2)
throw corrupted_stream_exception();
return mk_equations(num_fns, num-2, args, args[num-2], args[num-1]);
@ -232,6 +260,12 @@ void initialize_equations() {
throw corrupted_stream_exception();
return mk_equation(args[0], args[1]);
});
register_macro_deserializer(*g_no_equation_opcode,
[](deserializer &, unsigned num, expr const *) {
if (num != 0)
throw corrupted_stream_exception();
return mk_no_equation();
});
register_macro_deserializer(*g_decreasing_opcode,
[](deserializer &, unsigned num, expr const * args) {
if (num != 2)
@ -247,14 +281,17 @@ void initialize_equations() {
void finalize_equations() {
delete g_equations_result_opcode;
delete g_equation_opcode;
delete g_no_equation_opcode;
delete g_equations_opcode;
delete g_decreasing_opcode;
delete g_equations_result;
delete g_equation;
delete g_no_equation;
delete g_decreasing;
delete g_equations_result_name;
delete g_equations_name;
delete g_equation_name;
delete g_no_equation_name;
delete g_decreasing_name;
delete g_inaccessible_name;
}
@ -549,6 +586,8 @@ class equation_compiler_fn {
buffer<buffer<eqn>> res_eqns;
res_eqns.resize(m_fns.size());
for (expr eq : eqs) {
if (is_lambda_no_equation(eq))
continue; // skip marker
for (expr const & fn : m_fns)
eq = instantiate(binding_body(eq), fn);
buffer<expr> local_ctx;

4
src/library/definitional/equations.h
View file

@ -18,6 +18,10 @@ expr mk_equation(expr const & lhs, expr const & rhs);
/** \brief Return true if e is of the form <tt>fun a_1 ... a_n, equation</tt> */
bool is_lambda_equation(expr const & e);
/** \brief Placeholder to indicate no equations were provided (e.g., to a match-with expression) */
expr mk_no_equation();
bool is_no_equation(expr const & e);
bool is_decreasing(expr const & e);
expr const & decreasing_app(expr const & e);
expr const & decreasing_proof(expr const & e);

8
tests/lean/run/empty_match.lean Normal file
View file

@ -0,0 +1,8 @@
open nat
definition not_lt_zero (a : nat) : ¬ a < zero :=
assume H : a < zero,
match H with
end
check not_lt_zero