chore(frontends/lean): remove dead code
`abstract` can be implemented as a tactic on top of add_decl.
This commit is contained in:
Leonardo de Moura
parent
ecb563baa3
commit
93ccea11fc
7 changed files with 1 additions and 252 deletions
|
|
@ -4,7 +4,7 @@ parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
|
|||
notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
|
||||
inductive_cmds.cpp dependencies.cpp
|
||||
pp.cpp structure_cmd.cpp structure_instance.cpp
|
||||
init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
|
||||
init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp
|
||||
opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
|
||||
match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
|
||||
brackets.cpp tactic_notation.cpp)
|
||||
|
|
|
|||
|
|
@ -29,7 +29,6 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "frontends/lean/tokens.h"
|
||||
#include "frontends/lean/nested_declaration.h"
|
||||
#include "frontends/lean/match_expr.h"
|
||||
#include "frontends/lean/decl_util.h"
|
||||
#include "frontends/lean/brackets.h"
|
||||
|
|
@ -722,7 +721,6 @@ parse_table init_nud_table() {
|
|||
r = r.add({transition("suppose", mk_ext_action(parse_suppose))}, x0);
|
||||
r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
|
||||
r = r.add({transition("suffices", mk_ext_action(parse_suffices))}, x0);
|
||||
r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0);
|
||||
r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
|
||||
r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
|
||||
r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);
|
||||
|
|
|
|||
|
|
@ -28,7 +28,6 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/tokens.h"
|
||||
#include "frontends/lean/decl_attributes.h"
|
||||
#include "frontends/lean/update_environment_exception.h"
|
||||
#include "frontends/lean/nested_declaration.h"
|
||||
#include "frontends/lean/structure_cmd.h"
|
||||
#include "frontends/lean/definition_cmds.h"
|
||||
#include "frontends/lean/inductive_cmds.h"
|
||||
|
|
|
|||
|
|
@ -18,7 +18,6 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/pp.h"
|
||||
#include "frontends/lean/local_ref_info.h"
|
||||
#include "frontends/lean/decl_cmds.h"
|
||||
#include "frontends/lean/nested_declaration.h"
|
||||
#include "frontends/lean/prenum.h"
|
||||
#include "frontends/lean/elaborator.h"
|
||||
#include "frontends/lean/match_expr.h"
|
||||
|
|
@ -44,7 +43,6 @@ void initialize_frontend_lean_module() {
|
|||
initialize_pp();
|
||||
initialize_local_ref_info();
|
||||
initialize_decl_cmds();
|
||||
initialize_nested_declaration();
|
||||
initialize_match_expr();
|
||||
initialize_elaborator();
|
||||
initialize_notation_cmd();
|
||||
|
|
@ -55,7 +53,6 @@ void finalize_frontend_lean_module() {
|
|||
finalize_notation_cmd();
|
||||
finalize_elaborator();
|
||||
finalize_match_expr();
|
||||
finalize_nested_declaration();
|
||||
finalize_decl_cmds();
|
||||
finalize_local_ref_info();
|
||||
finalize_pp();
|
||||
|
|
|
|||
|
|
@ -1,214 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <string>
|
||||
#include "util/sstream.h"
|
||||
#include "util/fresh_name.h"
|
||||
#include "kernel/type_checker.h"
|
||||
#include "kernel/find_fn.h"
|
||||
#include "kernel/instantiate.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "library/locals.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/kernel_serializer.h"
|
||||
#include "library/replace_visitor.h"
|
||||
#include "library/module.h"
|
||||
#include "library/aliases.h"
|
||||
#include "frontends/lean/tokens.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "frontends/lean/nested_declaration.h"
|
||||
|
||||
namespace lean {
|
||||
static name * g_nested_decl = nullptr;
|
||||
static std::string * g_nested_decl_opcode = nullptr;
|
||||
|
||||
name const & get_nested_decl_name() { return *g_nested_decl; }
|
||||
std::string const & get_nested_decl_opcode() { return *g_nested_decl_opcode; }
|
||||
|
||||
class nested_decl_macro_definition_cell : public macro_definition_cell {
|
||||
optional<name> m_name;
|
||||
|
||||
void check_macro(expr const & m) const {
|
||||
if (!is_macro(m) || macro_num_args(m) != 1)
|
||||
throw exception(sstream() << "invalid nested declaration, incorrect number of arguments");
|
||||
}
|
||||
public:
|
||||
nested_decl_macro_definition_cell(optional<name> const & n):
|
||||
m_name(n) {}
|
||||
virtual name get_name() const { return get_nested_decl_name(); }
|
||||
virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
|
||||
check_macro(m);
|
||||
return ctx.check(macro_arg(m, 0), infer_only);
|
||||
}
|
||||
virtual optional<expr> expand(expr const & m, abstract_type_context &) const {
|
||||
check_macro(m);
|
||||
return some_expr(macro_arg(m, 0));
|
||||
}
|
||||
virtual void write(serializer & s) const {
|
||||
s.write_string(get_nested_decl_opcode());
|
||||
s << m_name;
|
||||
}
|
||||
virtual unsigned hash() const {
|
||||
return get_nested_decl_name().hash();
|
||||
}
|
||||
optional<name> const & get_decl_name() const { return m_name; }
|
||||
};
|
||||
|
||||
expr mk_nested_declaration(optional<name> const & n, expr const & e) {
|
||||
macro_definition def(new nested_decl_macro_definition_cell(n));
|
||||
return mk_macro(def, 1, &e);
|
||||
}
|
||||
|
||||
bool is_nested_declaration(expr const & e) {
|
||||
return is_macro(e) && macro_def(e).get_name() == get_nested_decl_name();
|
||||
}
|
||||
|
||||
expr update_nested_declaration(expr const & e, expr const & new_d) {
|
||||
lean_assert(is_nested_declaration(e));
|
||||
return mk_macro(macro_def(e), 1, &new_d);
|
||||
}
|
||||
|
||||
expr get_nested_declaration_arg(expr const & e) {
|
||||
lean_assert(is_nested_declaration(e));
|
||||
return macro_arg(e, 0);
|
||||
}
|
||||
|
||||
optional<name> const & get_nested_declaration_name(expr const & d) {
|
||||
lean_assert(is_nested_declaration(d));
|
||||
return static_cast<nested_decl_macro_definition_cell const*>(macro_def(d).raw())->get_decl_name();
|
||||
}
|
||||
|
||||
LEAN_THREAD_VALUE(bool, g_allow_nested_declarations, false);
|
||||
|
||||
allow_nested_decls_scope::allow_nested_decls_scope(bool enable) {
|
||||
m_saved = g_allow_nested_declarations;
|
||||
g_allow_nested_declarations = enable;
|
||||
}
|
||||
|
||||
allow_nested_decls_scope::~allow_nested_decls_scope() {
|
||||
g_allow_nested_declarations = m_saved;
|
||||
}
|
||||
|
||||
expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos) {
|
||||
try {
|
||||
optional<name> n;
|
||||
if (!g_allow_nested_declarations)
|
||||
throw parser_error("invalid 'abstract' expression, it is only allowed inside definitions", pos);
|
||||
if (p.curr_is_token(get_as_tk())) {
|
||||
p.next();
|
||||
n = p.check_id_next("invalid 'abstract' expression, identifier expected");
|
||||
}
|
||||
expr e = p.parse_expr();
|
||||
p.check_token_next(get_end_tk(), "invalid 'abstract' expression, 'end' expected");
|
||||
return p.save_pos(mk_nested_declaration(n, e), pos);
|
||||
} catch (exception & ex) {
|
||||
consume_until_end(p);
|
||||
ex.rethrow();
|
||||
lean_unreachable();
|
||||
}
|
||||
}
|
||||
|
||||
bool contains_nested_declarations(expr const & e) {
|
||||
return static_cast<bool>(find(e, [&](expr const & n, unsigned) { return is_nested_declaration(n); }));
|
||||
}
|
||||
|
||||
class extractor : public replace_visitor {
|
||||
environment m_env;
|
||||
io_state m_ios;
|
||||
type_checker m_tc;
|
||||
name m_dname;
|
||||
unsigned m_idx;
|
||||
public:
|
||||
extractor(environment const & env, io_state const & ios, name const & dname):
|
||||
m_env(env), m_ios(ios), m_tc(m_env), m_dname(dname), m_idx(1) {}
|
||||
|
||||
name mk_name_for(expr const & e) {
|
||||
lean_assert(is_nested_declaration(e));
|
||||
if (auto n = get_nested_declaration_name(e)) {
|
||||
return *n;
|
||||
} else {
|
||||
name ns = get_namespace(m_env);
|
||||
while (true) {
|
||||
name aux = m_dname.append_after(m_idx);
|
||||
m_idx++;
|
||||
if (!m_env.find(ns + aux))
|
||||
return aux;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
expr extract(expr const & e) {
|
||||
lean_assert(is_nested_declaration(e));
|
||||
expr const & d = visit(get_nested_declaration_arg(e));
|
||||
name new_name = mk_name_for(e);
|
||||
name new_real_name = get_namespace(m_env) + new_name;
|
||||
collected_locals locals;
|
||||
collect_locals(d, locals);
|
||||
buffer<name> uparams;
|
||||
collect_univ_params(d).to_buffer(uparams);
|
||||
expr new_value = Fun(locals.get_collected(), d);
|
||||
expr new_type = m_tc.infer(new_value);
|
||||
level_param_names new_ps = to_list(uparams);
|
||||
levels ls = param_names_to_levels(new_ps);
|
||||
m_env = module::add(m_env, check(m_env, mk_definition(m_env, new_real_name, new_ps,
|
||||
new_type, new_value)));
|
||||
if (new_name != new_real_name)
|
||||
m_env = add_expr_alias_rec(m_env, new_name, new_real_name);
|
||||
return mk_app(mk_constant(new_real_name, ls), locals.get_collected());
|
||||
}
|
||||
|
||||
expr visit_macro(expr const & e) override {
|
||||
if (is_nested_declaration(e)) {
|
||||
return extract(e);
|
||||
} else {
|
||||
return replace_visitor::visit_macro(e);
|
||||
}
|
||||
}
|
||||
|
||||
expr visit_binding(expr const & b) override {
|
||||
expr new_domain = visit(binding_domain(b));
|
||||
expr l = mk_local(mk_fresh_name(), new_domain);
|
||||
expr new_body = abstract(visit(instantiate(binding_body(b), l)), l);
|
||||
return update_binding(b, new_domain, new_body);
|
||||
}
|
||||
|
||||
expr visit_let(expr const & e) override {
|
||||
// TODO(Leo): improve
|
||||
return visit(instantiate(let_body(e), let_value(e)));
|
||||
}
|
||||
|
||||
environment const & get_env() const { return m_env; }
|
||||
};
|
||||
|
||||
std::tuple<environment, expr> extract_nested_declarations(environment const & env, io_state const & ios,
|
||||
name const & dname, expr const & e) {
|
||||
if (contains_nested_declarations(e)) {
|
||||
extractor ex(env, ios, dname);
|
||||
expr new_e = ex(e);
|
||||
return std::make_tuple(ex.get_env(), new_e);
|
||||
} else {
|
||||
return std::make_tuple(env, e);
|
||||
}
|
||||
}
|
||||
|
||||
void initialize_nested_declaration() {
|
||||
g_nested_decl = new name("nested_decl");
|
||||
g_nested_decl_opcode = new std::string("NDecl");
|
||||
register_macro_deserializer(get_nested_decl_opcode(),
|
||||
[](deserializer & d, unsigned num, expr const * args) {
|
||||
if (num != 1)
|
||||
throw corrupted_stream_exception();
|
||||
optional<name> n;
|
||||
d >> n;
|
||||
return mk_nested_declaration(n, args[0]);
|
||||
});
|
||||
}
|
||||
void finalize_nested_declaration() {
|
||||
delete g_nested_decl;
|
||||
delete g_nested_decl_opcode;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/flet.h"
|
||||
#include "kernel/expr.h"
|
||||
namespace lean {
|
||||
class parser;
|
||||
// auxiliary object used to temporarily enable nested declarations
|
||||
class allow_nested_decls_scope {
|
||||
bool m_saved;
|
||||
public:
|
||||
allow_nested_decls_scope(bool enable = true);
|
||||
~allow_nested_decls_scope();
|
||||
};
|
||||
expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos);
|
||||
std::tuple<environment, expr> extract_nested_declarations(environment const & env, io_state const & ios,
|
||||
name const & def_name, expr const & e);
|
||||
void initialize_nested_declaration();
|
||||
void finalize_nested_declaration();
|
||||
}
|
||||
|
|
@ -21,7 +21,6 @@ Author: Leonardo de Moura
|
|||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/tokens.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "frontends/lean/nested_declaration.h"
|
||||
#include "frontends/lean/decl_attributes.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -724,7 +723,6 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, notation
|
|||
}
|
||||
|
||||
static environment notation_cmd(parser & p) {
|
||||
allow_nested_decls_scope scope(true);
|
||||
bool overload = true;
|
||||
notation_entry_group grp = notation_entry_group::Main;
|
||||
bool persistent = true;
|
||||
|
|
@ -732,7 +730,6 @@ static environment notation_cmd(parser & p) {
|
|||
}
|
||||
|
||||
static environment infixl_cmd(parser & p) {
|
||||
allow_nested_decls_scope scope(true);
|
||||
bool overload = true;
|
||||
notation_entry_group grp = notation_entry_group::Main;
|
||||
bool persistent = true;
|
||||
|
|
@ -740,7 +737,6 @@ static environment infixl_cmd(parser & p) {
|
|||
}
|
||||
|
||||
static environment infixr_cmd(parser & p) {
|
||||
allow_nested_decls_scope scope(true);
|
||||
bool overload = true;
|
||||
notation_entry_group grp = notation_entry_group::Main;
|
||||
bool persistent = true;
|
||||
|
|
@ -748,7 +744,6 @@ static environment infixr_cmd(parser & p) {
|
|||
}
|
||||
|
||||
static environment postfix_cmd(parser & p) {
|
||||
allow_nested_decls_scope scope(true);
|
||||
bool overload = true;
|
||||
notation_entry_group grp = notation_entry_group::Main;
|
||||
bool persistent = true;
|
||||
|
|
@ -756,7 +751,6 @@ static environment postfix_cmd(parser & p) {
|
|||
}
|
||||
|
||||
static environment prefix_cmd(parser & p) {
|
||||
allow_nested_decls_scope scope(true);
|
||||
bool overload = true;
|
||||
notation_entry_group grp = notation_entry_group::Main;
|
||||
bool persistent = true;
|
||||
|
|
@ -790,7 +784,6 @@ static environment dispatch_notation_cmd(parser & p, bool overload, notation_ent
|
|||
}
|
||||
|
||||
environment local_notation_cmd(parser & p) {
|
||||
allow_nested_decls_scope scope(true);
|
||||
parser::in_notation_ctx ctx(p);
|
||||
bool overload = false; // REMARK: local notation override global one
|
||||
notation_entry_group grp = notation_entry_group::Main;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue