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

Rename get_exs in oper to get_deno

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-27 09:49:48 -07:00
parent 206c7fa203
commit 85daaea8ce
5 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/lean_frontend.cpp
View file

@ -99,7 +99,7 @@ struct frontend::imp {
/** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */
void remove_bindings(operator_info const & op) {
for (expr const & d : op.get_exprs()) {
for (expr const & d : op.get_denotations()) {
if (has_parent() && m_parent->find_op_for(d)) {
// parent has an association for d... we must hide it.
insert(m_expr_to_operator, d, operator_info());
@ -141,7 +141,7 @@ struct frontend::imp {
arguments should occur in the same positions.
*/
bool compatible_denotations(operator_info const & op, expr const & d) {
return std::all_of(op.get_exprs().begin(), op.get_exprs().end(), [&](expr const & prev_d) { return compatible_denotation(prev_d, d); });
return std::all_of(op.get_denotations().begin(), op.get_denotations().end(), [&](expr const & prev_d) { return compatible_denotation(prev_d, d); });
}
/**

2
src/frontends/lean/lean_operator_info.cpp
View file

@ -55,7 +55,7 @@ void operator_info::add_expr(expr const & d) { lean_assert(m_ptr); m_ptr->m_expr
bool operator_info::is_overloaded() const { return m_ptr && !is_nil(m_ptr->m_exprs) && !is_nil(cdr(m_ptr->m_exprs)); }
list<expr> const & operator_info::get_exprs() const { lean_assert(m_ptr); return m_ptr->m_exprs; }
list<expr> const & operator_info::get_denotations() const { lean_assert(m_ptr); return m_ptr->m_exprs; }
fixity operator_info::get_fixity() const { lean_assert(m_ptr); return m_ptr->m_fixity; }

4
src/frontends/lean/lean_operator_info.h
View file

@ -62,12 +62,12 @@ public:
bool is_overloaded() const;
/**
\brief Return the list of expressions for this operator.
\brief Return the list of denotations for this operator.
The list has size greater than 1 iff the operator has been
overloaded.
These are the possible interpretations for the operator.
*/
list<expr> const & get_exprs() const;
list<expr> const & get_denotations() const;
/** \brief Return the operator fixity. */
fixity get_fixity() const;

4
src/frontends/lean/lean_parser.cpp
View file

@ -390,7 +390,7 @@ class parser::imp {
resolve/decide which f_i should be used.
*/
expr mk_fun(operator_info const & op) {
list<expr> const & fs = op.get_exprs();
list<expr> const & fs = op.get_denotations();
lean_assert(!is_nil(fs));
auto it = fs.begin();
expr r = *it;
@ -410,7 +410,7 @@ class parser::imp {
new_args.push_back(f);
// I'm using the fact that all denotations are compatible.
// See lean_frontend.cpp for the definition of compatible denotations.
expr const & d = head(op.get_exprs());
expr const & d = head(op.get_denotations());
if (is_constant(d) && m_frontend.has_implicit_arguments(const_name(d))) {
std::vector<bool> const & imp_args = m_frontend.get_implicit_arguments(const_name(d));
unsigned i = 0;

10
src/tests/frontends/lean/lean_frontend.cpp
View file

@ -32,13 +32,13 @@ static void tst2() {
operator_info op3 = infixl(name("+"), 10);
op3.add_expr(Const(name{"Int", "plus"}));
op3.add_expr(Const(name{"Real", "plus"}));
std::cout << op3.get_exprs() << "\n";
lean_assert(length(op3.get_exprs()) == 2);
std::cout << op3.get_denotations() << "\n";
lean_assert(length(op3.get_denotations()) == 2);
operator_info op4 = op3.copy();
op4.add_expr(Const(name{"Complex", "plus"}));
std::cout << op4.get_exprs() << "\n";
lean_assert(length(op3.get_exprs()) == 2);
lean_assert(length(op4.get_exprs()) == 3);
std::cout << op4.get_denotations() << "\n";
lean_assert(length(op3.get_denotations()) == 2);
lean_assert(length(op4.get_denotations()) == 3);
lean_assert(op4.get_fixity() == fixity::Infixl);
lean_assert(op4.get_op_name() == op3.get_op_name());
lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix);