From 5b9bd279afb20117dfd25e3defcc935b6f80e2be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Oct 2014 08:26:39 -0700 Subject: [PATCH] chore(frontends/lean/parser): minor cleanup --- src/frontends/lean/parser.cpp | 22 ++++++++++++++-------- src/frontends/lean/parser.h | 14 ++++++++++---- 2 files changed, 24 insertions(+), 12 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 26355a1b7..e17c8ac5f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -126,7 +126,8 @@ void parser::cache_definition(name const & n, expr const & pre_type, expr const m_cache->add(m_env, n, pre_type, pre_value, ls, type, value); } -optional> parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value) { +auto parser::find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value) +-> optional> { if (m_cache) return m_cache->find(m_env, n, pre_type, pre_value); else @@ -596,7 +597,8 @@ elaborator_context parser::mk_elaborator_context(environment const & env, pos_in return elaborator_context(env, m_ios, m_local_level_decls, &pp, m_info_manager, true); } -elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp) { +elaborator_context parser::mk_elaborator_context(environment const & env, local_level_decls const & lls, + pos_info_provider const & pp) { return elaborator_context(env, m_ios, lls, &pp, m_info_manager, true); } @@ -632,8 +634,9 @@ std::tuple parser::elaborate_at(environment const & env return r; } -std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v, - bool is_opaque) { +auto parser::elaborate_definition(name const & n, expr const & t, expr const & v, + bool is_opaque) +-> std::tuple { parser_pos_provider pp = get_pos_provider(); elaborator_context eenv = mk_elaborator_context(pp); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); @@ -641,8 +644,9 @@ std::tuple parser::elaborate_definition(name cons return r; } -std::tuple parser::elaborate_definition_at(environment const & env, local_level_decls const & lls, - name const & n, expr const & t, expr const & v, bool is_opaque) { +auto parser::elaborate_definition_at(environment const & env, local_level_decls const & lls, + name const & n, expr const & t, expr const & v, bool is_opaque) +-> std::tuple { parser_pos_provider pp = get_pos_provider(); elaborator_context eenv = mk_elaborator_context(env, lls, pp); auto r = ::lean::elaborate(eenv, n, t, v, is_opaque); @@ -923,7 +927,8 @@ expr parser::parse_notation(parse_table t, expr * left) { scoped_set_parser scope(L, *this); lua_getglobal(L, a.get_lua_fn().c_str()); if (!lua_isfunction(L, -1)) - throw parser_error(sstream() << "failed to use notation implemented in Lua, Lua state does not contain function '" + throw parser_error(sstream() << "failed to use notation implemented in Lua, " + << "Lua state does not contain function '" << a.get_lua_fn() << "'", p); lua_pushinteger(L, p.first); lua_pushinteger(L, p.second); @@ -1360,7 +1365,8 @@ bool parser::curr_is_command_like() const { } } -void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v) { +void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, + expr const & t, expr const & v) { m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 01bbfd870..fb9e595bd 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -212,7 +212,8 @@ public: void cache_definition(name const & n, expr const & pre_type, expr const & pre_value, level_param_names const & ls, expr const & type, expr const & value); /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */ - optional> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value); + optional> + find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value); void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); } bool are_info_lines_valid(unsigned start_line, unsigned end_line) const; @@ -279,9 +280,11 @@ public: bool curr_is_token(name const & tk) const; /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */ void check_token_next(name const & tk, char const * msg); - /** \brief Check if the current token is an identifier, if it is return it and move to next token, otherwise throw an exception. */ + /** \brief Check if the current token is an identifier, if it is return it and move to next token, + otherwise throw an exception. */ name check_id_next(char const * msg); - /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token, otherwise throw an exception. */ + /** \brief Check if the current token is an atomic identifier, if it is, return it and move to next token, + otherwise throw an exception. */ name check_atomic_id_next(char const * msg); /** \brief Check if the current token is a constant, if it is, return it and move to next token, otherwise throw an exception. */ name check_constant_next(char const * msg); @@ -343,6 +346,8 @@ public: unsigned get_local_index(expr const & e) const { return get_local_index(local_pp_name(e)); } /** \brief Return the local parameter named \c n */ expr const * get_local(name const & n) const { return m_local_decls.find(n); } + /** \brief Return local declarations as a list of local constants. */ + list locals_to_context() const; /** \brief By default, when the parser finds a unknown identifier, it signs an error. @@ -355,7 +360,8 @@ public: /** \brief Elaborate \c e, and tolerate metavariables in the result. */ std::tuple elaborate_relaxed(expr const & e, list const & ctx = list()); /** \brief Elaborate \c e, and ensure it is a type. */ - std::tuple elaborate_type(expr const & e, list const & ctx = list(), bool clear_pre_info = true); + std::tuple elaborate_type(expr const & e, list const & ctx = list(), + bool clear_pre_info = true); /** \brief Elaborate \c e in the given environment. */ std::tuple elaborate_at(environment const & env, expr const & e); /** \brief Elaborate \c e (making sure the result does not have metavariables). */