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

Use consistent coding style for if-then-else

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-13 12:57:40 -07:00
parent 8c735f1daa
commit d54834279e
5 changed files with 49 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/frontends/lean/parser.cpp
View file

@ -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);
}
}
/*@}*/

6
src/frontends/lean/pp.cpp
View file

@ -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)) {

13
src/interval/interval_def.h
View file

@ -573,8 +573,7 @@ interval<T> & interval<T>::div(interval<T> 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<T> & interval<T>::operator*=(T const & o) {
return *this;
}
if(numeric_traits<T>::is_pos(o)) {
if (numeric_traits<T>::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<T> & interval<T>::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<T> & interval<T>::operator/=(T const & o) {
return *this;
}
if(numeric_traits<T>::is_pos(o)) {
if (numeric_traits<T>::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<T> & interval<T>::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);

2
src/kernel/builtin.cpp
View file

@ -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 {

3
src/kernel/normalizer.cpp
View file

@ -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;