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

refactor(kernel/macro_definition_cell): improve macro get_type API

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-07 16:28:02 -07:00
parent 16041e4948
commit 92c424936a
8 changed files with 30 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/expr.h
View file

@ -336,7 +336,7 @@ public:
macro_definition_cell():m_rc(0) {}
virtual ~macro_definition_cell() {}
virtual name get_name() const = 0;
virtual expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const = 0;
virtual pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const = 0;
virtual optional<expr> expand(expr const & m, extension_context & ctx) const = 0;
virtual optional<expr> expand1(expr const & m, extension_context & ctx) const { return expand(m, ctx); }
virtual unsigned trust_level() const;
@ -363,8 +363,8 @@ public:
macro_definition & operator=(macro_definition && s);
name get_name() const { return m_ptr->get_name(); }
expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const {
return m_ptr->get_type(m, arg_types, ctx);
pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const {
return m_ptr->get_type(m, ctx);
}
optional<expr> expand(expr const & m, extension_context & ctx) const { return m_ptr->expand(m, ctx); }
optional<expr> expand1(expr const & m, extension_context & ctx) const { return m_ptr->expand1(m, ctx); }

9
src/kernel/type_checker.cpp
View file

@ -184,13 +184,10 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) {
}
pair<expr, constraint_seq> type_checker::infer_macro(expr const & e, bool infer_only) {
buffer<expr> arg_types;
constraint_seq cs;
for (unsigned i = 0; i < macro_num_args(e); i++) {
arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only, cs));
}
auto def = macro_def(e);
expr t = def.get_type(e, arg_types.data(), m_tc_ctx);
pair<expr, constraint_seq> tcs = def.get_type(e, m_tc_ctx);
expr t = tcs.first;
constraint_seq cs = tcs.second;
if (!infer_only && def.trust_level() >= m_env.trust_lvl()) {
optional<expr> m = expand_macro(e);
if (!m)

4
src/library/annotation.cpp
View file

@ -33,9 +33,9 @@ public:
virtual name get_name() const { return get_annotation_name(); }
virtual format pp(formatter const &) const { return format(m_name); }
virtual void display(std::ostream & out) const { out << m_name; }
virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
virtual pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const {
check_macro(m);
return arg_types[0];
return ctx.infer_type(macro_arg(m, 0));
}
virtual optional<expr> expand(expr const & m, extension_context &) const {
check_macro(m);

2
src/library/choice.cpp
View file

@ -25,7 +25,7 @@ public:
virtual name get_name() const { return *g_choice_name; }
// Choice expressions must be replaced with metavariables before invoking the type checker.
// Choice expressions cannot be exported. They are transient/auxiliary objects.
virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); }
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_ex(); }
virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
virtual void write(serializer & s) const {
// we should be able to write choice expressions because of notation declarations

8
src/library/let.cpp
View file

@ -32,9 +32,9 @@ class let_value_definition_cell : public macro_definition_cell {
public:
let_value_definition_cell():m_id(next_let_value_id()) {}
virtual name get_name() const { return *g_let_value; }
virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
virtual pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const {
check_macro(m);
return arg_types[0];
return ctx.infer_type(macro_arg(m, 0));
}
virtual optional<expr> expand(expr const & m, extension_context &) const {
check_macro(m);
@ -75,9 +75,9 @@ public:
let_macro_definition_cell(name const & n):m_var_name(n) {}
name const & get_var_name() const { return m_var_name; }
virtual name get_name() const { return *g_let; }
virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
virtual pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const {
check_macro(m);
return arg_types[1];
return ctx.infer_type(macro_arg(m, 1));
}
virtual optional<expr> expand(expr const & m, extension_context &) const {
check_macro(m);

22
src/library/resolve_macro.cpp
View file

@ -139,13 +139,8 @@ public:
}
}
virtual expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const {
environment const & env = ctx.env();
check_num_args(env, m);
expr l = whnf(macro_arg(m, 0), ctx);
expr not_l = whnf(mk_app(*g_not, l), ctx);
expr C1 = arg_types[1];
expr C2 = arg_types[2];
expr mk_resolvent(environment const & env, extension_context & ctx, expr const & m,
expr const & l, expr const & not_l, expr const C1, expr const & C2) const {
buffer<expr> R; // resolvent
if (!collect(C1, l, R, ctx))
throw_kernel_exception(env, "invalid resolve macro, positive literal was not found", m);
@ -154,6 +149,16 @@ public:
return mk_bin_rop(*g_or, *g_false, R.size(), R.data());
}
virtual pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const {
environment const & env = ctx.env();
check_num_args(env, m);
expr l = whnf(macro_arg(m, 0), ctx);
expr not_l = whnf(mk_app(*g_not, l), ctx);
expr C1 = infer_type(macro_arg(m, 1), ctx);
expr C2 = infer_type(macro_arg(m, 2), ctx);
return mk_pair(mk_resolvent(env, ctx, m, l, not_l, C1, C2), constraint_seq());
}
// End of resolve_macro get_type implementation
// ----------------------------------------------
@ -171,8 +176,7 @@ public:
expr H2 = macro_arg(m, 2);
expr C1 = infer_type(H1, ctx);
expr C2 = infer_type(H2, ctx);
expr arg_types[3] = { expr() /* get_type() does not use first argument */, C1, C2 };
expr R = get_type(m, arg_types, ctx);
expr R = mk_resolvent(env, ctx, m, l, not_l, C1, C2);
return some_expr(mk_or_elim_tree1(l, not_l, C1, H1, C2, H2, R, ctx));
}

4
src/library/string.cpp
View file

@ -33,8 +33,8 @@ public:
return m_value < static_cast<string_macro const &>(d).m_value;
}
virtual name get_name() const { return *g_string_macro; }
virtual expr get_type(expr const &, expr const *, extension_context &) const {
return *g_string;
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const {
return mk_pair(*g_string, constraint_seq());
}
virtual optional<expr> expand(expr const &, extension_context &) const {
return some_expr(from_string_core(0, m_value));

4
src/library/typed_expr.cpp
View file

@ -34,9 +34,9 @@ class typed_expr_macro_definition_cell : public macro_definition_cell {
}
public:
virtual name get_name() const { return get_typed_expr_name(); }
virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
virtual pair<expr, constraint_seq> get_type(expr const & m, extension_context & ctx) const {
check_macro(m);
return arg_types[0];
return ctx.infer_type(macro_arg(m, 0));
}
virtual optional<expr> expand(expr const & m, extension_context &) const {
check_macro(m);