From d54834279e58c0f2ec2c7c019dfcfa5eff44887a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Sep 2013 12:57:40 -0700 Subject: [PATCH] Use consistent coding style for if-then-else Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 59 +++++++++++++++++++++++------------ src/frontends/lean/pp.cpp | 6 ++-- src/interval/interval_def.h | 13 +++----- src/kernel/builtin.cpp | 2 +- src/kernel/normalizer.cpp | 3 +- 5 files changed, 49 insertions(+), 34 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c225375b4..e0908f2d9 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -574,8 +574,7 @@ class parser::imp { } else { throw parser_error(sstream() << "invalid object reference, object '" << id << "' is not an expression.", p); } - } - else { + } else { throw parser_error(sstream() << "unknown identifier '" << id << "'", p); } } @@ -1451,24 +1450,44 @@ class parser::imp { m_expr_pos_info.clear(); m_last_cmd_pos = pos(); name const & cmd_id = curr_name(); - if (cmd_id == g_definition_kwd) parse_definition(); - else if (cmd_id == g_variable_kwd) parse_variable(); - else if (cmd_id == g_variables_kwd) parse_variables(); - else if (cmd_id == g_theorem_kwd) parse_theorem(); - else if (cmd_id == g_axiom_kwd) parse_axiom(); - else if (cmd_id == g_eval_kwd) parse_eval(); - else if (cmd_id == g_show_kwd) parse_show(); - else if (cmd_id == g_check_kwd) parse_check(); - else if (cmd_id == g_infix_kwd) parse_op(fixity::Infix); - else if (cmd_id == g_infixl_kwd) parse_op(fixity::Infixl); - else if (cmd_id == g_infixr_kwd) parse_op(fixity::Infixr); - else if (cmd_id == g_notation_kwd) parse_notation_decl(); - else if (cmd_id == g_echo_kwd) parse_echo(); - else if (cmd_id == g_set_kwd) parse_set(); - else if (cmd_id == g_import_kwd) parse_import(); - else if (cmd_id == g_help_kwd) parse_help(); - else if (cmd_id == g_coercion_kwd) parse_coercion(); - else { next(); throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos); } + if (cmd_id == g_definition_kwd) { + parse_definition(); + } else if (cmd_id == g_variable_kwd) { + parse_variable(); + } else if (cmd_id == g_variables_kwd) { + parse_variables(); + } else if (cmd_id == g_theorem_kwd) { + parse_theorem(); + } else if (cmd_id == g_axiom_kwd) { + parse_axiom(); + } else if (cmd_id == g_eval_kwd) { + parse_eval(); + } else if (cmd_id == g_show_kwd) { + parse_show(); + } else if (cmd_id == g_check_kwd) { + parse_check(); + } else if (cmd_id == g_infix_kwd) { + parse_op(fixity::Infix); + } else if (cmd_id == g_infixl_kwd) { + parse_op(fixity::Infixl); + } else if (cmd_id == g_infixr_kwd) { + parse_op(fixity::Infixr); + } else if (cmd_id == g_notation_kwd) { + parse_notation_decl(); + } else if (cmd_id == g_echo_kwd) { + parse_echo(); + } else if (cmd_id == g_set_kwd) { + parse_set(); + } else if (cmd_id == g_import_kwd) { + parse_import(); + } else if (cmd_id == g_help_kwd) { + parse_help(); + } else if (cmd_id == g_coercion_kwd) { + parse_coercion(); + } else { + next(); + throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos); + } } /*@}*/ diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index edd523616..6c46ed4e9 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1111,11 +1111,11 @@ class pp_fn { } name find_unused_prefix(expr const & e) { - if (!uses_prefix(e, g_kappa)) + if (!uses_prefix(e, g_kappa)) { return g_kappa; - else if (!uses_prefix(e, g_pho)) + } else if (!uses_prefix(e, g_pho)) { return g_pho; - else { + } else { unsigned i = 1; name n(g_nu, i); while (uses_prefix(e, n)) { diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index cea18ba96..99df26fca 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -573,8 +573,7 @@ interval & interval::div(interval const & o, interval_deps & deps) { if (i2.is_P1()) { deps.m_lower_deps = DEP_IN_LOWER1 | DEP_IN_LOWER2; deps.m_upper_deps = DEP_IN_UPPER1 | DEP_IN_LOWER2; - } - else { + } else { deps.m_lower_deps = DEP_IN_UPPER1 | DEP_IN_UPPER2; deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER2; } @@ -811,7 +810,7 @@ interval & interval::operator*=(T const & o) { return *this; } - if(numeric_traits::is_pos(o)) { + if (numeric_traits::is_pos(o)) { // [a, b] * c = [a*c, b*c] when c > 0 round_to_minus_inf(); lean::mul(m_lower, new_l_kind, m_lower, lower_kind(), o, XN_NUMERAL); @@ -819,8 +818,7 @@ interval & interval::operator*=(T const & o) { lean::mul(m_upper, new_u_kind, m_upper, upper_kind(), o, XN_NUMERAL); m_lower_inf = new_l_kind == XN_MINUS_INFINITY; m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - } - else { + } else { // [a, b] * c = [b*c, a*c] when c < 0 round_to_minus_inf(); lean::mul(tmp1, new_l_kind, m_upper, upper_kind(), o, XN_NUMERAL); @@ -848,7 +846,7 @@ interval & interval::operator/=(T const & o) { return *this; } - if(numeric_traits::is_pos(o)) { + if (numeric_traits::is_pos(o)) { // [a, b] / c = [a/c, b/c] when c > 0 round_to_minus_inf(); lean::div(m_lower, new_l_kind, m_lower, lower_kind(), o, XN_NUMERAL); @@ -856,8 +854,7 @@ interval & interval::operator/=(T const & o) { lean::div(m_upper, new_u_kind, m_upper, upper_kind(), o, XN_NUMERAL); m_lower_inf = new_l_kind == XN_MINUS_INFINITY; m_upper_inf = new_u_kind == XN_PLUS_INFINITY; - } - else { + } else { // [a, b] / c = [b/c, a/c] when c < 0 round_to_minus_inf(); lean::div(tmp1, new_l_kind, m_upper, upper_kind(), o, XN_NUMERAL); diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 30e3ac486..66e80a68a 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -130,7 +130,7 @@ public: else r = args[4]; // if A false a b --> b return true; - } if (num_args == 5 && args[3] == args[4]) { + } else if (num_args == 5 && args[3] == args[4]) { r = args[3]; // if A c a a --> a return true; } else { diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 418f66b58..f4ffab650 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -149,8 +149,7 @@ class normalizer::imp { object const & obj = m_env.get_object(const_name(a)); if (obj.is_definition() && !obj.is_opaque()) { r = normalize(obj.get_value(), value_stack(), 0); - } - else { + } else { r = svalue(a); } break;