fix(lean): fix warnings produced by cppcheck

Fix (relevant) warnings produced by http://cppcheck.sourceforge.net.
Most warnings produced were incorrect. The tool does not seem to support some of the C++11 new features.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -212,8 +212,6 @@ class parser::imp {
     bool curr_is_lcurly() const { return curr() == scanner::token::LeftCurlyBracket; }
     /** \brief Return true iff the current token is a ':' */
     bool curr_is_colon() const { return curr() == scanner::token::Colon; }
-    /** \brief Return true iff the current token is a ',' */
-    bool curr_is_comma() const { return curr() == scanner::token::Comma; }
     /** \brief Return true iff the current token is an 'in' token */
     bool curr_is_in() const { return curr() == scanner::token::In; }
 
@@ -230,8 +228,6 @@ class parser::imp {
     void check_colon_next(char const * msg) { check_next(scanner::token::Colon, msg); }
     /** \brief Throws a parser error if the current token is not ','. If it is, move to the next token. */
     void check_comma_next(char const * msg) { check_next(scanner::token::Comma, msg); }
-    /** \brief Throws a parser error if the current token is not '('. If it is, move to the next token. */
-    void check_lparen_next(char const * msg) { check_next(scanner::token::LeftParen, msg); }
     /** \brief Throws a parser error if the current token is not ')'. If it is, move to the next token. */
     void check_rparen_next(char const * msg) { check_next(scanner::token::RightParen, msg); }
     /** \brief Throws a parser error if the current token is not '}'. If it is, move to the next token. */
@@ -1660,9 +1656,8 @@ shell::~shell() {
 bool shell::operator()() {
 #ifdef LEAN_USE_READLINE
     bool errors = false;
-    char * input;
     while (true) {
-        input = readline("# ");
+        char * input = readline("# ");
         if (!input)
             return errors;
         add_history(input);

src/frontends/lean/pp.cpp

@@ -1149,6 +1149,7 @@ public:
         m_frontend(fe) {
         set_options(opts);
         m_interrupted = false;
+        m_num_steps   = 0;
     }
 
     format operator()(expr const & e) {

src/tests/kernel/level.cpp

@@ -46,7 +46,7 @@ static void tst2() {
         level l2 = env.add_uvar("l1", level());
         lean_unreachable();
     }
-    catch (exception ex) {
+    catch (exception & ex) {
         std::cout << "ok\n";
     }
 }
@@ -59,7 +59,7 @@ static void tst3() {
         level l3 = env.add_uvar("l3", l2 + (1<<30));
         lean_unreachable();
     }
-    catch (exception ex) {
+    catch (exception & ex) {
         std::cout << "ok\n";
     }
 }

src/tests/kernel/type_checker.cpp

@@ -69,7 +69,7 @@ static void tst2() {
         std::cout << F << "\n";
         std::cout << infer_type(F, env) << "\n";
     }
-    catch (exception ex) {
+    catch (exception & ex) {
         std::cout << "Error: " << ex.what() << "\n";
     }
 }

src/util/exception.cpp

@@ -27,7 +27,7 @@ char const * parser_exception::what() const noexcept {
         s << "(line: " << m_line << ", pos: " << m_pos << ") " << m_msg;
         buffer = s.str();
         return buffer.c_str();
-    } catch (std::exception ex) {
+    } catch (std::exception & ex) {
         // failed to generate extended message
         return m_msg.c_str();
     }

src/util/sexpr/format.cpp

@@ -213,7 +213,7 @@ format group(format const & f) {
 format above(format const & f1, format const & f2) {
     return format{f1, line(), f2};
 }
-format bracket(std::string const l, format const & x, std::string const r) {
+format bracket(std::string const & l, format const & x, std::string const & r) {
     return group(nest(l.size(), format{format(l), x, format(r)}));
 }
 format paren(format const & x) {

src/util/sexpr/format.h

@@ -192,7 +192,7 @@ public:
 
     friend format group(format const & f);
     friend format above(format const & f1, format const & f2);
-    friend format bracket(std::string const l, format const & x, std::string const r);
+    friend format bracket(std::string const & l, format const & x, std::string const & r);
     friend format wrap(format const & f1, format const & f2);
 
     // x + y = x <> y
@@ -241,7 +241,7 @@ format const & colon();
 format const & dot();
 format group(format const & f);
 format above(format const & f1, format const & f2);
-format bracket(std::string const l, format const & x, std::string const r);
+format bracket(std::string const & l, format const & x, std::string const & r);
 format paren(format const & x);
 format wrap(format const & f1, format const & f2);