From 85daaea8ce3b4fb48dee576dda9f8832fc9ae169 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Aug 2013 09:49:48 -0700 Subject: [PATCH] Rename get_exs in oper to get_deno Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_frontend.cpp | 4 ++-- src/frontends/lean/lean_operator_info.cpp | 2 +- src/frontends/lean/lean_operator_info.h | 4 ++-- src/frontends/lean/lean_parser.cpp | 4 ++-- src/tests/frontends/lean/lean_frontend.cpp | 10 +++++----- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index 6ee179d430..3a5151a8be 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -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); }); } /** diff --git a/src/frontends/lean/lean_operator_info.cpp b/src/frontends/lean/lean_operator_info.cpp index b7cbe0fd32..fed8a50c87 100644 --- a/src/frontends/lean/lean_operator_info.cpp +++ b/src/frontends/lean/lean_operator_info.cpp @@ -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 const & operator_info::get_exprs() const { lean_assert(m_ptr); return m_ptr->m_exprs; } +list 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; } diff --git a/src/frontends/lean/lean_operator_info.h b/src/frontends/lean/lean_operator_info.h index 06c5e60aa5..039f4fe8e8 100644 --- a/src/frontends/lean/lean_operator_info.h +++ b/src/frontends/lean/lean_operator_info.h @@ -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 const & get_exprs() const; + list const & get_denotations() const; /** \brief Return the operator fixity. */ fixity get_fixity() const; diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 198abafe83..96c413185b 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -390,7 +390,7 @@ class parser::imp { resolve/decide which f_i should be used. */ expr mk_fun(operator_info const & op) { - list const & fs = op.get_exprs(); + list 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 const & imp_args = m_frontend.get_implicit_arguments(const_name(d)); unsigned i = 0; diff --git a/src/tests/frontends/lean/lean_frontend.cpp b/src/tests/frontends/lean/lean_frontend.cpp index 18617cc8d9..9de1648b70 100644 --- a/src/tests/frontends/lean/lean_frontend.cpp +++ b/src/tests/frontends/lean/lean_frontend.cpp @@ -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);