refactor(kernel): revise macro_definition API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
6d30141a31
commit
3a19d9fee1
3 changed files with 9 additions and 15 deletions
|
@ -54,7 +54,7 @@ struct default_converter : public converter {
|
||||||
optional<expr> expand_macro(expr const & m, context & c) {
|
optional<expr> expand_macro(expr const & m, context & c) {
|
||||||
lean_assert(is_macro(m));
|
lean_assert(is_macro(m));
|
||||||
extended_context xctx(*this, c);
|
extended_context xctx(*this, c);
|
||||||
return macro_def(m).expand(macro_num_args(m), macro_args(m), xctx);
|
return macro_def(m).expand(m, xctx);
|
||||||
}
|
}
|
||||||
|
|
||||||
/** \brief Apply normalizer extensions to \c e. */
|
/** \brief Apply normalizer extensions to \c e. */
|
||||||
|
|
|
@ -297,9 +297,9 @@ public:
|
||||||
macro_definition_cell():m_rc(0) {}
|
macro_definition_cell():m_rc(0) {}
|
||||||
virtual ~macro_definition_cell() {}
|
virtual ~macro_definition_cell() {}
|
||||||
virtual name get_name() const = 0;
|
virtual name get_name() const = 0;
|
||||||
virtual expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context & ctx) const = 0;
|
virtual expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const = 0;
|
||||||
virtual optional<expr> expand1(unsigned num, expr const * args, extension_context & ctx) const = 0;
|
virtual optional<expr> expand(expr const & m, extension_context & ctx) const = 0;
|
||||||
virtual optional<expr> expand(unsigned num, expr const * args, 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;
|
virtual unsigned trust_level() const;
|
||||||
virtual bool operator==(macro_definition_cell const & other) const;
|
virtual bool operator==(macro_definition_cell const & other) const;
|
||||||
virtual void display(std::ostream & out) const;
|
virtual void display(std::ostream & out) const;
|
||||||
|
@ -330,11 +330,9 @@ public:
|
||||||
macro_definition & operator=(macro_definition && s);
|
macro_definition & operator=(macro_definition && s);
|
||||||
|
|
||||||
name get_name() const { return m_ptr->get_name(); }
|
name get_name() const { return m_ptr->get_name(); }
|
||||||
expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context & ctx) const {
|
expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const { return m_ptr->get_type(m, arg_types, ctx); }
|
||||||
return m_ptr->get_type(num, args, arg_types, 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); }
|
||||||
optional<expr> expand1(unsigned num, expr const * args, extension_context & ctx) const { return m_ptr->expand1(num, args, ctx); }
|
|
||||||
optional<expr> expand(unsigned num, expr const * args, extension_context & ctx) const { return m_ptr->expand(num, args, ctx); }
|
|
||||||
unsigned trust_level() const { return m_ptr->trust_level(); }
|
unsigned trust_level() const { return m_ptr->trust_level(); }
|
||||||
bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
|
bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
|
||||||
bool operator!=(macro_definition const & other) const { return !operator==(other); }
|
bool operator!=(macro_definition const & other) const { return !operator==(other); }
|
||||||
|
|
|
@ -13,7 +13,6 @@ Author: Leonardo de Moura
|
||||||
#include "kernel/type_checker.h"
|
#include "kernel/type_checker.h"
|
||||||
#include "kernel/expr_maps.h"
|
#include "kernel/expr_maps.h"
|
||||||
#include "kernel/instantiate.h"
|
#include "kernel/instantiate.h"
|
||||||
#include "kernel/max_sharing.h"
|
|
||||||
#include "kernel/free_vars.h"
|
#include "kernel/free_vars.h"
|
||||||
#include "kernel/metavar.h"
|
#include "kernel/metavar.h"
|
||||||
#include "kernel/error_msgs.h"
|
#include "kernel/error_msgs.h"
|
||||||
|
@ -78,10 +77,7 @@ struct type_checker::imp {
|
||||||
|
|
||||||
optional<expr> expand_macro(expr const & m) {
|
optional<expr> expand_macro(expr const & m) {
|
||||||
lean_assert(is_macro(m));
|
lean_assert(is_macro(m));
|
||||||
if (auto new_m = macro_def(m).expand(macro_num_args(m), macro_args(m), m_tc_ctx))
|
return macro_def(m).expand(m, m_tc_ctx);
|
||||||
return some_expr(max_sharing(*new_m));
|
|
||||||
else
|
|
||||||
return none_expr();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -319,7 +315,7 @@ struct type_checker::imp {
|
||||||
buffer<expr> arg_types;
|
buffer<expr> arg_types;
|
||||||
for (unsigned i = 0; i < macro_num_args(e); i++)
|
for (unsigned i = 0; i < macro_num_args(e); i++)
|
||||||
arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only));
|
arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only));
|
||||||
r = macro_def(e).get_type(macro_num_args(e), macro_args(e), arg_types.data(), m_tc_ctx);
|
r = macro_def(e).get_type(e, arg_types.data(), m_tc_ctx);
|
||||||
if (!infer_only && macro_def(e).trust_level() <= m_env.trust_lvl()) {
|
if (!infer_only && macro_def(e).trust_level() <= m_env.trust_lvl()) {
|
||||||
optional<expr> m = expand_macro(e);
|
optional<expr> m = expand_macro(e);
|
||||||
if (!m)
|
if (!m)
|
||||||
|
|
Loading…
Reference in a new issue